val va_qcode_Check_aesni_stdcall (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Check_aesni_stdcall win))
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 (()))))
val va_qcode_Check_aesni_stdcall (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Check_aesni_stdcall win))
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 (()))))
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
Vale.X64.QuickCode.va_mods_t Prims.bool Vale.X64.QuickCodes.qblock Prims.unit Prims.Cons Vale.X64.Decls.va_code Vale.Lib.X64.Cpuid.va_code_Check_aesni_support Prims.Nil Vale.X64.Machine_s.precode Vale.X64.Decls.ins Vale.X64.Decls.ocmp Vale.X64.Decls.va_state Vale.X64.QuickCodes.va_QSeq Vale.X64.QuickCodes.va_range1 Vale.Lib.X64.Cpuid.va_quick_Check_aesni_support Vale.X64.QuickCodes.va_QEmpty Vale.X64.State.vale_state Vale.X64.QuickCodes.quickCodes Vale.X64.QuickCode.va_quickCode Vale.Lib.X64.Cpuidstdcall.va_code_Check_aesni_stdcall
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
val va_qcode_Check_aesni_stdcall (va_mods: va_mods_t) (win: bool)
    : (va_quickCode unit (va_code_Check_aesni_stdcall win))
va_mods: Vale.X64.QuickCode.va_mods_t -> win: Prims.bool
  -> Vale.X64.QuickCode.va_quickCode Prims.unit
      (Vale.Lib.X64.Cpuidstdcall.va_code_Check_aesni_stdcall win)