val finv (x: elem) : elem
let finv (x:elem) : elem = x **% (prime - 2)
val finv (x: elem) : elem
let finv (x: elem) : elem =
x **% (prime - 2)
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 Spec.Curve25519.op_Star_Star_Percent Prims.op_Subtraction 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

let fadd (x:elem) (y:elem) : elem = (x + y) % prime
let fsub (x:elem) (y:elem) : elem = (x - y) % prime
let fmul (x:elem) (y:elem) : elem = (x * y) % prime

let ( +% ) = fadd
let ( -% ) = fsub
let ( *% ) = fmul

let fpow (x:elem) (b:nat) : elem = Lib.NatMod.pow_mod #prime x b
let ( **% ) = fpow
val finv (x: elem) : elem
x: Spec.Curve25519.elem -> Spec.Curve25519.elem