let setupBaseS_st (cs:S.ciphersuite) (p:Type0) =
     o_pkE: key_dh_public cs
  -> o_ctx: context_s cs
  -> skE: key_dh_secret cs
  -> pkR: serialized_point_dh cs
  -> infolen: size_t{v infolen <= max_length_info (S.hash_of_cs cs)}
  -> info: lbuffer uint8 infolen
  -> Stack UInt32.t
     (requires fun h0 ->
        p /\
        live h0 o_pkE /\
        ctx_invariant h0 o_ctx /\
        live h0 skE /\ live h0 pkR /\ live h0 info /\
        disjoint o_pkE skE /\ disjoint o_pkE pkR /\ disjoint o_pkE info /\
        B.loc_disjoint (ctx_loc o_ctx) (loc info) /\
        B.loc_disjoint (loc o_pkE) (ctx_loc o_ctx))
     (ensures fun h0 result h1 -> modifies (loc o_pkE |+| ctx_loc o_ctx) h0 h1 /\
       (let output = S.setupBaseS cs (as_seq h0 skE) (as_seq h0 pkR) (as_seq h0 info) in
        match result with
        | 0ul -> Some? output /\ (let pkE, ctx = Some?.v output in
          as_seq h1 o_pkE == pkE /\
          as_ctx h1 o_ctx == ctx)
        | 1ul -> None? output
        | _ -> False
        )
     )
let setupBaseS_st (cs: S.ciphersuite) (p: Type0) =

    o_pkE: key_dh_public cs ->
    o_ctx: context_s cs ->
    skE: key_dh_secret cs ->
    pkR: serialized_point_dh cs ->
    infolen: size_t{v infolen <= max_length_info (S.hash_of_cs cs)} ->
    info: lbuffer uint8 infolen
  -> Stack UInt32.t
      (requires
        fun h0 ->
          p /\ live h0 o_pkE /\ ctx_invariant h0 o_ctx /\ live h0 skE /\ live h0 pkR /\ live h0 info /\
          disjoint o_pkE skE /\ disjoint o_pkE pkR /\ disjoint o_pkE info /\
          B.loc_disjoint (ctx_loc o_ctx) (loc info) /\ B.loc_disjoint (loc o_pkE) (ctx_loc o_ctx))
      (ensures
        fun h0 result h1 ->
          modifies (loc o_pkE |+| ctx_loc o_ctx) h0 h1 /\
          (let output = S.setupBaseS cs (as_seq h0 skE) (as_seq h0 pkR) (as_seq h0 info) in
            match result with
            | 0ul ->
              Some? output /\
              (let pkE, ctx = Some?.v output in
                as_seq h1 o_pkE == pkE /\ as_ctx h1 o_ctx == ctx)
            | 1ul -> None? output
            | _ -> False))
Hacl.Impl.HPKE.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HPKE.fsti.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.HPKE.fsti
Spec.Agile.HPKE.ciphersuite Hacl.Impl.HPKE.key_dh_public Hacl.Impl.HPKE.context_s Hacl.Impl.HPKE.key_dh_secret Hacl.Impl.HPKE.serialized_point_dh 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 FStar.UInt32.t FStar.Monotonic.HyperStack.mem Prims.l_and Lib.Buffer.live Lib.Buffer.MUT Hacl.Impl.HPKE.ctx_invariant Lib.Buffer.disjoint LowStar.Monotonic.Buffer.loc_disjoint Hacl.Impl.HPKE.ctx_loc Lib.Buffer.loc Lib.Buffer.modifies Lib.Buffer.op_Bar_Plus_Bar FStar.Pervasives.Native.uu___is_Some FStar.Pervasives.Native.tuple2 Spec.Agile.HPKE.key_dh_public_s Spec.Agile.HPKE.encryption_context Prims.eq2 Lib.Sequence.seq Prims.l_or Prims.nat FStar.Seq.Base.length Lib.IntTypes.size Spec.Agile.HPKE.size_dh_public Lib.IntTypes.uint_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.Buffer.as_seq Hacl.Impl.HPKE.as_ctx Prims.logical FStar.Pervasives.Native.__proj__Some__item__v FStar.Pervasives.Native.uu___is_None Prims.l_False FStar.Pervasives.Native.option Spec.Agile.HPKE.setupBaseS Spec.Agile.HPKE.size_dh_key Spec.Agile.HPKE.size_dh_serialized
module Hacl.Impl.HPKE

open FStar.HyperStack
open FStar.HyperStack.All

module B = LowStar.Buffer
open Lib.Buffer
open Lib.IntTypes

module S = Spec.Agile.HPKE
module SAEAD = Spec.Agile.AEAD

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

inline_for_extraction noextract
let key_dh_public (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_dh_public cs))
inline_for_extraction noextract
let key_dh_secret (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_dh_key cs))
inline_for_extraction noextract
let serialized_point_dh (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_dh_serialized cs))
inline_for_extraction noextract
let key_aead (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_aead_key cs))
inline_for_extraction noextract
let nonce_aead (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_aead_nonce cs))

(* Redefining this to work around Low*'s limitation on buffer size *)
inline_for_extraction noextract
let max_length_info (a:S.hash_algorithm) =
  max_size_t - S.size_label_version - S.size_suite_id_hpke - S.size_label_info_hash - Spec.Hash.Definitions.block_length a

val context_s (cs:S.ciphersuite) : Type0
val ctx_loc (#cs:S.ciphersuite) (ctx:context_s cs) : GTot B.loc
val ctx_invariant (#cs:S.ciphersuite) (h:mem) (ctx:context_s cs) : GTot prop
val as_ctx (#cs:S.ciphersuite) (h:mem) (ctx:context_s cs) : GTot (S.encryption_context cs)

val frame_ctx (#cs:S.ciphersuite) (ctx:context_s cs) (l:B.loc) (h0 h1:mem)
  : Lemma (requires ctx_invariant h0 ctx /\ B.loc_disjoint (ctx_loc ctx) l /\ modifies l h0 h1)
          (ensures ctx_invariant h1 ctx /\ as_ctx h0 ctx == as_ctx h1 ctx)
          [SMTPat (modifies l h0 h1); SMTPat (ctx_invariant h0 ctx)]

inline_for_extraction noextract
val setupBaseS_st : cs: Spec.Agile.HPKE.ciphersuite -> p: Type0 -> Type0
cs: Spec.Agile.HPKE.ciphersuite -> p: Type0 -> Type0