val check_sha : normal lowstar_sha_t
let check_sha = as_normal_t #lowstar_sha_t lowstar_sha
val check_sha : normal lowstar_sha_t
let check_sha =
as_normal_t #lowstar_sha_t lowstar_sha
Vale.Stdcalls.X64.Cpuid.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Stdcalls.X64.Cpuid.fst
Vale.Stdcalls.X64.Cpuid.as_normal_t Vale.Stdcalls.X64.Cpuid.lowstar_sha_t Vale.Stdcalls.X64.Cpuid.lowstar_sha
module Vale.Stdcalls.X64.Cpuid
open FStar.Mul

(* And here's the check_aesni wrapper itself *)
let lowstar_aesni : lowstar_aesni_t  =
  IX64.wrap_weak_stdcall
    code_aesni
    dom
    (W.mk_prediction code_aesni dom [] (aesni_lemma code_aesni IA.win))

let check_aesni = as_normal_t #lowstar_aesni_t lowstar_aesni

(* And here's the check_aesni wrapper itself *)
let lowstar_sha : lowstar_sha_t  =
  IX64.wrap_weak_stdcall
    code_sha
    dom
    (W.mk_prediction code_sha dom [] (sha_lemma code_sha IA.win))
val check_sha : normal lowstar_sha_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Cpuid.lowstar_sha_t