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

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

(* And here's the sha 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 sha256_update : normal lowstar_sha_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Sha.lowstar_sha_t