val va_ens_Check_aesni_stdcall
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop
let va_ens_Check_aesni_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_aesni_stdcall va_b0 va_s0 win /\ va_ensure_total va_b0 va_s0 va_sM va_fM /\
    va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==> aesni_enabled /\ pclmulqdq_enabled) /\
    va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 /\ va_state_eq va_sM (va_update_flags va_sM
    (va_update_reg64 rR9 va_sM (va_update_reg64 rRdx va_sM (va_update_reg64 rRcx va_sM
    (va_update_reg64 rRbx va_sM (va_update_reg64 rRax va_sM (va_update_ok va_sM va_s0))))))))
val va_ens_Check_aesni_stdcall
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop
let va_ens_Check_aesni_stdcall
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop =
(va_req_Check_aesni_stdcall va_b0 va_s0 win /\ va_ensure_total va_b0 va_s0 va_sM va_fM /\
  va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==> aesni_enabled /\ pclmulqdq_enabled) /\
  va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 /\
  va_state_eq va_sM
    (va_update_flags va_sM
        (va_update_reg64 rR9
            va_sM
            (va_update_reg64 rRdx
                va_sM
                (va_update_reg64 rRcx
                    va_sM
                    (va_update_reg64 rRbx
                        va_sM
                        (va_update_reg64 rRax va_sM (va_update_ok va_sM 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 Vale.X64.Decls.va_fuel Prims.l_and Vale.Lib.X64.Cpuidstdcall.va_req_Check_aesni_stdcall Vale.X64.Decls.va_ensure_total Prims.b2t Vale.X64.Decls.va_get_ok Prims.l_imp Prims.l_not Prims.eq2 Prims.int Vale.X64.Decls.va_get_reg64 Vale.X64.Machine_s.rRax Vale.X64.CPU_Features_s.aesni_enabled Vale.X64.CPU_Features_s.pclmulqdq_enabled Vale.Def.Types_s.nat64 Vale.X64.Machine_s.rRbx Vale.X64.Decls.va_state_eq Vale.X64.Decls.va_update_flags Vale.X64.Decls.va_update_reg64 Vale.X64.Machine_s.rR9 Vale.X64.Machine_s.rRdx Vale.X64.Machine_s.rRcx Vale.X64.Decls.va_update_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
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)
let va_ens_Check_aesni_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
val va_ens_Check_aesni_stdcall
      (va_b0: va_code)
      (va_s0: va_state)
      (win: bool)
      (va_sM: va_state)
      (va_fM: va_fuel)
    : prop

    va_b0: Vale.X64.Decls.va_code ->
    va_s0: Vale.X64.Decls.va_state ->
    win: Prims.bool ->
    va_sM: Vale.X64.Decls.va_state ->
    va_fM: Vale.X64.Decls.va_fuel
  -> Prims.prop