val lowstar_avx:lowstar_avx_t
let lowstar_avx : lowstar_avx_t  =
  IX64.wrap_weak_stdcall
    code_avx
    dom
    (W.mk_prediction code_avx dom [] (avx_lemma code_avx IA.win))
val lowstar_avx:lowstar_avx_t
let lowstar_avx:lowstar_avx_t =
IX64.wrap_weak_stdcall code_avx dom (W.mk_prediction code_avx dom [] (avx_lemma code_avx IA.win))
Vale.Stdcalls.X64.Cpuid.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Stdcalls.X64.Cpuid.fst
Vale.Interop.X64.wrap_weak_stdcall Vale.Stdcalls.X64.Cpuid.code_avx Vale.Stdcalls.X64.Cpuid.dom Vale.AsLowStar.Wrapper.pre_rel_generic Vale.Interop.X64.max_stdcall Vale.Interop.X64.arg_reg_stdcall Prims.Nil Vale.Interop.Base.arg Vale.Stdcalls.X64.Cpuid.avx_pre Vale.AsLowStar.Wrapper.post_rel_generic Vale.Stdcalls.X64.Cpuid.avx_post Vale.AsLowStar.Wrapper.mk_prediction Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.Stdcalls.X64.Cpuid.avx_lemma Vale.Interop.Assumptions.win
module Vale.Stdcalls.X64.Cpuid
open FStar.Mul

(* And here's the check_aesni wrapper itself *)
let lowstar_aesni : lowstar_aesni_t  =
  IX64.wrap_weak_stdcall
    code_aesni
    dom
    (W.mk_prediction code_aesni dom [] (aesni_lemma code_aesni IA.win))

let check_aesni = as_normal_t #lowstar_aesni_t lowstar_aesni

(* And here's the check_aesni wrapper itself *)
let lowstar_sha : lowstar_sha_t  =
  IX64.wrap_weak_stdcall
    code_sha
    dom
    (W.mk_prediction code_sha dom [] (sha_lemma code_sha IA.win))

let check_sha = as_normal_t #lowstar_sha_t lowstar_sha

(* And here's the check_adx wrapper itself *)
let lowstar_adx : lowstar_adx_t  =
  IX64.wrap_weak_stdcall
    code_adx
    dom
    (W.mk_prediction code_adx dom [] (adx_lemma code_adx IA.win))

let check_adx_bmi2 = as_normal_t #lowstar_adx_t lowstar_adx

(* And here's the check_avx wrapper itself *)
val lowstar_avx:lowstar_avx_t
Vale.Stdcalls.X64.Cpuid.lowstar_avx_t