Revision f7d7872f0125902bb7504bccbf308df5c1da8813 authored by Jay Bosamiya on 07 June 2019, 00:20:49 UTC, committed by Jay Bosamiya on 07 June 2019, 00:20:49 UTC
1 parent 7c0a519
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
Computing file changes ...