val ctx_invariant (#cs:S.ciphersuite) (h:mem) (ctx:context_s cs) : GTot prop
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
val ctx_invariant (#cs:S.ciphersuite) (h:mem) (ctx:context_s cs) : GTot prop
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
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 FStar.Monotonic.HyperStack.mem Hacl.Impl.HPKE.context_s Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Lib.IntTypes.uint8 Hacl.Impl.HPKE.__proj__Mkcontext_s__item__ctx_key Hacl.Impl.HPKE.__proj__Mkcontext_s__item__ctx_nonce Hacl.Impl.HPKE.seq_aead Hacl.Impl.HPKE.__proj__Mkcontext_s__item__ctx_seq Hacl.Impl.HPKE.__proj__Mkcontext_s__item__ctx_exporter Lib.Buffer.disjoint Prims.prop
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
val ctx_invariant (#cs:S.ciphersuite) (h:mem) (ctx:context_s cs) : GTot prop
h: FStar.Monotonic.HyperStack.mem -> ctx: Hacl.Impl.HPKE.context_s cs -> Prims.GTot Prims.prop