val setupBaseR: setupBaseR_st cs vale_p
let setupBaseR = hpke_setupBaseR_higher #cs vale_p IHK.hkdf_expand512 IHK.hkdf_extract512 IDH.dh_c64 IHK.hkdf_expand256 IHK.hkdf_extract256 IDH.secret_to_public_c64
val setupBaseR: setupBaseR_st cs vale_p
let setupBaseR =
hpke_setupBaseR_higher #cs
  vale_p
  IHK.hkdf_expand512
  IHK.hkdf_extract512
  IDH.dh_c64
  IHK.hkdf_expand256
  IHK.hkdf_extract256
  IDH.secret_to_public_c64
Hacl.HPKE.Curve64_CP128_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.Curve64_CP128_SHA512.fst
Hacl.Meta.HPKE.hpke_setupBaseR_higher Hacl.HPKE.Curve64_CP128_SHA512.cs Hacl.HPKE.Curve64_CP128_SHA512.vale_p Hacl.HPKE.Interface.HKDF.hkdf_expand512 Hacl.HPKE.Interface.HKDF.hkdf_extract512 Hacl.HPKE.Interface.DH.dh_c64 Hacl.HPKE.Interface.HKDF.hkdf_expand256 Hacl.HPKE.Interface.HKDF.hkdf_extract256 Hacl.HPKE.Interface.DH.secret_to_public_c64
module Hacl.HPKE.Curve64_CP128_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"

let setupBaseS = hpke_setupBaseS_higher #cs vale_p IHK.hkdf_expand512 IHK.hkdf_extract512 IDH.secret_to_public_c64 IDH.dh_c64 IHK.hkdf_expand256 IHK.hkdf_extract256
val setupBaseR: setupBaseR_st cs vale_p
Hacl.Impl.HPKE.setupBaseR_st Hacl.HPKE.Curve64_CP128_SHA512.cs Hacl.HPKE.Curve64_CP128_SHA512.vale_p