val va_req_Check_aesni_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop
let va_req_Check_aesni_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_aesni_stdcall win) va_s0 /\ va_get_ok va_s0)
val va_req_Check_aesni_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop
let va_req_Check_aesni_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop =
(va_require_total va_b0 (va_code_Check_aesni_stdcall win) va_s0 /\ va_get_ok va_s0)
Vale.Lib.X64.Cpuidstdcall.fsti.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.Flags.fsti.checked Vale.X64.Decls.fsti.checked Vale.X64.CPU_Features_s.fst.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.fsti
Vale.X64.Decls.va_code Vale.X64.Decls.va_state Prims.bool Prims.l_and Vale.X64.Decls.va_require_total Vale.Lib.X64.Cpuidstdcall.va_code_Check_aesni_stdcall Prims.b2t Vale.X64.Decls.va_get_ok Prims.prop
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

//-- Check_aesni_stdcall

val va_code_Check_aesni_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_aesni_stdcall : win:bool -> Tot va_pbool
val va_req_Check_aesni_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop
va_b0: Vale.X64.Decls.va_code -> va_s0: Vale.X64.Decls.va_state -> win: Prims.bool -> Prims.prop