let expand_st (a:fixed_len_alg) =
  okm     : B.buffer uint8 ->
  prk     : B.buffer uint8 ->
  prklen  : pub_uint32 ->
  info    : B.buffer uint8 ->
  infolen : pub_uint32 ->
  len     : pub_uint32 ->
  Stack unit
  (requires fun h0 ->
    B.live h0 okm /\ B.live h0 prk /\ B.live h0 info /\
    B.disjoint okm prk /\
    v prklen == B.length prk /\
    v infolen == B.length info /\
    v len == B.length okm /\
    hash_length a <= v prklen /\
    Spec.Agile.HMAC.keysized a (v prklen) /\
    hash_length a + v infolen + 1 + block_length a < pow2 32 /\
    v len <= FStar.Mul.(255 * hash_length a))
  (ensures fun h0 _ h1 ->
    hash_block_length_fits a;
    B.modifies (B.loc_buffer okm) h0 h1 /\
    B.as_seq h1 okm == expand a (B.as_seq h0 prk) (B.as_seq h0 info) (v len))
let expand_st (a: fixed_len_alg) =

    okm: B.buffer uint8 ->
    prk: B.buffer uint8 ->
    prklen: pub_uint32 ->
    info: B.buffer uint8 ->
    infolen: pub_uint32 ->
    len: pub_uint32
  -> Stack unit
      (requires
        fun h0 ->
          B.live h0 okm /\ B.live h0 prk /\ B.live h0 info /\ B.disjoint okm prk /\
          v prklen == B.length prk /\ v infolen == B.length info /\ v len == B.length okm /\
          hash_length a <= v prklen /\ Spec.Agile.HMAC.keysized a (v prklen) /\
          hash_length a + v infolen + 1 + block_length a < pow2 32 /\
          v len <= FStar.Mul.(255 * hash_length a))
      (ensures
        fun h0 _ h1 ->
          hash_block_length_fits a;
          B.modifies (B.loc_buffer okm) h0 h1 /\
          B.as_seq h1 okm == expand a (B.as_seq h0 prk) (B.as_seq h0 info) (v len))
EverCrypt.HKDF.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked EverCrypt.HMAC.fsti.checked
EverCrypt.HKDF.fsti
Spec.Hash.Definitions.fixed_len_alg LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.pub_uint32 Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.live LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.disjoint Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.U32 Prims.b2t Prims.op_GreaterThanOrEqual Lib.IntTypes.v Lib.IntTypes.PUB LowStar.Monotonic.Buffer.length Prims.op_LessThanOrEqual Spec.Hash.Definitions.hash_length Spec.Agile.HMAC.keysized Prims.op_LessThan Prims.op_Addition Spec.Hash.Definitions.block_length Prims.pow2 FStar.Mul.op_Star LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq Spec.Agile.HKDF.expand EverCrypt.HKDF.hash_block_length_fits
(** Agile HKDF *)
module EverCrypt.HKDF

module B = LowStar.Buffer

open Spec.Agile.HKDF
open Spec.Hash.Definitions

open FStar.HyperStack.ST
open Lib.IntTypes

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

/// Auxiliary lemmas

let key_and_data_fits (a:hash_alg) :
  Lemma ((block_length a + pow2 32) `less_than_max_input_length` a)
=
  let open FStar.Mul in
  assert_norm (8 * 16 + pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125)

let hash_block_length_fits (a:hash_alg) :
  Lemma (if is_keccak a then True else hash_length a + pow2 32 + block_length a < Some?.v(max_input_length a))
=
  let open FStar.Mul in
  assert_norm (8 * 16 + 8 * 8 + pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125)

/// Types for expand and extract
/// Duplicated from Hacl.HKDF because we don't want clients to depend on Hacl.HKDF

inline_for_extraction noextract
let extract_st (a:fixed_len_alg) =
  prk     : B.buffer uint8 ->
  salt    : B.buffer uint8 ->
  saltlen : pub_uint32 ->
  ikm     : B.buffer uint8 ->
  ikmlen  : pub_uint32 ->
  Stack unit
  (requires fun h0 ->
    B.live h0 prk /\ B.live h0 salt /\ B.live h0 ikm /\
    B.disjoint salt prk /\ B.disjoint ikm prk /\
    B.length prk == hash_length a /\
    v saltlen == B.length salt /\
    v ikmlen == B.length ikm /\
    Spec.Agile.HMAC.keysized a (v saltlen) /\
    B.length ikm + block_length a < pow2 32)
  (ensures fun h0 _ h1 ->
    key_and_data_fits a;
    B.modifies (B.loc_buffer prk) h0 h1 /\
    B.as_seq h1 prk == extract a (B.as_seq h0 salt) (B.as_seq h0 ikm))

inline_for_extraction noextract
val expand_st : a: Spec.Hash.Definitions.fixed_len_alg -> Type0
a: Spec.Hash.Definitions.fixed_len_alg -> Type0