val test_one_hash: hash_vector -> Stack unit (fun _ -> true) (fun _ _ _ -> true)
let test_one_hash vec =
  let a, input, (LB expected_len expected), repeat = vec in
  if Spec.Hash.Definitions.is_shake a then
    failwith "unsupported shake algorithm"
  else
    let input_len = C.String.strlen input in
    let tlen = Hacl.Hash.Definitions.hash_len a in
    if expected_len <> tlen then
      failwith "Wrong length of expected tag\n"
    else if repeat = 0ul then
      failwith "Repeat must be non-zero\n"
    else if not (input_len <= (0xfffffffful - 1ul) / repeat) then
      failwith "Repeated input is too large\n"
    else begin
      push_frame();
      let computed = B.alloca 0uy tlen in
      assert_norm (v 0xfffffffful = pow2 32 - 1);
      assert (v input_len * v repeat + 1 < pow2 32);
      let total_input_len = input_len * repeat in
      let total_input = B.alloca 0uy (total_input_len + 1ul) in
      let total_input = B.sub total_input 0ul total_input_len in
      let h0 = get () in
      C.Loops.for 0ul repeat
      (fun h i -> B.live h total_input /\ B.modifies (B.loc_buffer total_input) h0 h)
      (fun i ->
        assert (v input_len * v i + v input_len <= v input_len * (v repeat - 1) + v input_len);
        assert (v input_len * v i + v input_len <= v input_len * v repeat);
        C.String.memcpy (B.sub total_input (input_len * i) input_len) input input_len
      );
      EverCrypt.Hash.uint32_fits_maxLength a total_input_len;
      assert (v total_input_len `Spec.Hash.Definitions.less_than_max_input_length` a);

      EverCrypt.Hash.Incremental.hash a computed total_input total_input_len;

      B.recall expected;
      let str = string_of_alg a in
      TestLib.compare_and_print str expected computed tlen;
      pop_frame()
    end
val test_one_hash: hash_vector -> Stack unit (fun _ -> true) (fun _ _ _ -> true)
let test_one_hash vec =
let a, input, LB expected_len expected, repeat = vec in
if Spec.Hash.Definitions.is_shake a
then failwith "unsupported shake algorithm"
else
  let input_len = C.String.strlen input in
  let tlen = Hacl.Hash.Definitions.hash_len a in
  if expected_len <> tlen
  then failwith "Wrong length of expected tag\n"
  else
    if repeat = 0ul
    then failwith "Repeat must be non-zero\n"
    else
      if not (input_len <= (0xfffffffful - 1ul) / repeat)
      then failwith "Repeated input is too large\n"
      else
        (push_frame ();
          let computed = B.alloca 0uy tlen in
          assert_norm (v 0xfffffffful = pow2 32 - 1);
          assert (v input_len * v repeat + 1 < pow2 32);
          let total_input_len = input_len * repeat in
          let total_input = B.alloca 0uy (total_input_len + 1ul) in
          let total_input = B.sub total_input 0ul total_input_len in
          let h0 = get () in
          C.Loops.for 0ul
            repeat
            (fun h i -> B.live h total_input /\ B.modifies (B.loc_buffer total_input) h0 h)
            (fun i ->
                assert (v input_len * v i + v input_len <=
                    v input_len * (v repeat - 1) + v input_len);
                assert (v input_len * v i + v input_len <= v input_len * v repeat);
                C.String.memcpy (B.sub total_input (input_len * i) input_len) input input_len);
          EverCrypt.Hash.uint32_fits_maxLength a total_input_len;
          assert ((v total_input_len) `Spec.Hash.Definitions.less_than_max_input_length` a);
          EverCrypt.Hash.Incremental.hash a computed total_input total_input_len;
          B.recall expected;
          let str = string_of_alg a in
          TestLib.compare_and_print str expected computed tlen;
          pop_frame ())
Test.NoHeap.fst.checked
TestLib.fsti.checked Test.Vectors.Poly1305.fst.checked Test.Vectors.Curve25519.fst.checked Test.Vectors.Chacha20Poly1305.fst.checked Test.Vectors.fst.checked Test.Lowstarize.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Poly1305.fsti.checked EverCrypt.HMAC.fsti.checked EverCrypt.HKDF.fsti.checked EverCrypt.Hash.Incremental.fst.checked EverCrypt.Hash.fsti.checked EverCrypt.Curve25519.fsti.checked EverCrypt.Cipher.fsti.checked EverCrypt.Chacha20Poly1305.fsti.checked C.String.fsti.checked C.Loops.fst.checked
Test.NoHeap.fst
Test.NoHeap.hash_vector Spec.Hash.Definitions.hash_alg C.String.t FStar.UInt32.t LowStar.Buffer.buffer FStar.UInt8.t Prims.l_and Prims.eq2 LowStar.Monotonic.Buffer.len LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.recallable Spec.Hash.Definitions.is_shake Test.NoHeap.failwith Prims.unit Prims.bool Prims.op_disEquality Prims.op_Equality FStar.UInt32.__uint_to_t Prims.op_Negation FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.op_Slash FStar.Integers.op_Subtraction FStar.HyperStack.ST.pop_frame TestLib.compare_and_print Test.NoHeap.string_of_alg LowStar.Monotonic.Buffer.recall EverCrypt.Hash.Incremental.hash Prims._assert Prims.b2t Spec.Hash.Definitions.less_than_max_input_length FStar.Integers.v EverCrypt.Hash.uint32_fits_maxLength C.Loops.for FStar.Monotonic.HyperStack.mem Prims.nat LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_LessThan C.String.memcpy LowStar.Buffer.sub FStar.Integers.op_Star FStar.Ghost.hide LowStar.Monotonic.Buffer.mbuffer FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.op_Plus FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.length FStar.UInt32.add FStar.UInt32.uint_to_t LowStar.Monotonic.Buffer.g_is_null LowStar.Buffer.alloca FStar.UInt8.__uint_to_t FStar.Integers.int_t FStar.Integers.op_Less Prims.pow2 FStar.Pervasives.assert_norm Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.uint8 FStar.HyperStack.ST.push_frame Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.int Prims.l_or Lib.IntTypes.range Prims.op_GreaterThanOrEqual Prims.op_Subtraction Prims.op_GreaterThan Lib.IntTypes.v Spec.Hash.Definitions.hash_length Hacl.Hash.Definitions.hash_len C.String.length C.String.strlen
module Test.NoHeap

module B = LowStar.Buffer
module L = Test.Lowstarize
module U32 = FStar.UInt32

open FStar.HyperStack.ST
open FStar.Integers
open LowStar.BufferOps
open Test.Lowstarize

let string_of_alg: Spec.Agile.Hash.hash_alg -> C.String.t =
  let open C.String in
  let open Spec.Agile.Hash in
  function
  | MD5 -> !$"MD5"
  | SHA1 -> !$"SHA1"
  | SHA2_224 -> !$"SHA2_224"
  | SHA2_256 -> !$"SHA2_256"
  | SHA2_384 -> !$"SHA2_384"
  | SHA2_512 -> !$"SHA2_512"
  | SHA3_224 -> !$"SHA3_224"
  | SHA3_256 -> !$"SHA3_256"
  | SHA3_384 -> !$"SHA3_384"
  | SHA3_512 -> !$"SHA3_512"
  | Blake2S -> !$"Blake2S"
  | Blake2B -> !$"Blake2B"
  | Shake128 -> !$"Shake128"
  | Shake256 -> !$"Shake256"

/// A module that contains stack-only tests, suitable for both C and Wasm. Other
/// tests that may make arbitrary use of the heap are in Test and Test.Hash.
///
/// .. note::
///   Tests in this module are *VERIFIED*. Please keep it this way.

noextract unfold inline_for_extraction
let (!$) = C.String.((!$))

noextract unfold inline_for_extraction
let failwith = LowStar.Failure.failwith

/// Using meta-evaluated Low* test vectors from Test.Vectors
/// ========================================================
///
/// Hashes
/// ------

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 300"
val test_one_hash: hash_vector -> Stack unit (fun _ -> true) (fun _ _ _ -> true)
vec: Test.NoHeap.hash_vector -> FStar.HyperStack.ST.Stack Prims.unit