val fdiv_cancel_lemma: x:elem -> y:elem -> z:elem{z <> zero} -> Lemma ((x *% z) /% (z *% y) == x /% y)
let fdiv_cancel_lemma x y z =
  prime_lemma ();
  LM.lemma_div_mod_prime_cancel #prime x y z
val fdiv_cancel_lemma: x:elem -> y:elem -> z:elem{z <> zero} -> Lemma ((x *% z) /% (z *% y) == x /% y)
let fdiv_cancel_lemma x y z =
prime_lemma ();
LM.lemma_div_mod_prime_cancel #prime x y z
Spec.Ed25519.Lemmas.fst.checked
Spec.Ed25519.PointOps.fst.checked Spec.Curve25519.Lemmas.fst.checked Spec.Curve25519.fst.checked prims.fst.checked Lib.NatMod.fsti.checked Lib.Exponentiation.fsti.checked Lib.ByteSequence.fsti.checked FStar.Tactics.Effect.fsti.checked FStar.Tactics.CanonCommSemiring.fst.checked FStar.Tactics.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Math.Fermat.fsti.checked FStar.Math.Euclid.fsti.checked FStar.Calc.fsti.checked FStar.Algebra.CommMonoid.fst.checked
Spec.Ed25519.Lemmas.fst
Spec.Curve25519.elem Prims.b2t Prims.op_disEquality Spec.Curve25519.zero Lib.NatMod.lemma_div_mod_prime_cancel Spec.Curve25519.prime Prims.unit Spec.Ed25519.Lemmas.prime_lemma
module Spec.Ed25519.Lemmas

open FStar.Mul

module Fermat = FStar.Math.Fermat
module Euclid = FStar.Math.Euclid

module LE = Lib.Exponentiation
module LM = Lib.NatMod

open Spec.Curve25519
open Spec.Curve25519.Lemmas
open Spec.Ed25519.PointOps

open FStar.Algebra.CommMonoid
open FStar.Tactics.CanonCommSemiring
open FStar.Tactics

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

[@canon_attr]
noextract
let elem_add_cm : cm elem =
  CM zero ( +% ) (LM.lemma_add_mod_one #prime) (LM.lemma_add_mod_assoc #prime) (LM.lemma_add_mod_comm #prime)

[@canon_attr]
noextract
let elem_mul_cm : cm elem =
  CM one ( *% ) (LM.lemma_mul_mod_one #prime) (LM.lemma_mul_mod_assoc #prime) (LM.lemma_mul_mod_comm #prime)

val fmul_zero_l: mult_zero_l_lemma elem elem_add_cm elem_mul_cm
let fmul_zero_l a = assert_norm (forall x. zero *% x == zero)

let ( ~% ) (a:elem) : elem = (-a) % prime

val fadd_opp (a:elem) : Lemma (a +% ~%a == zero)
let fadd_opp a =
  FStar.Math.Lemmas.lemma_mod_add_distr a (-a) prime;
  FStar.Math.Lemmas.small_mod 0 prime

[@canon_attr]
noextract
let elem_cr : cr elem =
  CR elem_add_cm elem_mul_cm ( ~% ) fadd_opp (LM.lemma_mod_distributivity_add_right #prime) fmul_zero_l

noextract
let ed25519_semiring () : Tac unit = canon_semiring elem_cr; trefl()


assume val prime_lemma: unit -> Lemma (Euclid.is_prime prime)
// see Theorem 3.3. from https://eprint.iacr.org/2007/286.pdf
// precondition: d is not a square in Z/prime
assume val denominator_lemma: p:aff_point -> q:aff_point -> Lemma
  (requires is_on_curve p /\ is_on_curve q)
  (ensures (let x1, y1 = p in let x2, y2 = q in
    1 +% d *% (x1 *% x2) *% (y1 *% y2) <> zero /\
    1 -% d *% (x1 *% x2) *% (y1 *% y2) <> zero))
assume val denominator_lemma1: y:elem -> Lemma (d *% (y *% y) +% one <> zero)

/////////////////////////////////////
//// Properties for finv and fdiv ///
/////////////////////////////////////

val fdiv_lemma: x:elem{x <> zero} -> Lemma (x /% x == one)
let fdiv_lemma x =
  prime_lemma ();
  LM.lemma_div_mod_prime #prime x

val fdiv_one_lemma: x:elem -> Lemma (x /% one == x)
let fdiv_one_lemma x =
  prime_lemma ();
  LM.lemma_div_mod_prime_one #prime x

val fdiv_one_lemma1: x:elem -> z:elem{z <> zero} -> Lemma (x *% (z *% finv z) == x)
let fdiv_one_lemma1 x z =
  fdiv_lemma z;
  LM.lemma_mul_mod_one #prime x

val fdiv_cancel_lemma: x:elem -> y:elem -> z:elem{z <> zero} -> Lemma ((x *% z) /% (z *% y) == x /% y)
val fdiv_cancel_lemma: x:elem -> y:elem -> z:elem{z <> zero} -> Lemma ((x *% z) /% (z *% y) == x /% y)

    x: Spec.Curve25519.elem ->
    y: Spec.Curve25519.elem ->
    z: Spec.Curve25519.elem{z <> Spec.Curve25519.zero}
  -> FStar.Pervasives.Lemma (ensures x *% z /% (z *% y) == x /% y)