diff options
Diffstat (limited to 'src/CompleteEdwardsCurve')
| -rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 400 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/DoubleAndAdd.v | 30 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 431 | ||||
| -rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 254 |
4 files changed, 467 insertions, 648 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index f70479c3a..683addd5d 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -1,47 +1,33 @@ Require Export Crypto.Spec.CompleteEdwardsCurve. -Require Import Crypto.ModularArithmetic.FField. -Require Import Crypto.ModularArithmetic.FNsatz. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. Require Import Crypto.CompleteEdwardsCurve.Pre. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Crypto.Util.Tuple. Module E. + Import Group Ring Field CompleteEdwardsCurve.E. Section CompleteEdwardsCurveTheorems. - Context {prm:TwistedEdwardsParams}. - Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *) - Existing Instance prime_q. - - Add Field Ffield_p' : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Add Field Ffield_notConstant : (OpaqueFieldTheory q) - (constants [notConstant]). - - Ltac clear_prm := - generalize dependent a; intro a; intros; - generalize dependent d; intro d; intros; - generalize dependent prime_q; intro prime_q; intros; - generalize dependent q; intro q; intros; - clear prm. - - Lemma point_eq : forall xy1 xy2 pf1 pf2, - xy1 = xy2 -> exist E.onCurve xy1 pf1 = exist E.onCurve xy2 pf2. - Proof. - destruct xy1, xy2; 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. - - Definition point_eqb (p1 p2:E.point) : bool := andb - (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2))) - (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))). - + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} + {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {prm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "x ^2" := (x*x) (at level 30). + Local Notation point := (@point F Feq Fone Fadd Fmul a d). + Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d). + + Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)). + + Definition eq (P Q:point) := fieldwise (n:=2) Feq (coordinates P) (coordinates Q). + Infix "=" := eq : E_scope. + + (* TODO: decide whether we still want something like this, then port Local Ltac t := unfold point_eqb; repeat match goal with @@ -55,246 +41,190 @@ Module E. | [H: _ |- _ ] => apply F_eqb_eq in H | _ => rewrite F_eqb_refl end; eauto. - + Lemma point_eqb_sound : forall p1 p2, point_eqb p1 p2 = true -> p1 = p2. Proof. t. Qed. - + Lemma point_eqb_complete : forall p1 p2, p1 = p2 -> point_eqb p1 p2 = true. Proof. t. Qed. - + Lemma point_eqb_neq : forall p1 p2, point_eqb p1 p2 = false -> p1 <> p2. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_complete in H0; congruence. Qed. - + Lemma point_eqb_neq_complete : forall p1 p2, p1 <> p2 -> point_eqb p1 p2 = false. Proof. intros. destruct (point_eqb p1 p2) eqn:Hneq; intuition. apply point_eqb_sound in Hneq. congruence. Qed. - + Lemma point_eqb_refl : forall p, point_eqb p p = true. Proof. t. Qed. - + Definition point_eq_dec (p1 p2:E.point) : {p1 = p2} + {p1 <> p2}. destruct (point_eqb p1 p2) eqn:H; match goal with | [ H: _ |- _ ] => apply point_eqb_sound in H | [ H: _ |- _ ] => apply point_eqb_neq in H end; eauto. Qed. - + Lemma point_eqb_correct : forall p1 p2, point_eqb p1 p2 = if point_eq_dec p1 p2 then true else false. Proof. intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete. Qed. - - Ltac Edefn := unfold E.add, E.add', E.zero; intros; - repeat match goal with - | [ p : E.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 E.onCurve in pf - | _ => eapply point_eq, (f_equal2 pair) - | _ => eapply point_eq - end. - Lemma add_comm : forall A B, (A+B = B+A)%E. - Proof. - Edefn; apply (f_equal2 div); ring. - Qed. - - Ltac unifiedAdd_nonzero := match goal with - | [ |- (?op 1 (d * _ * _ * _ * _ * - inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F] - => let Hadd := fresh "Hadd" in - pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd; - simpl in Hadd; - match goal with - | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] => - replace other with - (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) - * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring); - auto - end - end. - - Lemma add_assoc : forall A B C, (A+(B+C) = (A+B)+C)%E. - Proof. - Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz); - pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); - pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d); - cbv beta iota in *; - repeat split; field_nonzero idtac; unifiedAdd_nonzero. - Qed. - - Lemma add_0_r : forall P, (P + E.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. + *) - Lemma add_0_l : forall P, (E.zero + P)%E = P. - Proof. - intros; rewrite add_comm. apply add_0_r. - Qed. + (* TODO: move to util *) + Lemma decide_and : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}. + Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed. - Lemma mul_0_l : forall P, (0 * P = E.zero)%E. - Proof. - auto. - Qed. + Ltac destruct_points := + 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] + end. - Lemma mul_S_l : forall n P, (S n * P)%E = (P + n * P)%E. - Proof. - auto. - Qed. + Ltac expand_opp := + rewrite ?mul_opp_r, ?mul_opp_l, ?ring_sub_definition, ?inv_inv, <-?ring_sub_definition. - Lemma mul_add_l : forall a b P, ((a + b)%nat * P)%E = E.add (a * P)%E (b * P)%E. - Proof. - induction a; intros; rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?mul_0_l, ?add_0_l, ?mul_S_, ?IHa, ?add_assoc; auto. - Qed. + Local Hint Resolve char_gt_2. + Local Hint Resolve nonzero_a. + Local Hint Resolve square_a. + Local Hint Resolve nonsquare_d. + Local Hint Resolve @edwardsAddCompletePlus. + Local Hint Resolve @edwardsAddCompleteMinus. - Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. - Proof. - induction n; intros; auto. - rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity. - Qed. + Local Obligation Tactic := intros; destruct_points; simpl; field_algebra. + Program Definition opp (P:point) : point := + exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _. - Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. - Proof. - induction m; rewrite ?mul_S_l, ?add_0_l; auto. - Qed. - - (* solve for x ^ 2 *) - Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F. - - Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F. - intros ? eq_zero. - pose proof prime_q. - destruct square_a as [sqrt_a sqrt_a_id]. - rewrite <- sqrt_a_id in eq_zero. - destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero]. - + pose proof (nonsquare_d sqrt_d); auto. - + subst. - rewrite Fq_pow_zero in sqrt_a_id by congruence. - auto using nonzero_a. - Qed. - - Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F. - Proof. - intros y eq_zero. - pose proof prime_q. - eapply F_minus_swap in eq_zero. - eauto using (d_y2_a_nonzero y). - Qed. - - Lemma solve_correct : forall x y, E.onCurve (x, y) <-> - (x ^ 2 = solve_for_x2 y)%F. - Proof. - split. - + intro onCurve_x_y. - pose proof prime_q. - unfold E.onCurve in onCurve_x_y. - eapply F_div_mul; auto using (d_y2_a_nonzero y). - replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring. - rewrite F_sub_add_swap. - replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring. - rewrite onCurve_x_y. - ring. - + intro x2_eq. - unfold E.onCurve, solve_for_x2 in *. - rewrite x2_eq. - field. - auto using d_y2_a_nonzero. - Qed. - - - Program Definition opp (P:E.point) : E.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 F_square_opp; trivial. - Qed. - - Definition sub P Q := (P + opp Q)%E. - - Lemma opp_zero : opp E.zero = E.zero. - Proof. - pose proof @F_opp_0. - unfold opp, E.zero; eapply point_eq; congruence. - Qed. - - Lemma add_opp_r : forall P, (P + opp P = E.zero)%E. - Proof. - unfold opp; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]); - rewrite <-?@F_pow_2_r in *; - pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); - pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP); - field_nonzero idtac. - Qed. - - Lemma add_opp_l : forall P, (opp P + P = E.zero)%E. - Proof. - intros. rewrite add_comm. eapply add_opp_r. - Qed. - - Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E. - Proof. - intros. - assert ((B + A) + opp A = (C + A) + opp A)%E as Hc by congruence. - rewrite <-!add_assoc, !add_opp_r, !add_0_r in Hc; exact Hc. - Qed. - - Lemma add_cancel_l : forall A B C, (A+B = A+C -> B = C)%E. - Proof. - intros. - rewrite (add_comm A C) in H. - rewrite (add_comm A B) in H. - eauto using add_cancel_r. - Qed. - - Lemma shuffle_eq_add_opp : forall P Q R, (P + Q = R <-> Q = opp P + R)%E. - Proof. - split; intros. - { assert (opp P + (P + Q) = opp P + R)%E as Hc by congruence. - rewrite add_assoc, add_opp_l, add_comm, add_0_r in Hc; exact Hc. } - { subst. rewrite add_assoc, add_opp_r, add_comm, add_0_r; reflexivity. } - Qed. - - Lemma opp_opp : forall P, opp (opp P) = P. - Proof. - intros. - pose proof (add_opp_r P%E) as H. - rewrite add_comm in H. - rewrite shuffle_eq_add_opp in H. - rewrite add_0_r in H. - congruence. - Qed. - - Lemma opp_add : forall P Q, opp (P + Q)%E = (opp P + opp Q)%E. + Ltac bash_step := + match goal with + | |- _ => progress intros + | [H: _ /\ _ |- _ ] => destruct H + | |- _ => progress destruct_points + | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp] in * + | |- _ => split + | |- Feq _ _ => field_algebra + | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto 6] + | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances + end. + + Ltac bash := repeat bash_step. + + Global Instance Proper_add : Proper (eq==>eq==>eq) add. Proof. bash. Qed. + Global Instance Proper_opp : Proper (eq==>eq) opp. Proof. bash. Qed. + Global Instance Proper_coordinates : Proper (eq==>fieldwise (n:=2) Feq) coordinates. Proof. bash. Qed. + + Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp). + Proof. + bash. + (* TODO: port denominator-nonzero proofs for associativity *) + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. + match goal with | |- _ <> 0 => admit end. + Admitted. + + (* TODO: move to [Group] and [AbelianGroup] as appropriate *) + Lemma mul_0_l : forall P, (0 * P = zero)%E. + Proof. intros; reflexivity. Qed. + Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E. + Proof. intros; reflexivity. Qed. + Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E. Proof. - intros. - pose proof (add_opp_r (P+Q)%E) as H. - rewrite <-!add_assoc in H. - rewrite add_comm in H. - rewrite <-!add_assoc in H. - rewrite shuffle_eq_add_opp in H. - rewrite add_comm in H. - rewrite shuffle_eq_add_opp in H. - rewrite add_0_r in H. - assumption. + induction n; intros; + rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. Qed. - - Lemma opp_mul : forall n P, opp (E.mul n P) = E.mul n (opp P). + Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E. Proof. - pose proof opp_add; pose proof opp_zero. - induction n; simpl; intros; congruence. + induction n; intros; [reflexivity|]. + rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity. Qed. + Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E. + Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed. + Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E. + Admitted. + + Section PointCompression. + Local Notation "x ^2" := (x*x). + Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)). + + Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0. + Proof. + intros ? eq_zero. + destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero. + destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra. + Qed. + + Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y). + Proof. + unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero. + Qed. + End PointCompression. End CompleteEdwardsCurveTheorems. + + Section Homomorphism. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} + {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} + {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. + Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul phi}. + Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}. + Local Notation Fpoint := (@point F Feq Fone Fadd Fmul Fa Fd). + Local Notation Kpoint := (@point K Keq Kone Kadd Kmul Ka Kd). + + Create HintDb field_homomorphism discriminated. + Hint Rewrite <- + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + Ha + Hd + : field_homomorphism. + + Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( + let (x, y) := coordinates P in (phi x, phi y)) _. + Next Obligation. + destruct P as [[? ?] ?]; simpl. + rewrite_strat bottomup hints field_homomorphism. + eauto using is_homomorphism_phi_proper; assumption. + Qed. + + Context {point_phi:Fpoint->Kpoint} + {point_phi_Proper:Proper (eq==>eq) point_phi} + {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. + + Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi. + Proof. + repeat match goal with + | |- Group.is_homomorphism => split + | |- _ => intro + | |- _ /\ _ => split + | [H: _ /\ _ |- _ ] => destruct H + | [p: point |- _ ] => destruct p as [[??]?] + | |- context[point_phi] => setoid_rewrite point_phi_correct + | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in * + | |- Keq ?x ?x => reflexivity + | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism + | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] + end. + Qed. + End Homomorphism. End E. -Infix "-" := E.sub : E_scope.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/DoubleAndAdd.v b/src/CompleteEdwardsCurve/DoubleAndAdd.v deleted file mode 100644 index 50027349d..000000000 --- a/src/CompleteEdwardsCurve/DoubleAndAdd.v +++ /dev/null @@ -1,30 +0,0 @@ -Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Util.IterAssocOp. -Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Coq.Numbers.BinNums Coq.NArith.NArith Coq.NArith.Nnat Coq.ZArith.ZArith. - -Section EdwardsDoubleAndAdd. - Context {prm:TwistedEdwardsParams}. - Definition doubleAndAdd (bound n : nat) (P : E.point) : E.point := - iter_op E.add E.zero N.testbit_nat (N.of_nat n) P bound. - - Lemma scalarMult_double : forall n P, E.mul (n + n) P = E.mul n (P + P)%E. - Proof. - intros. - replace (n + n)%nat with (n * 2)%nat by omega. - induction n; simpl; auto. - rewrite E.add_assoc. - f_equal; auto. - Qed. - - Lemma doubleAndAdd_spec : forall bound n P, N.size_nat (N.of_nat n) <= bound -> - E.mul n P = doubleAndAdd bound n P. - Proof. - induction n; auto; intros; unfold doubleAndAdd; - rewrite iter_op_spec with (scToN := fun x => x); ( - unfold Morphisms.Proper, Morphisms.respectful, Equivalence.equiv; - intros; subst; try rewrite Nat2N.id; - reflexivity || assumption || apply E.add_assoc - || rewrite E.add_comm; apply E.add_0_r). - Qed. -End EdwardsDoubleAndAdd.
\ No newline at end of file diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index e91bc084b..25af83a0a 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -1,194 +1,154 @@ -Require Import Crypto.CompleteEdwardsCurve.Pre. -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 Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence. -Local Open Scope equiv_scope. -Local Open Scope F_scope. - -Section ExtendedCoordinates. - Context {prm:TwistedEdwardsParams}. - Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *) - Existing Instance prime_q. - - Add Field Ffield_p' : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - - Add Field Ffield_notConstant : (OpaqueFieldTheory q) - (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>). *) - Record extended := mkExtended {extendedX : F q; - extendedY : F q; - extendedZ : F q; - extendedT : F q}. - Local Notation "'(' X ',' Y ',' Z ',' T ')'" := (mkExtended X Y Z T). - - Definition twistedToExtended (P : (F q*F q)) : extended := - let '(x, y) := P in (x, y, 1, x*y). - Definition extendedToTwisted (P : extended) : F q * F q := - let '(X, Y, Z, T) := P in ((X/Z), (Y/Z)). - Definition rep (P:extended) (rP:(F q*F q)) : Prop := - let '(X, Y, Z, T) := P in - extendedToTwisted P = rP /\ - Z <> 0 /\ - T = X*Y/Z. - Local Hint Unfold twistedToExtended extendedToTwisted rep. - Local Notation "P '~=' rP" := (rep P rP) (at level 70). - - 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 - let y := fresh "y" p in - destruct p as [x y] - | [ p : extended |- _ ] => - let X := fresh "X" p in - let Y := fresh "Y" p in - let Z := fresh "Z" p in - let T := fresh "T" p in - destruct p as [X Y Z T] - | [ H: _ /\ _ |- _ ] => destruct H - | [ 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 - | [ |- @eq (F q * F q)%type _ _] => apply f_equal2 - | _ => progress 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 - | _ => solve [eapply @Fq_1_neq_0; eauto with typeclass_instances] - | _ => solve [eauto with typeclass_instances] - | [ H: a = _ |- _ ] => rewrite H - end. - - Lemma twistedToExtended_rep : forall P, twistedToExtended P ~= P. - Proof. - solveExtended. - Qed. - - Lemma extendedToTwisted_rep : forall P rP, P ~= rP -> extendedToTwisted P = rP. - Proof. - solveExtended. - Qed. - - Definition extendedPoint := { P:extended | rep P (extendedToTwisted P) /\ E.onCurve (extendedToTwisted P) }. - - Program Definition mkExtendedPoint : E.point -> extendedPoint := twistedToExtended. - Next Obligation. - destruct x; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. - Qed. - - Program Definition unExtendedPoint : extendedPoint -> E.point := extendedToTwisted. - Next Obligation. - destruct x; simpl; intuition. - Qed. - - Definition extendedPoint_eq P Q := unExtendedPoint P = unExtendedPoint Q. - Global Instance Equivalence_extendedPoint_eq : Equivalence extendedPoint_eq. - Proof. - repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. - Qed. - - Lemma unExtendedPoint_mkExtendedPoint : forall P, unExtendedPoint (mkExtendedPoint P) = P. - Proof. - destruct P; eapply E.point_eq; simpl; erewrite extendedToTwisted_rep; eauto using twistedToExtended_rep. - Qed. - - Global Instance Proper_mkExtendedPoint : Proper (eq==>equiv) mkExtendedPoint. - Proof. - repeat (econstructor || intro); unfold extendedPoint_eq in *; congruence. - Qed. - - Global Instance Proper_unExtendedPoint : Proper (equiv==>eq) unExtendedPoint. - Proof. - 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> *) - Definition unifiedAddM1' (P1 P2 : extended) : extended := - let '(X1, Y1, Z1, T1) := P1 in - let '(X2, Y2, Z2, T2) := P2 in - let A := (Y1-X1)*(Y2-X2) in - let B := (Y1+X1)*(Y2+X2) 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 - let H := B+A in - let X3 := E*F in - let Y3 := G*H in - let T3 := E*H in - let Z3 := F*G in - (X3, Y3, Z3, T3). - Local Hint Unfold E.add. - - Local Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q). - - 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; 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; - field_nonzero tnz. - Qed. - - Lemma unifiedAdd'_onCurve : forall P Q, E.onCurve P -> E.onCurve Q -> E.onCurve (E.add' P Q). - Proof. - intros; pose proof (proj2_sig (E.add (exist _ _ H) (exist _ _ H0))); eauto. - Qed. - - Program Definition unifiedAddM1 : extendedPoint -> extendedPoint -> extendedPoint := unifiedAddM1'. - Next Obligation. - destruct x, x0; simpl; intuition. - - erewrite extendedToTwisted_rep; eauto using unifiedAddM1'_rep. - - erewrite extendedToTwisted_rep. - (* It would be nice if I could use eauto here, but it gets evars wrong :( *) - 2: eapply unifiedAddM1'_rep. 5:apply H1. 4:apply H. 3:auto. 2:auto. - eauto using unifiedAdd'_onCurve. - Qed. - - Lemma unifiedAddM1_rep : forall P Q, E.add (unExtendedPoint P) (unExtendedPoint Q) = unExtendedPoint (unifiedAddM1 P Q). - Proof. - 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. - Qed. - - Global Instance Proper_unifiedAddM1 : Proper (equiv==>equiv==>equiv) unifiedAddM1. - Proof. - 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 E.point_eq; congruence. - Qed. +Require Export Crypto.Spec.CompleteEdwardsCurve. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. +Require Import Crypto.CompleteEdwardsCurve.Pre Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. +Require Import Coq.Logic.Eqdep_dec. +Require Import Crypto.Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Crypto.Util.Tuple. + +Module Extended. + Section ExtendedCoordinates. + Import Group Ring Field. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d} + {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {prm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}. + Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := Fzero. Local Notation "1" := Fone. + Local Infix "+" := Fadd. Local Infix "*" := Fmul. + Local Infix "-" := Fsub. Local Infix "/" := Fdiv. + Local Notation "x ^2" := (x*x) (at level 30). + Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d). + Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d). + + Add Field _edwards_curve_extended_field : (field_theory_for_stdlib_tactic (H:=field)). + + (** [Extended.point] represents a point on an elliptic curve using extended projective + * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *) + Definition point := { P | let '(X,Y,Z,T) := P in onCurve((X/Z), (Y/Z)) /\ Z<>0 /\ Z*T=X*Y }. + Definition coordinates (P:point) : F*F*F*F := proj1_sig P. + + Create HintDb bash discriminated. + Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash. + Ltac bash := + repeat match goal with + | |- Proper _ _ => intro + | _ => progress intros + | [ H: _ /\ _ |- _ ] => destruct H + | [ p:E.point |- _ ] => destruct p as [[??]?] + | [ p:point |- _ ] => destruct p as [[[[??]?]?]?] + | _ => progress autounfold with bash in * + | |- _ /\ _ => split + | _ => solve [neq01] + | _ => solve [eauto] + | _ => solve [intuition] + | _ => solve [etransitivity; eauto] + | |- Feq _ _ => field_algebra + | |- _ <> 0 => apply mul_nonzero_nonzero + | [ H : _ <> 0 |- _ <> 0 ] => + intro; apply H; + field_algebra; + solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2 + | apply E.char_gt_2] + end. + + Obligation Tactic := bash. + + Program Definition from_twisted (P:Epoint) : point := exist _ + (let (x,y) := E.coordinates P in (x, y, 1, x*y)) _. + + Program Definition to_twisted (P:point) : Epoint := exist _ + (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _. + + Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q). + + Local Hint Unfold from_twisted to_twisted eq : bash. + + Global Instance Equivalence_eq : Equivalence eq. Proof. split; split; bash. Qed. + Global Instance Proper_from_twisted : Proper (E.eq==>eq) from_twisted. Proof. bash. Qed. + Global Instance Proper_to_twisted : Proper (eq==>E.eq) to_twisted. Proof. bash. Qed. + Lemma to_twisted_from_twisted P : E.eq (to_twisted (from_twisted P)) P. Proof. bash. Qed. + + Section TwistMinus1. + Context {a_eq_minus1 : a = Fopp 1}. + Context {twice_d:F} {Htwice_d:twice_d = d + d}. + (** 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> *) + Definition add_coordinates P1 P2 : F*F*F*F := + let '(X1, Y1, Z1, T1) := P1 in + let '(X2, Y2, Z2, T2) := P2 in + let A := (Y1-X1)*(Y2-X2) in + let B := (Y1+X1)*(Y2+X2) 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 + let H := B+A in + let X3 := E*F in + let Y3 := G*H in + let T3 := E*H in + let Z3 := F*G in + (X3, Y3, Z3, T3). + + Local Hint Unfold E.add E.coordinates add_coordinates : bash. + + Lemma add_coordinates_correct (P Q:point) : + let '(X,Y,Z,T) := add_coordinates (coordinates P) (coordinates Q) in + let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in + (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z). + Proof. + destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. + pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ. + bash. + Qed. + + Obligation Tactic := idtac. + Program Definition add (P Q:point) : point := add_coordinates (coordinates P) (coordinates Q). + Next Obligation. + intros. + pose proof (add_coordinates_correct P Q) as Hrep. + pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon. + destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz1. + pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz2. + autounfold with bash in *; simpl in *. + destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. + bash. + Qed. + Local Hint Unfold add : bash. + + Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)). + Proof. + pose proof (add_coordinates_correct P Q) as Hrep. + destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]]. + autounfold with bash in *; simpl in *. + destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB. + split; reflexivity. + Qed. + + Global Instance Proper_add : Proper (eq==>eq==>eq) add. + Proof. + unfold eq. intros x y H x0 y0 H0. + transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity. + Qed. + + Lemma homomorphism_to_twisted : @Group.is_homomorphism point eq add Epoint E.eq E.add to_twisted. + Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed. + + Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)). + Proof. + pose proof (to_twisted_add (from_twisted P) (from_twisted Q)). + unfold eq; rewrite !to_twisted_from_twisted in *. + symmetry; assumption. + Qed. + + Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted. + Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed. + + (* TODO: decide whether we still need those, then port *) + (* Lemma unifiedAddM1_0_r : forall P, unifiedAddM1 P (mkExtendedPoint E.zero) === P. unfold equiv, extendedPoint_eq; intros. rewrite <-!unifiedAddM1_rep, unExtendedPoint_mkExtendedPoint, E.add_0_r; auto. @@ -210,30 +170,75 @@ Section ExtendedCoordinates. trivial. Qed. - 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|]. + Lemma scalarMultM1_rep : forall n P, unExtendedPoint (nat_iter_op unifiedAddM1 (mkExtendedPoint E.zero) n P) = E.mul n (unExtendedPoint P). + induction n; [simpl; rewrite !unExtendedPoint_mkExtendedPoint; reflexivity|]; intros. unfold E.mul; fold E.mul. rewrite <-IHn, unifiedAddM1_rep; auto. Qed. + *) + End TwistMinus1. + End ExtendedCoordinates. + + Section Homomorphism. + Import Group Ring Field. + Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd} + {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} + {Fprm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}. + Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd} + {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} + {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}. + Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul + K Keq Kone Kadd Kmul phi}. + Context {phi_nonzero : forall x, ~ Feq x Fzero -> ~ Keq (phi x) Kzero}. + Context {HFa: Feq Fa (Fopp Fone)} {HKa:Keq Ka (Kopp Kone)}. + Context {Hd:Keq (phi Fd) Kd} {Kdd Fdd} {HKdd:Keq Kdd (Kadd Kd Kd)} {HFdd:Feq Fdd (Fadd Fd Fd)}. + Local Notation Fpoint := (@point F Feq Fzero Fone Fadd Fmul Fdiv Fa Fd). + Local Notation Kpoint := (@point K Keq Kzero Kone Kadd Kmul Kdiv Ka Kd). + + Lemma Ha : Keq (phi Fa) Ka. + Proof. rewrite HFa, HKa, <-homomorphism_one. eapply homomorphism_opp. Qed. + + Lemma Hdd : Keq (phi Fdd) Kdd. + Proof. rewrite HFdd, HKdd. rewrite homomorphism_add. repeat f_equiv; auto. Qed. + + Create HintDb field_homomorphism discriminated. + Hint Rewrite <- + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + Ha + Hd + Hdd + : field_homomorphism. + + Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ ( + let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _. + Next Obligation. + destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl. + rewrite_strat bottomup hints field_homomorphism. + eauto 10 using is_homomorphism_phi_proper, phi_nonzero. + Qed. + + Context {point_phi:Fpoint->Kpoint} + {point_phi_Proper:Proper (eq==>eq) point_phi} + {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. - End TwistMinus1. - - 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. + Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi. + Proof. + repeat match goal with + | |- Group.is_homomorphism => split + | |- _ => intro + | |- _ /\ _ => split + | [H: _ /\ _ |- _ ] => destruct H + | [p: point |- _ ] => destruct p as [[[[] ?] ?] [? [? ?]]] + | |- context[point_phi] => setoid_rewrite point_phi_correct + | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates ref_phi] in * + | |- Keq ?x ?x => reflexivity + | |- Keq ?x ?y => rewrite_strat bottomup hints field_homomorphism + | [ H : Feq _ _ |- Keq (phi _) (phi _)] => solve [f_equiv; intuition] + end. + Qed. + End Homomorphism. +End Extended. diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index fea4a99b3..5314ee37c 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,186 +1,100 @@ -Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. +Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid. +Require Import Crypto.Algebra Crypto.Tactics.Nsatz. -Require Import Crypto.Spec.ModularArithmetic. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Local Open Scope F_scope. - +Generalizable All Variables. Section Pre. - Context {q : BinInt.Z}. - Context {a : F q}. - Context {d : F q}. - Context {prime_q : Znumtheory.prime q}. - Context {two_lt_q : 2 < q}. - Context {a_nonzero : a <> 0}. - Context {a_square : exists sqrt_a, sqrt_a^2 = a}. - Context {d_nonsquare : forall x, x^2 <> d}. - - Add Field Ffield_Z : (@Ffield_theory q _) - (morphism (@Fring_morph q), - preprocess [Fpreprocess], - postprocess [Fpostprocess], - constants [Fconstant], - div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - + Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)). + Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope. + Local Notation "0" := zero. Local Notation "1" := one. + Local Infix "+" := add. Local Infix "*" := mul. + Local Infix "-" := sub. Local Infix "/" := div. + Local Notation "x '^' 2" := (x*x) (at level 30). + + Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)). + + Context {a:F} {a_nonzero : a<>0} {a_square : exists sqrt_a, sqrt_a^2 = a}. + Context {d:F} {d_nonsquare : forall sqrt_d, sqrt_d^2 <> d}. + Context {char_gt_2 : 1+1 <> 0}. + (* the canonical definitions are in Spec *) - Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2). - Local Notation unifiedAdd' P1' P2' := ( - 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))) - ). - - Lemma char_gt_2 : ZToField 2 <> (0: F q). - intro; find_injection. - pose proof two_lt_q. - rewrite (Z.mod_small 2 q), Z.mod_0_l in *; omega. - Qed. + Definition onCurve (P:F*F) := let (x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2. + Definition unifiedAdd' (P1' P2':F*F) : F*F := + let (x1, y1) := P1' in + let (x2, y2) := P2' in + pair (((x1*y2 + y1*x2)/(1 + d*x1*x2*y1*y2))) (((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2))). - Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end. - Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end. - - Ltac whatsNotZero := - repeat match goal with - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: lhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (lhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: ?lhs = ?rhs |- _ ] => - match goal with [Ha: rhs <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (rhs <> 0) by (rewrite H; auto using Fq_1_neq_0) - | [H: (?a^?p)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - let Y:=fresh in let Z:=fresh in try ( - assert (p <> 0%N) as Z by (intro Y; inversion Y); - assert (a <> 0) by (eapply Fq_root_nonzero; eauto using Fq_1_neq_0); - clear Z) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: a <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (a <> 0) by (eapply F_mul_nonzero_l; eauto using Fq_1_neq_0) - | [H: (?a*?b)%F <> 0 |- _ ] => - match goal with [Ha: b <> 0 |- _ ] => fail 1 | _ => idtac end; - assert (b <> 0) by (eapply F_mul_nonzero_r; eauto using Fq_1_neq_0) - end. + Ltac use_sqrt_a := destruct a_square as [sqrt_a a_square']; rewrite <-a_square' in *. Lemma edwardsAddComplete' x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> + onCurve (pair x1 y1) -> + onCurve (pair x2 y2) -> (d*x1*x2*y1*y2)^2 <> 1. Proof. - intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero. - - pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. - destruct a_square as [sqrt_a a_square']. - rewrite <-a_square' in *. - - (* Furthermore... *) - pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt. - rewrite Hc2 in Heqt at 2. - replace (d * x1 ^ 2 * y1 ^ 2 * (1 + d * x2 ^ 2 * y2 ^ 2)) - with (d*x1^2*y1^2 + (d*x1*x2*y1*y2)^2) in Heqt by field. - rewrite Hcontra in Heqt. - replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field. - rewrite <-Hc1 in Heqt. - - (* main equation for both potentially nonzero denominators *) - destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0); - try lazymatch goal with [H: ?f (sqrt_a * x2) y2 <> 0 |- _ ] => - assert ((f (sqrt_a*x1) (d * x1 * x2 * y1 * y2*y1))^2 = - f ((sqrt_a^2)*x1^2 + (d * x1 * x2 * y1 * y2)^2*y1^2) - (d * x1 * x2 * y1 * y2*sqrt_a*(ZToField 2)*x1*y1)) as Heqw1 by field; - rewrite Hcontra in Heqw1; - replace (1 * y1^2) with (y1^2) in * by field; - rewrite <- Heqt in *; - assert (d = (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))^2 / - (x1 * y1 * (f (sqrt_a * x2) y2))^2) - by (rewriteAny; field; auto); - match goal with [H: d = (?n^2)/(?l^2) |- _ ] => - destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto) - end - end. - - assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field). - - replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field. - - (* contradiction: product of nonzero things is zero *) - destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition. - destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition. - apply Ha_nonzero; field. + unfold onCurve, not; use_sqrt_a; intros. + destruct (eq_dec (sqrt_a*x2 + y2) 0); destruct (eq_dec (sqrt_a*x2 - y2) 0); + lazymatch goal with + | [H: not (eq (?f (sqrt_a * x2) y2) 0) |- _ ] + => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1)) + /(f (sqrt_a * x2) y2 * x1 * y1 )) + | _ => apply a_nonzero + end; field_algebra; auto using Ring.opp_nonzero_nonzero; intro; nsatz_contradict. Qed. Lemma edwardsAddCompletePlus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 + d*x1*x2*y1*y2) <> 0. - Proof. - intros Hc1 Hc2; simpl in Hc1, Hc2. - intros; destruct (F_eq_dec (d*x1*x2*y1*y2) (0-1)) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field. - intro Hz; rewrite Hz in H; intuition. - Qed. - + onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + Lemma edwardsAddCompleteMinus x1 y1 x2 y2 : - onCurve (x1, y1) -> - onCurve (x2, y2) -> - (1 - d*x1*x2*y1*y2) <> 0. - Proof. - intros Hc1 Hc2. destruct (F_eq_dec (d*x1*x2*y1*y2) 1) as [H|H]. - - assert ((d*x1*x2*y1*y2)^2 = 1) by (rewriteAny; field). destruct (edwardsAddComplete' x1 y1 x2 y2); auto. - - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field. - intro Hz; rewrite Hz in H; apply H; field. - Qed. - - Definition zeroOnCurve : onCurve (0, 1). - simpl. field. - Qed. - - Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3 - (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) : - onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3). + onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0. + Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed. + + Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed. + + Lemma unifiedAdd'_onCurve : forall P1 P2, + onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2). Proof. - (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1; - * c=1 and an extra a in front of x^2 *) - - injection H; clear H; intros. - - Ltac t x1 y1 x2 y2 := - assert ((a*x2^2 + y2^2)*d*x1^2*y1^2 - = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto); - assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2 - = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field). - t x1 y1 x2 y2; t x2 y2 x1 y1. - - remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 - - (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T. - assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field). - assert (HT2: T = (a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +( - (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 * - y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field). - replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3. - - match goal with [ |- ?x = 1 ] => replace x with - ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 + - ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 - - d*((x1 * y2 + y1 * x2) * (y1 * y2 - a * x1 * x2)) ^ 2)/ - ((1-d^2*x1^2*x2^2*y1^2*y2^2)^2)) end. - - rewrite <-HT1, <-HT2; field; rewrite HT1. - replace ((1 - d ^ 2 * x1 ^ 2 * x2 ^ 2 * y1 ^ 2 * y2 ^ 2)) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) by field. - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. - - field; replace (1 - (d * x1 * x2 * y1 * y2) ^ 2) - with ((1 - d*x1*x2*y1*y2)*(1 + d*x1*x2*y1*y2)) - by field; - auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero, - edwardsAddCompleteMinus, edwardsAddCompletePlus. + unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2. + field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus. Qed. - - Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> - onCurve (unifiedAdd' P1 P2). +End Pre. + +Import Group Ring Field. + +(* TODO: move -- this does not need to be defined before [point] *) +Section RespectsFieldHomomorphism. + Context {F EQ ZERO ONE OPP ADD MUL SUB INV DIV} `{@field F EQ ZERO ONE OPP ADD SUB MUL INV DIV}. + Context {K eq zero one opp add mul sub inv div} `{@field K eq zero one opp add sub mul inv div}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Context {phi:F->K} `{@is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}. + Context {A D:F} {a d:K} {a_ok:phi A=a} {d_ok:phi D=d}. + + Let phip := fun (P':F*F) => let (x, y) := P' in (phi x, phi y). + + Let eqp := fun (P1' P2':K*K) => + let (x1, y1) := P1' in + let (x2, y2) := P2' in + and (eq x1 x2) (eq y1 y2). + + Create HintDb field_homomorphism discriminated. + Hint Rewrite + homomorphism_one + homomorphism_add + homomorphism_sub + homomorphism_mul + homomorphism_div + a_ok + d_ok + : field_homomorphism. + + Lemma morphism_unidiedAdd' : forall P Q:F*F, + eqp + (phip (unifiedAdd'(F:=F)(one:=ONE)(add:=ADD)(sub:=SUB)(mul:=MUL)(div:=DIV)(a:=A)(d:=D) P Q)) + (unifiedAdd'(F:=K)(one:=one)(add:=add)(sub:=sub)(mul:=mul)(div:=div)(a:=a)(d:=d) (phip P) (phip Q)). Proof. - intros; destruct P1, P2. - remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. - eapply unifiedAdd'_onCurve'; eauto. + intros [x1 y1] [x2 y2]. + cbv [unifiedAdd' phip eqp]; + apply conj; + (rewrite_strat topdown hints field_homomorphism); reflexivity. Qed. -End Pre.
\ No newline at end of file +End RespectsFieldHomomorphism.
\ No newline at end of file |