val lowstar_fmul1:lowstar_fmul1_t
let lowstar_fmul1 : lowstar_fmul1_t  =
  assert_norm (List.length fmul1_dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_Fmul1
    fmul1_dom
    (W.mk_prediction code_Fmul1 fmul1_dom [] (fmul1_lemma code_Fmul1 IA.win))
val lowstar_fmul1:lowstar_fmul1_t
let lowstar_fmul1:lowstar_fmul1_t =
assert_norm (List.length fmul1_dom + List.length ([] <: list arg) <= 4);
IX64.wrap_weak_stdcall code_Fmul1
  fmul1_dom
  (W.mk_prediction code_Fmul1 fmul1_dom [] (fmul1_lemma code_Fmul1 IA.win))
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.Interop.X64.wrap_weak_stdcall Vale.Stdcalls.X64.Fmul.code_Fmul1 Vale.Stdcalls.X64.Fmul.fmul1_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.Fmul.fmul1_pre Vale.AsLowStar.Wrapper.post_rel_generic Vale.Stdcalls.X64.Fmul.fmul1_post Vale.AsLowStar.Wrapper.mk_prediction Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.Stdcalls.X64.Fmul.fmul1_lemma Vale.Interop.Assumptions.win Prims.unit FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.List.Tot.Base.length Vale.Interop.Base.td Prims.list
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))

let fmul2_e = as_normal_t #lowstar_fmul2_t lowstar_fmul2

(* And here's the fmul1 wrapper itself *)
val lowstar_fmul1:lowstar_fmul1_t
Vale.Stdcalls.X64.Fmul.lowstar_fmul1_t