val va_code_Check_aesni_stdcall : win:bool -> Tot va_code
let va_code_Check_aesni_stdcall win =
  (va_Block (va_CCons (va_code_Check_aesni_support ()) (va_CNil ())))
val va_code_Check_aesni_stdcall : win:bool -> Tot va_code
let va_code_Check_aesni_stdcall win =
(va_Block (va_CCons (va_code_Check_aesni_support ()) (va_CNil ())))
Vale.Lib.X64.Cpuidstdcall.fst.checked
Vale.X64.State.fsti.checked Vale.X64.QuickCodes.fsti.checked Vale.X64.QuickCode.fst.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.InsBasic.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.checked Vale.Lib.X64.Cpuid.fsti.checked Vale.Lib.Meta.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Vale.Lib.X64.Cpuidstdcall.fst
Prims.bool Vale.X64.Decls.va_Block Vale.X64.Decls.va_CCons Vale.Lib.X64.Cpuid.va_code_Check_aesni_support Vale.X64.Decls.va_CNil Vale.X64.Decls.va_code
module Vale.Lib.X64.Cpuidstdcall
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.X64.Machine_s
open Vale.X64.Memory
open Vale.X64.State
open Vale.X64.Decls
open Vale.X64.InsBasic
open Vale.X64.QuickCode
open Vale.X64.QuickCodes
open Vale.X64.CPU_Features_s

open Vale.Lib.Meta
open Vale.Lib.X64.Cpuid
//-- Check_aesni_stdcall

[@ "opaque_to_smt" va_qattr]
val va_code_Check_aesni_stdcall : win:bool -> Tot va_code
win: Prims.bool -> Vale.X64.Decls.va_code