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/CompleteEdwardsCurve/Pre.v | |
parent | 41b48a78924a9689b9ab838eb74b1d14f267cdfe (diff) |
port some edwards curve theorems
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
-rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 186 |
1 files changed, 186 insertions, 0 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v new file mode 100644 index 000000000..e4dc140e1 --- /dev/null +++ b/src/CompleteEdwardsCurve/Pre.v @@ -0,0 +1,186 @@ +Require Import BinInt Znumtheory VerdiTactics. + +Require Import Crypto.Spec.ModularArithmetic. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Local Open Scope F_scope. + +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]). + + (* 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. + + 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. + + Lemma edwardsAddComplete' x1 y1 x2 y2 : + onCurve (x1, y1) -> + onCurve (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. + 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. + + 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). + 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. + Qed. + + Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 -> + onCurve (unifiedAdd' P1 P2). + Proof. + intros; destruct P1, P2. + remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. + eapply unifiedAdd'_onCurve'; eauto. + Qed. +End Pre.
\ No newline at end of file |