val has_adx_bmi2: Prims.unit
  -> Stack bool
      (fun _ -> True)
      (ensures
        (fun h0 b h1 ->
            B.(modifies B.loc_none h0 h1) /\
            (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled))))
let has_adx_bmi2 (): Stack bool
  (fun _ -> True)
  (ensures (fun h0 b h1 ->
    B.(modifies B.loc_none h0 h1) /\
    (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled))))
=
  let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
  let has_adx = EverCrypt.AutoConfig2.has_adx () in
  has_bmi2 && has_adx
val has_adx_bmi2: Prims.unit
  -> Stack bool
      (fun _ -> True)
      (ensures
        (fun h0 b h1 ->
            B.(modifies B.loc_none h0 h1) /\
            (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled))))
let has_adx_bmi2 ()
    : Stack bool
      (fun _ -> True)
      (ensures
        (fun h0 b h1 ->
            B.(modifies B.loc_none h0 h1) /\
            (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled)))) =
let has_bmi2 = EverCrypt.AutoConfig2.has_bmi2 () in
let has_adx = EverCrypt.AutoConfig2.has_adx () in
has_bmi2 && has_adx
EverCrypt.Curve25519.fst.checked
Vale.X64.CPU_Features_s.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Hacl.Curve25519_64.fsti.checked Hacl.Curve25519_51.fsti.checked FStar.Pervasives.fsti.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.AutoConfig2.fsti.checked
EverCrypt.Curve25519.fst
Prims.unit Prims.op_AmpAmp Prims.bool EverCrypt.AutoConfig2.has_adx EverCrypt.AutoConfig2.has_bmi2 FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none Prims.l_imp Prims.b2t Vale.X64.CPU_Features_s.adx_enabled Vale.X64.CPU_Features_s.bmi2_enabled
module EverCrypt.Curve25519

module B = LowStar.Buffer

[@ CInline ]
let has_adx_bmi2 (): Stack bool
  (fun _ -> True)
  (ensures (fun h0 b h1 ->
    B.(modifies B.loc_none h0 h1) /\
val has_adx_bmi2: Prims.unit
  -> Stack bool
      (fun _ -> True)
      (ensures
        (fun h0 b h1 ->
            B.(modifies B.loc_none h0 h1) /\
            (b ==> Vale.X64.CPU_Features_s.(adx_enabled /\ bmi2_enabled))))
_: Prims.unit -> FStar.HyperStack.ST.Stack Prims.bool