val test_many
      (#a: _)
      (label: C.String.t)
      (f: (a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)))
      (vec: L.lbuffer a)
    : Stack unit (fun _ -> True) (fun _ _ _ -> True)
let test_many #a (label: C.String.t)
  (f: a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)) (vec: L.lbuffer a):
  Stack unit (fun _ -> True) (fun _ _ _ -> True)
=
  C.String.print label;
  C.String.(print !$"\n");
  let L.LB len vs = vec in
  let f (i:UInt32.t{FStar.UInt32.(0 <= v i /\ v i < v len)}): Stack unit
    (requires fun h -> True)
    (ensures fun h0 _ h1 -> True)
  =
    let open LowStar.BufferOps in
    B.recall vs;
    f vs.(i)
  in
  C.Loops.for 0ul len (fun _ _ -> True) f
val test_many
      (#a: _)
      (label: C.String.t)
      (f: (a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)))
      (vec: L.lbuffer a)
    : Stack unit (fun _ -> True) (fun _ _ _ -> True)
let test_many
      #a
      (label: C.String.t)
      (f: (a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)))
      (vec: L.lbuffer a)
    : Stack unit (fun _ -> True) (fun _ _ _ -> True) =
C.String.print label;
(let open C.String in print !$"\n");
let L.LB len vs = vec in
let f (i: UInt32.t{let open FStar.UInt32 in 0 <= v i /\ v i < v len})
    : Stack unit (requires fun h -> True) (ensures fun h0 _ h1 -> True) =
  let open LowStar.BufferOps in
  B.recall vs;
  f vs.(i)
in
C.Loops.for 0ul len (fun _ _ -> True) f
Test.NoHeap.fsti.checked
Test.Lowstarize.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Hash.fsti.checked C.String.fsti.checked C.Loops.fst.checked
Test.NoHeap.fsti
C.String.t Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_True Test.Lowstarize.lbuffer FStar.UInt32.t LowStar.Buffer.buffer Prims.l_and Prims.eq2 LowStar.Monotonic.Buffer.len LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.recallable C.Loops.for FStar.UInt32.__uint_to_t Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_LessThan LowStar.BufferOps.op_Array_Access LowStar.Monotonic.Buffer.recall C.String.print C.String.op_Bang_Dollar
module Test.NoHeap

module H = EverCrypt.Hash
module B = LowStar.Buffer
module L = Test.Lowstarize

open FStar.HyperStack.ST

let vec8 = L.lbuffer UInt8.t

inline_for_extraction noextract
let test_many #a (label: C.String.t)
  (f: a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)) (vec: L.lbuffer a):
  Stack unit (fun _ -> True) (fun _ _ _ -> True)
val test_many
      (#a: _)
      (label: C.String.t)
      (f: (a -> Stack unit (fun _ -> True) (fun _ _ _ -> True)))
      (vec: L.lbuffer a)
    : Stack unit (fun _ -> True) (fun _ _ _ -> True)

    label: C.String.t ->
    f: (_: a -> FStar.HyperStack.ST.Stack Prims.unit) ->
    vec: Test.Lowstarize.lbuffer a
  -> FStar.HyperStack.ST.Stack Prims.unit