let p = Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled)
let p =
let open Vale.X64.CPU_Features_s in adx_enabled /\ bmi2_enabled
Hacl.Curve25519_64.fsti.checked
Vale.X64.CPU_Features_s.fst.checked prims.fst.checked Hacl.Impl.Curve25519.Generic.fsti.checked Hacl.Impl.Curve25519.Fields.fst.checked FStar.Pervasives.fsti.checked
Hacl.Curve25519_64.fsti
Prims.l_and Prims.b2t Vale.X64.CPU_Features_s.adx_enabled Vale.X64.CPU_Features_s.bmi2_enabled
module Hacl.Curve25519_64

open Hacl.Impl.Curve25519.Generic
open Hacl.Impl.Curve25519.Fields
val p : Prims.logical
Prims.logical