val test_hmac: vs:L.lbuffer hmac_vector -> Stack unit (fun _ -> True) (fun _ _ _ -> True)
let test_hmac = test_many !$"HMAC" test_one_hmac
val test_hmac: vs:L.lbuffer hmac_vector -> Stack unit (fun _ -> True) (fun _ _ _ -> True)
let test_hmac =
test_many !$"HMAC" test_one_hmac
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.test_many Test.NoHeap.hmac_vector Test.NoHeap.op_Bang_Dollar Test.NoHeap.test_one_hmac
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
/// ----

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 test_one_hmac: hmac_vector -> Stack unit (fun _ -> True) (fun _ _ _ -> True)
let test_one_hmac vec =
  let ha, (LB keylen key), (LB datalen data), (LB expectedlen expected) = vec in
  if Spec.Hash.Definitions.is_shake ha then
    failwith "unsupported shake algorithm"
  else if expectedlen <> Hacl.Hash.Definitions.hash_len ha then
    failwith "Wrong length of expected tag\n"
  else if not (keysized ha keylen) then
    failwith "Keysized predicate not satisfied\n"
  else if not (datalen <= 0xfffffffful - Hacl.Hash.Definitions.block_len ha) then
    failwith "Datalen predicate not satisfied\n"
  else if EverCrypt.HMAC.is_supported_alg ha then
    begin
    push_frame();
    assert (Spec.Agile.HMAC.keysized ha (v keylen));
    assert (v datalen + Spec.Hash.Definitions.block_length ha < pow2 32);
    B.recall key;
    B.recall data;
    let computed = B.alloca 0uy (Hacl.Hash.Definitions.hash_len ha) in
    EverCrypt.HMAC.compute ha computed key keylen data datalen;
    let str = string_of_alg ha  in
    B.recall expected;
    TestLib.compare_and_print str expected computed (Hacl.Hash.Definitions.hash_len ha);
    pop_frame()
    end
val test_hmac: vs:L.lbuffer hmac_vector -> Stack unit (fun _ -> True) (fun _ _ _ -> True)
vs: Test.Lowstarize.lbuffer Test.NoHeap.hmac_vector -> FStar.HyperStack.ST.Stack Prims.unit