val cpu_has_movbe:cached_flag Vale.X64.CPU_Features_s.movbe_enabled
let cpu_has_movbe: cached_flag Vale.X64.CPU_Features_s.movbe_enabled =
  B.gcmalloc_of_list HS.root [ false ]
val cpu_has_movbe:cached_flag Vale.X64.CPU_Features_s.movbe_enabled
let cpu_has_movbe:cached_flag Vale.X64.CPU_Features_s.movbe_enabled =
B.gcmalloc_of_list HS.root [false]
EverCrypt.AutoConfig2.fst.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.Cpuid.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked EverCrypt.TargetConfig.fsti.checked
EverCrypt.AutoConfig2.fst
LowStar.Buffer.gcmalloc_of_list EverCrypt.AutoConfig2.flag Vale.X64.CPU_Features_s.movbe_enabled FStar.Monotonic.HyperHeap.root Prims.Cons Prims.Nil LowStar.Monotonic.Buffer.mbuffer LowStar.Buffer.trivial_preorder Prims.l_and Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length FStar.Pervasives.normalize_term FStar.List.Tot.Base.length Prims.b2t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.recallable
module EverCrypt.AutoConfig2

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module S = FStar.Seq

open FStar.HyperStack.ST

#set-options "--max_fuel 0 --max_ifuel 0"

(** Only partially specified; the flag may be false because it has been
  intentionally disabled by the client, for instance. *)

type flag (b: bool) =
  b':bool { b' ==> b }

(** Flags, cached in a mutable global reference *)

let eternal_pointer a = buf:B.buffer a { B.recallable buf /\ B.length buf = 1 }

unfold
let cached_flag (b: bool) = eternal_pointer (flag b)

let cpu_has_shaext: cached_flag Vale.X64.CPU_Features_s.sha_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_aesni: cached_flag Vale.X64.CPU_Features_s.aesni_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_pclmulqdq: cached_flag Vale.X64.CPU_Features_s.pclmulqdq_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_avx2: cached_flag Vale.X64.CPU_Features_s.avx2_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_avx: cached_flag Vale.X64.CPU_Features_s.avx_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_bmi2: cached_flag Vale.X64.CPU_Features_s.bmi2_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_adx: cached_flag Vale.X64.CPU_Features_s.adx_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_sse: cached_flag Vale.X64.CPU_Features_s.sse_enabled =
  B.gcmalloc_of_list HS.root [ false ]
val cpu_has_movbe:cached_flag Vale.X64.CPU_Features_s.movbe_enabled
EverCrypt.AutoConfig2.eternal_pointer (EverCrypt.AutoConfig2.flag Vale.X64.CPU_Features_s.movbe_enabled
    )