diff options
author | Jason Gross <jgross@mit.edu> | 2016-06-10 17:25:28 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-06-10 17:25:28 -0400 |
commit | 7129157393f420268c9399dc9b4119469994bf63 (patch) | |
tree | 62f4443c4e7b01c73e76af7589d20037386908d5 /src/CompleteEdwardsCurve/Pre.v | |
parent | 969cb56234750c320768ae39e934b18ce2883aef (diff) |
More changes for 8.5
[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
Diffstat (limited to 'src/CompleteEdwardsCurve/Pre.v')
-rw-r--r-- | src/CompleteEdwardsCurve/Pre.v | 46 |
1 files changed, 24 insertions, 22 deletions
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v index fea4a99b3..322db1792 100644 --- a/src/CompleteEdwardsCurve/Pre.v +++ b/src/CompleteEdwardsCurve/Pre.v @@ -1,9 +1,11 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics. +Require Import Coq.omega.Omega. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Local Open Scope Z_scope. Local Open Scope F_scope. - + Section Pre. Context {q : BinInt.Z}. Context {a : F q}. @@ -20,8 +22,8 @@ Section Pre. postprocess [Fpostprocess], constants [Fconstant], div (@Fmorph_div_theory q), - power_tac (@Fpower_theory q) [Fexp_tac]). - + 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' := ( @@ -29,7 +31,7 @@ Section Pre. 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. @@ -38,7 +40,7 @@ Section Pre. 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 |- _ ] => @@ -67,11 +69,11 @@ Section Pre. (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. + + 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. @@ -80,7 +82,7 @@ Section Pre. 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 |- _ ] => @@ -97,11 +99,11 @@ Section Pre. 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. @@ -119,7 +121,7 @@ Section Pre. - 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) -> @@ -130,27 +132,27 @@ Section Pre. - 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 *) - + * 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). @@ -158,7 +160,7 @@ Section Pre. (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 - @@ -175,7 +177,7 @@ Section Pre. 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. @@ -183,4 +185,4 @@ Section Pre. remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r. eapply unifiedAdd'_onCurve'; eauto. Qed. -End Pre.
\ No newline at end of file +End Pre. |