aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject5
-rw-r--r--src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v52
-rw-r--r--src/CompleteEdwardsCurve/Pre.v (renamed from src/CompleteEwardsCurve/Pre.v)0
-rw-r--r--src/Curves/PointFormats.v52
-rw-r--r--src/ModularArithmetic/ModularArithmeticTheorems.v30
-rw-r--r--src/ModularArithmetic/PrimeFieldTheorems.v7
-rw-r--r--src/ModularArithmetic/Tutorial.v7
-rw-r--r--src/Spec/CompleteEdwardsCurve.v (renamed from src/Spec/CompleteEwardsCurve.v)24
8 files changed, 114 insertions, 63 deletions
diff --git a/_CoqProject b/_CoqProject
index c1e10953f..02a3c797d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,5 +1,6 @@
-R src Crypto
-src/CompleteEwardsCurve/Pre.v
+src/CompleteEdwardsCurve/Pre.v
+src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
src/Curves/PointFormats.v
src/Curves/ScalarMult.v
src/Galois/BaseSystem.v
@@ -17,7 +18,7 @@ src/ModularArithmetic/PrimeFieldTheorems.v
src/ModularArithmetic/Tutorial.v
src/Rep/ECRep.v
src/Rep/GaloisRep.v
-src/Spec/CompleteEwardsCurve.v
+src/Spec/CompleteEdwardsCurve.v
src/Spec/ModularArithmetic.v
src/Specific/EdDSA25519.v
src/Specific/GF25519.v
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
new file mode 100644
index 000000000..90f5907fd
--- /dev/null
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -0,0 +1,52 @@
+Require Export Crypto.Spec.CompleteEdwardsCurve.
+
+Require Import Crypto.CompleteEdwardsCurve.Pre.
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Eqdep_dec.
+Require Import Crypto.Tactics.VerdiTactics.
+
+Section CompleteEdwardsCurveTheorems.
+ Context {prm:TwistedEdwardsParams}.
+ Existing Instance prime_q.
+ Add Field Ffield_Z : (@Ffield_theory q _)
+ (morphism (@Fring_morph q),
+ preprocess [idtac],
+ postprocess [try exact Fq_1_neq_0; try assumption],
+ constants [Fconstant],
+ div (@Fmorph_div_theory q),
+ power_tac (@Fpower_theory q) [Fexp_tac]).
+
+ Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
+ mkPoint p1 pf1 = mkPoint p2 pf2.
+ Proof.
+ destruct p1, p2; intros; find_injection; intros; subst; apply f_equal.
+ apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
+ Qed.
+ Hint Resolve point_eq.
+
+ Ltac Edefn := unfold unifiedAdd, zero; intros;
+ repeat match goal with
+ | [ p : point |- _ ] =>
+ let x := fresh "x" p in
+ let y := fresh "y" p in
+ let pf := fresh "pf" p in
+ destruct p as [[x y] pf]; unfold onCurve in pf
+ | _ => eapply point_eq, f_equal2
+ | _ => eapply point_eq
+ end.
+ Lemma twistedAddComm : forall A B, (A+B = B+A)%E.
+ Proof.
+ Edefn; f_equal; field.
+ Qed.
+
+ Lemma twistedAddAssoc : forall A B C, A+(B+C) = (A+B)+C.
+ Proof.
+ (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
+ Admitted.
+
+ Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
+ Proof.
+ Edefn; repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+ ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl.
+ Qed.
+End CompleteEdwardsCurveTheorems. \ No newline at end of file
diff --git a/src/CompleteEwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index e4dc140e1..e4dc140e1 100644
--- a/src/CompleteEwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
diff --git a/src/Curves/PointFormats.v b/src/Curves/PointFormats.v
index 8137abc4c..2ea04cde5 100644
--- a/src/Curves/PointFormats.v
+++ b/src/Curves/PointFormats.v
@@ -137,56 +137,8 @@ Module CompleteTwistedEdwardsCurve (M : Modulus) (Import P : TwistedEdwardsParam
- Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0.
- intros.
-
- induction p; inversion H.
-
- revert H H1; generalize x; induction p; intros.
-
- - simpl in H; apply mul_zero_why in H; destruct H; intuition.
-
- + subst; intuition.
-
- + apply IHp in H.
- rewrite H1.
- simpl in H1.
- apply mul_zero_why in H1; destruct H1; intuition.
- rewrite H0 in H.
- apply mul_zero_why in H; destruct H; intuition.
-
- simpl; intuition.
-
- - simpl in H1; apply IHp in H1; simpl; intuition.
- simpl in H; rewrite H in H1; rewrite H.
- apply mul_zero_why in H1; destruct H1; intuition.
-
- - simpl in H; subst; intuition.
-
- Qed.
-
- Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0.
- intros; intuition.
-
- induction p.
-
- - apply H; intuition.
-
- - apply H.
- rewrite H1 in *.
- induction p.
-
- + simpl.
- field.
-
- + simpl in *.
- replace (0 * 0) with 0 in * by field.
- apply IHp; intuition.
- induction p; inversion H2.
-
- + simpl; intuition.
-
- Qed.
+ Lemma root_zero : forall (x: GF) (p: N), x^p = 0 -> x = 0. Admitted.
+ Lemma root_nonzero : forall x p, x^p <> 0 -> (p <> 0)%N -> x <> 0. Admitted.
Lemma char_gt_2 : inject 2 <> 0.
intro H; inversion H; clear H.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 474cd03e1..6c79e6891 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -389,4 +389,34 @@ Section VariousModulo.
Proof.
intros; ring.
Qed.
+
+ Lemma F_add_0_r : forall x : F m, (x + 0)%F = x.
+ Proof.
+ intros; ring.
+ Qed.
+
+ Lemma F_add_0_l : forall x : F m, (0 + x)%F = x.
+ Proof.
+ intros; ring.
+ Qed.
+
+ Lemma F_sub_0_r : forall x : F m, (x - 0)%F = x.
+ Proof.
+ intros; ring.
+ Qed.
+
+ Lemma F_sub_0_l : forall x : F m, (0 - x)%F = opp x.
+ Proof.
+ intros; ring.
+ Qed.
+
+ Lemma F_mul_1_r : forall x : F m, (x * 1)%F = x.
+ Proof.
+ intros; ring.
+ Qed.
+
+ Lemma F_mul_1_l : forall x : F m, (1 * x)%F = x.
+ Proof.
+ intros; ring.
+ Qed.
End VariousModulo. \ No newline at end of file
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 338903b26..6a862fb3b 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -56,7 +56,7 @@ Section VariousModPrime.
Add Field Ffield_Z : (@Ffield_theory q _)
(morphism (@Fring_morph q),
preprocess [Fpreprocess],
- postprocess [Fpostprocess],
+ postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
constants [Fconstant],
div (@Fmorph_div_theory q),
power_tac (@Fpower_theory q) [Fexp_tac]).
@@ -133,6 +133,11 @@ Section VariousModPrime.
+ intuition.
+ apply IHp; auto.
Qed.
+
+ Lemma F_div_1_r : forall x : F q, (x/1)%F = x.
+ Proof.
+ intros; field. (* TODO: Warning: Collision between bound variables ... *)
+ Qed.
Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
Proof.
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index e84659c9e..a4cbcb5ca 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -104,5 +104,12 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
intros.
field.
Qed.
+
+ Lemma realisticFraction : forall x y d : F modulus, (x * 1 + y * 0) / (1 + d * x * 0 * y * 1) = x.
+ Proof.
+ intros.
+ field; try exact Fq_1_neq_0.
+ Qed.
+
End TimesZeroParametricTestModule.
diff --git a/src/Spec/CompleteEwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 8eeefe03b..3586e1f95 100644
--- a/src/Spec/CompleteEwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -1,6 +1,6 @@
Require BinInt Znumtheory.
-Require Crypto.CompleteEwardsCurve.Pre.
+Require Crypto.CompleteEdwardsCurve.Pre.
Require Import Crypto.Spec.ModularArithmetic.
Local Open Scope F_scope.
@@ -9,10 +9,11 @@ Class TwistedEdwardsParams := {
q : BinInt.Z;
a : F q;
d : F q;
- modulus_prime : Znumtheory.prime q;
- a_nonzero : a <> 0;
- a_square : exists sqrt_a, sqrt_a^2 = a;
- d_nonsquare : forall x, x^2 <> d
+ prime_q : Znumtheory.prime q;
+ two_lt_q : BinInt.Z.lt 2 q;
+ nonzero_a : a <> 0;
+ square_a : exists sqrt_a, sqrt_a^2 = a;
+ nonsquare_d : forall x, x^2 <> d
}.
Section TwistedEdwardsCurves.
@@ -27,7 +28,7 @@ Section TwistedEdwardsCurves.
Definition point := { P | onCurve P}.
Definition mkPoint (xy:F q * F q) (pf:onCurve xy) : point := exist onCurve xy pf.
- Definition zero : point := mkPoint (0, 1) Pre.zeroOnCurve.
+ Definition zero : point := mkPoint (0, 1) (@Pre.zeroOnCurve _ _ _ prime_q).
(* NOTE: the two matches on P1 can probably be merged, not sure whether good idea... *)
Definition unifiedAdd (P1 P2 : point) : point :=
@@ -37,12 +38,15 @@ Section TwistedEdwardsCurves.
( let '(x1, y1) := P1' in
let '(x2, y2) := P2' in
(((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))))
- (Pre.unifiedAdd'_onCurve _ _ pf1 pf2).
- Local Infix "+" := unifiedAdd.
+ (@Pre.unifiedAdd'_onCurve _ _ _ prime_q two_lt_q nonzero_a square_a nonsquare_d _ _ pf1 pf2).
Fixpoint scalarMult (n:nat) (P : point) : point :=
match n with
| O => zero
- | S n' => P + scalarMult n' P
+ | S n' => unifiedAdd P (scalarMult n' P)
end.
-End TwistedEdwardsCurves. \ No newline at end of file
+End TwistedEdwardsCurves.
+
+Delimit Scope E_scope with E.
+Infix "+" := unifiedAdd : E_scope.
+Infix "*" := scalarMult : E_scope. \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 19:46:47 +0000