val 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)}
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
val 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)}
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
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 EverCrypt.Helpers.uint32_t Prims.b2t Spec.Hash.Definitions.less_than_max_input_length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.lte Hacl.Hash.Definitions.block_len Prims.bool Hacl.Hash.Definitions.hash_len
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 }):
val 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)}

    a: Spec.Hash.Definitions.fixed_len_alg ->
    len:
      EverCrypt.Helpers.uint32_t
        {Spec.Hash.Definitions.less_than_max_input_length (Lib.IntTypes.v len) a}
  -> x: EverCrypt.Helpers.uint32_t{FStar.UInt32.lte x (Hacl.Hash.Definitions.block_len a)}