let vale_p = Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled)
let vale_p =
let open Vale.X64.CPU_Features_s in adx_enabled /\ bmi2_enabled
Hacl.HPKE.Curve64_CP32_SHA256.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Spec.Agile.HPKE.fsti.checked Spec.Agile.Hash.fsti.checked Spec.Agile.DH.fst.checked Spec.Agile.AEAD.fsti.checked prims.fst.checked Hacl.Impl.HPKE.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Hacl.HPKE.Curve64_CP32_SHA256.fsti
Prims.l_and Prims.b2t Vale.X64.CPU_Features_s.adx_enabled Vale.X64.CPU_Features_s.bmi2_enabled
module Hacl.HPKE.Curve64_CP32_SHA256

open Hacl.Impl.HPKE
module S = Spec.Agile.HPKE
module DH = Spec.Agile.DH
module AEAD = Spec.Agile.AEAD
module Hash = Spec.Agile.Hash

noextract unfold
let cs:S.ciphersuite = (DH.DH_Curve25519, Hash.SHA2_256, S.Seal AEAD.CHACHA20_POLY1305, Hash.SHA2_256)
val vale_p : Prims.logical
Prims.logical