val setupBaseS: setupBaseS_st cs True
let setupBaseS = hpke_setupBaseS_higher #cs True IHK.hkdf_expand512 IHK.hkdf_extract512 IDH.secret_to_public_c51 IDH.dh_c51 IHK.hkdf_expand256 IHK.hkdf_extract256
val setupBaseS: setupBaseS_st cs True
let setupBaseS =
hpke_setupBaseS_higher #cs
  True
  IHK.hkdf_expand512
  IHK.hkdf_extract512
  IDH.secret_to_public_c51
  IDH.dh_c51
  IHK.hkdf_expand256
  IHK.hkdf_extract256
Hacl.HPKE.Curve51_CP32_SHA512.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_SHA512.fst
Hacl.Meta.HPKE.hpke_setupBaseS_higher Hacl.HPKE.Curve51_CP32_SHA512.cs Prims.l_True Hacl.HPKE.Interface.HKDF.hkdf_expand512 Hacl.HPKE.Interface.HKDF.hkdf_extract512 Hacl.HPKE.Interface.DH.secret_to_public_c51 Hacl.HPKE.Interface.DH.dh_c51 Hacl.HPKE.Interface.HKDF.hkdf_expand256 Hacl.HPKE.Interface.HKDF.hkdf_extract256
module Hacl.HPKE.Curve51_CP32_SHA512

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"
val setupBaseS: setupBaseS_st cs True
Hacl.Impl.HPKE.setupBaseS_st Hacl.HPKE.Curve51_CP32_SHA512.cs Prims.l_True