diff options
author | jadep <jade.philipoom@gmail.com> | 2016-04-28 13:13:08 -0400 |
---|---|---|
committer | jadep <jade.philipoom@gmail.com> | 2016-04-28 13:13:08 -0400 |
commit | cd07805915328fd5ee8d41b6cdd4d0340aa156aa (patch) | |
tree | 04a869de660aaa874fca7be13f9fefb86c12cafb | |
parent | 248282849e9b287fe817e64ccf53e09fa3991cbe (diff) |
Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.
-rw-r--r-- | src/BaseSystemProofs.v | 13 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingPre.v | 40 | ||||
-rw-r--r-- | src/Encoding/ModularWordEncodingTheorems.v | 26 | ||||
-rw-r--r-- | src/Encoding/PointEncodingPre.v | 58 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularArithmeticTheorems.v | 13 | ||||
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 14 | ||||
-rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 38 | ||||
-rw-r--r-- | src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 30 | ||||
-rw-r--r-- | src/Spec/Ed25519.v | 4 | ||||
-rw-r--r-- | src/Spec/PointEncoding.v | 4 | ||||
-rw-r--r-- | src/Util/ListUtil.v | 20 | ||||
-rw-r--r-- | src/Util/WordUtil.v | 25 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 17 |
13 files changed, 136 insertions, 166 deletions
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v index 84374fe8f..ab56cb711 100644 --- a/src/BaseSystemProofs.v +++ b/src/BaseSystemProofs.v @@ -17,6 +17,18 @@ Section BaseSystemProofs. unfold decode'; intros; f_equal; apply combine_truncate_l. Qed. + Lemma decode'_splice : forall xs ys bs, + decode' bs (xs ++ ys) = + decode' (firstn (length xs) bs) xs + decode' (skipn (length xs) bs) ys. + Proof. + unfold decode'. + induction xs; destruct ys, bs; boring. + + rewrite combine_truncate_r. + do 2 rewrite Z.add_0_r; auto. + + unfold accumulate. + apply Z.add_assoc. + Qed. + Lemma add_rep : forall bs us vs, decode' bs (add us vs) = decode' bs us + decode' bs vs. Proof. unfold decode', accumulate; induction bs; destruct us, vs; boring; ring. @@ -487,4 +499,5 @@ Section BaseSystemProofs. rewrite rev_length; omega. Qed. + End BaseSystemProofs. diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v index cb2f5a045..417344b43 100644 --- a/src/Encoding/ModularWordEncodingPre.v +++ b/src/Encoding/ModularWordEncodingPre.v @@ -3,8 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Bedrock.Word. Require Import Crypto.Tactics.VerdiTactics. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.WordUtil. +Require Import Crypto.Util.ZUtil Crypto.Util.WordUtil. Require Import Crypto.Spec.Encoding. Local Open Scope nat_scope. @@ -21,45 +20,12 @@ Section ModularWordEncodingPre. else None . - (* TODO : move to ZUtil *) - Lemma bound_check_N : forall x : F m, (Z.to_N x < Npow2 sz)%N. - Proof. - intro. - pose proof (FieldToZ_range x m_pos) as x_range. - rewrite <- Nnat.N2Nat.id. - rewrite Npow2_nat. - replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N. - apply (Nat2N_inj_lt _ (pow2 sz)). - rewrite Zpow_pow2. - destruct x_range as [x_low x_high]. - apply Z2Nat.inj_lt in x_high; try omega. - rewrite <- ZUtil.pow_Z2N_Zpow by omega. - replace (Z.to_nat 2) with 2%nat by auto. - omega. - Qed. - - (* TODO: move to WordUtil *) - Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N -> - wordToN (NToWord sz n) = n. - Proof. - intros. - rewrite wordToN_nat, NToWord_nat. - rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto. - Qed. - - (* TODO: move to WordUtil *) - Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w. - Proof. - intros. - rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id. - apply natToWord_wordToNat. - Qed. - Lemma Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x. Proof. unfold Fm_dec, Fm_enc; intros. pose proof (FieldToZ_range x m_pos). - rewrite wordToN_NToWord_idempotent by apply bound_check_N. + rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N; + assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega). rewrite Z2N.id by omega. rewrite ZToField_idempotent. break_if; auto; omega. diff --git a/src/Encoding/ModularWordEncodingTheorems.v b/src/Encoding/ModularWordEncodingTheorems.v index 83f199d90..a74ccb522 100644 --- a/src/Encoding/ModularWordEncodingTheorems.v +++ b/src/Encoding/ModularWordEncodingTheorems.v @@ -1,10 +1,11 @@ Require Import Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems. -Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. +Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithmetic.ModularArithmeticTheorems. Require Import Bedrock.Word. Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.Spec.Encoding. +Require Import Crypto.Util.ZUtil. Require Import Crypto.Spec.ModularWordEncoding. @@ -47,29 +48,6 @@ Section SignBit. rewrite sign_bit_parity; auto. Qed. - (* TODO : move to ZUtil *) - Lemma Z_odd_mod : forall a b, (b <> 0)%Z -> - Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. - Proof. - intros. - rewrite Zmod_eq_full by assumption. - rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. - break_if; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. - Qed. - - (* TODO : move to ModularArithmeticTheorems *) - Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z. - Proof. - intros. - rewrite FieldToZ_opp. - rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega. - rewrite mod_FieldToZ. - replace 0%Z with (@FieldToZ m 0) by auto. - intro false_eq. - rewrite <-F_eq in false_eq. - congruence. - Qed. - Lemma sign_bit_opp : forall (x : F m), x <> 0 -> negb (sign_bit x) = sign_bit (opp x). Proof. intros. diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v index 9b65d9819..e023da0ea 100644 --- a/src/Encoding/PointEncodingPre.v +++ b/src/Encoding/PointEncodingPre.v @@ -118,28 +118,6 @@ Section PointEncoding. | None => None end. - (* TODO : move *) - Lemma sqrt_mod_q_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0. - Proof. - unfold sqrt_mod_q; intros. - break_if. - - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end. - ring. - - match goal with - | [H : sqrt_minus1 * _ = 0 |- _ ]=> - apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ]; - [ | eapply Fq_root_zero; eauto ] - end. - unfold sqrt_minus1 in sqrt_minus1_zero. - rewrite sqrt_minus1_zero in sqrt_minus1_valid. - exfalso. - pose proof (@F_opp_spec q 1) as opp_spec_1. - rewrite <-sqrt_minus1_valid in opp_spec_1. - assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring. - rewrite ring_subst in *. - apply Fq_1_neq_0; assumption. - Qed. - Lemma point_coordinates_encoding_canonical : forall w p, point_dec_coordinates sign_bit w = Some p -> point_enc_coordinates p = w. Proof. @@ -151,7 +129,7 @@ Section PointEncoding. do 2 (break_if; try congruence); inversion coord_dec_Some; subst. + destruct (F_eq_dec (sqrt_mod_q (E.solve_for_x2 f1)) 0%F) as [sqrt_0 | ?]. - rewrite sqrt_0 in *. - apply sqrt_mod_q_0 in sqrt_0. + apply sqrt_mod_q_root_0 in sqrt_0; try assumption. rewrite sqrt_0 in *. break_if; [symmetry; auto using Bool.eqb_prop | ]. rewrite sign_bit_zero in *. @@ -195,19 +173,6 @@ Proof. exact (encoding_valid y). Qed. -(* -Lemma wordToN_enc_neq_opp : forall x, x <> 0 -> (wordToN (enc (opp x)) <> wordToN (enc x))%N. -Proof. - intros x x_nonzero. - intro false_eq. - apply x_nonzero. - apply F_eq_opp_zero; try apply two_lt_q. - apply wordToN_inj in false_eq. - apply encoding_inj in false_eq. - auto. -Qed. -*) - Lemma sign_bit_opp_eq_iff : forall x y, y <> 0 -> (sign_bit x <> sign_bit y <-> sign_bit x = sign_bit (opp y)). Proof. @@ -242,25 +207,6 @@ Proof. reflexivity. Qed. -(* TODO : move *) -Lemma sqrt_mod_q_of_0 : @sqrt_mod_q q 0 = 0. -Proof. - unfold sqrt_mod_q. - rewrite !Fq_pow_zero. - break_if; ring. - - congruence. - intro false_eq. - SearchAbout Z.to_N. - rewrite <-(N2Z.id 0) in false_eq. - rewrite N2Z.inj_0 in false_eq. - pose proof (prime_ge_2 q prime_q). - apply Z2N.inj in false_eq; zero_bounds. - assert (0 < q / 8 + 1)%Z. - apply Z.add_nonneg_pos; zero_bounds. - omega. -Qed. - Lemma point_encoding_coordinates_valid : forall p, E.onCurve p -> point_dec_coordinates sign_bit (point_enc_coordinates p) = Some p. Proof. @@ -277,7 +223,7 @@ Proof. rewrite !Fq_pow_zero, sqrt_mod_q_of_0, Fq_pow_zero by congruence. rewrite if_F_eq_dec_if_F_eqb, sign_bit_zero. reflexivity. - + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_0 in false_eq; + + assert (sqrt_mod_q (x ^ 2) <> 0) by (intro false_eq; apply sqrt_mod_q_root_0 in false_eq; try assumption; apply Fq_root_zero in false_eq; rewrite false_eq, F_eqb_refl in eqb_x_0; congruence). replace (F_eqb (sqrt_mod_q (x ^ 2)) 0) with false by (symmetry; apply F_eqb_neq_complete; assumption). diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v index 954fac15d..8b1ae9f93 100644 --- a/src/ModularArithmetic/ModularArithmeticTheorems.v +++ b/src/ModularArithmetic/ModularArithmeticTheorems.v @@ -697,4 +697,17 @@ Section VariousModulo. replace y with ((y - b) + b) by ring. rewrite Hxayb; ring. Qed. + + Lemma F_FieldToZ_add_opp : forall x : F m, x <> 0 -> (FieldToZ x + FieldToZ (opp x) = m)%Z. + Proof. + intros. + rewrite FieldToZ_opp. + rewrite Z_mod_nz_opp_full, mod_FieldToZ; try omega. + rewrite mod_FieldToZ. + replace 0%Z with (@FieldToZ m 0) by auto. + intro false_eq. + rewrite <-F_eq in false_eq. + congruence. + Qed. + End VariousModulo. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index f39f32ea5..2989bfa12 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -178,20 +178,6 @@ Section PseudoMersenneProofs. } Qed. - (* TODO: move to BaseSystemProofs *) - Lemma decode'_splice : forall xs ys bs, - BaseSystem.decode' bs (xs ++ ys) = - BaseSystem.decode' (firstn (length xs) bs) xs + - BaseSystem.decode' (skipn (length xs) bs) ys. - Proof. - unfold BaseSystem.decode'. - induction xs; destruct ys, bs; boring. - + rewrite combine_truncate_r. - do 2 rewrite Z.add_0_r; auto. - + unfold BaseSystem.accumulate. - apply Z.add_assoc. - Qed. - Lemma set_nth_sum : forall n x us, (n < length us)%nat -> BaseSystem.decode base (set_nth n x us) = (x - nth_default 0 us n) * nth_default 0 base n + BaseSystem.decode base us. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 759085dc6..8a69a0c54 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -472,6 +472,44 @@ Section SquareRootsPrime5Mod8. field. Qed. + Lemma sqrt_mod_q_of_0 : sqrt_mod_q 0 = 0. + Proof. + unfold sqrt_mod_q. + rewrite !Fq_pow_zero. + break_if; ring. + + congruence. + intro false_eq. + rewrite <-(N2Z.id 0) in false_eq. + rewrite N2Z.inj_0 in false_eq. + pose proof (prime_ge_2 q prime_q). + apply Z2N.inj in false_eq; zero_bounds. + assert (0 < q / 8 + 1)%Z. + apply Z.add_nonneg_pos; zero_bounds. + omega. + Qed. + + Lemma sqrt_mod_q_root_0 : forall x : F q, sqrt_mod_q x = 0 -> x = 0. + Proof. + unfold sqrt_mod_q; intros. + break_if. + - match goal with [ H : ?sqrt_x ^ 2 = x, H' : ?sqrt_x = 0 |- _ ] => rewrite <-H, H' end. + ring. + - match goal with + | [H : sqrt_minus1 * _ = 0 |- _ ]=> + apply Fq_mul_zero_why in H; destruct H as [sqrt_minus1_zero | ? ]; + [ | eapply Fq_root_zero; eauto ] + end. + unfold sqrt_minus1 in sqrt_minus1_zero. + rewrite sqrt_minus1_zero in sqrt_minus1_valid. + exfalso. + pose proof (@F_opp_spec q 1) as opp_spec_1. + rewrite <-sqrt_minus1_valid in opp_spec_1. + assert (((1 + 0 ^ 2) : F q) = (1 : F q)) as ring_subst by ring. + rewrite ring_subst in *. + apply Fq_1_neq_0; assumption. + Qed. + End SquareRootsPrime5Mod8. Local Open Scope F_scope. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 0a58c81d2..1a7b3316e 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -89,26 +89,6 @@ Section PseudoMersenneBaseParamProofs. - rewrite IHl by auto; ring. Qed. - (* TODO : move to LsitUtil *) - Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x, - P x -> (forall y, In y l -> forall z, P z -> P (f y z)) -> - P (fold_right f x l). - Proof. - induction l; intros ? ? step; auto. - simpl. - apply step; try apply in_eq. - apply IHl; auto. - intros y in_y_l. - apply (in_cons a) in in_y_l. - auto. - Qed. - - (* TODO : move to ListUtil *) - Lemma In_firstn : forall {T} n l (x : T), In x (firstn n l) -> In x l. - Proof. - induction n; destruct l; boring. - Qed. - Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. Proof. unfold sum_firstn; intros. @@ -163,16 +143,6 @@ Section PseudoMersenneBaseParamProofs. rewrite two_p_correct in nth_err_x. congruence. Qed. - - - (* TODO : move to ZUtil *) - Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. - Proof. - intros. - replace b with (b - c + c) by ring. - rewrite Z.pow_add_r by omega. - apply Z_mod_mult. - Qed. Lemma base_matches_modulus: forall i j, (i < length base)%nat -> diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v index 505797987..9ae03dcd5 100644 --- a/src/Spec/Ed25519.v +++ b/src/Spec/Ed25519.v @@ -146,8 +146,8 @@ Qed. Lemma b_minus1_nonzero : 0 < b - 1. Proof. cbv. omega. Qed. Definition PointEncoding : encoding of E.point as (word b) := - (@point_encoding _ _ b_minus1_nonzero b_valid q_5mod8 sqrt_minus1_valid FqEncoding - (@sign_bit _ prime_q two_lt_q _ b_valid) sign_bit_zero sign_bit_opp). + (@point_encoding curve25519params (b - 1) q_5mod8 sqrt_minus1_valid FqEncoding + (@sign_bit _ prime_q two_lt_q (b - 1) b_valid) sign_bit_zero sign_bit_opp). Definition H : forall n : nat, word n -> word (b + b). Admitted. Definition B : E.point. Admitted. (* TODO: B = decodePoint (y=4/5, x="positive") *) diff --git a/src/Spec/PointEncoding.v b/src/Spec/PointEncoding.v index 3668632f4..484c5f0df 100644 --- a/src/Spec/PointEncoding.v +++ b/src/Spec/PointEncoding.v @@ -33,10 +33,10 @@ Section PointEncoding. Definition point_dec := Eval hnf in (proj1_sig point_dec_with_spec). Definition point_encoding_valid : forall p : E.point, point_dec (point_enc p) = Some p := - @PointEncodingPre.point_encoding_valid _ _ sz_nonzero bound_check q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp. + @PointEncodingPre.point_encoding_valid _ _ q_5mod8 sqrt_minus1_valid _ _ sign_bit_zero sign_bit_opp. Definition point_encoding_canonical : forall x_enc x, point_dec x_enc = Some x -> point_enc x = x_enc := - PointEncodingPre.point_encoding_canonical . + PointEncodingPre.point_encoding_canonical. Instance point_encoding : encoding of E.point as (Word.word (S sz)) := { enc := point_enc; diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index b640fb8e8..36d8a3ad3 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -563,4 +563,22 @@ Proof. induction l; intros; simpl; try tauto. rewrite <- IHl. intuition (subst; auto). -Qed.
\ No newline at end of file +Qed. + +Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x, + P x -> (forall y, In y l -> forall z, P z -> P (f y z)) -> + P (fold_right f x l). +Proof. + induction l; intros ? ? step; auto. + simpl. + apply step; try apply in_eq. + apply IHl; auto. + intros y in_y_l. + apply (in_cons a) in in_y_l. + auto. +Qed. + +Lemma In_firstn : forall {T} n l (x : T), In x (firstn n l) -> In x l. +Proof. + induction n; destruct l; boring. +Qed. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 17d04c60a..d655d046d 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -1,5 +1,6 @@ Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.NatUtil. Require Import Bedrock.Word. Local Open Scope nat_scope. @@ -21,6 +22,30 @@ Proof. auto. Qed. +Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N -> + wordToN (NToWord sz n) = n. +Proof. + intros. + rewrite wordToN_nat, NToWord_nat. + rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto. +Qed. + +Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w. +Proof. + intros. + rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id. + apply natToWord_wordToNat. +Qed. + +Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N. +Proof. + intros x n bound_nat. + rewrite <- Nnat.N2Nat.id, Npow2_nat. + replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N. + apply (Nat2N_inj_lt _ (pow2 n)). + rewrite pow2_id; assumption. +Qed. + Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n. refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with | eq_refl => w diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 9f7b1d645..bc7e9d740 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -280,6 +280,23 @@ Proof. assumption. Qed. +Lemma Z_odd_mod : forall a b, (b <> 0)%Z -> + Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. +Proof. + intros. + rewrite Zmod_eq_full by assumption. + rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. + case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. +Qed. + +Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. +Proof. + intros. + replace b with (b - c + c) by ring. + rewrite Z.pow_add_r by omega. + apply Z_mod_mult. +Qed. + (* prove that known nonnegative numbers are nonnegative *) Ltac zero_bounds' := repeat match goal with |