Content - 1c0f9c3587f524ac6afb5ffb2befc95a34366b82 - bf79d01/lib/Lib.Loops.fst

visit type:

Tip revision: bc1b759fe5f471c827d2b6d292e530e36a6d3a67 authored by Jonathan Protzenko on 02 April 2019, 05:59:21 UTC
Merge remote-tracking branch 'origin/fstar-master' into evercrypt-v0.1+

Tip revision: bc1b759

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))

Browse the archive

https://github.com/project-everest/hacl-star