From a189b8ad9943cec026ea2797789d8dc72a6d3336 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 14 Mar 2019 15:04:10 -0400 Subject: remove extraneous module identifiers --- src/Arithmetic/BarrettReduction.v | 42 ++++++++++----------- src/Arithmetic/BaseConversion.v | 6 +-- src/Arithmetic/FancyMontgomeryReduction.v | 2 +- src/Arithmetic/Freeze.v | 21 ++++++----- src/Arithmetic/WordByWordMontgomery.v | 52 +++++++++++++------------- src/PushButtonSynthesis/BarrettReduction.v | 12 +++--- src/PushButtonSynthesis/WordByWordMontgomery.v | 34 ++++++++--------- 7 files changed, 85 insertions(+), 84 deletions(-) (limited to 'src') diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v index b679a168c..2f1f272ac 100644 --- a/src/Arithmetic/BarrettReduction.v +++ b/src/Arithmetic/BarrettReduction.v @@ -61,7 +61,7 @@ Section Generic. Local Lemma M_pos : 0 < M. Proof. assert (0 <= b ^ (k - 1)) by Z.zero_bounds. lia. Qed. Local Lemma M_upper : M < weight n. - Proof. rewrite UniformWeight.uweight_eq_alt'. lia. Qed. + Proof. rewrite uweight_eq_alt'. lia. Qed. Local Lemma x_upper : x < b ^ (2 * k). Proof. assert (0 < b ^ k) by Z.zero_bounds. @@ -115,15 +115,15 @@ Module Fancy. (k_pos : 0 < k) (* this can be inferred from other arguments but is easier to put here for tactics *) (k_eq : k = width * Z.of_nat sz). (* sz = 1, width = k = 256 *) - Local Notation w := (UniformWeight.uweight width). Local Notation eval := (Positional.eval w). + Local Notation w := (uweight width). Local Notation eval := (Positional.eval w). Context (mut Mt : list Z) (mut_correct : mut = partition w (sz+1) mu) (Mt_correct : Mt = partition w sz M). Context (mu_eq : mu = 2 ^ (2 * k) / M) (muHigh_one : mu / w sz = 1) (M_range : 2^(k-1) < M < 2^k). - Local Lemma wprops : @weight_properties w. Proof. apply UniformWeight.uwprops; auto with lia. Qed. + Local Lemma wprops : @weight_properties w. Proof. apply uwprops; auto with lia. Qed. Local Hint Resolve wprops. Hint Rewrite mut_correct Mt_correct : pull_partition. - Lemma w_eq_2k : w sz = 2^k. Proof. rewrite UniformWeight.uweight_eq_alt' by auto. congruence. Qed. + Lemma w_eq_2k : w sz = 2^k. Proof. rewrite uweight_eq_alt' by auto. congruence. Qed. Lemma mu_range : 2^k <= mu < 2^(k+1). Proof. rewrite mu_eq. assert (0 < 2^(k-1)) by Z.zero_bounds. @@ -140,7 +140,7 @@ Module Fancy. Proof. pose proof mu_range. assert (0 < 2^k) by auto with zarith. assert (2^(k+1) = 2 * w sz); [ | lia]. - rewrite k_eq, UniformWeight.uweight_eq_alt'. + rewrite k_eq, uweight_eq_alt'. rewrite Z.pow_add_r, Z.pow_1_r by lia. lia. Qed. Lemma M_range' : 0 <= M < w sz. (* more convenient form, especially for mod_small *) @@ -206,20 +206,20 @@ Module Fancy. cbv [shiftr']. induction m; intros; [ reflexivity | ]. rewrite !partition_step, seq_snoc. autorewrite with distr_length natsimplify push_map push_nth_default. - rewrite IHm, Z.rshi_correct, UniformWeight.uweight_S by auto with zarith. + rewrite IHm, Z.rshi_correct, uweight_S by auto with zarith. rewrite <-Z.mod_pull_div by auto with zarith. destruct (Nat.eq_dec (S m) tn); [subst tn | ]; rewrite !nth_default_partition by omega. { rewrite nth_default_out_of_bounds by distr_length. autorewrite with zsimplify. Z.rewrite_mod_small. rewrite Z.div_div_comm by auto with zarith; reflexivity. } { repeat match goal with - | _ => rewrite UniformWeight.uweight_pull_mod by auto with zarith + | _ => rewrite uweight_pull_mod by auto with zarith | _ => rewrite Z.mod_mod_small by auto with zarith | _ => rewrite <-Znumtheory.Zmod_div_mod by (Z.zero_bounds; auto with zarith) - | _ => rewrite UniformWeight.uweight_eq_alt with (n:=1%nat) by auto with zarith + | _ => rewrite uweight_eq_alt with (n:=1%nat) by auto with zarith | |- context [(t / w (S m)) mod 2^width * 2^width] => replace (t / w (S m)) with (t / w m / 2^width) by - (rewrite UniformWeight.uweight_S, Z.div_div by auto with zarith; f_equal; lia); + (rewrite uweight_S, Z.div_div by auto with zarith; f_equal; lia); rewrite Z.mod_pull_div with (b:=2^width) by auto with zarith; rewrite Z.mul_div_eq' by auto with zarith | _ => progress autorewrite with natsimplify zsimplify_fast zsimplify @@ -239,11 +239,11 @@ Module Fancy. pose proof (Z.mod_pos_bound n width ltac:(omega)). assert (t / 2 ^ (n - n mod width) < w (tn - Z.to_nat (n / width))). { apply Z.div_lt_upper_bound; [solve [Z.zero_bounds] | ]. - rewrite UniformWeight.uweight_eq_alt' in *. + rewrite uweight_eq_alt' in *. rewrite <-Z.pow_add_r, Nat2Z.inj_sub, Z2Nat.id, <-Z.mul_div_eq by auto with zarith. autorewrite with push_Zmul zsimplify. auto with zarith. } repeat match goal with - | _ => progress rewrite ?UniformWeight.uweight_skipn_partition, ?UniformWeight.uweight_eq_alt' by auto with lia + | _ => progress rewrite ?uweight_skipn_partition, ?uweight_eq_alt' by auto with lia | _ => rewrite Z2Nat.id by Z.zero_bounds | _ => rewrite Z.mul_div_eq_full by auto with zarith | _ => rewrite shiftr'_correct by auto with zarith @@ -267,16 +267,16 @@ Module Fancy. Qed. Lemma low_correct n a : (sz <= n)%nat -> low (partition w n a) = partition w sz a. - Proof. cbv [low]; auto using UniformWeight.uweight_firstn_partition with lia. Qed. + Proof. cbv [low]; auto using uweight_firstn_partition with lia. Qed. Lemma high_correct a : high (partition w (sz*2) a) = partition w sz (a / w sz). - Proof. cbv [high]. rewrite UniformWeight.uweight_skipn_partition by lia. f_equal; lia. Qed. + Proof. cbv [high]. rewrite uweight_skipn_partition by lia. f_equal; lia. Qed. Lemma fill_correct n m a : (n <= m)%nat -> fill m (partition w n a) = partition w m (a mod w n). Proof. cbv [fill]; intros. distr_length. rewrite <-partition_0 with (weight:=w). - rewrite UniformWeight.uweight_partition_app by lia. + rewrite uweight_partition_app by lia. f_equal; lia. Qed. Hint Rewrite low_correct high_correct fill_correct using lia : pull_partition. @@ -335,7 +335,7 @@ Module Fancy. repeat match goal with | _ => progress autorewrite with pull_partition | _ => progress rewrite ?Ha, ?Ha0b1 - | _ => rewrite UniformWeight.uweight_partition_app by lia; + | _ => rewrite uweight_partition_app by lia; replace (sz+sz)%nat with (sz*2)%nat by lia | _ => rewrite Z.mod_pull_div by auto with zarith | _ => progress Z.rewrite_mod_small @@ -343,8 +343,8 @@ Module Fancy. end. Qed. - Hint Rewrite UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : weight_to_pow. - Hint Rewrite <-UniformWeight.uweight_S UniformWeight.uweight_eq_alt' using lia : pow_to_weight. + Hint Rewrite uweight_S uweight_eq_alt' using lia : weight_to_pow. + Hint Rewrite <-uweight_S uweight_eq_alt' using lia : pow_to_weight. Lemma q1_range x : 0 <= x < w (sz * 2) -> @@ -416,7 +416,7 @@ Module Fancy. intros; cbv [cond_sub Let_In Z.cc_l]. autorewrite with pull_partition. rewrite nth_default_partition by lia. rewrite weight_0 by auto. autorewrite with zsimplify_fast. - rewrite UniformWeight.uweight_eq_alt' with (n:=1%nat). autorewrite with push_Zof_nat zsimplify. + rewrite uweight_eq_alt' with (n:=1%nat). autorewrite with push_Zof_nat zsimplify. rewrite <-Znumtheory.Zmod_div_mod by auto using Zpow_facts.Zpower_divide with zarith. rewrite Positional.select_eq with (n:=sz) by (distr_length; apply w). rewrite Rows.sub_partitions by (break_innermost_match; distr_length; auto). @@ -452,7 +452,7 @@ Module Fancy. Lemma w_eq_22k : w (sz * 2) = 2 ^ (2 * k). Proof. replace (sz * 2)%nat with (sz + sz)%nat by lia. - rewrite UniformWeight.uweight_sum_indices, w_eq_2k, <-Z.pow_add_r by lia. + rewrite uweight_sum_indices, w_eq_2k, <-Z.pow_add_r by lia. f_equal; lia. Qed. @@ -549,7 +549,7 @@ Module Fancy. partition w 2 (xLow + 2^k * xHigh) = [xLow;xHigh]. Proof. replace k with width in M_range |- * by nia; intros. cbv [partition map seq]. - rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia. + rewrite !uweight_S, !weight_0 by auto with zarith lia. autorewrite with zsimplify. rewrite <-Z.mod_pull_div by Z.zero_bounds. autorewrite with zsimplify. reflexivity. @@ -568,7 +568,7 @@ Module Fancy. replace 2%nat with (sz*2)%nat by lia. rewrite fancy_reduce'_correct by nia. rewrite sz_eq_1; cbv [partition map seq hd]. - rewrite !UniformWeight.uweight_S, !weight_0 by auto with zarith lia. + rewrite !uweight_S, !weight_0 by auto with zarith lia. autorewrite with zsimplify. reflexivity. Qed. End Def. diff --git a/src/Arithmetic/BaseConversion.v b/src/Arithmetic/BaseConversion.v index c06dd3d71..dde04ae2a 100644 --- a/src/Arithmetic/BaseConversion.v +++ b/src/Arithmetic/BaseConversion.v @@ -215,14 +215,14 @@ Module BaseConversion. Lemma widemul_correct a b : length a = m -> length b = m -> - widemul a b = Partition.partition sw nout (seval m a * seval m b). + widemul a b = partition sw nout (seval m a * seval m b). Proof. apply mul_converted_partitions; auto with zarith. Qed. Derive widemul_inlined SuchThat (forall a b, length a = m -> length b = m -> - widemul_inlined a b = Partition.partition sw nout (seval m a * seval m b)) + widemul_inlined a b = partition sw nout (seval m a * seval m b)) As widemul_inlined_correct. Proof. intros. @@ -238,7 +238,7 @@ Module BaseConversion. SuchThat (forall a b, length a = m -> length b = m -> - widemul_inlined_reverse a b = Partition.partition sw nout (seval m a * seval m b)) + widemul_inlined_reverse a b = partition sw nout (seval m a * seval m b)) As widemul_inlined_reverse_correct. Proof. intros. diff --git a/src/Arithmetic/FancyMontgomeryReduction.v b/src/Arithmetic/FancyMontgomeryReduction.v index 258b2327e..51b578bed 100644 --- a/src/Arithmetic/FancyMontgomeryReduction.v +++ b/src/Arithmetic/FancyMontgomeryReduction.v @@ -91,7 +91,7 @@ Module MontgomeryReduction. autorewrite with widemul. rewrite Rows.add_partitions, Rows.add_div by (distr_length; apply wprops; omega). (* rewrite R_two_pow. *) - cbv [Partition.partition seq]. + cbv [partition seq]. repeat match goal with | _ => progress rewrite ?eval1, ?eval2 | _ => progress rewrite ?Z.zselect_correct, ?Z.add_modulo_correct diff --git a/src/Arithmetic/Freeze.v b/src/Arithmetic/Freeze.v index d59812dea..e766e7aea 100644 --- a/src/Arithmetic/Freeze.v +++ b/src/Arithmetic/Freeze.v @@ -3,6 +3,7 @@ Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. Require Import Crypto.Arithmetic.BaseConversion. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. Require Import Crypto.Arithmetic.Saturated. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.ListUtil. @@ -77,7 +78,7 @@ Module Freeze. | rewrite Rows.conditional_add_partitions | rewrite Rows.sub_partitions | rewrite Rows.sub_div - | rewrite Partition.eval_partition + | rewrite eval_partition | progress distr_length | progress pull_Zmod (* | progress break_innermost_match_step @@ -115,7 +116,7 @@ Module Freeze. (Hp : 0 <= Positional.eval weight n p < 2*modulus) (Hplen : length p = n) (Hmlen : length m = n) - : @freeze n mask m p = Partition.partition weight n (Positional.eval weight n p mod modulus). + : @freeze n mask m p = partition weight n (Positional.eval weight n p mod modulus). Proof using wprops. pose proof (@weight_positive weight wprops n). pose proof (fun v => Z.mod_pos_bound v (weight n) ltac:(lia)). @@ -124,7 +125,7 @@ Module Freeze. erewrite <- eval_freeze by eassumption. cbv [freeze]; eta_expand. rewrite Rows.conditional_add_partitions by (auto; rewrite Rows.sub_partitions; auto; distr_length). - rewrite !Partition.eval_partition by assumption. + rewrite !eval_partition by assumption. apply Partition.partition_Proper; [ assumption .. | ]. cbv [Z.equiv_modulo]. pull_Zmod; reflexivity. @@ -251,7 +252,7 @@ Section freeze_mod_ops. : forall (f : list Z) (Hf : length f = n) (Hf_small : 0 <= eval weight n f < weight n), - to_bytes f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f). + to_bytes f = partition bytes_weight bytes_n (Positional.eval weight n f). Proof using Hn_nz limbwidth_good. clear -Hn_nz limbwidth_good. intros; cbv [to_bytes]. @@ -264,7 +265,7 @@ Section freeze_mod_ops. (Hf : length f = n) (Hf_small : 0 <= eval weight n f < weight n), eval bytes_weight bytes_n (to_bytesmod f) = eval weight n f - /\ to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f). + /\ to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f). Proof using Hn_nz limbwidth_good. split; apply eval_to_bytes || apply to_bytes_partitions; assumption. Qed. @@ -274,7 +275,7 @@ Section freeze_mod_ops. (Hf : length f = n) (Hf_bounded : 0 <= eval weight n f < 2 * m), (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m - /\ freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m). + /\ freeze_to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f mod m). Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. clear -m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. intros; subst m s. @@ -298,7 +299,7 @@ Section freeze_mod_ops. : forall (f : list Z) (Hf : length f = n) (Hf_bounded : 0 <= eval weight n f < 2 * m), - freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m). + freeze_to_bytesmod f = partition bytes_weight bytes_n (Positional.eval weight n f mod m). Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. intros; now apply eval_freeze_to_bytesmod_and_partitions. Qed. @@ -319,7 +320,7 @@ Section freeze_mod_ops. Lemma from_bytes_partitions : forall (f : list Z) (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), - from_bytes f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + from_bytes f = partition weight n (Positional.eval bytes_weight bytes_n f). Proof using limbwidth_good. clear -limbwidth_good. intros; cbv [from_bytes]. @@ -336,7 +337,7 @@ Section freeze_mod_ops. Lemma from_bytesmod_partitions : forall (f : list Z) (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), - from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + from_bytesmod f = partition weight n (Positional.eval bytes_weight bytes_n f). Proof using limbwidth_good. apply from_bytes_partitions. Qed. Lemma eval_from_bytesmod_and_partitions @@ -344,7 +345,7 @@ Section freeze_mod_ops. (Hf : length f = bytes_n) (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f - /\ from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + /\ from_bytesmod f = partition weight n (Positional.eval bytes_weight bytes_n f). Proof using limbwidth_good Hn_nz. now (split; [ apply eval_from_bytesmod | apply from_bytes_partitions ]). Qed. diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v index 2477d212e..3fb3437c1 100644 --- a/src/Arithmetic/WordByWordMontgomery.v +++ b/src/Arithmetic/WordByWordMontgomery.v @@ -34,7 +34,7 @@ Module WordByWordMontgomery. Section with_args. Context (lgr : Z) (m : Z). - Local Notation weight := (UniformWeight.uweight lgr). + Local Notation weight := (uweight lgr). Let T (n : nat) := list Z. Let r := (2^lgr). Definition eval {n} : T n -> Z := Positional.eval weight n. @@ -138,7 +138,7 @@ Module WordByWordMontgomery. Local Lemma r_big : r > 1. Proof using lgr_big. clear -lgr_big; subst r. auto with zarith. Qed. - Local Notation wprops := (@UniformWeight.uwprops lgr lgr_big). + Local Notation wprops := (@uwprops lgr lgr_big). Local Hint Immediate (wprops). Local Hint Immediate (weight_0 wprops). @@ -155,8 +155,8 @@ Module WordByWordMontgomery. Lemma R_plusR_le : R + R <= weight (S R_numlimbs). Proof using lgr_big. clear - lgr_big. - etransitivity; [ | apply UniformWeight.uweight_double_le; omega ]. - rewrite UniformWeight.uweight_eq_alt by omega. + etransitivity; [ | apply uweight_double_le; omega ]. + rewrite uweight_eq_alt by omega. subst r R; omega. Qed. @@ -165,7 +165,7 @@ Module WordByWordMontgomery. Proof using lgr_big. clear - lgr_big. cbv [partition]. rewrite map_map. apply map_ext; intros. - rewrite UniformWeight.uweight_S by omega. + rewrite uweight_S by omega. rewrite <-Z.mod_pull_div by auto with zarith. replace (r - 1) with (Z.ones lgr) by (rewrite Z.ones_equiv; subst r; reflexivity). rewrite <-Z.land_comm, Z.land_ones by omega. @@ -226,7 +226,7 @@ Module WordByWordMontgomery. | [ H : small ?v |- context[length ?v] ] => erewrite length_small by eassumption end | rewrite Positional.eval_cons by distr_length - | progress rewrite ?weight_0, ?UniformWeight.uweight_1 by auto; + | progress rewrite ?weight_0, ?uweight_1 by auto; autorewrite with zsimplify_fast | rewrite (weight_0 wprops) | rewrite <- Z.div_mod'' by auto with omega @@ -257,7 +257,7 @@ Module WordByWordMontgomery. | _ => progress cbn [recursive_partition] | H : small _ |- _ => rewrite H; clear H | _ => rewrite recursive_partition_equiv by auto using wprops - | _ => rewrite UniformWeight.uweight_eval_shift by distr_length + | _ => rewrite uweight_eval_shift by distr_length | _ => progress push end. @@ -280,7 +280,7 @@ Module WordByWordMontgomery. 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. + rewrite <-uweight_recursive_partition_equiv with (i:=1%nat) by omega. push. apply Partition.partition_Proper; [ solve [auto] | ]. cbv [Z.equiv_modulo]. autorewrite with zsimplify. @@ -319,7 +319,7 @@ Module WordByWordMontgomery. rewrite weight_0 by auto. autorewrite with push_eval zsimplify_fast. split; [reflexivity | ]. - rewrite UniformWeight.uweight_S, UniformWeight.uweight_eq_alt by omega. + rewrite uweight_S, uweight_eq_alt by omega. subst r; nia. } Qed. @@ -331,7 +331,7 @@ Module WordByWordMontgomery. clear -lgr_big Ha Hb. autounfold with loc; destruct (zerop n); subst. { destruct a, b; cbn; try omega; split; auto with zarith. } - { pose proof (UniformWeight.uweight_double_le lgr ltac:(omega) n). + { pose proof (uweight_double_le lgr ltac:(omega) n). eta_expand; split; [ | lia ]. rewrite Rows.add_partitions, Rows.add_div by auto. rewrite partition_step. @@ -345,7 +345,7 @@ Module WordByWordMontgomery. autounfold with loc in *; subst; intros. rewrite Rows.add_partitions by auto using Positional.length_extend_to_length. autorewrite with push_eval. - split; try apply partition_eq_mod; auto; rewrite UniformWeight.uweight_eq_alt by omega; subst r; Z.rewrite_mod_small; auto with zarith. + split; try apply partition_eq_mod; auto; rewrite uweight_eq_alt by omega; subst r; Z.rewrite_mod_small; auto with zarith. Qed. Local Lemma conditional_sub_correct : forall v, small v -> 0 <= eval v < eval N + R -> canon_rep (eval v + if eval N <=? eval v then -eval N else 0) (conditional_sub v N). @@ -356,12 +356,12 @@ Module WordByWordMontgomery. repeat match goal with H : small _ |- _ => rewrite H; clear H end. autorewrite with push_eval. - assert (weight R_numlimbs < weight (S R_numlimbs)) by (rewrite !UniformWeight.uweight_eq_alt by omega; autorewrite with push_Zof_nat; auto with zarith). + assert (weight R_numlimbs < weight (S R_numlimbs)) by (rewrite !uweight_eq_alt by omega; autorewrite with push_Zof_nat; auto with zarith). assert (eval N mod weight R_numlimbs < weight (S R_numlimbs)) by (pose proof (Z.mod_pos_bound (eval N) (weight R_numlimbs) ltac:(auto)); omega). rewrite Rows.conditional_sub_partitions by (repeat (autorewrite with distr_length push_eval; auto using partition_eq_mod with zarith)). rewrite drop_high_to_length_partition by omega. autorewrite with push_eval. - assert (weight R_numlimbs = R) by (rewrite UniformWeight.uweight_eq_alt by omega; subst R; reflexivity). + assert (weight R_numlimbs = R) by (rewrite uweight_eq_alt by omega; subst R; reflexivity). Z.rewrite_mod_small. break_match; autorewrite with zsimplify_fast; Z.ltb_to_lt. { split; [ reflexivity | ]. @@ -379,7 +379,7 @@ Module WordByWordMontgomery. rewrite H; clear H end. rewrite Rows.sub_then_maybe_add_partitions by (autorewrite with push_eval distr_length; auto with zarith). autorewrite with push_eval. - assert (weight R_numlimbs = R) by (rewrite UniformWeight.uweight_eq_alt by omega; subst r R; reflexivity). + assert (weight R_numlimbs = R) by (rewrite uweight_eq_alt by omega; subst r R; reflexivity). Z.rewrite_mod_small. split; [ reflexivity | ]. break_match; Z.ltb_to_lt; lia. @@ -972,7 +972,7 @@ Module WordByWordMontgomery. (n : nat) (m : Z). Let r := 2^bitwidth. - Local Notation weight := (UniformWeight.uweight bitwidth). + Local Notation weight := (uweight bitwidth). Local Notation eval := (@eval bitwidth n). Let m_enc := partition weight n m. Local Coercion Z.of_nat : nat >-> Z. @@ -985,7 +985,7 @@ Module WordByWordMontgomery. (n_nz : n <> 0%nat) (m_small : m < r^n). - Local Notation wprops := (@UniformWeight.uwprops bitwidth bitwidth_big). + Local Notation wprops := (@uwprops bitwidth bitwidth_big). Local Notation small := (@small bitwidth n). Local Hint Immediate (wprops). @@ -998,7 +998,7 @@ Module WordByWordMontgomery. Proof using m_small m_big bitwidth_big. clear -m_small m_big bitwidth_big. cbv [eval m_enc]; autorewrite with push_eval; auto. - rewrite UniformWeight.uweight_eq_alt by omega. + rewrite uweight_eq_alt by omega. Z.rewrite_mod_small; reflexivity. Qed. Local Lemma r'_pow_correct : (r'^n * r^n) mod (eval m_enc) = 1. @@ -1012,7 +1012,7 @@ Module WordByWordMontgomery. Proof using m_small m_big bitwidth_big. clear -m_small m_big bitwidth_big. cbv [m_enc small eval]; autorewrite with push_eval; auto. - rewrite UniformWeight.uweight_eq_alt by omega. + rewrite uweight_eq_alt by omega. Z.rewrite_mod_small; reflexivity. Qed. @@ -1029,7 +1029,7 @@ Module WordByWordMontgomery. | _ => exact small_m_enc | [ H : small ?x |- context[eval ?x] ] => rewrite H; cbv [eval]; rewrite eval_partition by auto - | [ |- context[weight _] ] => rewrite UniformWeight.uweight_eq_alt by auto with omega + | [ |- context[weight _] ] => rewrite uweight_eq_alt by auto with omega | _=> progress Z.rewrite_mod_small | _ => progress Z.zero_bounds | [ |- _ mod ?x < ?x ] => apply Z.mod_pos_bound @@ -1142,7 +1142,7 @@ Module WordByWordMontgomery. Local Ltac t_valid v := cbv [valid]; repeat apply conj; auto; cbv [small eval]; autorewrite with push_eval; auto; - rewrite ?UniformWeight.uweight_eq_alt by omega; + rewrite ?uweight_eq_alt by omega; Z.rewrite_mod_small; rewrite ?(Z.mod_small (_ mod m)) by (subst r; Z.div_mod_to_quot_rem; lia); rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia); @@ -1155,7 +1155,7 @@ Module WordByWordMontgomery. [ | now t_valid v.. ]. push_Zmod; rewrite !eval_from_montgomerymod; [ | now t_valid v.. ]. cbv [eval]; autorewrite with push_eval; auto. - rewrite ?UniformWeight.uweight_eq_alt by omega. + rewrite ?uweight_eq_alt by omega. rewrite ?(Z.mod_small v) by (subst r; Z.div_mod_to_quot_rem; lia). rewrite ?(Z.mod_small (_ mod m)) by (subst r; Z.div_mod_to_quot_rem; lia). pull_Zmod. @@ -1258,16 +1258,16 @@ Module WordByWordMontgomery. Qed. Lemma to_bytesmod_correct - : (forall a (_ : valid a), Positional.eval (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a) + : (forall a (_ : valid a), Positional.eval (uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a) = eval a mod m) - /\ (forall a (_ : valid a), to_bytesmod a = partition (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (eval a mod m)). + /\ (forall a (_ : valid a), to_bytesmod a = partition (uweight 8) (bytes_n bitwidth 1 n) (eval a mod m)). Proof using n_nz m_small bitwidth_big. clear -n_nz m_small bitwidth_big. generalize (@length_small bitwidth n); cbv [valid small to_bytesmod eval]; split; intros; (etransitivity; [ apply eval_to_bytesmod | ]); - fold weight in *; fold (UniformWeight.uweight 8) in *; subst r; + fold weight in *; fold (uweight 8) in *; subst r; try solve [ intuition eauto with omega ]. - all: repeat first [ rewrite UniformWeight.uweight_eq_alt by omega + all: repeat first [ rewrite uweight_eq_alt by omega | omega | reflexivity | progress Z.rewrite_mod_small ]. @@ -1275,7 +1275,7 @@ Module WordByWordMontgomery. Lemma eval_to_bytesmod : (forall a (_ : valid a), - Positional.eval (UniformWeight.uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a) + Positional.eval (uweight 8) (bytes_n bitwidth 1 n) (to_bytesmod a) = eval a mod m). Proof. apply to_bytesmod_correct. Qed. End modops. diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 19014ffec..3946a39c2 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -30,7 +30,7 @@ Import Compilers.defaults. Import COperationSpecifications.Primitives. Import COperationSpecifications.BarrettReduction. -Import Associational Positional Arithmetic.BarrettReduction. +Import Associational Positional. Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) @@ -71,12 +71,12 @@ Section rbarrett_red. Lemma mut_correct : 0 < machine_wordsize -> - Partition.partition (UniformWeight.uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1]. + partition (uweight machine_wordsize) (1 + 1) (muLow + 2 ^ machine_wordsize) = [muLow; 1]. Proof. intros; cbn. subst muLow. assert (0 < 2^machine_wordsize) by ZeroBounds.Z.zero_bounds. pose proof (Z.mod_pos_bound mu (2^machine_wordsize) ltac:(lia)). - rewrite !UniformWeight.uweight_S, weight_0; auto using UniformWeight.uwprops with lia. + rewrite !uweight_S, weight_0; auto using uwprops with lia. autorewrite with zsimplify. Modulo.push_Zmod. autorewrite with zsimplify. Modulo.pull_Zmod. rewrite <-Modulo.Z.mod_pull_div by lia. @@ -86,10 +86,10 @@ Section rbarrett_red. Lemma Mt_correct : 0 < machine_wordsize -> 2^(machine_wordsize - 1) < M < 2^machine_wordsize -> - Partition.partition (UniformWeight.uweight machine_wordsize) 1 M = [M]. + partition (uweight machine_wordsize) 1 M = [M]. Proof. intros; cbn. assert (0 < 2^(machine_wordsize-1)) by ZeroBounds.Z.zero_bounds. - rewrite !UniformWeight.uweight_S, weight_0; auto using UniformWeight.uwprops with lia. + rewrite !uweight_S, weight_0; auto using uwprops with lia. autorewrite with zsimplify. RewriteModSmall.Z.rewrite_mod_small. reflexivity. Qed. @@ -177,7 +177,7 @@ Section rbarrett_red. | progress cbv [weight] | rewrite mut_correct | rewrite Mt_correct - | rewrite UniformWeight.uweight_eq_alt' + | rewrite uweight_eq_alt' | rewrite Z.pow_mul_r by lia ]. Local Strategy -100 [barrett_red]. (* needed for making Qed not take forever *) diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index aae25a578..5743d2c6a 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -99,7 +99,7 @@ Section __. end. Let n_bytes := bytes_n machine_wordsize 1 n. Let prime_upperbound_list : list Z - := Partition.partition (UniformWeight.uweight machine_wordsize) n (s-1). + := Partition.partition (uweight machine_wordsize) n (s-1). Let prime_bytes_upperbound_list : list Z := Partition.partition (weight 8 1) n_bytes (s-1). Let upperbounds : list Z := prime_upperbound_list. @@ -140,8 +140,8 @@ Section __. (negb ((r * r') mod m =? 1)%Z, Pipeline.Values_not_provably_equalZ "(r * r') mod m ≠ 1" ((r * r') mod m) 1); (negb ((m * m') mod r =? (-1) mod r)%Z, Pipeline.Values_not_provably_equalZ "(m * m') mod r ≠ (-1) mod r" ((m * m') mod r) ((-1) mod r)); (negb (s <=? r^n), Pipeline.Value_not_leZ "r^n ≤ s" s (r^n)); - (negb (s <=? UniformWeight.uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (UniformWeight.uweight machine_wordsize n)); - (negb (UniformWeight.uweight machine_wordsize n =? UniformWeight.uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (UniformWeight.uweight machine_wordsize n) (UniformWeight.uweight 8 n_bytes))]. + (negb (s <=? uweight machine_wordsize n), Pipeline.Value_not_leZ "weight n < s (needed for from_bytes)" s (uweight machine_wordsize n)); + (negb (uweight machine_wordsize n =? uweight 8 n_bytes), Pipeline.Values_not_provably_equalZ "weight n ≠ bytes_weight n_bytes (needed for from_bytes)" (uweight machine_wordsize n) (uweight 8 n_bytes))]. Local Arguments Z.mul !_ !_. Local Ltac use_curve_good_t := @@ -179,9 +179,9 @@ Section __. /\ 1 < m /\ m < r^n /\ s = 2^Z.log2 s - /\ s <= UniformWeight.uweight machine_wordsize n - /\ s <= UniformWeight.uweight 8 n_bytes - /\ UniformWeight.uweight machine_wordsize n = UniformWeight.uweight 8 n_bytes. + /\ s <= uweight machine_wordsize n + /\ s <= uweight 8 n_bytes + /\ uweight machine_wordsize n = uweight 8 n_bytes. Proof. clear -curve_good. cbv [check_args fold_right] in curve_good. @@ -520,10 +520,10 @@ Section __. { cbv [Partition.partition seq map In]; tauto. } { intros *; rewrite Partition.partition_step, in_app_iff; cbn [List.In]. intros; destruct_head'_or; subst *; eauto; try tauto; []. - rewrite UniformWeight.uweight_S by lia. - assert (0 < UniformWeight.uweight machine_wordsize n') by now apply UniformWeight.uwprops. + rewrite uweight_S by lia. + assert (0 < uweight machine_wordsize n') by now apply uwprops. assert (0 < 2 ^ machine_wordsize) by auto with zarith. - assert (0 < 2 ^ machine_wordsize * UniformWeight.uweight machine_wordsize n') by nia. + assert (0 < 2 ^ machine_wordsize * uweight machine_wordsize n') by nia. rewrite <- Z.mod_pull_div by lia. rewrite Z.le_sub_1_iff. auto with zarith. } @@ -533,9 +533,9 @@ Section __. Lemma bounded_by_prime_bounds_of_valid_gen lgr n' x (Hlgr : 0 < lgr) (Hs : s = 2^Z.log2 s) - (Hs' : s <= UniformWeight.uweight lgr n') + (Hs' : s <= uweight lgr n') (H : WordByWordMontgomery.valid lgr n' m x) - : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (UniformWeight.uweight lgr) n' (s-1)))) x = true. + : ZRange.type.base.option.is_bounded_by (t:=base.type.list base.type.Z) (Some (List.map (fun v => Some r[0~>v]%zrange) (Partition.partition (uweight lgr) n' (s-1)))) x = true. Proof using curve_good. pose proof use_curve_good as use_curve_good. clear -H use_curve_good curve_good Hlgr Hs Hs'. @@ -567,13 +567,13 @@ Section __. assert (1 < 2^Z.log2 s) by auto with zarith. generalize dependent (Z.log2 s); intro lgs; intros. - edestruct (UniformWeight.uwprops lgr); try lia. - assert (forall i : nat, 0 <= UniformWeight.uweight lgr i) by (intro z; specialize (weight_positive z); lia). + edestruct (uwprops lgr); try lia. + assert (forall i : nat, 0 <= uweight lgr i) by (intro z; specialize (weight_positive z); lia). apply Bool.andb_true_intro; split; apply OrdersEx.Z_as_OT.leb_le; [apply Z.div_nonneg | apply Z.div_le_mono_nonneg]; trivial. apply Z.mod_pos_bound; trivial. - cbv [UniformWeight.uweight]. + cbv [uweight]. cbv [weight]. rewrite Z.div_1_r. rewrite Z.opp_involutive. @@ -632,12 +632,12 @@ Section __. cbv [bytes_valid] in H. destruct H as [_ H]. pose proof use_curve_good. - cbv [UniformWeight.uweight] in *; destruct_head'_and; lia. + cbv [uweight] in *; destruct_head'_and; lia. Qed. Local Ltac solve_extra_bounds_side_conditions := solve [ cbn [lower upper fst snd] in *; Bool.split_andb; Z.ltb_to_lt; lia - | cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto + | cbv [valid small eval uweight n_bytes] in *; destruct_head'_and; auto | now apply weight_bounded_of_bytes_valid | eapply length_of_valid; eassumption ]. @@ -702,7 +702,7 @@ Section __. | progress autorewrite with interp interp_gen_cache push_eval | progress autounfold with push_eval | progress autorewrite with distr_length in * - | solve [ cbv [valid small eval UniformWeight.uweight n_bytes] in *; destruct_head'_and; auto ] ]. + | solve [ cbv [valid small eval uweight n_bytes] in *; destruct_head'_and; auto ] ]. (** TODO: DESIGN DECISION: -- cgit v1.2.3