val nat_to_bytes_2 (l:size_t) (b:lbuffer uint8 2ul)
  : Stack unit
     (requires fun h -> live h b /\ v l <= 255 * 128)
     (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
       as_seq h1 b `Seq.equal` Lib.ByteSequence.nat_to_bytes_be 2 (v l)
     )
let nat_to_bytes_2 l tmp =
  assert_norm (UInt32.v 0x10000ul == pow2 16);
  [@inline_let]
  let l16 = secret (FStar.Int.Cast.Full.uint32_to_uint16 l) in
  assert (v l16 == v l);
  Lib.ByteBuffer.uint_to_bytes_be tmp l16;
  let h1 = ST.get () in

  let open Lib.ByteSequence in
  calc (==) {
    Seq.index (as_seq h1 tmp) 0;
  (==) { }
    Seq.index (uint_to_bytes_be l16) 0;
  (==) { index_uint_to_bytes_be_i l16 1 }
    uint #U8 (v l / pow2 (8 * 1) % pow2 8);
  (==) { Lib.ByteSequence.index_nat_to_intseq_be #U8 #SEC 2 (v l) 1 }
    Seq.index (Lib.ByteSequence.nat_to_bytes_be 2 (v l)) 0;
 };

  calc (==) {
    Seq.index (as_seq h1 tmp) 1;
  (==) { }
    Seq.index (uint_to_bytes_be l16) 1;
  (==) { index_uint_to_bytes_be_i l16 0 }
    uint #U8 (v l / pow2 (8 * 0) % pow2 8);
  (==) { Lib.ByteSequence.index_nat_to_intseq_be #U8 #SEC 2 (v l) 0 }
    Seq.index (Lib.ByteSequence.nat_to_bytes_be 2 (v l)) 1;
 }
val nat_to_bytes_2 (l:size_t) (b:lbuffer uint8 2ul)
  : Stack unit
     (requires fun h -> live h b /\ v l <= 255 * 128)
     (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
       as_seq h1 b `Seq.equal` Lib.ByteSequence.nat_to_bytes_be 2 (v l)
     )
let nat_to_bytes_2 l tmp =
assert_norm (UInt32.v 0x10000ul == pow2 16);
[@@ inline_let ]let l16 = secret (FStar.Int.Cast.Full.uint32_to_uint16 l) in
assert (v l16 == v l);
Lib.ByteBuffer.uint_to_bytes_be tmp l16;
let h1 = ST.get () in
let open Lib.ByteSequence in
calc ( == ) {
  Seq.index (as_seq h1 tmp) 0;
  ( == ) { () }
  Seq.index (uint_to_bytes_be l16) 0;
  ( == ) { index_uint_to_bytes_be_i l16 1 }
  uint #U8 (v l / pow2 (8 * 1) % pow2 8);
  ( == ) { Lib.ByteSequence.index_nat_to_intseq_be #U8 #SEC 2 (v l) 1 }
  Seq.index (Lib.ByteSequence.nat_to_bytes_be 2 (v l)) 0;
};
calc ( == ) {
  Seq.index (as_seq h1 tmp) 1;
  ( == ) { () }
  Seq.index (uint_to_bytes_be l16) 1;
  ( == ) { index_uint_to_bytes_be_i l16 0 }
  uint #U8 (v l / pow2 (8 * 0) % pow2 8);
  ( == ) { Lib.ByteSequence.index_nat_to_intseq_be #U8 #SEC 2 (v l) 0 }
  Seq.index (Lib.ByteSequence.nat_to_bytes_be 2 (v l)) 1;
}
Hacl.Impl.HPKE.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HPKE.fst.checked Spec.Agile.HPKE.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Meta.Attribute.fst.checked LowStar.Monotonic.Buffer.fsti.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.HPKE.Interface.HKDF.fst.checked Hacl.HPKE.Interface.Hash.fst.checked Hacl.HPKE.Interface.DH.fst.checked Hacl.HPKE.Interface.AEAD.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.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.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Calc.fsti.checked C.Loops.fst.checked
Hacl.Impl.HPKE.fst
Lib.IntTypes.size_t Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t FStar.Calc.calc_finish Prims.eq2 FStar.Seq.Base.index Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.ByteSequence.nat_to_bytes_be Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Lib.IntTypes.uint Prims.op_Modulus Prims.op_Division Prims.pow2 FStar.Mul.op_Star Lib.ByteSequence.uint_to_bytes_be Lib.IntTypes.U16 FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Hacl.Impl.HPKE.index_uint_to_bytes_be_i Lib.ByteSequence.index_nat_to_intseq_be FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.ByteBuffer.uint_to_bytes_be Prims._assert Prims.int Prims.l_or Lib.IntTypes.range Lib.IntTypes.int_t FStar.Int.Cast.uint32_to_uint16 Lib.IntTypes.secret FStar.Pervasives.assert_norm Prims.b2t Prims.op_GreaterThan FStar.UInt.size FStar.UInt32.n FStar.UInt32.v
module Hacl.Impl.HPKE

module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All

module MB = LowStar.Monotonic.Buffer

open Lib.IntTypes
open Lib.Buffer
open FStar.Mul

module S = Spec.Agile.HPKE
module SHa = Spec.Agile.Hash
module SDH = Spec.Agile.DH
module SAEAD = Spec.Agile.AEAD
module DH = Hacl.HPKE.Interface.DH
module HKDF = Hacl.HPKE.Interface.HKDF
module AEAD = Hacl.HPKE.Interface.AEAD
module Hash = Hacl.HPKE.Interface.Hash

friend Spec.Agile.HPKE

#set-options "--z3rlimit 20 --fuel 0 --ifuel 0 --record_options"

(* Defining basic types for the different arguments of HPKE functions *)

inline_for_extraction noextract
let seq_aead (cs:S.ciphersuite) = n:UInt64.t{UInt64.v n <= S.max_seq cs}
inline_for_extraction noextract
let exporter_secret (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_kdf cs))
inline_for_extraction noextract
let key_kem (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_kem_key cs))

inline_for_extraction noextract
let nsize_aead_key (cs:S.ciphersuite) : (s:size_t{v s == S.size_aead_key cs}) =
  match cs with
  | _, _, S.ExportOnly, _ -> 0ul
  | _, _, S.Seal SAEAD.AES128_GCM, _ -> 16ul
  | _, _, S.Seal SAEAD.AES256_GCM, _ -> 32ul
  | _, _, S.Seal SAEAD.CHACHA20_POLY1305, _ -> 32ul

inline_for_extraction noextract
let nsize_aead_nonce (cs:S.ciphersuite) : (s:size_t{v s == S.size_aead_nonce cs}) =
  match cs with
  | _, _, S.ExportOnly, _ -> 0ul
  | _, _, S.Seal _, _ -> 12ul

inline_for_extraction noextract
let nsize_kem_key (cs:S.ciphersuite) : (s:size_t{v s == S.size_kem_key cs}) =
  match cs with
  | _, SHa.SHA2_256, _, _ -> 32ul

inline_for_extraction noextract
let nsize_serialized_dh (cs:S.ciphersuite) : (s:size_t{v s == S.size_dh_serialized cs /\ s == DH.nsize_public (S.kem_dh_of_cs cs)}) =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> 32ul
  | SDH.DH_P256, _, _, _ -> 64ul

inline_for_extraction noextract
let nsize_public_dh (cs:S.ciphersuite) : (s:size_t{v s == S.size_dh_public cs}) =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> 32ul
  | SDH.DH_P256, _, _, _ -> 65ul

inline_for_extraction noextract
let nsize_two_public_dh (cs:S.ciphersuite) : (s:size_t{v s == S.size_dh_public cs + S.size_dh_public cs}) =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> 64ul
  | SDH.DH_P256, _, _, _ -> 130ul

inline_for_extraction noextract
let nsize_ks_ctx (cs:S.ciphersuite) : (s:size_t{v s == S.size_ks_ctx cs}) =
  match cs with
  | _, _, _, SHa.SHA2_256 -> 65ul
  | _, _, _, SHa.SHA2_384 -> 97ul
  | _, _, _, SHa.SHA2_512 -> 129ul

inline_for_extraction noextract
let nsize_hash_length (cs:S.ciphersuite) : (s:size_t{v s == S.size_kdf cs}) =
  match cs with
  | _, _, _, SHa.SHA2_256 -> 32ul
  | _, _, _, SHa.SHA2_384 -> 48ul
  | _, _, _, SHa.SHA2_512 -> 64ul

inline_for_extraction noextract
let nsize_kem_hash_length (cs:S.ciphersuite) : (s:size_t{v s == S.size_kem_kdf cs}) =
  match cs with
  | _, SHa.SHA2_256, _, _ -> 32ul

inline_for_extraction noextract
let nsize_hash_length_plus_one (cs:S.ciphersuite) : size_t =
  match cs with
  | _, _, _, SHa.SHA2_256 -> 33ul
  | _, _, _, SHa.SHA2_384 -> 49ul
  | _, _, _, SHa.SHA2_512 -> 65ul

noeq
type context_s (cs:S.ciphersuite) =
  { ctx_key : key_aead cs;
    ctx_nonce : nonce_aead cs;
    ctx_seq : lbuffer (seq_aead cs) 1ul;
    ctx_exporter : exporter_secret cs
  }

let ctx_loc #cs ctx =
  loc ctx.ctx_key |+| loc ctx.ctx_nonce |+| loc ctx.ctx_seq |+| loc ctx.ctx_exporter

let ctx_invariant #cs h ctx =
  live h ctx.ctx_key /\ live h ctx.ctx_nonce /\ live h ctx.ctx_seq /\ live h ctx.ctx_exporter /\
  disjoint ctx.ctx_key ctx.ctx_nonce /\ disjoint ctx.ctx_key ctx.ctx_exporter /\
  disjoint ctx.ctx_key ctx.ctx_seq /\ disjoint ctx.ctx_nonce ctx.ctx_seq /\
  disjoint ctx.ctx_nonce ctx.ctx_exporter /\ disjoint ctx.ctx_seq ctx.ctx_exporter

let as_ctx #cs h ctx =
  (as_seq h ctx.ctx_key,
   as_seq h ctx.ctx_nonce,
   UInt64.v (Seq.index (as_seq h ctx.ctx_seq) 0),
   as_seq h ctx.ctx_exporter)

let frame_ctx #cs ctx l h0 h1 = ()

let lemma_includes_ctx_loc (#cs:S.ciphersuite) (ctx:context_s cs) : Lemma
  (B.loc_includes (ctx_loc ctx) (loc ctx.ctx_key) /\
   B.loc_includes (ctx_loc ctx) (loc ctx.ctx_nonce) /\
   B.loc_includes (ctx_loc ctx) (loc ctx.ctx_seq) /\
   B.loc_includes (ctx_loc ctx) (loc ctx.ctx_exporter))
  = ()

noextract inline_for_extraction
val deserialize_public_key:
     #cs:S.ciphersuite
  -> pk: key_dh_public cs
  -> Stack (lbuffer uint8 (nsize_serialized_dh cs))
    (requires fun h -> live h pk)
    (ensures fun h0 b h1 -> live h1 b /\ h0 == h1 /\
      (match S.kem_dh_of_cs cs with
      | SDH.DH_Curve25519 -> b == pk
      | SDH.DH_P256 -> b == gsub pk 1ul 64ul))

let deserialize_public_key #cs pk =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> pk
  | SDH.DH_P256, _, _, _ -> sub pk 1ul 64ul

noextract inline_for_extraction
val serialize_public_key:
     #cs:S.ciphersuite
  -> pk: key_dh_public cs
  -> b: (lbuffer uint8 (nsize_serialized_dh cs))
  -> Stack unit
    (requires fun h -> live h pk /\ live h b /\
      (match S.kem_dh_of_cs cs with
      | SDH.DH_Curve25519 -> b == pk
      | SDH.DH_P256 -> b == gsub pk 1ul 64ul))
    (ensures fun h0 _ h1 -> modifies (loc pk) h0 h1 /\
      as_seq h1 pk `Seq.equal` S.serialize_public_key cs (as_seq h0 b))

let serialize_public_key #cs pk b =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> ()
  | SDH.DH_P256, _, _, _ -> upd pk 0ul (u8 4)

noextract inline_for_extraction
val prepare_dh:
     #cs:S.ciphersuite
  -> pk: serialized_point_dh cs
  -> Stack (lbuffer uint8 32ul)
    (requires fun h -> live h pk)
    (ensures fun h0 b h1 -> live h1 b /\ h0 == h1 /\
      (match S.kem_dh_of_cs cs with
      | SDH.DH_Curve25519 -> b == pk
      | SDH.DH_P256 -> b == gsub pk 0ul 32ul))

let prepare_dh #cs pk =
  match cs with
  | SDH.DH_Curve25519, _, _, _ -> pk
  | SDH.DH_P256, _, _, _ -> sub pk 0ul 32ul

noextract inline_for_extraction
val init_id_mode:
 m:S.mode ->
 b:lbuffer uint8 1ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.id_of_mode m)

#push-options "--ifuel 1"

let init_id_mode m b =
  match m with
  | S.Base -> upd b 0ul (u8 0)
  | S.PSK -> upd b 0ul (u8 1)
  | S.Auth -> upd b 0ul (u8 2)
  | S.AuthPSK -> upd b 0ul (u8 3)

#pop-options

noextract inline_for_extraction
val init_label_hpke:
 b:lbuffer uint8 4ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.label_HPKE)

#push-options "--z3rlimit 40 --fuel 4"

let init_label_hpke b =
  upd b 0ul (u8 0x48);
  upd b 1ul (u8 0x50);
  upd b 2ul (u8 0x4b);
  upd b 3ul (u8 0x45);
  Lib.Sequence.of_list_index S.label_HPKE_list 0;
  Lib.Sequence.of_list_index S.label_HPKE_list 1;
  Lib.Sequence.of_list_index S.label_HPKE_list 2;
  Lib.Sequence.of_list_index S.label_HPKE_list 3

#pop-options

noextract inline_for_extraction
val init_label_kem:
 b:lbuffer uint8 3ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.label_KEM)

#push-options "--z3rlimit 40 --fuel 3"

let init_label_kem b =
  upd b 0ul (u8 0x4b);
  upd b 1ul (u8 0x45);
  upd b 2ul (u8 0x4d);
  Lib.Sequence.of_list_index S.label_KEM_list 0;
  Lib.Sequence.of_list_index S.label_KEM_list 1;
  Lib.Sequence.of_list_index S.label_KEM_list 2

#pop-options

noextract inline_for_extraction
val init_label_version:
 b:lbuffer uint8 7ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.label_version)

#push-options "--z3rlimit 40 --fuel 7"

let init_label_version b =
  upd b 0ul (u8 0x48);
  upd b 1ul (u8 0x50);
  upd b 2ul (u8 0x4b);
  upd b 3ul (u8 0x45);
  upd b 4ul (u8 0x2d);
  upd b 5ul (u8 0x76);
  upd b 6ul (u8 0x31);
  Lib.Sequence.of_list_index S.label_version_list 0;
  Lib.Sequence.of_list_index S.label_version_list 1;
  Lib.Sequence.of_list_index S.label_version_list 2;
  Lib.Sequence.of_list_index S.label_version_list 3;
  Lib.Sequence.of_list_index S.label_version_list 4;
  Lib.Sequence.of_list_index S.label_version_list 5;
  Lib.Sequence.of_list_index S.label_version_list 6

#pop-options

noextract inline_for_extraction
val init_id_kem:
   #cs:S.ciphersuite
 -> b:lbuffer uint8 2ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.id_kem cs)

let init_id_kem #cs b =
  match cs with
  | SDH.DH_P256, SHa.SHA2_256, _, _ ->
    upd b 0ul (u8 0); upd b 1ul (u8 16)
  | SDH.DH_Curve25519, SHa.SHA2_256, _, _ ->
    upd b 0ul (u8 0); upd b 1ul (u8 32)

noextract inline_for_extraction
val init_id_kdf:
   #cs:S.ciphersuite
 -> b:lbuffer uint8 2ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.id_kdf cs)

let init_id_kdf #cs b =
  match cs with
  | _, _, _, SHa.SHA2_256 ->
    upd b 0ul (u8 0); upd b 1ul (u8 1)
  | _, _, _, SHa.SHA2_384 ->
    upd b 0ul (u8 0); upd b 1ul (u8 2)
  | _, _, _, SHa.SHA2_512 ->
    upd b 0ul (u8 0); upd b 1ul (u8 3)

noextract inline_for_extraction
val init_id_aead:
   #cs:S.ciphersuite
 -> b:lbuffer uint8 2ul ->
 Stack unit
   (requires fun h -> live h b)
   (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
     as_seq h1 b `Seq.equal` S.id_aead cs)

let init_id_aead #cs b =
  match cs with
  | _, _, S.Seal SAEAD.AES128_GCM, _  ->
    upd b 0ul (u8 0); upd b 1ul (u8 1)
  | _, _, S.Seal SAEAD.AES256_GCM, _  ->
    upd b 0ul (u8 0); upd b 1ul (u8 2)
  | _, _, S.Seal SAEAD.CHACHA20_POLY1305, _  ->
    upd b 0ul (u8 0); upd b 1ul (u8 3)
  | _, _, S.ExportOnly, _  ->
    upd b 0ul (u8 255); upd b 1ul (u8 255)

noextract inline_for_extraction
val init_suite_id:
     #cs:S.ciphersuite
  -> suite_id:lbuffer uint8 10ul ->
  Stack unit
    (requires fun h -> live h suite_id)
    (ensures fun h0 _ h1 -> modifies (loc suite_id) h0 h1 /\
      as_seq h1 suite_id == S.suite_id_hpke cs)

#push-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let init_suite_id #cs suite_id =
  init_label_hpke (sub suite_id 0ul 4ul);
  init_id_kem #cs (sub suite_id 4ul 2ul);
  init_id_kdf #cs (sub suite_id 6ul 2ul);
  init_id_aead #cs (sub suite_id 8ul 2ul);
  let h1 = ST.get () in
  assert (as_seq h1 suite_id `Seq.equal` S.suite_id_hpke cs)

#pop-options

noextract inline_for_extraction
val init_suite_kem:
     #cs:S.ciphersuite
  -> suite_id:lbuffer uint8 5ul ->
  Stack unit
    (requires fun h -> live h suite_id)
    (ensures fun h0 _ h1 -> modifies (loc suite_id) h0 h1 /\
      as_seq h1 suite_id == S.suite_id_kem cs)

#push-options "--z3rlimit 50 --fuel 0 --ifuel 0"

let init_suite_kem #cs suite_id =
  init_label_kem (sub suite_id 0ul 3ul);
  init_id_kem #cs (sub suite_id 3ul 2ul);
  let h1 = ST.get () in
  assert (as_seq h1 suite_id `Seq.equal` S.suite_id_kem cs)

#pop-options

noextract inline_for_extraction
val labeled_extract_hash:
    #cs:S.ciphersuite
  -> o_hash: lbuffer uint8 (nsize_hash_length cs)
  -> suite_id_len:size_t
  -> suite_id:lbuffer uint8 suite_id_len
  -> saltlen:size_t
  -> salt:lbuffer uint8 saltlen
  -> labellen:size_t
  -> label:lbuffer uint8 labellen
  -> ikmlen:size_t
  -> ikm:lbuffer uint8 ikmlen ->
  Stack unit
    (requires fun h ->
      live h o_hash /\ live h suite_id /\ live h salt /\ live h label /\ live h ikm /\
      disjoint salt o_hash /\
      Spec.Agile.HMAC.keysized (S.hash_of_cs cs) (v saltlen) /\
      7 + v suite_id_len + v labellen + v ikmlen + SHa.block_length (S.hash_of_cs cs) <= max_size_t /\
      S.labeled_extract_ikm_length_pred (S.hash_of_cs cs) (v suite_id_len + v labellen + v ikmlen)
      )
    (ensures fun h0 _ h1 -> modifies (loc o_hash) h0 h1 /\
      as_seq h1 o_hash `Seq.equal` S.labeled_extract (S.hash_of_cs cs) (as_seq h0 suite_id) (as_seq h0 salt) (as_seq h0 label) (as_seq h0 ikm))


#push-options "--z3rlimit 500 --z3refresh"

[@ Meta.Attribute.inline_]
let labeled_extract_hash #cs o_hash suite_id_len suite_id saltlen salt labellen label ikmlen ikm =
  push_frame ();
  let h0 = ST.get () in
  let len = 7ul +. suite_id_len +. labellen +. ikmlen in
  let tmp = create len (u8 0) in

  init_label_version (sub tmp 0ul 7ul);
  copy (sub tmp 7ul suite_id_len) suite_id;
  copy (sub tmp (7ul +. suite_id_len) labellen) label;
  copy (sub tmp (7ul +. suite_id_len +. labellen) ikmlen) ikm;

  assert_norm (pow2 32 == max_size_t + 1);

  let h1 = ST.get () in
  assert (as_seq h1 tmp `Seq.equal`
    (((S.label_version `Seq.append` as_seq h0 suite_id) `Seq.append` (as_seq h0 label)) `Seq.append` (as_seq h0 ikm)));

  HKDF.hkdf_extract #cs o_hash salt saltlen tmp len;

  pop_frame ()

#pop-options

noextract inline_for_extraction
val labeled_extract_kem:
    #cs:S.ciphersuite
  -> o_hash: lbuffer uint8 (nsize_kem_hash_length cs)
  -> suite_id_len:size_t
  -> suite_id:lbuffer uint8 suite_id_len
  -> saltlen:size_t
  -> salt:lbuffer uint8 saltlen
  -> labellen:size_t
  -> label:lbuffer uint8 labellen
  -> ikmlen:size_t
  -> ikm:lbuffer uint8 ikmlen ->
  Stack unit
    (requires fun h ->
      live h o_hash /\ live h suite_id /\ live h salt /\ live h label /\ live h ikm /\
      disjoint salt o_hash /\
      Spec.Agile.HMAC.keysized (S.kem_hash_of_cs cs) (v saltlen) /\
      7 + v suite_id_len + v labellen + v ikmlen + SHa.block_length (S.kem_hash_of_cs cs) <= max_size_t /\
      S.labeled_extract_ikm_length_pred (S.kem_hash_of_cs cs) (v suite_id_len + v labellen + v ikmlen)
      )
    (ensures fun h0 _ h1 -> modifies (loc o_hash) h0 h1 /\
      as_seq h1 o_hash `Seq.equal` S.labeled_extract (S.kem_hash_of_cs cs) (as_seq h0 suite_id) (as_seq h0 salt) (as_seq h0 label) (as_seq h0 ikm))

#push-options "--z3rlimit 400 --z3refresh"

[@ Meta.Attribute.inline_]
let labeled_extract_kem #cs o_hash suite_id_len suite_id saltlen salt labellen label ikmlen ikm =
  push_frame ();
  let h0 = ST.get () in
  let len = 7ul +. suite_id_len +. labellen +. ikmlen in
  let tmp = create len (u8 0) in

  init_label_version (sub tmp 0ul 7ul);
  copy (sub tmp 7ul suite_id_len) suite_id;
  copy (sub tmp (7ul +. suite_id_len) labellen) label;
  copy (sub tmp (7ul +. suite_id_len +. labellen) ikmlen) ikm;

  assert_norm (pow2 32 == max_size_t + 1);

  let h1 = ST.get () in
  assert (as_seq h1 tmp `Seq.equal`
    (((S.label_version `Seq.append` as_seq h0 suite_id) `Seq.append` (as_seq h0 label)) `Seq.append` (as_seq h0 ikm)));

  HKDF.hkdf_extract_kem #cs o_hash salt saltlen tmp len;

  pop_frame ()

#pop-options

/// Specializing Lib.ByteSequence.uint_to_bytes_be to avoid the forall in the postcondition
val index_uint_to_bytes_be_i: #t:inttype{unsigned t} -> #l:secrecy_level -> u:uint_t t l -> i:nat{i < numbytes t}
  -> Lemma
    (Seq.index (Lib.ByteSequence.uint_to_bytes_be #t #l u) (numbytes t - i - 1) == uint #U8 #l (v u / pow2 (8 * i) % pow2 8))

let index_uint_to_bytes_be_i u i = Lib.ByteSequence.index_uint_to_bytes_be u

noextract inline_for_extraction
val nat_to_bytes_2 (l:size_t) (b:lbuffer uint8 2ul)
  : Stack unit
     (requires fun h -> live h b /\ v l <= 255 * 128)
     (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
       as_seq h1 b `Seq.equal` Lib.ByteSequence.nat_to_bytes_be 2 (v l)
     )

#push-options "--z3rlimit 100"
val nat_to_bytes_2 (l:size_t) (b:lbuffer uint8 2ul)
  : Stack unit
     (requires fun h -> live h b /\ v l <= 255 * 128)
     (ensures fun h0 _ h1 -> modifies (loc b) h0 h1 /\
       as_seq h1 b `Seq.equal` Lib.ByteSequence.nat_to_bytes_be 2 (v l)
     )
l: Lib.IntTypes.size_t -> b: Lib.Buffer.lbuffer Lib.IntTypes.uint8 2ul
  -> FStar.HyperStack.ST.Stack Prims.unit