diff options
Diffstat (limited to 'src/PushButtonSynthesis')
12 files changed, 17 insertions, 17 deletions
diff --git a/src/PushButtonSynthesis/BarrettReduction.v b/src/PushButtonSynthesis/BarrettReduction.v index 504a26a0c..19014ffec 100644 --- a/src/PushButtonSynthesis/BarrettReduction.v +++ b/src/PushButtonSynthesis/BarrettReduction.v @@ -10,7 +10,7 @@ Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Language. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.BarrettReduction. Require Import Crypto.BoundsPipeline. Require Import Crypto.Fancy.Compiler. Require Import Crypto.COperationSpecifications. diff --git a/src/PushButtonSynthesis/BarrettReductionReificationCache.v b/src/PushButtonSynthesis/BarrettReductionReificationCache.v index 265ada2d2..a36a4d5ee 100644 --- a/src/PushButtonSynthesis/BarrettReductionReificationCache.v +++ b/src/PushButtonSynthesis/BarrettReductionReificationCache.v @@ -3,11 +3,11 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.BarrettReduction. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. -Import Associational Positional Arithmetic.BarrettReduction. +Import BarrettReduction. Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v index 73204eb53..f61ece27c 100644 --- a/src/PushButtonSynthesis/MontgomeryReduction.v +++ b/src/PushButtonSynthesis/MontgomeryReduction.v @@ -14,7 +14,8 @@ Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. Require Import Crypto.Language. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.FancyMongomeryReduction. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.Fancy.Compiler. @@ -35,7 +36,7 @@ Import COperationSpecifications.Primitives. Import COperationSpecifications.MontgomeryReduction. -Import Associational Positional Arithmetic.MontgomeryReduction. +Import Associational Positional MontgomeryReduction. Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) @@ -184,4 +185,4 @@ Section rmontred. { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower]. rewrite Bool.andb_true_iff, !Z.leb_le. lia. } Qed. -End rmontred.
\ No newline at end of file +End rmontred. diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v index f787063a4..80af335df 100644 --- a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v +++ b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v @@ -1,7 +1,7 @@ (** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.FancyMontgomeryReduction. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. diff --git a/src/PushButtonSynthesis/Primitives.v b/src/PushButtonSynthesis/Primitives.v index 575e4057a..70448938e 100644 --- a/src/PushButtonSynthesis/Primitives.v +++ b/src/PushButtonSynthesis/Primitives.v @@ -20,7 +20,7 @@ Require Import Crypto.Util.Tactics.ConstrFail. Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Primitives. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/SaturatedSolinas.v b/src/PushButtonSynthesis/SaturatedSolinas.v index 0e7aaf6b2..162b6a3c0 100644 --- a/src/PushButtonSynthesis/SaturatedSolinas.v +++ b/src/PushButtonSynthesis/SaturatedSolinas.v @@ -22,7 +22,7 @@ Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v index ccc48e2cd..0f811e3cf 100644 --- a/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v +++ b/src/PushButtonSynthesis/SaturatedSolinasReificationCache.v @@ -1,12 +1,10 @@ (** * Push-Button Synthesis of Saturated Solinas: Reification Cache *) Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Saturated. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. -Import Associational Positional. - Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *) Module Export SaturatedSolinas. diff --git a/src/PushButtonSynthesis/SmallExamples.v b/src/PushButtonSynthesis/SmallExamples.v index daa50c9e9..f5d7d1f29 100644 --- a/src/PushButtonSynthesis/SmallExamples.v +++ b/src/PushButtonSynthesis/SmallExamples.v @@ -5,7 +5,7 @@ Require Import Coq.Lists.List. Require Import Crypto.Util.ZRange. Require Import Crypto.Language. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. Require Import Crypto.BoundsPipeline. Import ListNotations. Local Open Scope Z_scope. Local Open Scope list_scope. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinas.v b/src/PushButtonSynthesis/UnsaturatedSolinas.v index 0ac4c6cf4..509f5cdad 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinas.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinas.v @@ -24,7 +24,7 @@ Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v index 3cee63c4e..8379838f6 100644 --- a/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v +++ b/src/PushButtonSynthesis/UnsaturatedSolinasReificationCache.v @@ -1,7 +1,7 @@ (** * Push-Button Synthesis of Unsaturated Solinas: Reification Cache *) Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. diff --git a/src/PushButtonSynthesis/WordByWordMontgomery.v b/src/PushButtonSynthesis/WordByWordMontgomery.v index c92e0615a..aae25a578 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomery.v +++ b/src/PushButtonSynthesis/WordByWordMontgomery.v @@ -33,7 +33,8 @@ Require Import Crypto.LanguageWf. Require Import Crypto.Language. Require Import Crypto.AbstractInterpretation. Require Import Crypto.CStringification. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.WordByWordMontgomery. Require Import Crypto.BoundsPipeline. Require Import Crypto.COperationSpecifications. Require Import Crypto.PushButtonSynthesis.ReificationCache. diff --git a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v index ac429cdb5..c43633d2d 100644 --- a/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v +++ b/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v @@ -2,7 +2,7 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Arithmetic. +Require Import Crypto.Arithmetic.WordByWordMontgomery. Require Import Crypto.Language. Require Import Crypto.PushButtonSynthesis.ReificationCache. Local Open Scope Z_scope. |