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
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
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.hash_algorithm Prims.op_Subtraction Lib.IntTypes.max_size_t Spec.Agile.HPKE.size_label_version Spec.Agile.HPKE.size_suite_id_hpke Spec.Agile.HPKE.size_label_info_hash Spec.Hash.Definitions.block_length Prims.int
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
val max_length_info : a: Spec.Agile.HPKE.hash_algorithm -> Prims.int
a: Spec.Agile.HPKE.hash_algorithm -> Prims.int