val fmul2_e : normal lowstar_fmul2_t
let fmul2_e = as_normal_t #lowstar_fmul2_t lowstar_fmul2
val fmul2_e : normal lowstar_fmul2_t
let fmul2_e =
as_normal_t #lowstar_fmul2_t lowstar_fmul2
Vale.Stdcalls.X64.Fmul.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked
Vale.Stdcalls.X64.Fmul.fst
Vale.Stdcalls.X64.Fmul.as_normal_t Vale.Stdcalls.X64.Fmul.lowstar_fmul2_t Vale.Stdcalls.X64.Fmul.lowstar_fmul2
module Vale.Stdcalls.X64.Fmul
open FStar.Mul

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

(* And here's the fmul wrapper itself *)
let lowstar_fmul : lowstar_fmul_t  =
  assert_norm (List.length fmul_dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_Fmul
    fmul_dom
    (W.mk_prediction code_Fmul fmul_dom [] (fmul_lemma code_Fmul IA.win))

let fmul_e = as_normal_t #lowstar_fmul_t lowstar_fmul

(* And here's the fmul2 wrapper itself *)
let lowstar_fmul2 : lowstar_fmul2_t  =
  assert_norm (List.length fmul_dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_Fmul2
    fmul_dom
    (W.mk_prediction code_Fmul2 fmul_dom [] (fmul2_lemma code_Fmul2 IA.win))
val fmul2_e : normal lowstar_fmul2_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Fmul.lowstar_fmul2_t