val lowstar_Fsqr:lowstar_Fsqr_t
let lowstar_Fsqr : lowstar_Fsqr_t  =
  assert_norm (List.length fsqr_dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_Fsqr
    fsqr_dom
    (W.mk_prediction code_Fsqr fsqr_dom [] (fsqr_lemma code_Fsqr IA.win))
val lowstar_Fsqr:lowstar_Fsqr_t
let lowstar_Fsqr:lowstar_Fsqr_t =
assert_norm (List.length fsqr_dom + List.length ([] <: list arg) <= 4);
IX64.wrap_weak_stdcall code_Fsqr
  fsqr_dom
  (W.mk_prediction code_Fsqr fsqr_dom [] (fsqr_lemma code_Fsqr IA.win))
Vale.Stdcalls.X64.Fsqr.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked
Vale.Stdcalls.X64.Fsqr.fst
Vale.Interop.X64.wrap_weak_stdcall Vale.Stdcalls.X64.Fsqr.code_Fsqr Vale.Stdcalls.X64.Fsqr.fsqr_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.Fsqr.fsqr_pre Vale.AsLowStar.Wrapper.post_rel_generic Vale.Stdcalls.X64.Fsqr.fsqr_post Vale.AsLowStar.Wrapper.mk_prediction Vale.Interop.X64.regs_modified_stdcall Vale.Interop.X64.xmms_modified_stdcall Vale.Stdcalls.X64.Fsqr.fsqr_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.Fsqr
open FStar.Mul

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

(* And here's the fsqr wrapper itself *)
val lowstar_Fsqr:lowstar_Fsqr_t
Vale.Stdcalls.X64.Fsqr.lowstar_Fsqr_t