let key_dh_secret (cs:S.ciphersuite) = lbuffer uint8 (size (S.size_dh_key cs))
let key_dh_secret (cs: S.ciphersuite) =
lbuffer uint8 (size (S.size_dh_key cs))
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 Lib.Buffer.lbuffer Lib.IntTypes.uint8 Lib.IntTypes.size Spec.Agile.HPKE.size_dh_key
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))
val key_dh_secret : cs: Spec.Agile.HPKE.ciphersuite -> Type0
cs: Spec.Agile.HPKE.ciphersuite -> Type0