diff options
Diffstat (limited to 'src/CompleteEdwardsCurve/ExtendedCoordinates.v')
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 121 |
1 files changed, 63 insertions, 58 deletions
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index e918ac128..e91bc084b 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -3,7 +3,7 @@ Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.ModularArithmetic.FField. Require Import Crypto.Tactics.VerdiTactics. -Require Import Util.IterAssocOp BinNat NArith. +Require Import Util.IterAssocOp BinNat NArith. Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. Local Open Scope equiv_scope. Local Open Scope F_scope. @@ -19,10 +19,10 @@ Section ExtendedCoordinates. postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], constants [Fconstant], div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). + power_tac (@Fpower_theory q) [Fexp_tac]). Add Field Ffield_notConstant : (OpaqueFieldTheory q) - (constants [notConstant]). + (constants [notConstant]). (** [extended] represents a point on an elliptic curve using extended projective * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) @@ -44,8 +44,8 @@ Section ExtendedCoordinates. Local Hint Unfold twistedToExtended extendedToTwisted rep. Local Notation "P '~=' rP" := (rep P rP) (at level 70). - Ltac unfoldExtended := - repeat progress (autounfold; unfold onCurve, unifiedAdd, unifiedAdd', rep in *; intros); + Ltac unfoldExtended := + repeat progress (autounfold; unfold E.onCurve, E.add, E.add', rep in *; intros); repeat match goal with | [ p : (F q*F q)%type |- _ ] => let x := fresh "x" p in @@ -61,7 +61,7 @@ Section ExtendedCoordinates. | [ H: @eq (F q * F q)%type _ _ |- _ ] => invcs H | [ H: @eq F q ?x _ |- _ ] => isVar x; rewrite H; clear H end. - + Ltac solveExtended := unfoldExtended; repeat match goal with | [ |- _ /\ _ ] => split @@ -83,14 +83,14 @@ Section ExtendedCoordinates. solveExtended. Qed. - Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ onCurve (extendedToTwisted P) }. + Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }. - Program Definition mkExtendedPoint : point -> extendedPoint := twistedToExtended. + Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended. Next Obligation. destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. Qed. - Program Definition unExtendedPoint : extendedPoint -> point := extendedToTwisted. + Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted. Next Obligation. destruct x; simpl; intuition. Qed. @@ -103,7 +103,7 @@ Section ExtendedCoordinates. Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P. Proof. - destruct P; eapply point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. + destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. Qed. Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint. @@ -116,6 +116,8 @@ Section ExtendedCoordinates. repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. Qed. + Definition twice_d := d + d. + Section TwistMinus1. Context (a_eq_minus1 : a = opp 1). (** Second equation from <http://eprint.iacr.org/2008/522.pdf> section 3.1, also <https://www.hyperelliptic.org/EFD/g1p/auto-twisted-extended-1.html#addition-add-2008-hwcd-3> and <https://tools.ietf.org/html/draft-josefsson-eddsa-ed25519-03> *) @@ -124,8 +126,8 @@ Section ExtendedCoordinates. let '(X2, Y2, Z2, T2) := P2 in let A := (Y1-X1)*(Y2-X2) in let B := (Y1+X1)*(Y2+X2) in - let C := T1*ZToField 2*d*T2 in - let D := Z1*ZToField 2 *Z2 in + let C := T1*twice_d*T2 in + let D := Z1*(Z2+Z2) in let E := B-A in let F := D-C in let G := D+C in @@ -135,47 +137,30 @@ Section ExtendedCoordinates. let T3 := E*H in let Z3 := F*G in (X3, Y3, Z3, T3). - Local Hint Unfold unifiedAdd. + Local Hint Unfold E.add. + + Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). - Lemma unifiedAddM1'_rep: forall P Q rP rQ, onCurve rP -> onCurve rQ -> - P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (unifiedAdd' rP rQ). + Lemma F_mul_2_l : forall x : F q, ZToField 2 * x = x + x. + intros. ring. + Qed. + + Lemma unifiedAddM1'_rep: forall P Q rP rQ, E.onCurve rP -> E.onCurve rQ -> + P ~= rP -> Q ~= rQ -> (unifiedAddM1' P Q) ~= (E.add' rP rQ). Proof. intros P Q rP rQ HoP HoQ HrP HrQ. pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d). - unfoldExtended; rewrite a_eq_minus1 in *; simpl in *. + unfoldExtended; unfold twice_d; rewrite a_eq_minus1 in *; simpl in *. repeat rewrite <-F_mul_2_l. repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto; 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. - - Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). - (* If we we had reasoning modulo associativity and commutativity, - * the following tactic would probably solve all remaining goals here: - repeat match goal with [H1: @eq (F p) _ _, H2: @eq (F p) _ _ |- _ ] => - let H := fresh "H" in ( - pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H; - match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end - ) || ( - pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H; - match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end - ); tnz - end. *) - - - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. - - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ) - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz. + ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; + field_nonzero tnz. Qed. - Lemma unifiedAdd'_onCurve : forall P Q, onCurve P -> onCurve Q -> onCurve (unifiedAdd' P Q). + Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q). Proof. - intros; pose proof (proj2_sig (unifiedAdd (mkPoint _ H) (mkPoint _ H0))); eauto. + intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto. Qed. Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'. @@ -188,9 +173,9 @@ Section ExtendedCoordinates. eauto using unifiedAdd'_onCurve. Qed. - Lemma unifiedAddM1_rep : forall P Q, unifiedAdd (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). + Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). Proof. - destruct P, Q; unfold unExtendedPoint, unifiedAdd, unifiedAddM1; eapply point_eq; simpl in *; intuition. + destruct P, Q; unfold unExtendedPoint, E.add, unifiedAddM1; eapply E.point_eq; simpl in *; intuition. pose proof (unifiedAddM1'_rep x x0 (extendedToTwisted x) (extendedToTwisted x0)); destruct (unifiedAddM1' x x0); unfold rep in *; intuition. @@ -201,34 +186,54 @@ Section ExtendedCoordinates. repeat (econstructor || intro). repeat match goal with [H: _ === _ |- _ ] => inversion H; clear H end; unfold equiv, extendedPoint_eq. rewrite <-!unifiedAddM1_rep. - destruct x, y, x0, y0; simpl in *; eapply point_eq; congruence. + destruct x, y, x0, y0; simpl in *; eapply E.point_eq; congruence. Qed. - Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint zero) === P. + Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. Qed. - Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint zero) P === P. + Lemma unifiedAddM1_0_l : forall P, unifiedAddM1 (mkExtendedPoint E.zero) P === P. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, twistedAddComm, unExtendedPoint_mkExtendedPoint, zeroIsIdentity; auto. + rewrite <-!unifiedAddM1_rep, E.add_comm, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. Qed. Lemma unifiedAddM1_assoc : forall a b c, unifiedAddM1 a (unifiedAddM1 b c) === unifiedAddM1 (unifiedAddM1 a b) c. Proof. unfold equiv, extendedPoint_eq; intros. - rewrite <-!unifiedAddM1_rep, twistedAddAssoc; auto. + rewrite <-!unifiedAddM1_rep, E.add_assoc; auto. + Qed. + + Lemma testbit_conversion_identity : forall x i, N.testbit_nat x i = N.testbit_nat ((fun a => a) x) i. + Proof. + trivial. Qed. - - Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint zero). - Definition scalarMultM1_spec := iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint zero) unifiedAddM1_0_l. - Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P) = scalarMult n (unExtendedPoint P). - intros; rewrite scalarMultM1_spec, Nat2N.id. + + Definition scalarMultM1 := iter_op unifiedAddM1 (mkExtendedPoint E.zero) N.testbit_nat. + Definition scalarMultM1_spec := + iter_op_spec unifiedAddM1 unifiedAddM1_assoc (mkExtendedPoint E.zero) unifiedAddM1_0_l + N.testbit_nat (fun x => x) testbit_conversion_identity. + Lemma scalarMultM1_rep : forall n P, unExtendedPoint (scalarMultM1 (N.of_nat n) P (N.size_nat (N.of_nat n))) = E.mul n (unExtendedPoint P). + intros; rewrite scalarMultM1_spec, Nat2N.id; auto. induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]. - unfold scalarMult; fold scalarMult. + unfold E.mul; fold E.mul. rewrite <-IHn, unifiedAddM1_rep; auto. Qed. End TwistMinus1. -End ExtendedCoordinates.
\ No newline at end of file + 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 ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; repeat split; trivial. + Qed. + + Lemma negateExtended_correct : forall P, E.opp (unExtendedPoint P) = unExtendedPoint (negateExtended P). + Proof. + unfold E.opp, unExtendedPoint, negateExtended; destruct P as [[]]; simpl; intros. + eapply E.point_eq; repeat rewrite ?F_div_opp_1, ?F_mul_opp_l, ?F_square_opp; trivial. + Qed. +End ExtendedCoordinates. |