val fadd (x y: felem) : felem
let fadd (x y:felem) : felem = (x + y) % prime
val fadd (x y: felem) : felem
let fadd (x y: felem) : felem =
(x + y) % prime
Spec.P256.PointOps.fst.checked
prims.fst.checked Lib.Sequence.fsti.checked Lib.RawIntTypes.fsti.checked Lib.NatMod.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
Spec.P256.PointOps.fst
Spec.P256.PointOps.felem Prims.op_Modulus Prims.op_Addition Spec.P256.PointOps.prime
module Spec.P256.PointOps

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

module M = Lib.NatMod
module BSeq = Lib.ByteSequence

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

///  Base field

// 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff
let prime: (a:pos{a = 0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff /\ a < pow2 256}) =
  let p = pow2 256 - pow2 224 + pow2 192 + pow2 96 - 1 in
  assert_norm (0xffffffff00000001000000000000000000000000ffffffffffffffffffffffff = p);
  assert_norm (p < pow2 256); p

let felem = x:nat{x < prime}
let zero : felem = 0
let one  : felem = 1
val fadd (x y: felem) : felem
x: Spec.P256.PointOps.felem -> y: Spec.P256.PointOps.felem -> Spec.P256.PointOps.felem