val aff_point_double_lemma: p:aff_point{is_on_curve p} ->
  Lemma (aff_point_double p == aff_point_add p p)
let aff_point_double_lemma p =
  let x, y = p in
  let k1 = x *% y +% y *% x in
  let k2 = 1 +% d *% (x *% x) *% (y *% y) in
  let k3 = y *% y +% x *% x in
  let k4 = 1 -% d *% (x *% x) *% (y *% y) in

  let k5 = 2 *% x *% y in
  let k6 = y *% y -% x *% x in
  let k7 = y *% y +% x *% x in
  let k8 = 2 -% y *% y +% x *% x in
  assert (aff_point_add p p == (k1 /% k2, k3 /% k4));
  assert (aff_point_double p == (k5 /% k6, k7 /% k8));

  calc (==) {
    k1;
    (==) { }
    x *% y +% y *% x;
    (==) { assert (x *% y +% y *% x == 2 *% x *% y) by (ed25519_semiring ()) }
    2 *% x *% y;
    (==) { }
    k5;
    };

  calc (==) {
    k2;
    (==) { }
    1 +% d *% (x *% x) *% (y *% y);
    (==) { }
    y *% y -% x *% x;
    (==) { }
    k6;
    };

  calc (==) {
    k4;
    (==) { }
    1 -% d *% (x *% x) *% (y *% y);
    (==) { lemma_aff_double_aux x y }
    2 -% y *% y +% x *% x;
    (==) { }
    k8;
    }
val aff_point_double_lemma: p:aff_point{is_on_curve p} ->
  Lemma (aff_point_double p == aff_point_add p p)
let aff_point_double_lemma p =
let x, y = p in
let k1 = x *% y +% y *% x in
let k2 = 1 +% d *% (x *% x) *% (y *% y) in
let k3 = y *% y +% x *% x in
let k4 = 1 -% d *% (x *% x) *% (y *% y) in
let k5 = 2 *% x *% y in
let k6 = y *% y -% x *% x in
let k7 = y *% y +% x *% x in
let k8 = 2 -% y *% y +% x *% x in
assert (aff_point_add p p == (k1 /% k2, k3 /% k4));
assert (aff_point_double p == (k5 /% k6, k7 /% k8));
calc ( == ) {
  k1;
  ( == ) { () }
  x *% y +% y *% x;
  ( == ) { FStar.Tactics.Effect.assert_by_tactic (x *% y +% y *% x == 2 *% x *% y)
    (fun _ ->
        ();
        (ed25519_semiring ())) }
  2 *% x *% y;
  ( == ) { () }
  k5;
};
calc ( == ) {
  k2;
  ( == ) { () }
  1 +% d *% (x *% x) *% (y *% y);
  ( == ) { () }
  y *% y -% x *% x;
  ( == ) { () }
  k6;
};
calc ( == ) {
  k4;
  ( == ) { () }
  1 -% d *% (x *% x) *% (y *% y);
  ( == ) { lemma_aff_double_aux x y }
  2 -% y *% y +% x *% x;
  ( == ) { () }
  k8;
}
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.Ed25519.PointOps.aff_point Spec.Ed25519.PointOps.is_on_curve Spec.Curve25519.elem FStar.Calc.calc_finish Prims.eq2 Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step Spec.Curve25519.op_Plus_Percent Spec.Curve25519.op_Subtraction_Percent Spec.Curve25519.op_Star_Percent Spec.Ed25519.PointOps.d FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Spec.Ed25519.Lemmas.lemma_aff_double_aux FStar.Tactics.Effect.assert_by_tactic Spec.Ed25519.Lemmas.ed25519_semiring Prims._assert FStar.Pervasives.Native.tuple2 Spec.Ed25519.PointOps.aff_point_double FStar.Pervasives.Native.Mktuple2 Spec.Curve25519.op_Slash_Percent Spec.Ed25519.PointOps.aff_point_add
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)
let fdiv_cancel_lemma x y z =
  prime_lemma ();
  LM.lemma_div_mod_prime_cancel #prime x y z

val fdiv_to_one_denominator: x1:elem -> x2:elem -> z1:elem{z1 <> zero} -> z2:elem{z2 <> zero} ->
  Lemma (x1 /% z1 *% (x2 /% z2) == x1 *% x2 /% (z1 *% z2))
let fdiv_to_one_denominator x1 x2 z1 z2 =
  prime_lemma ();
  LM.lemma_div_mod_prime_to_one_denominator #prime x1 x2 z1 z2


val fmul_zero_lemma: x:elem -> y:elem -> Lemma (x *% y == 0 <==> (x == 0 \/ y == 0))
let fmul_zero_lemma x y =
  prime_lemma ();
  if x = 0 || y = 0 then ()
  else
    if (x *% y) = 0 then
      Fermat.mod_mult_congr prime x 0 y
    else ()


val fmul_nonzero_lemma: x:elem -> y:elem -> Lemma
  (requires x <> zero /\ y <> zero)
  (ensures  x *% y <> zero)
let fmul_nonzero_lemma x y =
  fmul_zero_lemma x y


val finv2_nonzero_lemma: x:elem -> y:elem -> Lemma
  (requires x <> zero /\ y <> zero)
  (ensures  finv (x *% y) <> zero)
let finv2_nonzero_lemma x y =
  fmul_nonzero_lemma x y;
  fdiv_lemma (x *% y)


////////////////////////////////////////////
//// Addition laws in affine coordinates ///
////////////////////////////////////////////

val lemma_aff_double_aux: x:elem -> y:elem -> Lemma
  (requires 1 +% d *% (x *% x) *% (y *% y) == y *% y -% x *% x)
  (ensures  1 -% d *% (x *% x) *% (y *% y) == 2 -% y *% y +% x *% x)
let lemma_aff_double_aux x y =
  Math.Lemmas.mod_add_both (1 + d *% (x *% x) *% (y *% y)) (y *% y -% x *% x) (-1) prime;
  assert ((d *% (x *% x) *% (y *% y)) % prime == (y *% y -% x *% x - 1) % prime);
  Math.Lemmas.small_mod (d *% (x *% x) *% (y *% y)) prime;
  assert (d *% (x *% x) *% (y *% y) == y *% y -% x *% x -% 1);

  calc (==) {
    1 -% d *% (x *% x) *% (y *% y);
    (==) { }
    1 -% (y *% y -% x *% x -% 1);
    (==) { }
    (1 - (y *% y -% x *% x - 1) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_sub_distr 1 (y *% y -% x *% x - 1) prime }
    (2 - (y *% y - x *% x) % prime) % prime;
    (==) { Math.Lemmas.lemma_mod_sub_distr 2 (y *% y - x *% x) prime }
    (2 - (y *% y - x *% x)) % prime;
    (==) { Math.Lemmas.lemma_mod_plus_distr_l (2 - y *% y) (x *% x) prime }
    2 -% y *% y +% x *% x;
    }

//see Theorem 3.1. from https://eprint.iacr.org/2007/286.pdf
let aff_point_add_lemma p q = admit()

let aff_point_add_assoc_lemma p q s = admit()

#restart-solver
let aff_point_at_infinity_lemma p =
  let x1, y1 = p in
  let x2, y2 = aff_point_at_infinity in
  let k1 = x1 *% y2 +% y1 *% x2 in
  let k2 = 1 +% d *% (x1 *% x2) *% (y1 *% y2) in
  let k3 = y1 *% y2 +% x1 *% x2 in
  let k4 = 1 -% d *% (x1 *% x2) *% (y1 *% y2) in
  assert (aff_point_add p aff_point_at_infinity == (k1 /% k2, k3 /% k4));
  assert (x2 == zero /\ y2 == one);

  calc (==) {
    k1;
    (==) { }
    x1 *% one +% y1 *% zero;
    (==) { Math.Lemmas.small_mod x1 prime }
    x1;
    };

  calc (==) {
    k2;
    (==) { }
    1 +% d *% (x1 *% zero) *% (y1 *% one);
    (==) { }
    1;
    };

  calc (==) {
    k3;
    (==) { }
    y1 *% one +% x1 *% zero;
    (==) { Math.Lemmas.small_mod y1 prime }
    y1;
    };

  calc (==) {
    k4;
    (==) { }
    1 -% d *% (x1 *% zero) *% (y1 *% one);
    (==) { }
    1;
    };

  fdiv_one_lemma k1;
  fdiv_one_lemma k3

let aff_point_add_comm_lemma p q = ()
val aff_point_double_lemma: p:aff_point{is_on_curve p} ->
  Lemma (aff_point_double p == aff_point_add p p)
p: Spec.Ed25519.PointOps.aff_point{Spec.Ed25519.PointOps.is_on_curve p}
  -> FStar.Pervasives.Lemma
    (ensures Spec.Ed25519.PointOps.aff_point_double p == Spec.Ed25519.PointOps.aff_point_add p p)