val lowstar_sha:lowstar_sha_t
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 lowstar_sha:lowstar_sha_t
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))
Vale.Stdcalls.X64.Sha.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Stdcalls.X64.Sha.fst
Vale.Interop.X64.wrap_weak_stdcall Vale.Stdcalls.X64.Sha.code_sha Vale.Stdcalls.X64.Sha.dom Vale.AsLowStar.Wrapper.pre_rel_generic Vale.Interop.X64.max_stdcall Vale.Interop.X64.arg_reg_stdcall Prims.Nil Vale.Interop.Base.arg Vale.Stdcalls.X64.Sha.sha_pre Vale.AsLowStar.Wrapper.post_rel_generic Vale.Stdcalls.X64.Sha.sha_post Vale.AsLowStar.Wrapper.mk_prediction Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.Stdcalls.X64.Sha.sha_lemma Vale.Interop.Assumptions.win
module Vale.Stdcalls.X64.Sha
open FStar.Mul

#reset-options "--z3rlimit 50"
let z3rlimit_hack x = ()

(* And here's the sha wrapper itself *)
val lowstar_sha:lowstar_sha_t
Vale.Stdcalls.X64.Sha.lowstar_sha_t