let code_aesni = VC.va_code_Check_aesni_stdcall IA.win
let code_aesni =
VC.va_code_Check_aesni_stdcall IA.win
Vale.Stdcalls.X64.Cpuid.fsti.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Lib.X64.Cpuidstdcall.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Stdcalls.X64.Cpuid.fsti
Vale.Lib.X64.Cpuidstdcall.va_code_Check_aesni_stdcall Vale.Interop.Assumptions.win
module Vale.Stdcalls.X64.Cpuid

open FStar.Mul
open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters

module VC = Vale.Lib.X64.Cpuidstdcall

(* A little utility to trigger normalization in types *)
noextract
let as_t (#a:Type) (x:normal a) : a = x
noextract
let as_normal_t (#a:Type) (x:a) : normal a = x

[@__reduce__] noextract
let dom: IX64.arity_ok_stdcall td = []

(* Need to rearrange the order of arguments *)
[@__reduce__] noextract
let aesni_pre : VSig.vale_pre dom =
  fun (c:V.va_code)
    (va_s0:V.va_state) ->
      VC.va_req_Check_aesni_stdcall c va_s0 IA.win

[@__reduce__] noextract
let aesni_post : VSig.vale_post dom =
  fun (c:V.va_code)
    (va_s0:V.va_state)
    (va_s1:V.va_state)
    (f:V.va_fuel) ->
      VC.va_ens_Check_aesni_stdcall c va_s0 IA.win va_s1 f

(* The vale lemma doesn't quite suffice to prove the modifies clause
   expected of the interop layer *)
[@__reduce__] noextract
let aesni_lemma'
    (code:V.va_code)
    (_win:bool)
    (va_s0:V.va_state)
 : Ghost (V.va_state & V.va_fuel)
     (requires
       aesni_pre code va_s0)
     (ensures (fun (va_s1, f) ->
       V.eval_code code va_s0 f va_s1 /\
       VSig.vale_calling_conventions_stdcall va_s0 va_s1 /\
       aesni_post code va_s0 va_s1 f))
 = VC.va_lemma_Check_aesni_stdcall code va_s0 IA.win

(* Prove that vm_lemma' has the required type *)
noextract
let aesni_lemma = as_t #(VSig.vale_sig_stdcall aesni_pre aesni_post) aesni_lemma'
val code_aesni : Vale.X64.Decls.va_code
Vale.X64.Decls.va_code