diff options
Diffstat (limited to 'src/Arithmetic/WordByWordMontgomery.v')
| -rw-r--r-- | src/Arithmetic/WordByWordMontgomery.v | 81 |
1 files changed, 26 insertions, 55 deletions
diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v index f52dbdeb1..2477d212e 100644 --- a/src/Arithmetic/WordByWordMontgomery.v +++ b/src/Arithmetic/WordByWordMontgomery.v @@ -1,65 +1,36 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Crypto.Algebra.Ring. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.Freeze. Require Import Crypto.Arithmetic.ModularArithmeticTheorems. +Require Import Crypto.Arithmetic.Partition. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.UniformWeight. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.Tactics.SetEvars. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. + Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Import ListNotations. Local Open Scope Z_scope. Module WordByWordMontgomery. - Import Partition. - Local Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg. Section with_args. Context (lgr : Z) (m : Z). @@ -201,14 +172,14 @@ Module WordByWordMontgomery. auto with zarith. Qed. - Let partition_Proper := (@partition_Proper _ wprops). + Let partition_Proper := (@Partition.partition_Proper _ wprops). Local Existing Instance partition_Proper. Lemma eval_nonzero n A : @small n A -> nonzero A = 0 <-> @eval n A = 0. Proof using lgr_big. clear -lgr_big partition_Proper. cbv [nonzero eval small]; intro Heq. do 2 rewrite Heq. - rewrite !eval_partition, Z.mod_mod by auto. + rewrite !eval_partition, Z.mod_mod by auto with zarith. generalize (Positional.eval weight n A); clear Heq A. induction n as [|n IHn]. { cbn; rewrite weight_0 by auto; intros; autorewrite with zsimplify_const; omega. } @@ -229,7 +200,7 @@ Module WordByWordMontgomery. rewrite <- !Z.mul_add_distr_l, Z.mul_eq_0. nia. } rewrite Heq at 1; rewrite IHn. - rewrite Z.mod_mod by auto. + rewrite Z.mod_mod by auto with zarith. generalize (weight_multiples ltac:(auto) n). generalize (weight_positive ltac:(auto) n). generalize (weight_positive ltac:(auto) (S n)). |