diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 45 |
1 files changed, 40 insertions, 5 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index a0699ec17..6d6dc0f9f 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -2474,7 +2474,7 @@ hd 0 p). Hint Rewrite length_from_columns using eassumption : distr_length. Hint Rewrite length_sum_rows using solve [ reflexivity | eassumption | distr_length; eauto ] : distr_length. Hint Rewrite length_fst_extract_row length_snd_extract_row length_flatten length_flatten' length_partition length_fst_from_columns' length_snd_from_columns' : distr_length. - Hint Rewrite @eval_partition : push_eval. + Hint Rewrite @eval_partition using auto : push_eval. End Rows. Module BaseConversion. @@ -3064,6 +3064,30 @@ Module UniformWeight. rewrite !Z.pow_succ_r by auto using Nat2Z.is_nonneg. ring. Qed. + + (* Because the weight is uniform, we can start partitioning from + any index and end up with the same result. *) + Lemma uweight_recursive_partition_change_start lgr (Hr : 0 <= lgr) n : + forall i j x, + Partition.recursive_partition (uweight lgr) n i x + = Partition.recursive_partition (uweight lgr) n j x. + Proof. + induction n; intros; [reflexivity | ]. + cbn [Partition.recursive_partition]. + rewrite !uweight_eq_alt by omega. + autorewrite with push_Zof_nat push_Zpow. + rewrite <-!Z.pow_sub_r by auto using Z.pow_nonzero with omega. + rewrite !Z.sub_succ_l. + autorewrite with zsimplify_fast. + erewrite IHn. reflexivity. + Qed. + Lemma uweight_recursive_partition_equiv lgr (Hr : 0 < lgr) n i x: + Partition.partition (uweight lgr) n x = + Partition.recursive_partition (uweight lgr) n i x. + Proof. + rewrite Partition.recursive_partition_equiv by auto using uwprops. + auto using uweight_recursive_partition_change_start with omega. + Qed. End UniformWeight. Module WordByWordMontgomery. @@ -3279,7 +3303,7 @@ Module WordByWordMontgomery. repeat match goal with | _ => progress cbn [recursive_partition] | H : small _ |- _ => rewrite H; clear H - | _ => rewrite recursive_partition_equiv by auto using UniformWeight.uwprops + | _ => rewrite recursive_partition_equiv by auto using wprops | _ => rewrite UniformWeight.uweight_eval_shift by distr_length | _ => progress push end. @@ -3297,7 +3321,18 @@ Module WordByWordMontgomery. push_recursive_partition; cbn [Rows.divmod snd hd]. autorewrite with zsimplify; reflexivity. Qed. - Local Axiom small_div : forall n v, small v -> small (fst (@divmod n v)). + Lemma small_div : forall n v, small v -> small (fst (@divmod n v)). + Proof. + pose proof r_big as r_big. + clear - r_big lgr_big. intros; autounfold with loc. + push_recursive_partition. cbn [Rows.divmod fst tl]. + rewrite <-recursive_partition_equiv by auto. + rewrite <-UniformWeight.uweight_recursive_partition_equiv with (i:=1%nat) by omega. + push. + apply Partition.partition_Proper; [ solve [auto] | ]. + cbv [Z.equiv_modulo]. autorewrite with zsimplify. + reflexivity. + Qed. Local Lemma eval_scmul: forall n a v, small v -> 0 <= a < r -> 0 <= eval v < r^Z.of_nat n -> eval (@scmul n a v) = a * eval v. Proof using lgr_big. generalize (@length_small); clear -lgr_big; intro. @@ -3475,7 +3510,7 @@ Module WordByWordMontgomery. Lemma small_A' : small A'. - Proof using small_A. repeat autounfold with word_by_word_montgomery; t_small. Qed. + Proof using small_A lgr_big. repeat autounfold with word_by_word_montgomery; t_small. Qed. Lemma small_S3 : small S3. @@ -3589,7 +3624,7 @@ Module WordByWordMontgomery. (S_bound : 0 <= eval S < eval N + eval B). Lemma small_fst_redc_body : small (fst (redc_body A_S)). - Proof using S_bound small_A small_S. destruct A_S; apply small_A'; assumption. Qed. + Proof using S_bound small_A small_S lgr_big. destruct A_S; apply small_A'; assumption. Qed. Lemma small_snd_redc_body : small (snd (redc_body A_S)). Proof using small_S small_N small_B small_A lgr_big S_bound B_bounds N_nz N_lt_R. destruct A_S; unfold redc_body; apply small_S3; assumption. |