val hash_sha512:Hash.hash_st Spec.Agile.Hash.SHA2_512
let hash_sha512 : Hash.hash_st Spec.Agile.Hash.SHA2_512 =
  Hacl.Streaming.SHA2.hash_512
val hash_sha512:Hash.hash_st Spec.Agile.Hash.SHA2_512
let hash_sha512:Hash.hash_st Spec.Agile.Hash.SHA2_512 =
Hacl.Streaming.SHA2.hash_512
Hacl.HPKE.Interface.Hash.fst.checked
Spec.Agile.HPKE.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Meta.Attribute.fst.checked Hacl.Streaming.SHA2.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Pervasives.fsti.checked
Hacl.HPKE.Interface.Hash.fst
Hacl.Streaming.SHA2.hash_512
module Hacl.HPKE.Interface.Hash

module S = Spec.Agile.HPKE
module Hash = Hacl.Hash.Definitions

[@ Meta.Attribute.specialize ]
noextract
assume val hash: #cs:S.ciphersuite -> Hash.hash_st (S.hash_of_cs cs)

(** Instantiations of hash **)

inline_for_extraction noextract
let hash_sha256 : Hash.hash_st Spec.Agile.Hash.SHA2_256 =
  Hacl.Streaming.SHA2.hash_256
inline_for_extraction noextract
val hash_sha512:Hash.hash_st Spec.Agile.Hash.SHA2_512
Hacl.Hash.Definitions.hash_st Spec.Hash.Definitions.SHA2_512