val keysized (a: H.alg) (l: UInt32.t) : Tot (b: bool{b ==> Spec.Agile.HMAC.keysized a (UInt32.v l)})
let keysized (a:H.alg) (l: UInt32.t): Tot (b:bool{b ==> Spec.Agile.HMAC.keysized a (UInt32.v l) }) =
  EverCrypt.Hash.uint32_fits_maxLength a l;
  assert (v l `Spec.Hash.Definitions.less_than_max_input_length` a);
  assert_norm (v 0xfffffffful = pow2 32 - 1);
  l <= 0xfffffffful - Hacl.Hash.Definitions.block_len a
val keysized (a: H.alg) (l: UInt32.t) : Tot (b: bool{b ==> Spec.Agile.HMAC.keysized a (UInt32.v l)})
let keysized (a: H.alg) (l: UInt32.t) : Tot (b: bool{b ==> Spec.Agile.HMAC.keysized a (UInt32.v l)}) =
EverCrypt.Hash.uint32_fits_maxLength a l;
assert ((v l) `Spec.Hash.Definitions.less_than_max_input_length` a);
assert_norm (v 0xfffffffful = pow2 32 - 1);
l <= 0xfffffffful - Hacl.Hash.Definitions.block_len a
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
EverCrypt.Hash.alg FStar.UInt32.t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.op_Subtraction FStar.UInt32.__uint_to_t Hacl.Hash.Definitions.block_len Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_Equality FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.v Prims.pow2 Prims._assert Spec.Hash.Definitions.less_than_max_input_length EverCrypt.Hash.uint32_fits_maxLength Prims.bool Prims.l_imp Spec.Agile.HMAC.keysized FStar.UInt32.v
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)
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

let test_hash = test_many !$"Hashes" test_one_hash

/// HMAC
/// ----
val keysized (a: H.alg) (l: UInt32.t) : Tot (b: bool{b ==> Spec.Agile.HMAC.keysized a (UInt32.v l)})
a: EverCrypt.Hash.alg -> l: FStar.UInt32.t
  -> b: Prims.bool{b ==> Spec.Agile.HMAC.keysized a (FStar.UInt32.v l)}