diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-02-12 14:44:48 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-02-12 14:45:10 -0500 |
commit | 34875f01c422e5665a73f076e7e17b9c7e1d5aa0 (patch) | |
tree | 378f93450b3515858b12b6404e52031a92eae50d /src | |
parent | 41b48a78924a9689b9ab838eb74b1d14f267cdfe (diff) |
port some edwards curve theorems
Diffstat (limited to 'src')
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 52 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/Pre.v (renamed from src/CompleteEwardsCurve/Pre.v) | 0 | ||||
-rw-r--r-- | src/Curves/PointFormats.v | 52 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 30 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 7 | ||||
-rw-r--r-- | src/ModularArithmetic/Tutorial.v | 7 | ||||
-rw-r--r-- | src/Spec/CompleteEdwardsCurve.v (renamed from src/Spec/CompleteEwardsCurve.v) | 24 |
7 files changed, 111 insertions, 61 deletions
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 |