let hmac_vector = Spec.Hash.Definitions.hash_alg & vec8 & vec8 & vec8
let hmac_vector =
Spec.Hash.Definitions.hash_alg & vec8 & vec8 & vec8
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
FStar.Pervasives.Native.tuple4 Spec.Hash.Definitions.hash_alg Test.NoHeap.vec8
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)
=
  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

let hash_vector = Spec.Hash.Definitions.hash_alg & C.String.t & vec8 & UInt32.t
val test_hash: vs:L.lbuffer hash_vector -> Stack unit (fun _ -> True) (fun _ _ _ -> True)
val hmac_vector : Type0
Type0