diff options
author | Jade Philipoom <jadep@mit.edu> | 2016-02-16 13:29:14 -0500 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:40:30 -0400 |
commit | 2f3461b1248ae7f48e906a537d547e00fd3bcb6c (patch) | |
tree | 1e5ba8896b548147fa8aaf2496aac1e769b0a5c6 /src | |
parent | 085f11ef01a7fd1659c529bd4815710c7a1fc35e (diff) |
cleaned up and ported definition to solve for x ^ 2 in the curve equation
Diffstat (limited to 'src')
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 57 |
1 files changed, 45 insertions, 12 deletions
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index cddb17f63..a6b61d2dd 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -50,6 +50,9 @@ Section CompleteEdwardsCurveTheorems. ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r; exact eq_refl. 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. @@ -61,7 +64,7 @@ Section CompleteEdwardsCurveTheorems. 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. @@ -70,18 +73,48 @@ Section CompleteEdwardsCurveTheorems. eauto using (d_y2_a_nonzero y). Qed. - (* solve for x ^ 2 *) - Lemma onCurve_solve_x2 : (forall x y, onCurve (x, y) -> - x ^ 2 = (y ^ 2 - 1) / (d * (y ^ 2) - a))%F. + Lemma solve_correct : forall x y, onCurve (x, y) <-> + (x ^ 2 = solve_for_x2 y)%F. Proof. - intros ? ? onCurve_x_y. - pose proof prime_q. - unfold 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. + split. + + intro onCurve_x_y. + pose proof prime_q. + unfold 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 onCurve, solve_for_x2 in *. + rewrite x2_eq. + field. + auto using d_y2_a_nonzero. + Qed. + + (* TODO : move to ModularArithmeticTheorems? *) + Definition sqrt_valid (a : F q) := ((sqrt_mod_q a) ^ 2 = a)%F. + + Lemma solve_sqrt_valid : forall (p : point), + sqrt_valid (solve_for_x2 (snd (proj1_sig p))). + Admitted. + + Lemma solve_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (sqrt_mod_q (solve_for_x2 y), y). + Proof. + intros. + unfold sqrt_valid in *. + apply solve_correct; auto. + Qed. + + Lemma solve_opp_onCurve: forall (y : F q), sqrt_valid (solve_for_x2 y) -> + onCurve (opp (sqrt_mod_q (solve_for_x2 y)), y). + Proof. + intros y sqrt_valid_x2. + unfold sqrt_valid in *. + apply solve_correct. + rewrite <- sqrt_valid_x2 at 2. ring. Qed. |