val add_scalar_e : normal lowstar_add1_t
let add_scalar_e //: normal lowstar_add1_t
  = as_normal_t #lowstar_add1_t lowstar_add1
val add_scalar_e : normal lowstar_add1_t
let add_scalar_e =
as_normal_t #lowstar_add1_t lowstar_add1
Vale.Stdcalls.X64.Fadd.fst.checked
Vale.X64.State.fsti.checked Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Memory.fsti.checked Vale.X64.Machine_s.fst.checked Vale.X64.Decls.fsti.checked Vale.Interop.X64.fsti.checked Vale.Interop.Base.fst.checked Vale.Interop.Assumptions.fst.checked Vale.Def.Types_s.fst.checked Vale.Curve25519.X64.FastWide.fsti.checked Vale.Curve25519.X64.FastUtil.fsti.checked Vale.Curve25519.X64.FastHybrid.fsti.checked Vale.AsLowStar.Wrapper.fsti.checked Vale.AsLowStar.ValeSig.fst.checked Vale.AsLowStar.LowStarSig.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Vale.Stdcalls.X64.Fadd.fst
Vale.Stdcalls.X64.Fadd.as_normal_t Vale.Stdcalls.X64.Fadd.lowstar_add1_t Vale.Stdcalls.X64.Fadd.lowstar_add1
module Vale.Stdcalls.X64.Fadd
open FStar.Mul

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

open FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open Vale.Def.Types_s

open Vale.Interop.Base
module IX64 = Vale.Interop.X64
module VSig = Vale.AsLowStar.ValeSig
module LSig = Vale.AsLowStar.LowStarSig
module ME = Vale.X64.Memory
module V = Vale.X64.Decls
module IA = Vale.Interop.Assumptions
module W = Vale.AsLowStar.Wrapper
open Vale.X64.MemoryAdapters
module VS = Vale.X64.State
module MS = Vale.X64.Machine_s

module FU = Vale.Curve25519.X64.FastUtil
module FH = Vale.Curve25519.X64.FastHybrid
module FW = Vale.Curve25519.X64.FastWide

(* And here's the fadd wrapper itself *)
let lowstar_add1 : lowstar_add1_t  =
  assert_norm (List.length dom + List.length ([]<:list arg) <= 4);
  IX64.wrap_weak_stdcall
    code_add1
    dom
    (W.mk_prediction code_add1 dom [] (add1_lemma code_add1 IA.win))
val add_scalar_e : normal lowstar_add1_t
Vale.Interop.Base.normal Vale.Stdcalls.X64.Fadd.lowstar_add1_t