val va_codegen_success_Check_avx_stdcall : win:bool -> Tot va_pbool
let va_codegen_success_Check_avx_stdcall win =
  (va_pbool_and (va_codegen_success_Check_avx_support ()) (va_ttrue ()))
val va_codegen_success_Check_avx_stdcall : win:bool -> Tot va_pbool
let va_codegen_success_Check_avx_stdcall win =
(va_pbool_and (va_codegen_success_Check_avx_support ()) (va_ttrue ()))
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_pbool_and Vale.Lib.X64.Cpuid.va_codegen_success_Check_avx_support Vale.X64.Decls.va_ttrue Vale.X64.Decls.va_pbool
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]
let va_code_Check_aesni_stdcall win =
  (va_Block (va_CCons (va_code_Check_aesni_support ()) (va_CNil ())))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Check_aesni_stdcall win =
  (va_pbool_and (va_codegen_success_Check_aesni_support ()) (va_ttrue ()))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Check_aesni_stdcall (va_mods:va_mods_t) (win:bool) : (va_quickCode unit
  (va_code_Check_aesni_stdcall win)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 41 column 24 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_quick_Check_aesni_support ()) (va_QEmpty (()))))



[@"opaque_to_smt"]
let va_lemma_Check_aesni_stdcall va_b0 va_s0 win =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok] in
  let va_qc = va_qcode_Check_aesni_stdcall va_mods win in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Check_aesni_stdcall win) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 29 column 1 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 38 column 56 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRax va_sM =!= 0 ==> aesni_enabled /\ pclmulqdq_enabled) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 39 column 24 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Check_aesni_stdcall win va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Check_aesni_stdcall (va_code_Check_aesni_stdcall win) va_s0 win in
  va_lemma_upd_update va_sM;
  assert (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_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Check_sha_stdcall

[@ "opaque_to_smt" va_qattr]
let va_code_Check_sha_stdcall win =
  (va_Block (va_CCons (va_code_Check_sha_support ()) (va_CNil ())))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Check_sha_stdcall win =
  (va_pbool_and (va_codegen_success_Check_sha_support ()) (va_ttrue ()))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Check_sha_stdcall (va_mods:va_mods_t) (win:bool) : (va_quickCode unit
  (va_code_Check_sha_stdcall win)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 55 column 22 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_quick_Check_sha_support ()) (va_QEmpty (()))))



[@"opaque_to_smt"]
let va_lemma_Check_sha_stdcall va_b0 va_s0 win =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok] in
  let va_qc = va_qcode_Check_sha_stdcall va_mods win in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Check_sha_stdcall win) va_qc va_s0 (fun
    va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 45 column 1 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 52 column 33 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRax va_sM =!= 0 ==> sha_enabled) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 53 column 24 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Check_sha_stdcall win va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Check_sha_stdcall (va_code_Check_sha_stdcall win) va_s0 win in
  va_lemma_upd_update va_sM;
  assert (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_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Check_adx_bmi2_stdcall

[@ "opaque_to_smt" va_qattr]
let va_code_Check_adx_bmi2_stdcall win =
  (va_Block (va_CCons (va_code_Check_adx_bmi2_support ()) (va_CNil ())))

[@ "opaque_to_smt" va_qattr]
let va_codegen_success_Check_adx_bmi2_stdcall win =
  (va_pbool_and (va_codegen_success_Check_adx_bmi2_support ()) (va_ttrue ()))

[@ "opaque_to_smt" va_qattr]
let va_qcode_Check_adx_bmi2_stdcall (va_mods:va_mods_t) (win:bool) : (va_quickCode unit
  (va_code_Check_adx_bmi2_stdcall win)) =
  (qblock va_mods (fun (va_s:va_state) -> let (va_old_s:va_state) = va_s in va_QSeq va_range1
    "***** PRECONDITION NOT MET AT line 68 column 27 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_quick_Check_adx_bmi2_support ()) (va_QEmpty (()))))



[@"opaque_to_smt"]
let va_lemma_Check_adx_bmi2_stdcall va_b0 va_s0 win =
  let (va_mods:va_mods_t) = [va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok] in
  let va_qc = va_qcode_Check_adx_bmi2_stdcall va_mods win in
  let (va_sM, va_fM, va_g) = va_wp_sound_code_norm (va_code_Check_adx_bmi2_stdcall win) va_qc va_s0
    (fun va_s0 va_sM va_g -> let () = va_g in label va_range1
    "***** POSTCONDITION NOT MET AT line 58 column 1 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_ok va_sM) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 65 column 49 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRax va_sM =!= 0 ==> adx_enabled /\ bmi2_enabled) /\ label va_range1
    "***** POSTCONDITION NOT MET AT line 66 column 24 of file /home/gebner/everest/hacl-star/vale/code/lib/util/x64/stdcalls/Vale.Lib.X64.Cpuidstdcall.vaf *****"
    (va_get_reg64 rRbx va_sM == va_get_reg64 rRbx va_s0)) in
  assert_norm (va_qc.mods == va_mods);
  va_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax; va_Mod_ok]) va_sM va_s0;
  (va_sM, va_fM)


[@"opaque_to_smt"]
let va_wpProof_Check_adx_bmi2_stdcall win va_s0 va_k =
  let (va_sM, va_f0) = va_lemma_Check_adx_bmi2_stdcall (va_code_Check_adx_bmi2_stdcall win) va_s0
    win in
  va_lemma_upd_update va_sM;
  assert (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_lemma_norm_mods ([va_Mod_flags; va_Mod_reg64 rR9; va_Mod_reg64 rRdx; va_Mod_reg64 rRcx;
    va_Mod_reg64 rRbx; va_Mod_reg64 rRax]) va_sM va_s0;
  let va_g = () in
  (va_sM, va_f0, va_g)

//--
//-- Check_avx_stdcall

[@ "opaque_to_smt" va_qattr]
let va_code_Check_avx_stdcall win =
  (va_Block (va_CCons (va_code_Check_avx_support ()) (va_CNil ())))

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