diff options
author | Jason Gross <jasongross9@gmail.com> | 2016-07-18 19:09:46 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2016-07-18 19:09:46 +0200 |
commit | 07ca661557d86b96d1ee0a9b9013d0834158571f (patch) | |
tree | 78980ce7dbbf836f1d109159332600370ed224e6 /src/ModularArithmetic/ModularBaseSystemProofs.v | |
parent | 0fd535b57b93bada6cc00c2e372f2f94d2768567 (diff) |
Move some definitions to Pow2Base (#24)
* Move some definitions to Pow2Base
These definitions don't depend on PseudoMersenneBaseParams, only on
limb_widths, and we'll want them for BarrettReduction / P256.
* Fix for Coq 8.4
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 188 |
1 files changed, 47 insertions, 141 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 7e33ab20f..e5ae285de 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -10,6 +10,7 @@ Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Util.Tactics. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. @@ -22,7 +23,8 @@ Section PseudoMersenneProofs. Local Notation "u .+ x" := (add u x). Local Notation "u .* x" := (ModularBaseSystem.mul u x). Local Hint Unfold rep. - Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. + Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. + Local Hint Resolve log_cap_nonneg. Local Notation base := (base_from_limb_widths limb_widths). Local Notation log_cap i := (nth_default 0 limb_widths i). @@ -166,6 +168,11 @@ Section PseudoMersenneProofs. rewrite <- Zplus_mod; auto. Qed. + Lemma pseudomersenne_add': forall x y0 y1 z, (z - x + ((2^k) * y0 * y1)) mod modulus = (c * y0 * y1 - x + z) mod modulus. + Proof. + intros; rewrite <- !Z.add_opp_r, <- !Z.mul_assoc, pseudomersenne_add; apply f_equal2; omega. + Qed. + Lemma extended_shiftadd: forall (us : BaseSystem.digits), BaseSystem.decode ext_base us = BaseSystem.decode base (firstn (length base) us) @@ -207,7 +214,7 @@ Section PseudoMersenneProofs. apply Max.max_l; omega. Qed. - Lemma length_mul : forall u v, + Lemma length_mul : forall u v, length u = length base -> length v = length base -> length (u .* v) = length base. @@ -231,56 +238,6 @@ Section PseudoMersenneProofs. apply ZToField_mul. } 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. - Proof. - intros. - unfold BaseSystem.decode. - nth_inbounds; auto. (* TODO(andreser): nth_inbounds should do this auto*) - unfold splice_nth. - rewrite <- (firstn_skipn n us) at 4. - do 2 rewrite decode'_splice. - remember (length (firstn n us)) as n0. - ring_simplify. - remember (BaseSystem.decode' (firstn n0 base) (firstn n us)). - rewrite (skipn_nth_default n us 0) by omega. - rewrite firstn_length in Heqn0. - rewrite Min.min_l in Heqn0 by omega; subst n0. - destruct (le_lt_dec (length base) n). { - rewrite nth_default_out_of_bounds by auto. - rewrite skipn_all by omega. - do 2 rewrite decode_base_nil. - ring_simplify; auto. - } { - rewrite (skipn_nth_default n base 0) by omega. - do 2 rewrite decode'_cons. - ring_simplify; ring. - } - Qed. - - Lemma add_to_nth_sum : forall n x us, (n < length us)%nat -> - BaseSystem.decode base (add_to_nth n x us) = - x * nth_default 0 base n + BaseSystem.decode base us. - Proof. - unfold add_to_nth; intros; rewrite set_nth_sum; try ring_simplify; auto. - Qed. - - Lemma add_to_nth_nth_default : forall n x l i, (0 <= i < length l)%nat -> - nth_default 0 (add_to_nth n x l) i = - if (eq_nat_dec i n) then x + nth_default 0 l i else nth_default 0 l i. - Proof. - intros. - unfold add_to_nth. - rewrite set_nth_nth_default by assumption. - break_if; subst; reflexivity. - Qed. - - Lemma length_add_to_nth : forall n x l, length (add_to_nth n x l) = length l. - Proof. - unfold add_to_nth; intros; apply length_set_nth. - Qed. - Lemma nth_default_base_positive : forall i, (i < length base)%nat -> nth_default 0 base i > 0. Proof. @@ -310,14 +267,6 @@ Section PseudoMersenneProofs. apply FieldToZ_ZToField. Qed. - Lemma log_cap_nonneg : forall i, 0 <= log_cap i. - Proof. - unfold nth_default; intros. - case_eq (nth_error limb_widths i); intros; try omega. - apply limb_widths_nonneg. - eapply nth_error_value_In; eauto. - Qed. Local Hint Resolve log_cap_nonneg. - Definition carry_done us := forall i, (i < length base)%nat -> 0 <= nth_default 0 us i /\ Z.shiftr (nth_default 0 us i) (log_cap i) = 0. @@ -374,7 +323,7 @@ Section CarryProofs. Local Notation base := (base_from_limb_widths limb_widths). Local Notation log_cap i := (nth_default 0 limb_widths i). Local Notation "u ~= x" := (rep u x). - Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. + Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg. Lemma base_length_lt_pred : (pred (length base) < length base)%nat. Proof. @@ -382,40 +331,6 @@ Section CarryProofs. Qed. Hint Resolve base_length_lt_pred. - Lemma nth_default_base_succ : forall i, (S i < length base)%nat -> - nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i. - Proof. - intros. - repeat rewrite nth_default_base by (omega || eauto). - rewrite <- Z.pow_add_r by eauto using log_cap_nonneg. - destruct (NPeano.Nat.eq_dec i 0). - + subst; f_equal. - unfold sum_firstn. - destruct limb_widths; auto. - + erewrite sum_firstn_succ; eauto. - apply nth_error_Some_nth_default. - rewrite <- base_length; omega. - Qed. - - Lemma carry_simple_decode_eq : forall i us, - (length us = length base) -> - (i < (pred (length base)))%nat -> - BaseSystem.decode base (carry_simple i us) = BaseSystem.decode base us. - Proof. - unfold carry_simple. intros. - rewrite add_to_nth_sum by (rewrite length_set_nth; omega). - rewrite set_nth_sum by omega. - unfold Z.pow2_mod. - rewrite Z.land_ones by apply log_cap_nonneg. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. - rewrite nth_default_base_succ by omega. - rewrite Z.mul_assoc. - rewrite (Z.mul_comm _ (2 ^ log_cap i)). - rewrite Z.mul_div_eq; try ring. - apply Z.gt_lt_iff. - apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg. - Qed. - Lemma carry_decode_eq_reduce : forall us, (length us = length base) -> BaseSystem.decode base (carry_and_reduce (pred (length base)) us) mod modulus @@ -442,9 +357,9 @@ Section CarryProofs. + rewrite nth_default_base by (omega || eauto). rewrite <- Z.add_opp_l, <- Z.opp_sub_distr. unfold Z.pow2_mod. - rewrite Z.land_ones by apply log_cap_nonneg. - rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg). - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + rewrite Z.land_ones by eauto using log_cap_nonneg. + rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || eauto using log_cap_nonneg). + rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. rewrite Zopp_mult_distr_r. rewrite Z.mul_comm. rewrite Z.mul_assoc. @@ -460,21 +375,23 @@ Section CarryProofs. ring. Qed. - Lemma carry_length : forall i us, - (length us = length base)%nat -> - (length (carry i us) = length base)%nat. - Proof. - unfold carry, carry_simple, carry_and_reduce, add_to_nth. - intros; break_if; subst; repeat (rewrite length_set_nth); auto. - Qed. - Hint Resolve carry_length. + Lemma length_carry_and_reduce : forall i us, length (carry_and_reduce i us) = length us. + Proof. intros; unfold carry_and_reduce; autorewrite with distr_length; reflexivity. Qed. + Hint Rewrite @length_carry_and_reduce : distr_length. + + Lemma length_carry : forall i us, length (carry i us) = length us. + Proof. intros; unfold carry; break_if; autorewrite with distr_length; reflexivity. Qed. + Hint Rewrite @length_carry : distr_length. + + Local Hint Extern 1 (length _ = _) => progress autorewrite with distr_length. Lemma carry_rep : forall i us x, (length us = length base) -> (i < length base)%nat -> us ~= x -> carry i us ~= x. Proof. - pose carry_length. pose carry_decode_eq_reduce. pose carry_simple_decode_eq. + pose proof length_carry. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths). + specialize_by eauto. intros; split; auto. unfold rep, decode, carry in *. intuition; break_if; subst; eauto; apply F_eq; simpl; intuition. @@ -497,13 +414,6 @@ Section CarryProofs. induction is; boring. Qed. - (* TODO : move? *) - Lemma make_chain_lt : forall x i : nat, In i (make_chain x) -> (i < x)%nat. - Proof. - induction x; simpl; intuition. - Qed. - - Lemma carry_full_length : forall us, (length us = length base)%nat -> length (carry_full us) = length base. Proof. @@ -529,7 +439,7 @@ Section CarryProofs. Qed. Lemma carry_mul_length : forall us vs, - length us = length base -> length vs = length base -> + length us = length base -> length vs = length base -> length (carry_mul us vs) = length base. Proof. intros; cbv [carry_mul]. @@ -538,6 +448,8 @@ Section CarryProofs. End CarryProofs. +Hint Rewrite @length_carry_and_reduce @length_carry : distr_length. + Section CanonicalizationProofs. Context `{prm : PseudoMersenneBaseParams}. Local Notation base := (base_from_limb_widths limb_widths). @@ -553,10 +465,11 @@ Section CanonicalizationProofs. (two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus). (* BEGIN groundwork proofs *) + Local Hint Resolve (@log_cap_nonneg limb_widths) limb_widths_nonneg. Lemma pow_2_log_cap_pos : forall i, 0 < 2 ^ log_cap i. Proof. - intros; apply Z.pow_pos_nonneg; auto using log_cap_nonneg; omega. + intros; apply Z.pow_pos_nonneg; eauto using log_cap_nonneg; omega. Qed. Local Hint Resolve pow_2_log_cap_pos. @@ -568,12 +481,11 @@ Section CanonicalizationProofs. omega. Qed. - Local Hint Resolve log_cap_nonneg. Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_bound i. Proof. intros. unfold Z.pow2_mod. - rewrite Z.land_ones by apply log_cap_nonneg. + rewrite Z.land_ones by eauto using log_cap_nonneg. unfold max_bound, Z.ones. rewrite Z.shiftl_1_l, <-Z.lt_le_pred. apply Z_mod_lt. @@ -598,7 +510,7 @@ Section CanonicalizationProofs. Proof. intros. unfold Z.pow2_mod. - rewrite Z.land_ones by apply log_cap_nonneg. + rewrite Z.land_ones by eauto using log_cap_nonneg. apply Z.mod_small. split; try omega. rewrite <- max_bound_log_cap. @@ -617,17 +529,10 @@ Section CanonicalizationProofs. Lemma max_bound_nonneg : forall i, 0 <= max_bound i. Proof. - unfold max_bound; intros; auto using Z.ones_nonneg. + unfold max_bound; intros; eauto using Z.ones_nonneg. Qed. Local Hint Resolve max_bound_nonneg. - Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b). - Proof. - intros. - unfold Z.pow2_mod. - rewrite Z.land_ones; auto. - Qed. - Lemma shiftr_eq_0_max_bound : forall i a, Z.shiftr a (log_cap i) = 0 -> a <= max_bound i. Proof. @@ -678,7 +583,7 @@ Section CanonicalizationProofs. (* automation *) Ltac carry_length_conditions' := unfold carry_full, add_to_nth; - rewrite ?length_set_nth, ?carry_length, ?carry_sequence_length; + rewrite ?length_set_nth, ?length_carry, ?carry_sequence_length; try omega; try solve [pose proof base_length; pose proof base_length_nonzero; omega || auto ]. Ltac carry_length_conditions := try split; try omega; repeat carry_length_conditions'. @@ -931,9 +836,9 @@ Section CanonicalizationProofs. replace (2 ^ B) with (2 ^ (B - log_cap i) + (2 ^ B - 2 ^ (B - log_cap i))) by omega. split; [ zero_bounds | ]. apply Z.add_lt_mono; try omega. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.div_lt_upper_bound; try apply pow_2_log_cap_pos. - rewrite <-Z.pow_add_r by (apply log_cap_nonneg || apply B_compat_log_cap). + rewrite <-Z.pow_add_r by (eauto using log_cap_nonneg || apply B_compat_log_cap). replace (log_cap i + (B - log_cap i)) with B by ring. omega. Qed. @@ -976,7 +881,7 @@ Section CanonicalizationProofs. apply Z.add_le_mono. + apply carry_bounds_0_upper; auto; omega. + apply Z.mul_le_mono_pos_l; auto using c_pos. - apply Z.shiftr_ones; auto; + apply Z.shiftr_ones; eauto; [ | pose proof (B_compat_log_cap (pred (length base))); omega ]. split. - apply carry_bounds_lower; auto; omega. @@ -1014,7 +919,7 @@ Section CanonicalizationProofs. apply carry_full_bounds; auto; omega. + rewrite <-max_bound_log_cap, <-Z.add_1_l. apply Z.add_le_mono. - - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + - rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.div_floor; auto. destruct i. * simpl. @@ -1047,7 +952,7 @@ Section CanonicalizationProofs. - apply carry_bounds_0_upper; carry_length_conditions. - etransitivity; [ | replace c with (c * 1) by ring; reflexivity ]. apply Z.mul_le_mono_pos_l; try (pose proof c_pos; omega). - rewrite Z.shiftr_div_pow2 by auto. + rewrite Z.shiftr_div_pow2 by eauto. apply Z.div_le_upper_bound; auto. ring_simplify. apply carry_sequence_carry_full_bounds_same; auto. @@ -1060,7 +965,7 @@ Section CanonicalizationProofs. 0 <= nth_default 0 (carry_sequence (make_chain i) (carry_full (carry_full us))) i <= 2 ^ log_cap i) -> - 0 <= nth_default 0 (carry_simple i + 0 <= nth_default 0 (carry_simple limb_widths i (carry_sequence (make_chain i) (carry_full (carry_full us)))) (S i) <= 2 ^ log_cap (S i). Proof. unfold carry_simple; intros ? ? PCB length_eq ? IH. @@ -1072,7 +977,7 @@ Section CanonicalizationProofs. apply carry_full_bounds; carry_length_conditions. carry_seq_lower_bound. + rewrite <-max_bound_log_cap, <-Z.add_1_l. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.add_le_mono. - apply Z.div_le_upper_bound; auto. ring_simplify. apply IH. omega. @@ -1096,7 +1001,7 @@ Section CanonicalizationProofs. - eapply carry_full_bounds; eauto; carry_length_conditions. carry_seq_lower_bound. + rewrite <-max_bound_log_cap, <-Z.add_1_l. - rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg. + rewrite Z.shiftr_div_pow2 by eauto using log_cap_nonneg. apply Z.add_le_mono. - apply Z.div_floor; auto. eapply Z.le_lt_trans; [ eapply carry_full_2_bounds_0; eauto | ]. @@ -1183,7 +1088,7 @@ Section CanonicalizationProofs. remember ((nth_default 0 (carry_full (carry_full us)) 0)) as x. apply Z.le_trans with (m := (max_bound 0 + c) - (1 + max_bound 0)); try omega. replace x with ((x - 2 ^ log_cap 0) + (1 * 2 ^ log_cap 0)) by ring. - rewrite pow2_mod_spec by auto. + rewrite Z.pow2_mod_spec by eauto. cbv [make_chain carry_sequence fold_right]. rewrite Z.mod_add by (pose proof (pow_2_log_cap_pos 0); omega). rewrite <-max_bound_log_cap, <-Z.add_1_l, Z.mod_small; @@ -1200,6 +1105,7 @@ Section CanonicalizationProofs. assumption. Qed. + (* END proofs about second carry loop *) (* BEGIN proofs about third carry loop *) @@ -1230,7 +1136,7 @@ Section CanonicalizationProofs. apply Z.add_le_mono; try assumption. etransitivity; [ | replace c with (c * 1) by ring; reflexivity ]. apply Z.mul_le_mono_pos_l; try omega. - rewrite Z.shiftr_div_pow2 by auto. + rewrite Z.shiftr_div_pow2 by eauto. apply Z.div_le_upper_bound; auto. ring_simplify. apply carry_full_2_bounds_same; auto. @@ -1299,8 +1205,8 @@ Section CanonicalizationProofs. Proof. unfold max_ones. apply Z.ones_nonneg. + clear. pose proof limb_widths_nonneg. - clear c_reduce1 lt_1_length_base. induction limb_widths as [|?? IHl]. cbv; congruence. simpl. @@ -1732,7 +1638,7 @@ Section CanonicalizationProofs. rewrite decode_base_nil. apply Z.gt_lt; auto using nth_default_base_positive. + rewrite decode_firstn_succ by (auto || omega). - rewrite nth_default_base_succ by omega. + rewrite nth_default_base_succ by (eauto || omega). eapply Z.lt_le_trans. - apply Z.add_lt_mono_r. apply IHn; auto; omega. @@ -2103,4 +2009,4 @@ Section CanonicalizationProofs. eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs.
\ No newline at end of file +End CanonicalizationProofs. |