val va_req_Check_osxsave_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop
let va_req_Check_osxsave_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_osxsave_stdcall win) va_s0 /\ va_get_ok va_s0)
val va_req_Check_osxsave_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop
let va_req_Check_osxsave_stdcall (va_b0: va_code) (va_s0: va_state) (win: bool) : prop =
(va_require_total va_b0 (va_code_Check_osxsave_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_osxsave_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
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)
  (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_lemma_Check_aesni_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_aesni_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> 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)))))))))
[@ va_qattr]
let va_wp_Check_aesni_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in 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_k va_sM (())))

val va_wpProof_Check_aesni_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_aesni_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_aesni_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_aesni_stdcall (win:bool) : (va_quickCode unit (va_code_Check_aesni_stdcall win))
  =
  (va_QProc (va_code_Check_aesni_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_aesni_stdcall win)
    (va_wpProof_Check_aesni_stdcall win))
//--
//-- Check_sha_stdcall

val va_code_Check_sha_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_sha_stdcall : win:bool -> Tot va_pbool
let va_req_Check_sha_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_sha_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_sha_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_sha_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 ==> sha_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_lemma_Check_sha_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_sha_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> sha_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)))))))))
[@ va_qattr]
let va_wp_Check_sha_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    sha_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_sha_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_sha_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_sha_stdcall win) ([va_Mod_flags;
    va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_sha_stdcall (win:bool) : (va_quickCode unit (va_code_Check_sha_stdcall win)) =
  (va_QProc (va_code_Check_sha_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_sha_stdcall win)
    (va_wpProof_Check_sha_stdcall win))
//--
//-- Check_adx_bmi2_stdcall

val va_code_Check_adx_bmi2_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_adx_bmi2_stdcall : win:bool -> Tot va_pbool
let va_req_Check_adx_bmi2_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_adx_bmi2_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_adx_bmi2_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_adx_bmi2_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 ==> adx_enabled /\ bmi2_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_lemma_Check_adx_bmi2_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_adx_bmi2_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> adx_enabled /\ bmi2_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)))))))))
[@ va_qattr]
let va_wp_Check_adx_bmi2_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    adx_enabled /\ bmi2_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k
    va_sM (())))

val va_wpProof_Check_adx_bmi2_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit ->
  Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_adx_bmi2_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_adx_bmi2_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_adx_bmi2_stdcall (win:bool) : (va_quickCode unit (va_code_Check_adx_bmi2_stdcall
  win)) =
  (va_QProc (va_code_Check_adx_bmi2_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64
    rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_adx_bmi2_stdcall
    win) (va_wpProof_Check_adx_bmi2_stdcall win))
//--
//-- Check_avx_stdcall

val va_code_Check_avx_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_avx_stdcall : win:bool -> Tot va_pbool
let va_req_Check_avx_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_avx_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_avx_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_avx_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 ==> avx_cpuid_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_lemma_Check_avx_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_avx_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> avx_cpuid_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)))))))))
[@ va_qattr]
let va_wp_Check_avx_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    avx_cpuid_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_avx_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_avx_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_avx_stdcall win) ([va_Mod_flags;
    va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_avx_stdcall (win:bool) : (va_quickCode unit (va_code_Check_avx_stdcall win)) =
  (va_QProc (va_code_Check_avx_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_avx_stdcall win)
    (va_wpProof_Check_avx_stdcall win))
//--
//-- Check_avx2_stdcall

val va_code_Check_avx2_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_avx2_stdcall : win:bool -> Tot va_pbool
let va_req_Check_avx2_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_avx2_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_avx2_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_avx2_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 ==> avx2_cpuid_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_lemma_Check_avx2_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_avx2_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> avx2_cpuid_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)))))))))
[@ va_qattr]
let va_wp_Check_avx2_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0
  =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    avx2_cpuid_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_avx2_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_avx2_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_avx2_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_avx2_stdcall (win:bool) : (va_quickCode unit (va_code_Check_avx2_stdcall win)) =
  (va_QProc (va_code_Check_avx2_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_avx2_stdcall win)
    (va_wpProof_Check_avx2_stdcall win))
//--
//-- Check_movbe_stdcall

val va_code_Check_movbe_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_movbe_stdcall : win:bool -> Tot va_pbool
let va_req_Check_movbe_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_movbe_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_movbe_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_movbe_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 ==> movbe_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_lemma_Check_movbe_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_movbe_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> movbe_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)))))))))
[@ va_qattr]
let va_wp_Check_movbe_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    movbe_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_movbe_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_movbe_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_movbe_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_movbe_stdcall (win:bool) : (va_quickCode unit (va_code_Check_movbe_stdcall win))
  =
  (va_QProc (va_code_Check_movbe_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_movbe_stdcall win)
    (va_wpProof_Check_movbe_stdcall win))
//--
//-- Check_sse_stdcall

val va_code_Check_sse_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_sse_stdcall : win:bool -> Tot va_pbool
let va_req_Check_sse_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_sse_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_sse_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_sse_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 ==> sse_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_lemma_Check_sse_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_sse_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> sse_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)))))))))
[@ va_qattr]
let va_wp_Check_sse_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) : Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    sse_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_sse_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_sse_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_sse_stdcall win) ([va_Mod_flags;
    va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax])
    va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_sse_stdcall (win:bool) : (va_quickCode unit (va_code_Check_sse_stdcall win)) =
  (va_QProc (va_code_Check_sse_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_sse_stdcall win)
    (va_wpProof_Check_sse_stdcall win))
//--
//-- Check_rdrand_stdcall

val va_code_Check_rdrand_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_rdrand_stdcall : win:bool -> Tot va_pbool
let va_req_Check_rdrand_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_rdrand_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_rdrand_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_rdrand_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 ==> rdrand_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_lemma_Check_rdrand_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_rdrand_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> rdrand_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)))))))))
[@ va_qattr]
let va_wp_Check_rdrand_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM = va_upd_flags va_x_efl (va_upd_reg64
    rR9 va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0 ==>
    rdrand_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM (())))

val va_wpProof_Check_rdrand_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_rdrand_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_rdrand_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx;
    va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_rdrand_stdcall (win:bool) : (va_quickCode unit (va_code_Check_rdrand_stdcall
  win)) =
  (va_QProc (va_code_Check_rdrand_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) (va_wp_Check_rdrand_stdcall win)
    (va_wpProof_Check_rdrand_stdcall win))
//--
//-- Check_avx512_stdcall

val va_code_Check_avx512_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_avx512_stdcall : win:bool -> Tot va_pbool
let va_req_Check_avx512_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) : prop =
  (va_require_total va_b0 (va_code_Check_avx512_stdcall win) va_s0 /\ va_get_ok va_s0)
let va_ens_Check_avx512_stdcall (va_b0:va_code) (va_s0:va_state) (win:bool) (va_sM:va_state)
  (va_fM:va_fuel) : prop =
  (va_req_Check_avx512_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 ==> avx512_cpuid_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 rR11 va_sM (va_update_reg64 rR10 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_lemma_Check_avx512_stdcall : va_b0:va_code -> va_s0:va_state -> win:bool
  -> Ghost (va_state & va_fuel)
  (requires (va_require_total va_b0 (va_code_Check_avx512_stdcall win) va_s0 /\ va_get_ok va_s0))
  (ensures (fun (va_sM, va_fM) -> va_ensure_total va_b0 va_s0 va_sM va_fM /\ va_get_ok va_sM /\
    (va_get_reg64 rRax va_sM =!= 0 ==> avx512_cpuid_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 rR11 va_sM
    (va_update_reg64 rR10 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)))))))))))
[@ va_qattr]
let va_wp_Check_avx512_stdcall (win:bool) (va_s0:va_state) (va_k:(va_state -> unit -> Type0)) :
  Type0 =
  (va_get_ok va_s0 /\ (forall (va_x_rax:nat64) (va_x_rbx:nat64) (va_x_rcx:nat64) (va_x_rdx:nat64)
    (va_x_r9:nat64) (va_x_r10:nat64) (va_x_r11:nat64) (va_x_efl:Vale.X64.Flags.t) . let va_sM =
    va_upd_flags va_x_efl (va_upd_reg64 rR11 va_x_r11 (va_upd_reg64 rR10 va_x_r10 (va_upd_reg64 rR9
    va_x_r9 (va_upd_reg64 rRdx va_x_rdx (va_upd_reg64 rRcx va_x_rcx (va_upd_reg64 rRbx va_x_rbx
    (va_upd_reg64 rRax va_x_rax va_s0))))))) in va_get_ok va_sM /\ (va_get_reg64 rRax va_sM =!= 0
    ==> avx512_cpuid_enabled) /\ va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0 ==> va_k va_sM
    (())))

val va_wpProof_Check_avx512_stdcall : win:bool -> va_s0:va_state -> va_k:(va_state -> unit -> Type0)
  -> Ghost (va_state & va_fuel & unit)
  (requires (va_t_require va_s0 /\ va_wp_Check_avx512_stdcall win va_s0 va_k))
  (ensures (fun (va_sM, va_f0, va_g) -> va_t_ensure (va_code_Check_avx512_stdcall win)
    ([va_Mod_flags; va_Mod_reg64 rR11; va_Mod_reg64 rR10; va_Mod_reg64 rR9; va_Mod_reg64 rRdx;
    va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) va_s0 va_k ((va_sM, va_f0, va_g))))
[@ "opaque_to_smt" va_qattr]
let va_quick_Check_avx512_stdcall (win:bool) : (va_quickCode unit (va_code_Check_avx512_stdcall
  win)) =
  (va_QProc (va_code_Check_avx512_stdcall win) ([va_Mod_flags; va_Mod_reg64 rR11; va_Mod_reg64
    rR10; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx; va_Mod_reg64 rRbx; va_Mod_reg64
    rRax]) (va_wp_Check_avx512_stdcall win) (va_wpProof_Check_avx512_stdcall win))
//--
//-- Check_osxsave_stdcall

val va_code_Check_osxsave_stdcall : win:bool -> Tot va_code

val va_codegen_success_Check_osxsave_stdcall : win:bool -> Tot va_pbool
val va_req_Check_osxsave_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