diff options
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction')
5 files changed, 22 insertions, 5 deletions
diff --git a/src/Arithmetic/MontgomeryReduction/Definition.v b/src/Arithmetic/MontgomeryReduction/Definition.v index 04c097460..e5cdcc603 100644 --- a/src/Arithmetic/MontgomeryReduction/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/Definition.v @@ -2,7 +2,7 @@ (** This file implements Montgomery Form, Montgomery Reduction, and Montgomery Multiplication on [Z]. We follow Wikipedia. *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v index 5f459e52d..e6be440fb 100644 --- a/src/Arithmetic/MontgomeryReduction/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/Proofs.v @@ -4,7 +4,9 @@ Wikipedia. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Structures.Equalities. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SimplifyRepeatedIfs. Require Import Crypto.Util.Notations. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v index 266fc1f6f..3dd7fc0b3 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v @@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Algebra.Ring. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Tactics.SetEvars. Require Import Crypto.Util.Tactics.SubstEvars. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v index 9ca2cf4e9..9eabc5ce4 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v @@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Definition. Require Import Crypto.Algebra.Ring. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Tactics.SetEvars. Require Import Crypto.Util.Tactics.SubstEvars. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 6d2925d6b..35c9e377b 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -6,7 +6,6 @@ Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Proofs. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. |