val recall: unit -> Stack unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 ->
    B.(loc_not_unused_in h1 `loc_includes` (fp ())) /\ h0 == h1))
let recall () =
  B.recall cpu_has_shaext;
  B.recall cpu_has_aesni;
  B.recall cpu_has_pclmulqdq;
  B.recall cpu_has_avx2;
  B.recall cpu_has_avx;
  B.recall cpu_has_bmi2;
  B.recall cpu_has_adx;
  B.recall cpu_has_sse;
  B.recall cpu_has_movbe;
  B.recall cpu_has_rdrand;
  B.recall cpu_has_avx512
val recall: unit -> Stack unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 ->
    B.(loc_not_unused_in h1 `loc_includes` (fp ())) /\ h0 == h1))
let recall () =
B.recall cpu_has_shaext;
B.recall cpu_has_aesni;
B.recall cpu_has_pclmulqdq;
B.recall cpu_has_avx2;
B.recall cpu_has_avx;
B.recall cpu_has_bmi2;
B.recall cpu_has_adx;
B.recall cpu_has_sse;
B.recall cpu_has_movbe;
B.recall cpu_has_rdrand;
B.recall cpu_has_avx512
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
Prims.unit LowStar.Monotonic.Buffer.recall EverCrypt.AutoConfig2.flag Vale.X64.CPU_Features_s.avx512_enabled LowStar.Buffer.trivial_preorder EverCrypt.AutoConfig2.cpu_has_avx512 Vale.X64.CPU_Features_s.rdrand_enabled EverCrypt.AutoConfig2.cpu_has_rdrand Vale.X64.CPU_Features_s.movbe_enabled EverCrypt.AutoConfig2.cpu_has_movbe Vale.X64.CPU_Features_s.sse_enabled EverCrypt.AutoConfig2.cpu_has_sse Vale.X64.CPU_Features_s.adx_enabled EverCrypt.AutoConfig2.cpu_has_adx Vale.X64.CPU_Features_s.bmi2_enabled EverCrypt.AutoConfig2.cpu_has_bmi2 Vale.X64.CPU_Features_s.avx_enabled EverCrypt.AutoConfig2.cpu_has_avx Vale.X64.CPU_Features_s.avx2_enabled EverCrypt.AutoConfig2.cpu_has_avx2 Vale.X64.CPU_Features_s.pclmulqdq_enabled EverCrypt.AutoConfig2.cpu_has_pclmulqdq Vale.X64.CPU_Features_s.aesni_enabled EverCrypt.AutoConfig2.cpu_has_aesni Vale.X64.CPU_Features_s.sha_enabled EverCrypt.AutoConfig2.cpu_has_shaext
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 ]
let cpu_has_movbe: cached_flag Vale.X64.CPU_Features_s.movbe_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_rdrand: cached_flag Vale.X64.CPU_Features_s.rdrand_enabled =
  B.gcmalloc_of_list HS.root [ false ]
let cpu_has_avx512: cached_flag Vale.X64.CPU_Features_s.avx512_enabled =
  B.gcmalloc_of_list HS.root [ false ]

inline_for_extraction
let mk_getter #b (f: cached_flag b): getter b = fun () ->
  B.recall f;
  B.index f 0ul

let has_shaext = mk_getter cpu_has_shaext
let has_aesni = mk_getter cpu_has_aesni
let has_pclmulqdq = mk_getter cpu_has_pclmulqdq
let has_avx2 = mk_getter cpu_has_avx2
let has_avx = mk_getter cpu_has_avx
let has_bmi2 = mk_getter cpu_has_bmi2
let has_adx = mk_getter cpu_has_adx
let has_sse = mk_getter cpu_has_sse
let has_movbe = mk_getter cpu_has_movbe
let has_rdrand = mk_getter cpu_has_rdrand
let has_avx512 = mk_getter cpu_has_avx512

let fp () =
  B.loc_buffer cpu_has_shaext `B.loc_union`
  B.loc_buffer cpu_has_aesni `B.loc_union`
  B.loc_buffer cpu_has_pclmulqdq `B.loc_union`
  B.loc_buffer cpu_has_avx2 `B.loc_union`
  B.loc_buffer cpu_has_avx `B.loc_union`
  B.loc_buffer cpu_has_bmi2 `B.loc_union`
  B.loc_buffer cpu_has_adx `B.loc_union`
  B.loc_buffer cpu_has_sse `B.loc_union`
  B.loc_buffer cpu_has_movbe `B.loc_union`
  B.loc_buffer cpu_has_rdrand `B.loc_union`
  B.loc_buffer cpu_has_avx512
val recall: unit -> Stack unit
  (requires (fun _ -> True))
  (ensures (fun h0 _ h1 ->
    B.(loc_not_unused_in h1 `loc_includes` (fp ())) /\ h0 == h1))
_: Prims.unit -> FStar.HyperStack.ST.Stack Prims.unit