val fadd (x y: elem) : elem
let fadd (x:elem) (y:elem) : elem = (x + y) % prime
val fadd (x y: elem) : elem
let fadd (x y: elem) : elem =
(x + y) % prime
Spec.Curve25519.fst.checked
Spec.Curve25519.Lemmas.fst.checked prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked
Spec.Curve25519.fst
Spec.Curve25519.elem Prims.op_Modulus Prims.op_Addition Spec.Curve25519.prime
module Spec.Curve25519

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.ByteSequence

open Spec.Curve25519.Lemmas

#set-options "--z3rlimit 30 --ifuel 0 --fuel 0"

(* Field types and parameters *)
let prime : pos = pow2 255 - 19

type elem = x:nat{x < prime}
let zero : elem = 0
let one  : elem = 1
val fadd (x y: elem) : elem
x: Spec.Curve25519.elem -> y: Spec.Curve25519.elem -> Spec.Curve25519.elem