From b7aa0385bfbedccd486154900571e7244eca51a1 Mon Sep 17 00:00:00 2001 From: Jade Philipoom Date: Tue, 16 Feb 2016 21:22:17 -0500 Subject: moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from CompleteEdwardsCurve, where the precondition is not in scope. --- .../CompleteEdwardsCurveTheorems.v | 25 ---------------- src/ModularArithmetic/PrimeFieldTheorems.v | 2 +- src/Spec/Ed25519.v | 5 +++- src/Spec/PointEncoding.v | 33 ++++++++++++++++++++++ 4 files changed, 38 insertions(+), 27 deletions(-) diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index a6b61d2dd..dd40a4510 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -93,29 +93,4 @@ Section CompleteEdwardsCurveTheorems. 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. - End CompleteEdwardsCurveTheorems. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index fe0398ff4..80fb0dfa8 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -197,7 +197,7 @@ Section VariousModPrime. Proof. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. - + Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). Proof. split; intro A. diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 04e6a5fc2..c12799751 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -115,7 +115,10 @@ Qed. Definition FlEncoding : encoding of F (Z.of_nat l) as word b := @modular_word_encoding (Z.of_nat l) b l_pos l_bound. -Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding. +Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed. +(* Admitting until field exponentiation can compute this in reasonable time *) +Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (CompleteEdwardsCurve.q / 4)) ^ 2 = opp 1)%F. Admitted. +Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index ea662a6b7..18097b676 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -21,6 +21,39 @@ Section PointEncoding. div (@Fmorph_div_theory q), power_tac (@Fpower_theory q) [Fexp_tac]). + 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))). + Proof. + intros. + destruct p as [[x y] onCurve_xy]; simpl. + rewrite (solve_correct x y) in onCurve_xy. + rewrite <- onCurve_xy. + unfold sqrt_valid. + eapply sqrt_mod_q_valid; eauto. + unfold isSquare; eauto. + Grab Existential Variables. eauto. + Qed. + + 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. + Definition sign_bit (x : F q) := (wordToN (enc (opp x))