val openBase: openBase_st cs True
let openBase = hpke_openBase_higher #cs True IAEAD.aead_decrypt_cp32 setupBaseR
val openBase: openBase_st cs True
let openBase =
hpke_openBase_higher #cs True IAEAD.aead_decrypt_cp32 setupBaseR
Hacl.HPKE.Curve51_CP32_SHA256.fst.checked
prims.fst.checked Hacl.Meta.HPKE.fst.checked Hacl.Meta.HPKE.fst.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.Pervasives.fsti.checked
Hacl.HPKE.Curve51_CP32_SHA256.fst
Hacl.Meta.HPKE.hpke_openBase_higher Hacl.HPKE.Curve51_CP32_SHA256.cs Prims.l_True Hacl.HPKE.Interface.AEAD.aead_decrypt_cp32 Hacl.HPKE.Curve51_CP32_SHA256.setupBaseR
module Hacl.HPKE.Curve51_CP32_SHA256

open Hacl.Meta.HPKE

module IDH = Hacl.HPKE.Interface.DH
module IHK = Hacl.HPKE.Interface.HKDF
module IHash = Hacl.HPKE.Interface.Hash
module IAEAD = Hacl.HPKE.Interface.AEAD

friend Hacl.Meta.HPKE

#set-options "--fuel 0 --ifuel 0"

let setupBaseS = hpke_setupBaseS_higher #cs True IHK.hkdf_expand256 IHK.hkdf_extract256 IDH.secret_to_public_c51 IDH.dh_c51 IHK.hkdf_expand256 IHK.hkdf_extract256

let setupBaseR = hpke_setupBaseR_higher #cs True IHK.hkdf_expand256 IHK.hkdf_extract256 IDH.dh_c51 IHK.hkdf_expand256 IHK.hkdf_extract256 IDH.secret_to_public_c51

let sealBase = hpke_sealBase_higher #cs True IAEAD.aead_encrypt_cp32 setupBaseS
val openBase: openBase_st cs True
Hacl.Impl.HPKE.openBase_st Hacl.HPKE.Curve51_CP32_SHA256.cs Prims.l_True