val setupBaseR: #cs:S.ciphersuite -> setupBaseR_st cs True
let setupBaseR #cs o_ctx enc skR infolen info =
  push_frame();
  let pkR = create (nsize_serialized_dh cs) (u8 0) in
  let res1 = DH.secret_to_public #cs pkR skR in
  if res1 = 0ul then (
    let shared = create (nsize_kem_key cs) (u8 0) in
    let res2 = decap #cs shared enc skR in
    if res2 = 0ul then (
      key_schedule_base #cs o_ctx shared infolen info;
      pop_frame ();
      0ul
    ) else (
      pop_frame ();
      1ul
    )
  ) else (
    pop_frame ();
    1ul
  )
val setupBaseR: #cs:S.ciphersuite -> setupBaseR_st cs True
let setupBaseR #cs o_ctx enc skR infolen info =
push_frame ();
let pkR = create (nsize_serialized_dh cs) (u8 0) in
let res1 = DH.secret_to_public #cs pkR skR in
if res1 = 0ul
then
  (let shared = create (nsize_kem_key cs) (u8 0) in
    let res2 = decap #cs shared enc skR in
    if res2 = 0ul
    then
      (key_schedule_base #cs o_ctx shared infolen info;
        pop_frame ();
        0ul)
    else
      (pop_frame ();
        1ul))
else
  (pop_frame ();
    1ul)
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.context_s Hacl.Impl.HPKE.key_dh_public Hacl.Impl.HPKE.key_dh_secret Lib.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.HPKE.max_length_info Spec.Agile.HPKE.hash_of_cs Lib.Buffer.lbuffer Lib.IntTypes.uint8 Prims.op_Equality FStar.UInt32.t FStar.UInt32.__uint_to_t Prims.unit FStar.HyperStack.ST.pop_frame Hacl.Impl.HPKE.key_schedule_base Prims.bool Hacl.Impl.HPKE.decap Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Hacl.Impl.HPKE.nsize_kem_key Lib.Buffer.create Lib.IntTypes.u8 Hacl.HPKE.Interface.DH.secret_to_public Hacl.Impl.HPKE.nsize_serialized_dh 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_]
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 ()

noextract
val encap:
     #cs:S.ciphersuite
  -> o_shared: key_kem cs
  -> o_enc: key_dh_public cs
  -> skE: key_dh_secret cs
  -> pkR: serialized_point_dh cs
  -> Stack UInt32.t
    (requires fun h0 ->
      live h0 o_shared /\ live h0 o_enc /\
      live h0 skE /\ live h0 pkR /\
      disjoint o_shared skE /\ disjoint o_shared pkR /\
      disjoint o_shared o_enc /\ disjoint o_enc skE /\ disjoint o_enc pkR)
    (ensures fun h0 result h1 -> modifies (loc o_shared |+| loc o_enc) h0 h1 /\
      (let output = S.encap cs (as_seq h0 skE) (as_seq h0 pkR) in
       match result with
       | 0ul -> Some? output /\ (let shared, enc = Some?.v output in
         as_seq h1 o_shared `Seq.equal` shared /\ as_seq h1 o_enc `Seq.equal` enc)
       | 1ul -> None? output
       | _ -> False)
     )

#restart-solver
#push-options "--z3rlimit 600 --z3refresh --ifuel 1"

[@ Meta.Attribute.inline_]
let encap #cs o_shared o_enc skE pkR =
  let h0 = ST.get () in
  let o_pkE = deserialize_public_key #cs o_enc in
  let res1 = DH.secret_to_public #cs o_pkE skE in
  if res1 = 0ul then (
    push_frame ();
    let h1 = ST.get () in
    assert (Some?.v (SDH.secret_to_public (S.kem_dh_of_cs cs) (as_seq h0 skE)) == as_seq h1 o_pkE);
    serialize_public_key o_enc o_pkE;
    let h2 = ST.get () in
    assert (as_seq h2 o_enc == S.serialize_public_key cs (as_seq h1 o_pkE));
    let o_dh = create (nsize_serialized_dh cs) (u8 0) in
    let res2 = DH.dh #cs o_dh skE pkR in
    if res2 = 0ul then (
      let h3 = ST.get () in
      assert (as_seq h3 o_dh == Some?.v (SDH.dh (S.kem_dh_of_cs cs) (as_seq h0 skE) (as_seq h0 pkR)));
      let o_kemcontext = create (nsize_two_public_dh cs) (u8 0) in
      copy (sub o_kemcontext 0ul (nsize_public_dh cs)) o_enc;
      let o_pkRm = sub o_kemcontext (nsize_public_dh cs) (nsize_public_dh cs) in
      let o_pkR = deserialize_public_key #cs o_pkRm in
      copy o_pkR pkR;
      serialize_public_key o_pkRm o_pkR;
      let h4 = ST.get () in
      assert (as_seq h4 o_pkRm == S.serialize_public_key cs (as_seq h0 pkR));


      let o_dhm = prepare_dh #cs o_dh in
      let h5 = ST.get () in
      assert (as_seq h5 o_kemcontext `Seq.equal` (as_seq h2 o_enc `Seq.append` as_seq h4 o_pkRm));
      extract_and_expand o_shared o_dhm (nsize_two_public_dh cs) o_kemcontext;
      let h6 = ST.get () in
      assert (as_seq h6 o_enc `Seq.equal` as_seq h2 o_enc);
      assert (as_seq h6 o_shared `Seq.equal` S.extract_and_expand cs (as_seq h5 o_dhm) (as_seq h5 o_kemcontext));
      pop_frame();
      0ul
    ) else (
      pop_frame ();
      1ul
    )

  ) else (
    assert (None? (S.encap cs (as_seq h0 skE) (as_seq h0 pkR)));
    1ul
  )

#pop-options

noextract
val decap:
     #cs:S.ciphersuite
  -> o_shared: key_kem cs
  -> enc: key_dh_public cs
  -> skR: key_dh_secret cs
  -> Stack UInt32.t
    (requires fun h0 ->
      live h0 o_shared /\ live h0 enc /\ live h0 skR /\
      disjoint o_shared enc /\ disjoint o_shared skR
    )
    (ensures fun h0 result h1 -> modifies (loc o_shared) h0 h1 /\
      (let output = S.decap cs (as_seq h0 enc) (as_seq h0 skR) in
       match result with
       | 0ul -> Some? output /\ as_seq h1 o_shared `Seq.equal` Some?.v output
       | 1ul -> None? output
       | _ -> False)
     )

#push-options "--z3rlimit 300 --z3refresh --ifuel 1"

[@ Meta.Attribute.inline_ ]
let decap #cs o_shared enc skR =
  push_frame ();
  let h0 = ST.get () in
  let pkE = deserialize_public_key #cs enc in
  let dh = create (nsize_serialized_dh cs) (u8 0) in
  let res1 = DH.dh #cs dh skR pkE in
  if res1 = 0ul then (
    let kemcontext = create (nsize_two_public_dh cs) (u8 0) in
    let pkRm = sub kemcontext (nsize_public_dh cs) (nsize_public_dh cs) in
    let pkR = deserialize_public_key #cs pkRm in

    let res2 = DH.secret_to_public #cs pkR skR in
    let h1 = ST.get () in

    if res2 = 0ul then (
      let h_m = ST.get () in
      assert (as_seq h_m enc `Seq.equal` as_seq h0 enc);
      copy (sub kemcontext 0ul (nsize_public_dh cs)) enc;

      serialize_public_key #cs pkRm pkR;

      let h2 = ST.get () in
      assert (as_seq h2 kemcontext `Seq.equal` (as_seq h0 enc `Seq.append` S.serialize_public_key cs (as_seq h1 pkR)));

      let dhm = prepare_dh #cs dh in

      extract_and_expand #cs o_shared dhm (nsize_two_public_dh cs) kemcontext;
      pop_frame ();
      0ul
    ) else (
      pop_frame ();
      1ul
    )
  ) else (
    pop_frame ();
    1ul
  )

#pop-options

noextract inline_for_extraction
val build_context_default:
     #cs:S.ciphersuite
  -> o_context: lbuffer uint8 (nsize_ks_ctx cs)
  -> psk_id_hash:lbuffer uint8 (nsize_hash_length cs)
  -> info_hash:lbuffer uint8 (nsize_hash_length cs)
  -> Stack unit
    (requires fun h0 ->
      live h0 o_context /\ live h0 psk_id_hash /\ live h0 info_hash /\
      disjoint o_context psk_id_hash /\ disjoint o_context info_hash)
    (ensures fun h0 _ h1 -> modifies (loc o_context) h0 h1 /\
      as_seq h1 o_context `Seq.equal` S.build_context cs S.Base (as_seq h0 psk_id_hash) (as_seq h0 info_hash))

let build_context_default #cs o_context psk_id_hash info_hash =
  init_id_mode S.Base (sub o_context 0ul 1ul);
  copy (sub o_context 1ul (nsize_hash_length cs)) psk_id_hash;
  copy (sub o_context (nsize_hash_length_plus_one cs) (nsize_hash_length cs)) info_hash

noextract inline_for_extraction
val key_schedule_core_base:
     #cs:S.ciphersuite
  -> o_ctx: context_s cs
  -> o_context : lbuffer uint8 (nsize_ks_ctx cs)
  -> o_secret : lbuffer uint8 (nsize_hash_length cs)
  -> suite_id : lbuffer uint8 10ul
  -> shared: key_kem cs
  -> infolen: size_t{v infolen <= max_length_info (S.hash_of_cs cs)}
  -> info: lbuffer uint8 infolen
  -> Stack unit
       (requires fun h0 ->
         ctx_invariant h0 o_ctx /\ live h0 o_context /\ live h0 o_secret /\
         live h0 shared /\ live h0 info /\ live h0 suite_id /\
         as_seq h0 suite_id == S.suite_id_hpke cs /\
         MB.all_disjoint [ctx_loc o_ctx; loc o_context; loc o_secret; loc shared; loc info; loc suite_id]
       )
       (ensures fun h0 _ h1 -> modifies (loc o_ctx.ctx_exporter |+| loc o_context |+| loc o_secret) h0 h1 /\
         (let context, exp_secret, secret = S.key_schedule_core cs S.Base (as_seq h0 shared) (as_seq h0 info) None in
          as_seq h1 o_context `Seq.equal` context /\
          as_seq h1 (o_ctx.ctx_exporter) `Seq.equal` exp_secret /\
          as_seq h1 o_secret `Seq.equal` secret)
       )

#push-options "--z3rlimit 300 --z3refresh"

[@ Meta.Attribute.inline_]
let key_schedule_core_base #cs o_ctx o_context o_secret suite_id shared infolen info =
  let h0' = ST.get () in
  lemma_includes_ctx_loc o_ctx;
  push_frame();
  let hi = ST.get () in
  [@inline_let]
  let l_psk_id_hash:list uint8 = [u8 0x70; u8 0x73; u8 0x6b; u8 0x5f; u8 0x69; u8 0x64; u8 0x5f; u8 0x68; u8 0x61; u8 0x73; u8 0x68] in
  assert_norm(l_psk_id_hash == S.label_psk_id_hash_list);
  let label_psk_id_hash = createL l_psk_id_hash in

  let hi1 = ST.get () in
  assert (modifies (loc suite_id) hi hi1);

  let o_psk_id_hash = create (nsize_hash_length cs) (u8 0) in
  let empty = sub suite_id 0ul 0ul in
  let h0 = ST.get() in
  assert (as_seq h0 empty `Seq.equal` Lib.ByteSequence.lbytes_empty);

  labeled_extract_hash #cs o_psk_id_hash 10ul suite_id 0ul empty 11ul label_psk_id_hash 0ul empty;
  let h1 = ST.get() in
  assert (as_seq h1 o_psk_id_hash `Seq.equal` S.labeled_extract (S.hash_of_cs cs) (S.suite_id_hpke cs) Lib.ByteSequence.lbytes_empty S.label_psk_id_hash S.default_psk_id);

  assert (modifies (loc o_psk_id_hash) hi1 h1);
  assert (modifies (loc suite_id |+| loc o_psk_id_hash) hi h1);

  [@inline_let]
  let l_label_info_hash:list uint8 = [u8 0x69; u8 0x6e; u8 0x66; u8 0x6f; u8 0x5f; u8 0x68; u8 0x61; u8 0x73; u8 0x68] in
  assert_norm (l_label_info_hash == S.label_info_hash_list);
  let label_info_hash = createL l_label_info_hash in

  let o_info_hash = create (nsize_hash_length cs) (u8 0) in

  labeled_extract_hash #cs o_info_hash 10ul suite_id 0ul empty 9ul label_info_hash infolen info;

  let h2 = ST.get () in
  assert (modifies (loc o_info_hash) h1 h2);
  assert (modifies (loc suite_id |+| loc o_psk_id_hash |+| loc o_info_hash) hi h2);

  build_context_default #cs o_context o_psk_id_hash o_info_hash;

  let h3 = ST.get () in
  assert (modifies (loc o_context) h2 h3);
  assert (modifies (loc suite_id |+| loc o_psk_id_hash |+| loc o_info_hash |+| loc o_context) hi h3);

  [@inline_let]
  let l_label_secret:list uint8 = [u8 0x73; u8 0x65; u8 0x63; u8 0x72; u8 0x65; u8 0x74] in
  assert_norm (l_label_secret == S.label_secret_list);
  let label_secret = createL l_label_secret in

  labeled_extract_hash #cs o_secret 10ul suite_id (nsize_kem_key cs) shared 6ul label_secret 0ul empty;

  let h4 = ST.get () in
  assert (modifies (loc o_secret) h3 h4);
  assert (modifies (loc suite_id |+| loc o_psk_id_hash |+| loc o_info_hash |+| loc o_context |+| loc o_secret) hi h4);

  [@inline_let]
  let l_label_exp:list uint8 = [u8 0x65; u8 0x78; u8 0x70] in
  assert_norm (l_label_exp == S.label_exp_list);
  let label_exp = createL l_label_exp in

  labeled_expand_hash #cs 10ul suite_id (nsize_hash_length cs) o_secret 3ul label_exp (nsize_ks_ctx cs) o_context (nsize_hash_length cs) o_ctx.ctx_exporter;

  let hf = ST.get () in
  assert (modifies (loc o_ctx.ctx_exporter) h4 hf);
  assert (modifies (loc suite_id |+| loc o_psk_id_hash |+| loc o_info_hash |+| loc o_context |+| loc o_secret |+| loc o_ctx.ctx_exporter) hi hf);

  pop_frame()

#pop-options

noextract inline_for_extraction
val key_schedule_end_base:
     #cs:S.ciphersuite
  -> o_ctx: context_s cs
  -> suite_id:lbuffer uint8 10ul
  -> context: lbuffer uint8 (nsize_ks_ctx cs)
  -> secret: lbuffer uint8 (nsize_hash_length cs) ->
  Stack unit
    (requires fun h -> ctx_invariant h o_ctx /\ live h context /\ live h secret /\ live h suite_id /\
      B.loc_disjoint (ctx_loc o_ctx) (loc context) /\
      B.loc_disjoint (ctx_loc o_ctx) (loc secret) /\
      B.loc_disjoint (ctx_loc o_ctx) (loc suite_id) /\
      disjoint context secret /\
      as_seq h suite_id == S.suite_id_hpke cs
    )
    (ensures fun h0 _ h1 -> modifies (ctx_loc o_ctx) h0 h1 /\
      as_ctx h1 o_ctx == S.key_schedule_end cs S.Base (as_seq h0 context) (as_seq h0 o_ctx.ctx_exporter) (as_seq h0 secret)
    )

[@ Meta.Attribute.inline_]
let key_schedule_end_base #cs o_ctx suite_id context secret =
  match cs with
  | _, _, S.ExportOnly, _ ->
    upd o_ctx.ctx_seq 0ul 0uL;
    let h1 = ST.get () in
    assert (as_seq h1 o_ctx.ctx_key `Seq.equal` Lib.ByteSequence.lbytes_empty);
    assert (as_seq h1 o_ctx.ctx_nonce `Seq.equal` Lib.ByteSequence.lbytes_empty)

  | _ ->
    push_frame ();
    [@inline_let]
    let l_label_key:list uint8 = [u8 0x6b; u8 0x65; u8 0x79] in
    assert_norm (l_label_key == S.label_key_list);
    let label_key = createL l_label_key in

    labeled_expand_hash #cs 10ul suite_id (nsize_hash_length cs) secret 3ul label_key (nsize_ks_ctx cs) context (nsize_aead_key cs) o_ctx.ctx_key;

    [@inline_let]
    let l_label_base_nonce:list uint8 = [u8 0x62; u8 0x61; u8 0x73; u8 0x65; u8 0x5f; u8 0x6e; u8 0x6f; u8 0x6e; u8 0x63; u8 0x65] in
    assert_norm (l_label_base_nonce == S.label_base_nonce_list);
    let label_base_nonce = createL l_label_base_nonce in

    labeled_expand_hash #cs 10ul suite_id (nsize_hash_length cs) secret 10ul label_base_nonce (nsize_ks_ctx cs) context (nsize_aead_nonce cs) o_ctx.ctx_nonce;

    upd o_ctx.ctx_seq 0ul 0uL;
    pop_frame ()


noextract
val key_schedule_base:
     #cs:S.ciphersuite
  -> o_ctx: context_s cs
  -> shared: key_kem cs
  -> infolen: size_t{v infolen <= max_length_info (S.hash_of_cs cs)}
  -> info: lbuffer uint8 infolen
  -> Stack unit
       (requires fun h0 ->
         ctx_invariant h0 o_ctx /\ live h0 shared /\ live h0 info /\
         B.loc_disjoint (ctx_loc o_ctx) (loc shared) /\
         B.loc_disjoint (ctx_loc o_ctx) (loc info) /\
         disjoint shared info
       )
       (ensures fun h0 _ h1 -> modifies (ctx_loc o_ctx) h0 h1 /\
         (let ctx = S.key_schedule cs S.Base (as_seq h0 shared) (as_seq h0 info) None in
         as_ctx h1 o_ctx == ctx))

#push-options "--z3rlimit 100 --z3refresh"

[@ Meta.Attribute.inline_ ]
let key_schedule_base #cs o_ctx shared infolen info =
  push_frame();
  let o_context = create (nsize_ks_ctx cs) (u8 0) in
  let o_secret = create (nsize_hash_length cs) (u8 0) in

  let suite_id = create 10ul (u8 0) in
  init_suite_id #cs suite_id;

  key_schedule_core_base #cs o_ctx o_context o_secret suite_id shared infolen info;
  key_schedule_end_base #cs o_ctx suite_id o_context o_secret;
  pop_frame()

#pop-options

#push-options "--z3rlimit 200 --z3refresh"

[@ Meta.Attribute.specialize]
let setupBaseS #cs o_pkE o_ctx skE pkR infolen info =
  push_frame();
  let o_shared = create (nsize_kem_key cs) (u8 0) in
  let res = encap o_shared o_pkE skE pkR in
  if res = 0ul then (
    key_schedule_base o_ctx o_shared infolen info;
    pop_frame();
    res
  ) else (pop_frame (); res)

#pop-options

#push-options "--z3rlimit 600 --z3refresh --ifuel 1"

[@ Meta.Attribute.specialize]
val setupBaseR: #cs:S.ciphersuite -> setupBaseR_st cs True
Hacl.Impl.HPKE.setupBaseR_st cs Prims.l_True