val extract_and_expand:
     #cs: S.ciphersuite
  -> o_shared: key_kem cs
  -> dh: lbuffer uint8 32ul
  -> ctxlen : size_t
  -> kemcontext: lbuffer uint8 ctxlen
  -> Stack unit
     (requires fun h ->
       live h o_shared /\ live h dh /\ live h kemcontext /\
       disjoint o_shared dh /\ disjoint o_shared kemcontext /\
       SHa.hash_length (S.kem_hash_of_cs cs) + v ctxlen + 28 + SHa.block_length (S.kem_hash_of_cs cs) <= max_size_t
     )
     (ensures fun h0 _ h1 -> modifies (loc o_shared) h0 h1 /\
       as_seq h1 o_shared `Seq.equal` S.extract_and_expand cs (as_seq h0 dh) (as_seq h0 kemcontext))
let extract_and_expand #cs o_shared dh ctxlen kemcontext =
  push_frame ();

  let o_eae_prk = create (nsize_kem_hash_length cs) (u8 0) in

  let suite_id_kem = create 5ul (u8 0) in
  init_suite_kem #cs suite_id_kem;

  let empty = sub suite_id_kem 0ul 0ul in
  let h0 = ST.get() in
  assert (as_seq h0 empty `Seq.equal` Lib.ByteSequence.lbytes_empty);

  [@inline_let]
  let l_label_eae_prk:list uint8 = [u8 0x65; u8 0x61; u8 0x65; u8 0x5f; u8 0x70; u8 0x72; u8 0x6b] in
  assert_norm (l_label_eae_prk == S.label_eae_prk_list);
  let label_eae_prk = createL l_label_eae_prk in

  labeled_extract_kem #cs o_eae_prk 5ul suite_id_kem 0ul empty 7ul label_eae_prk 32ul dh;

  [@inline_let]
  let l_label_shared_secret:list uint8 = [u8 0x73; u8 0x68; u8 0x61; u8 0x72; u8 0x65; u8 0x64; u8 0x5f; u8 0x73; u8 0x65; u8 0x63; u8 0x72; u8 0x65; u8 0x74] in
  assert_norm (l_label_shared_secret == S.label_shared_secret_list);
  let label_shared_secret = createL l_label_shared_secret in

  labeled_expand_kem #cs 5ul suite_id_kem (nsize_kem_hash_length cs) o_eae_prk 13ul label_shared_secret ctxlen kemcontext (nsize_kem_key cs) o_shared;

  pop_frame ()
val extract_and_expand:
     #cs: S.ciphersuite
  -> o_shared: key_kem cs
  -> dh: lbuffer uint8 32ul
  -> ctxlen : size_t
  -> kemcontext: lbuffer uint8 ctxlen
  -> Stack unit
     (requires fun h ->
       live h o_shared /\ live h dh /\ live h kemcontext /\
       disjoint o_shared dh /\ disjoint o_shared kemcontext /\
       SHa.hash_length (S.kem_hash_of_cs cs) + v ctxlen + 28 + SHa.block_length (S.kem_hash_of_cs cs) <= max_size_t
     )
     (ensures fun h0 _ h1 -> modifies (loc o_shared) h0 h1 /\
       as_seq h1 o_shared `Seq.equal` S.extract_and_expand cs (as_seq h0 dh) (as_seq h0 kemcontext))
let extract_and_expand #cs o_shared dh ctxlen kemcontext =
push_frame ();
let o_eae_prk = create (nsize_kem_hash_length cs) (u8 0) in
let suite_id_kem = create 5ul (u8 0) in
init_suite_kem #cs suite_id_kem;
let empty = sub suite_id_kem 0ul 0ul in
let h0 = ST.get () in
assert ((as_seq h0 empty) `Seq.equal` Lib.ByteSequence.lbytes_empty);
[@@ inline_let ]let l_label_eae_prk:list uint8 =
  [u8 0x65; u8 0x61; u8 0x65; u8 0x5f; u8 0x70; u8 0x72; u8 0x6b]
in
assert_norm (l_label_eae_prk == S.label_eae_prk_list);
let label_eae_prk = createL l_label_eae_prk in
labeled_extract_kem #cs o_eae_prk 5ul suite_id_kem 0ul empty 7ul label_eae_prk 32ul dh;
[@@ inline_let ]let l_label_shared_secret:list uint8 =
  [
    u8 0x73; u8 0x68; u8 0x61; u8 0x72; u8 0x65; u8 0x64; u8 0x5f; u8 0x73; u8 0x65; u8 0x63;
    u8 0x72; u8 0x65; u8 0x74
  ]
in
assert_norm (l_label_shared_secret == S.label_shared_secret_list);
let label_shared_secret = createL l_label_shared_secret in
labeled_expand_kem #cs 5ul suite_id_kem (nsize_kem_hash_length cs) o_eae_prk 13ul
  label_shared_secret ctxlen kemcontext (nsize_kem_key cs) o_shared;
pop_frame ()
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
Spec.Agile.HPKE.ciphersuite Hacl.Impl.HPKE.key_kem Lib.Buffer.lbuffer Lib.IntTypes.uint8 FStar.UInt32.__uint_to_t Lib.IntTypes.size_t FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.HPKE.labeled_expand_kem Hacl.Impl.HPKE.nsize_kem_hash_length Hacl.Impl.HPKE.nsize_kem_key Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.mk_int Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Pervasives.normalize_term Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 FStar.List.Tot.Base.length Lib.Buffer.createL Lib.IntTypes.size Lib.IntTypes.size_nat FStar.Pervasives.assert_norm Prims.eq2 Prims.list Spec.Agile.HPKE.label_shared_secret_list Prims.Cons Lib.IntTypes.u8 Prims.Nil Hacl.Impl.HPKE.labeled_extract_kem Spec.Agile.HPKE.label_eae_prk_list Prims._assert FStar.Seq.Base.equal Lib.Buffer.as_seq Lib.ByteSequence.lbytes_empty FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get FStar.UInt32.uint_to_t FStar.UInt32.t Lib.Buffer.sub Hacl.Impl.HPKE.init_suite_kem Lib.Buffer.create FStar.HyperStack.ST.push_frame
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"
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;
 }
#pop-options

noextract inline_for_extraction
val labeled_expand_hash_pre:
    #cs:S.ciphersuite
  -> suite_id_len:size_t
  -> suite_id:lbuffer uint8 suite_id_len
  -> labellen:size_t
  -> label:lbuffer uint8 labellen
  -> infolen:size_t
  -> info:lbuffer uint8 infolen
  -> l:size_t
  -> tmplen:size_t
  -> tmp: lbuffer uint8 tmplen ->
  Stack unit
    (requires fun h ->
      live h tmp /\ live h suite_id /\ live h label /\ live h info /\
      disjoint tmp suite_id /\ disjoint tmp label /\ disjoint tmp info /\

      Spec.Agile.HKDF.expand_output_length_pred (S.hash_of_cs cs) (v l) /\
      v tmplen == 9 + v suite_id_len + v labellen + v infolen)
  (ensures fun h0 _ h1 -> modifies (loc tmp) h0 h1 /\
    as_seq h1 tmp `Seq.equal` (
    (((Lib.ByteSequence.nat_to_bytes_be 2 (v l)
      `Seq.append` S.label_version)
      `Seq.append` (as_seq h0 suite_id))
      `Seq.append` (as_seq h0 label))
      `Seq.append` (as_seq h0 info)
      )
  )

#push-options "--z3rlimit 300"

[@ Meta.Attribute.inline_]
let labeled_expand_hash_pre #cs suite_id_len suite_id labellen label infolen info l tmplen tmp =
  nat_to_bytes_2 l (sub tmp 0ul 2ul);
  init_label_version (sub tmp 2ul 7ul);
  copy (sub tmp 9ul suite_id_len) suite_id;
  copy (sub tmp (9ul +. suite_id_len) labellen) label;
  copy (sub tmp (9ul +. suite_id_len +. labellen) infolen) info

#pop-options

noextract inline_for_extraction
val labeled_expand_hash:
    #cs:S.ciphersuite
  -> suite_id_len:size_t
  -> suite_id:lbuffer uint8 suite_id_len
  -> prklen:size_t
  -> prk:lbuffer uint8 prklen
  -> labellen:size_t
  -> label:lbuffer uint8 labellen
  -> infolen:size_t
  -> info:lbuffer uint8 infolen
  -> l:size_t
  -> o_hash: lbuffer uint8 l ->
  Stack unit
    (requires fun h ->
      live h o_hash /\ live h suite_id /\ live h prk /\ live h label /\ live h info /\
      disjoint o_hash prk /\
      Spec.Hash.Definitions.hash_length (S.hash_of_cs cs) <= v prklen /\
      Spec.Agile.HMAC.keysized (S.hash_of_cs cs) (v prklen) /\

      SHa.hash_length (S.hash_of_cs cs) + 9 + v suite_id_len + v labellen + v infolen + SHa.block_length (S.hash_of_cs cs) + 1 <= max_size_t /\
      Spec.Agile.HKDF.expand_output_length_pred (S.hash_of_cs cs) (v l))
    (ensures fun h0 _ h1 -> modifies (loc o_hash) h0 h1 /\
      as_seq h1 o_hash `Seq.equal` S.labeled_expand (S.hash_of_cs cs) (as_seq h0 suite_id) (as_seq h0 prk) (as_seq h0 label) (as_seq h0 info) (v l)
    )

#push-options "--z3rlimit 200"

[@ Meta.Attribute.inline_]
let labeled_expand_hash #cs suite_id_len suite_id prklen prk labellen label infolen info l o_hash =
  push_frame ();
  let h0 = ST.get () in
  let len = 9ul +. suite_id_len +. labellen +. infolen in
  let tmp = create len (u8 0) in

  labeled_expand_hash_pre #cs suite_id_len suite_id labellen label infolen info l len tmp;

  HKDF.hkdf_expand #cs o_hash prk prklen tmp len l;

  pop_frame ()

#pop-options

noextract inline_for_extraction
val labeled_expand_kem:
    #cs:S.ciphersuite
  -> suite_id_len:size_t
  -> suite_id:lbuffer uint8 suite_id_len
  -> prklen:size_t
  -> prk:lbuffer uint8 prklen
  -> labellen:size_t
  -> label:lbuffer uint8 labellen
  -> infolen:size_t
  -> info:lbuffer uint8 infolen
  -> l:size_t
  -> o_hash: lbuffer uint8 l ->
  Stack unit
    (requires fun h ->
      live h o_hash /\ live h suite_id /\ live h prk /\ live h label /\ live h info /\
      disjoint o_hash prk /\
      Spec.Hash.Definitions.hash_length (S.kem_hash_of_cs cs) <= v prklen /\
      Spec.Agile.HMAC.keysized (S.kem_hash_of_cs cs) (v prklen) /\
      SHa.hash_length (S.kem_hash_of_cs cs) + 9 + v suite_id_len + v labellen + v infolen + SHa.block_length (S.kem_hash_of_cs cs) + 1 <= max_size_t /\
      S.labeled_expand_info_length_pred (S.kem_hash_of_cs cs) (v suite_id_len + v labellen + v infolen) /\
      Spec.Agile.HKDF.expand_output_length_pred (S.kem_hash_of_cs cs) (v l))
    (ensures fun h0 _ h1 -> modifies (loc o_hash) h0 h1 /\
      as_seq h1 o_hash `Seq.equal` S.labeled_expand (S.kem_hash_of_cs cs) (as_seq h0 suite_id) (as_seq h0 prk) (as_seq h0 label) (as_seq h0 info) (v l)
    )

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

let helper (cs: S.ciphersuite) (l: size_t): Lemma
  (requires Spec.Agile.HKDF.expand_output_length_pred (S.kem_hash_of_cs cs) (v l))
  (ensures (v l <= 255 * 128))
=
  ()

[@ Meta.Attribute.inline_]
let labeled_expand_kem #cs suite_id_len suite_id prklen prk labellen label infolen info l o_hash =
  let h00 = ST.get () in
  push_frame ();
  let h0 = ST.get () in
  let len = 9ul +. suite_id_len +. labellen +. infolen in
  let tmp = create len (u8 0) in

  helper cs l;
  nat_to_bytes_2 l (sub tmp 0ul 2ul);
  let h1 = ST.get () in
  init_label_version (sub tmp 2ul 7ul);
  let h2 = ST.get () in
  B.modifies_trans (loc tmp) h0 h1 (loc tmp) h2;
  copy (sub tmp 9ul suite_id_len) suite_id;
  let h3 = ST.get () in
  B.modifies_trans (loc tmp) h0 h2 (loc tmp) h3;
  copy (sub tmp (9ul +. suite_id_len) labellen) label;
  let h4 = ST.get () in
  B.modifies_trans (loc tmp) h0 h3 (loc tmp) h4;
  copy (sub tmp (9ul +. suite_id_len +. labellen) infolen) info;
  let h5 = ST.get () in
  B.modifies_trans (loc tmp) h0 h4 (loc tmp) h5;

  assert (as_seq h5 tmp `Seq.equal` (
    (((Lib.ByteSequence.nat_to_bytes_be 2 (v l)
      `Seq.append` S.label_version)
      `Seq.append` (as_seq h0 suite_id))
      `Seq.append` (as_seq h0 label))
      `Seq.append` (as_seq h0 info)
      ));

  HKDF.hkdf_expand_kem #cs o_hash prk prklen tmp len l;
  let h6 = ST.get () in

  B.modifies_trans (loc tmp) h0 h5 (loc o_hash) h6;

  pop_frame ();

  let h7 = ST.get () in
  B.modifies_fresh_frame_popped h00 h0 (loc o_hash) h6 h7

#pop-options

noextract inline_for_extraction
val extract_and_expand:
     #cs: S.ciphersuite
  -> o_shared: key_kem cs
  -> dh: lbuffer uint8 32ul
  -> ctxlen : size_t
  -> kemcontext: lbuffer uint8 ctxlen
  -> Stack unit
     (requires fun h ->
       live h o_shared /\ live h dh /\ live h kemcontext /\
       disjoint o_shared dh /\ disjoint o_shared kemcontext /\
       SHa.hash_length (S.kem_hash_of_cs cs) + v ctxlen + 28 + SHa.block_length (S.kem_hash_of_cs cs) <= max_size_t
     )
     (ensures fun h0 _ h1 -> modifies (loc o_shared) h0 h1 /\
       as_seq h1 o_shared `Seq.equal` S.extract_and_expand cs (as_seq h0 dh) (as_seq h0 kemcontext))

[@ Meta.Attribute.inline_]
val extract_and_expand:
     #cs: S.ciphersuite
  -> o_shared: key_kem cs
  -> dh: lbuffer uint8 32ul
  -> ctxlen : size_t
  -> kemcontext: lbuffer uint8 ctxlen
  -> Stack unit
     (requires fun h ->
       live h o_shared /\ live h dh /\ live h kemcontext /\
       disjoint o_shared dh /\ disjoint o_shared kemcontext /\
       SHa.hash_length (S.kem_hash_of_cs cs) + v ctxlen + 28 + SHa.block_length (S.kem_hash_of_cs cs) <= max_size_t
     )
     (ensures fun h0 _ h1 -> modifies (loc o_shared) h0 h1 /\
       as_seq h1 o_shared `Seq.equal` S.extract_and_expand cs (as_seq h0 dh) (as_seq h0 kemcontext))

    o_shared: Hacl.Impl.HPKE.key_kem cs ->
    dh: Lib.Buffer.lbuffer Lib.IntTypes.uint8 32ul ->
    ctxlen: Lib.IntTypes.size_t ->
    kemcontext: Lib.Buffer.lbuffer Lib.IntTypes.uint8 ctxlen
  -> FStar.HyperStack.ST.Stack Prims.unit