diff options
| -rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 18 | ||||
| -rw-r--r-- | src/ModularArithmetic/Pre.v | 41 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 6 | ||||
| -rw-r--r-- | src/Spec/Ed25519.v | 18 |
4 files changed, 58 insertions, 25 deletions
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index c199a551f..f96be4566 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -1,4 +1,5 @@ -Require Import Spec.ModularArithmetic. +Require Import Crypto.Spec.ModularArithmetic. +Require Import Crypto.ModularArithmetic.Pre. Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. @@ -181,7 +182,7 @@ Section FandZ. Fdefn. Qed. - Lemma FieldToZ_pow : forall (x : F m) n, m <> 0%Z -> + Lemma FieldToZ_pow_Zpow_mod : forall (x : F m) n, (FieldToZ x ^ Z.of_N n mod m = FieldToZ (x ^ n)%F)%Z. Proof. intros. @@ -194,13 +195,20 @@ Section FandZ. rewrite Z.pow_succ_r by apply N2Z.is_nonneg. rewrite <- N.add_1_l. rewrite pow_succ. - rewrite Z.mul_mod by auto. + rewrite <- Zmult_mod_idemp_r. rewrite IHn. - rewrite mod_FieldToZ. - apply FieldToZ_mul; auto. + apply FieldToZ_mul. } Qed. + Lemma FieldToZ_pow_efficient : forall (x : F m) n, FieldToZ (x^n) = powmod m (FieldToZ x) n. + Proof. + intros. + rewrite powmod_Zpow_mod. + rewrite <-FieldToZ_pow_Zpow_mod. + reflexivity. + Qed. + Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m -> b mod m = (- a) mod m. Proof. diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v index c6d1ca911..3432488c4 100644 --- a/src/ModularArithmetic/Pre.v +++ b/src/ModularArithmetic/Pre.v @@ -44,8 +44,8 @@ Definition opp_impl: Defined. Definition mulmod m := fun a b => a * b mod m. -Definition pow_impl_pos m := Pos.iter_op (mulmod m). -Definition pow_impl_N m a x := match x with N0 => 1 mod m | Npos p => @pow_impl_pos m p a end. +Definition powmod_pos m := Pos.iter_op (mulmod m). +Definition powmod m a x := match x with N0 => 1 mod m | Npos p => powmod_pos m p (a mod m) end. Lemma mulmod_assoc: forall m x y z : Z, mulmod m x (mulmod m y z) = mulmod m (mulmod m x y) z. @@ -55,21 +55,21 @@ Proof. apply Z.mul_assoc. Qed. -Lemma pow_impl_N_correct: +Lemma powmod_1plus: forall m a : Z, - a = a mod m -> - forall x : N, pow_impl_N m a (1 + x) = (a * (pow_impl_N m a x mod m)) mod m. + forall x : N, powmod m a (1 + x) = (a * (powmod m a x mod m)) mod m. Proof. - intros m a pfa x. + intros m a x. rewrite N.add_1_l. - cbv beta delta [pow_impl_N N.succ]. - destruct x; [simpl; rewrite ?Zdiv.Zmult_mod_idemp_r, Z.mul_1_r; auto|]. - unfold pow_impl_pos. + cbv beta delta [powmod N.succ]. + destruct x. simpl; rewrite ?Zdiv.Zmult_mod_idemp_r, Z.mul_1_r; auto. + unfold powmod_pos. rewrite Pos.iter_op_succ by (apply mulmod_assoc). unfold mulmod. rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal. Qed. + Lemma N_pos_1plus : forall p, (N.pos p = 1 + (N.pred (N.pos p)))%N. intros. rewrite <-N.pos_pred_spec. @@ -79,14 +79,26 @@ Lemma N_pos_1plus : forall p, (N.pos p = 1 + (N.pred (N.pos p)))%N. discriminate. Qed. +Lemma powmod_Zpow_mod : forall m a n, powmod m a n = (a^Z.of_N n) mod m. +Proof. + induction n using N.peano_ind; [auto|]. + rewrite <-N.add_1_l. + rewrite powmod_1plus. + rewrite IHn. + rewrite Zmod_mod. + rewrite N.add_1_l. + rewrite N2Z.inj_succ. + rewrite Z.pow_succ_r by (apply N2Z.is_nonneg). + rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal. +Qed. + Definition pow_impl_sig {m} : {z : Z | z = z mod m} -> N -> {z : Z | z = z mod m}. intros a x. - exists (pow_impl_N m (proj1_sig a) x). + exists (powmod m (proj1_sig a) x). destruct x; [simpl; rewrite Zmod_mod; reflexivity|]. rewrite N_pos_1plus. - rewrite pow_impl_N_correct. - - rewrite Zmod_mod; reflexivity. - - destruct a; auto. + rewrite powmod_1plus. + rewrite Zmod_mod; reflexivity. Defined. Definition pow_impl: @@ -105,9 +117,8 @@ Definition pow_impl: intros m. exists pow_impl_sig. split; [eauto using exist_reduced_eq|]; intros. apply exist_reduced_eq. - rewrite pow_impl_N_correct. + rewrite powmod_1plus. rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal. - destruct a; auto. Qed. Lemma mul_mod_modulus_r : forall x m, (x*m) mod m = 0. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 2cc494224..a49138c86 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -227,13 +227,13 @@ Section VariousModPrime. + pose proof (FieldToZ_nonzero_range a a_nonzero); omega. + replace (q / 2)%Z with (Z.of_N (Z.to_N (q / 2))) by (apply Z2N.id; apply Z.div_pos; prime_bound). - rewrite FieldToZ_pow by omega. + rewrite FieldToZ_pow_Zpow_mod by omega. rewrite A. replace (FieldToZ 1) with (1 mod q) by auto. apply Z.mod_1_l; omega. } { apply F_eq. - rewrite <- FieldToZ_pow by omega. + rewrite <- FieldToZ_pow_Zpow_mod by omega. rewrite Z2N.id by (apply Z.div_pos; omega). replace (FieldToZ 1) with 1%Z by (rewrite FieldToZ_ZToField at 1; symmetry; apply Zmod_1_l; omega). @@ -367,4 +367,4 @@ Section SquareRootsPrime5Mod8. field. Qed. -End SquareRootsPrime5Mod8. +End SquareRootsPrime5Mod8.
\ No newline at end of file diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index c12799751..adc40dae6 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -116,8 +116,22 @@ Definition FlEncoding : encoding of F (Z.of_nat l) as word b := @modular_word_encoding (Z.of_nat l) b l_pos l_bound. 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. + +Hint Rewrite + @FieldToZ_pow_efficient + @FieldToZ_ZToField + @FieldToZ_opp + @FieldToZ_ZToField : ZToField + . + +Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F. +Proof. + apply F_eq. + autorewrite with ZToField. + vm_compute. + reflexivity. +Qed. + Definition PointEncoding := @point_encoding TEParams (b - 1) FqEncoding q_5mod8 sqrt_minus1_valid. Definition H : forall n : nat, word n -> word (b + b). Admitted. |