val fsqr_e : normal lowstar_Fsqr_t
let fsqr_e = as_normal_t #lowstar_Fsqr_t lowstar_Fsqr
val fsqr_e : normal lowstar_Fsqr_t
let fsqr_e =
as_normal_t #lowstar_Fsqr_t lowstar_Fsqr
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.Stdcalls.X64.Fsqr.as_normal_t Vale.Stdcalls.X64.Fsqr.lowstar_Fsqr_t Vale.Stdcalls.X64.Fsqr.lowstar_Fsqr
module Vale.Stdcalls.X64.Fsqr
open FStar.Mul

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

(* And here's the fsqr wrapper itself *)
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 fsqr_e : normal lowstar_Fsqr_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Fsqr.lowstar_Fsqr_t