Skip to main content

Browse the archive

Revision 01bafa0a1d2f266368a8ee5e3242922d8593496d authored by Chris Hawblitzel on 10 June 2019, 04:34:56 UTC, committed by Chris Hawblitzel on 10 June 2019, 04:34:56 UTC 
Update hints
1 parent 807fcd0
Raw File
Lib.Loops.fst 
module Lib.Loops

open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.RawIntTypes

let for start finish inv f =
  C.Loops.for
    (size_to_UInt32 start)
    (size_to_UInt32 finish)
    (fun h i -> v start <= i /\ i <= v finish /\ inv h i)
    (fun i -> f (size_from_UInt32 i))

let while inv guard test body =
  let test: unit -> Stack bool
    (requires inv)
    (ensures  fun _ b h -> inv h /\ b == guard h)
  = test
  in
  C.Loops.while #inv #(fun b h -> inv h /\ b == guard h) test body
back to top