val mk_wrap_key (a: fixed_len_alg) (hash: D.hash_st a) : wrap_key_st a
let mk_wrap_key (a: fixed_len_alg) (hash: D.hash_st a): wrap_key_st a =
fun output key len ->
  [@inline_let] //18-08-02 does *not* prevents unused-but-set-variable warning in C
  let i = helper_smtpat a len in
  let nkey = B.sub output 0ul i in
  let zeroes = B.sub output i (D.block_len a `FStar.UInt32.sub` i) in
  LowStar.Ignore.ignore zeroes;
  (**) assert B.(loc_disjoint (loc_buffer nkey) (loc_buffer zeroes));
  (**) let h0 = ST.get () in
  (**) assert (Seq.equal (B.as_seq h0 zeroes) (Seq.create (v (D.block_len a `FStar.UInt32.sub` i)) (u8 0)));
  if len `FStar.UInt32.lte` D.block_len a then begin
    B.blit key 0ul nkey 0ul len;
    let h1 = ST.get () in
    (**) assert (Seq.equal (B.as_seq h1 zeroes) (B.as_seq h0 zeroes));
    (**) assert (Seq.equal (B.as_seq h1 nkey) (B.as_seq h0 key));
    (**) assert (Seq.equal (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes)));
    (**) Seq.lemma_eq_elim (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes));
    (**) assert (B.as_seq h1 output == wrap a (B.as_seq h0 key))
  end else begin
    hash key len nkey;
    (**) let h1 = ST.get () in
    (**) assert (Seq.equal (B.as_seq h1 zeroes) (B.as_seq h0 zeroes));
    (**) assert (Seq.equal (B.as_seq h1 nkey) (Spec.Agile.Hash.hash a (B.as_seq h0 key)));
    (**) assert (Seq.equal (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes)));
    (**) Seq.lemma_eq_elim (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes));
    (**) assert (B.as_seq h1 output == wrap a (B.as_seq h0 key))
  end
val mk_wrap_key (a: fixed_len_alg) (hash: D.hash_st a) : wrap_key_st a
let mk_wrap_key (a: fixed_len_alg) (hash: D.hash_st a) : wrap_key_st a =
fun output key len ->
  [@@ inline_let ]let i = helper_smtpat a len in
  let nkey = B.sub output 0ul i in
  let zeroes = B.sub output i ((D.block_len a) `FStar.UInt32.sub` i) in
  LowStar.Ignore.ignore zeroes;
  assert B.(loc_disjoint (loc_buffer nkey) (loc_buffer zeroes));
  let h0 = ST.get () in
  assert (Seq.equal (B.as_seq h0 zeroes)
        (Seq.create (v ((D.block_len a) `FStar.UInt32.sub` i)) (u8 0)));
  if len `FStar.UInt32.lte` (D.block_len a)
  then
    (B.blit key 0ul nkey 0ul len;
      let h1 = ST.get () in
      assert (Seq.equal (B.as_seq h1 zeroes) (B.as_seq h0 zeroes));
      assert (Seq.equal (B.as_seq h1 nkey) (B.as_seq h0 key));
      assert (Seq.equal (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes)));
      Seq.lemma_eq_elim (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes));
      assert (B.as_seq h1 output == wrap a (B.as_seq h0 key)))
  else
    (hash key len nkey;
      let h1 = ST.get () in
      assert (Seq.equal (B.as_seq h1 zeroes) (B.as_seq h0 zeroes));
      assert (Seq.equal (B.as_seq h1 nkey) (Spec.Agile.Hash.hash a (B.as_seq h0 key)));
      assert (Seq.equal (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes)));
      Seq.lemma_eq_elim (B.as_seq h1 output) (S.append (B.as_seq h1 nkey) (B.as_seq h1 zeroes));
      assert (B.as_seq h1 output == wrap a (B.as_seq h0 key)))
Hacl.HMAC.fst.checked
Spec.Loops.fst.checked Spec.Hash.Lemmas.fsti.checked Spec.Hash.Incremental.Definitions.fst.checked Spec.Hash.Incremental.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fst.checked Spec.Agile.HMAC.fst.checked Spec.Agile.Hash.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Ignore.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.UpdateMulti.fst.checked Hacl.Streaming.SHA2.fst.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Hash.SHA2.fsti.checked Hacl.Hash.SHA1.fsti.checked Hacl.Hash.Definitions.fst.checked Hacl.Hash.Blake2.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.Full.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked C.Loops.fst.checked
Hacl.HMAC.fst
Spec.Hash.Definitions.fixed_len_alg Hacl.Hash.Definitions.hash_st LowStar.Buffer.buffer Lib.IntTypes.uint8 Prims.eq2 Prims.int Prims.l_or Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_disEquality LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Hash.Definitions.block_length Prims.l_and Spec.Hash.Definitions.less_than_max_input_length LowStar.Monotonic.Buffer.disjoint FStar.UInt32.t Prims.op_Equality Lib.IntTypes.range Lib.IntTypes.U32 Lib.IntTypes.v Lib.IntTypes.PUB FStar.UInt32.lte Hacl.Hash.Definitions.block_len Prims._assert FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq Spec.Agile.HMAC.wrap Prims.unit FStar.Seq.Base.lemma_eq_elim FStar.Seq.Base.append FStar.Seq.Base.equal FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.blit FStar.UInt32.__uint_to_t Prims.bool Spec.Agile.Hash.hash FStar.Seq.Base.create FStar.UInt32.sub Lib.IntTypes.u8 LowStar.Monotonic.Buffer.loc_disjoint LowStar.Monotonic.Buffer.loc_buffer LowStar.Ignore.ignore LowStar.Monotonic.Buffer.mbuffer Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC LowStar.Buffer.sub FStar.Ghost.hide EverCrypt.Helpers.uint32_t Hacl.HMAC.helper_smtpat Hacl.HMAC.wrap_key_st
module Hacl.HMAC

module S = FStar.Seq
module D = Hacl.Hash.Definitions
module ST = FStar.HyperStack.ST
module B = LowStar.Buffer
module MB = LowStar.Monotonic.Buffer
module C = Hacl.Impl.Blake2.Core

open FStar.HyperStack.ST
open LowStar.BufferOps

open Spec.Hash.Definitions
open Spec.Agile.HMAC
open Spec.Agile.Hash
open Spec.Hash.Incremental
open Spec.Hash.Incremental.Definitions
open Spec.Hash.Lemmas
friend Spec.Agile.HMAC
friend Spec.Agile.Hash

let _: squash (inversion hash_alg) = allow_inversion hash_alg

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 50"

/// Helpers

inline_for_extraction
val xor_bytes_inplace:
  a: B.buffer uint8 ->
  b: B.buffer uint8 ->
  len: UInt32.t {v len = B.length a /\ v len = B.length b} ->
  Stack unit
  (requires fun h0 -> B.disjoint a b /\ B.live h0 a /\ B.live h0 b)
  (ensures fun h0 _ h1 ->
    B.(modifies (loc_buffer a) h0 h1) /\
    B.as_seq h1 a == Spec.Loops.seq_map2 ( ^. ) (B.as_seq h0 a) (B.as_seq h0 b))
inline_for_extraction
let xor_bytes_inplace a b len =
  C.Loops.in_place_map2 a b len ( ^. )

/// Agile implementation

// we rely on the output being zero-initialized for the correctness of padding
inline_for_extraction noextract
let wrap_key_st (a: fixed_len_alg) =
  output: B.buffer uint8 { B.length output == block_length a } ->
  key: B.buffer uint8 {B.length key `less_than_max_input_length` a /\ B.disjoint output key} ->
  len: UInt32.t {v len = B.length key} ->
  Stack unit
    (requires fun h0 ->
      B.live h0 output /\ B.live h0 key /\
      B.as_seq h0 output == Seq.create (block_length a) (u8 0))
    (ensures fun h0 _ h1 ->
      B.(modifies (loc_buffer output) h0 h1) /\
      B.as_seq h1 output == wrap a (B.as_seq h0 key))

/// This one is only to avoid a warning about a pattern that is not encoding properly.
inline_for_extraction
let helper_smtpat (a: fixed_len_alg) (len: uint32_t{ v len `less_than_max_input_length` a }):
  x:uint32_t { x `FStar.UInt32.lte` D.block_len a } =
  if len `FStar.UInt32.lte` D.block_len a then len else D.hash_len a

#set-options "--z3rlimit 40"

inline_for_extraction noextract
val mk_wrap_key (a: fixed_len_alg) (hash: D.hash_st a) : wrap_key_st a
a: Spec.Hash.Definitions.fixed_len_alg -> hash: Hacl.Hash.Definitions.hash_st a
  -> Hacl.HMAC.wrap_key_st a