diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-04-25 17:37:05 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:44:46 -0400 |
commit | ddb2d8ad8c765ce03d296e76e4e0855977131f08 (patch) | |
tree | 46085ee6647699335129c40c9105062a0c7708d9 /src | |
parent | 37e2a9e80607eb8771aea1b371f464a8d7ce8464 (diff) |
refactor field lemmas out of ed25519
Diffstat (limited to 'src')
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 22 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 10 | ||||
-rw-r--r-- | src/Specific/Ed25519.v | 31 |
3 files changed, 39 insertions, 24 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index ddb689547..954fac15d 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -513,6 +513,11 @@ Section VariousModulo. ring. Qed. + Lemma F_opp_0 : opp (0 : F m) = 0%F. + Proof. + intros; ring. + Qed. + Lemma F_opp_swap : forall x y : F m, opp x = y <-> x = opp y. Proof. split; intro; subst; ring. @@ -523,6 +528,23 @@ Section VariousModulo. intros; ring. Qed. + Lemma F_square_opp : forall x : F m, (opp x ^ 2 = x ^ 2)%F. + Proof. + intros; ring. + Qed. + + Lemma F_mul_opp_r : forall x y : F m, (x * opp y = opp (x * y))%F. + intros; ring. + Qed. + + Lemma F_mul_opp_l : forall x y : F m, (opp x * y = opp (x * y))%F. + intros; ring. + Qed. + + Lemma F_mul_opp_both : forall x y : F m, (opp x * opp y = x * y)%F. + intros; ring. + Qed. + Lemma F_add_0_r : forall x : F m, (x + 0)%F = x. Proof. intros; ring. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 68ce16d7c..de755f542 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -249,6 +249,16 @@ Section VariousModPrime. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. + Lemma F_inv_0 : inv 0 = (0 : F q). + Proof. + destruct (@F_inv_spec q); auto. + Qed. + + Lemma F_div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. + Proof. + intros; destruct (F_eq_dec y 0); [subst;unfold div;rewrite !F_inv_0|]; field. + Qed. + Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). Proof. split; intro A. diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index e2036e12e..f02c24ffb 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -59,9 +59,7 @@ Proof. end. } Qed. -Axiom xB : F q. -Axiom yB : F q. -Axiom B_proj : proj1_sig B = (xB, yB). +Lemma B_proj : proj1_sig B = (fst(proj1_sig B), snd(proj1_sig B)). destruct B as [[]]; reflexivity. Qed. Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms. @@ -92,26 +90,19 @@ Axiom decode_scalar_correct : forall x, decode_scalar x = option_map (fun x : F Local Infix "==?" := point_eqb (at level 70) : E_scope. Local Infix "==?" := ModularArithmeticTheorems.F_eq_dec (at level 70) : F_scope. -Axiom square_opp : forall (x:F q), (opp x ^ 2 = x ^ 2)%F. - Program Definition negate (P:point) : point := let '(x, y) := proj1_sig P in (opp x, y). Next Obligation. Proof. pose (proj2_sig P) as H; rewrite <-Heq_anonymous in H; simpl in H. - rewrite square_opp; trivial. + rewrite F_square_opp; trivial. Qed. Definition point_sub P Q := (P + negate Q)%E. Infix "-" := point_sub : E_scope. -Lemma opp0 m : opp (0 : F m) = 0%F. -Proof. - Fdefn; rewrite Zdiv.Zminus_mod, !Zdiv.Z_mod_same_full, !Zdiv.Zmod_0_l; eauto. (* TODO: ring? *) -Qed. - Lemma negate_zero : negate zero = zero. Proof. - pose proof opp0. + pose proof @F_opp_0. unfold negate, zero; eapply point_eq'; congruence. Qed. @@ -128,21 +119,13 @@ Axiom solve_for_R : forall A B C, (A ==? B + C)%E = (B ==? A - C)%E. Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). Local Notation "2" := (ZToField 2) : F_scope. -Lemma mul_opp_1 : forall x y : F q, (opp x * y = opp (x * y))%F. - (* field *) -Admitted. - -Lemma div_opp_1 : forall x y : F q, (opp x / y = opp (x / y))%F. - (* field *) -Admitted. - Definition negateExtended' P := let '(X, Y, Z, T) := P in (opp X, Y, Z, opp T). Program Definition negateExtended (P:extendedPoint) : extendedPoint := negateExtended' (proj1_sig P). Next Obligation. Proof. unfold negateExtended', rep; destruct P as [[X Y Z T] H]; simpl. destruct H as [[[] []] ?]; subst. - repeat rewrite ?div_opp_1, ?mul_opp_1, ?square_opp; repeat split; trivial. -Qed. + repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial. +Admitted. Axiom negateExtended_correct : forall P, negate (unExtendedPoint P) = unExtendedPoint (negateExtended P). @@ -501,8 +484,8 @@ Proof. unfold curve25519params, q. (* TODO: do we really wanna do it here? *) rewrite (rep2F_F2rep 0%F). rewrite (rep2F_F2rep 1%F). - rewrite (rep2F_F2rep xB%F). - rewrite (rep2F_F2rep yB%F). + match goal with |- context [?x] => match x with (fst (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. + match goal with |- context [?x] => match x with (snd (proj1_sig B)) => idtac x; rewrite (rep2F_F2rep x) end end. rewrite !FRepMul_correct. repeat match goal with |- appcontext [ ?E ] => match E with (rep2F ?x, rep2F ?y, rep2F ?z, rep2F ?t) => |