diff options
Diffstat (limited to 'src/LegacyArithmetic')
21 files changed, 58 insertions, 26 deletions
diff --git a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v index 8d4b59ceb..5ff67d7ec 100644 --- a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v +++ b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v @@ -8,7 +8,8 @@ Require Import Crypto.LegacyArithmetic.Double.Proofs.Multiply. Require Import Crypto.LegacyArithmetic.ArchitectureToZLike. Require Import Crypto.LegacyArithmetic.ZBounded. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/BarretReduction.v b/src/LegacyArithmetic/BarretReduction.v index e278dc082..37c4d4915 100644 --- a/src/LegacyArithmetic/BarretReduction.v +++ b/src/LegacyArithmetic/BarretReduction.v @@ -4,7 +4,6 @@ Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. Require Import Crypto.Arithmetic.BarrettReduction.HAC. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Notations. Local Open Scope small_zlike_scope. diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v index 3f426e98b..359b4313b 100644 --- a/src/LegacyArithmetic/BaseSystem.v +++ b/src/LegacyArithmetic/BaseSystem.v @@ -1,7 +1,7 @@ Require Import Coq.Lists.List. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. Require Export Crypto.Util.FixCoqMistakes. Import Nat. diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v index f0f0a80d2..042fdb270 100644 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ b/src/LegacyArithmetic/BaseSystemProofs.v @@ -1,5 +1,5 @@ Require Import Coq.Lists.List Coq.micromega.Psatz. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.ListUtil. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.LegacyArithmetic.BaseSystem. diff --git a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v index 0f07c6299..8588836ee 100644 --- a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v +++ b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v @@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v index 1cd5bf06d..c0748cf8e 100644 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ b/src/LegacyArithmetic/Double/Proofs/Decode.v @@ -3,7 +3,7 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v index 2c7f87dd7..13847b50a 100644 --- a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v @@ -3,7 +3,7 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Local Open Scope Z_scope. Local Opaque tuple_decoder. diff --git a/src/LegacyArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v index 98692ed7f..ebe19cc46 100644 --- a/src/LegacyArithmetic/Double/Proofs/Multiply.v +++ b/src/LegacyArithmetic/Double/Proofs/Multiply.v @@ -5,7 +5,10 @@ Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.SpreadLeftImmediate. Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.Tactics.SimplifyProjections. Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v index 4f6a79e8d..b2d53a33a 100644 --- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -4,7 +4,10 @@ Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SimplifyProjections. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v index 2230e36b6..1944f99b2 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v @@ -3,8 +3,8 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Definitions. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v index 41234bf6e..98cf3cf9c 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v @@ -1,8 +1,17 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.Ztestbit. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated. +Require Export Crypto.Util.ZUtil.ZSimplify.Core. +Require Export Crypto.Util.ZUtil.ZSimplify.Simple. +Require Export Crypto.Util.ZUtil.LandLorShiftBounds. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v index 16e7c5d6a..245e03480 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v @@ -3,8 +3,6 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v index 00a6d03cd..7210d80d5 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v @@ -3,8 +3,8 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Definitions. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v index c50d43616..0cbc237d2 100644 --- a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v @@ -3,7 +3,11 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/Interface.v b/src/LegacyArithmetic/Interface.v index 4a671eb4c..9a652bbd4 100644 --- a/src/LegacyArithmetic/Interface.v +++ b/src/LegacyArithmetic/Interface.v @@ -1,6 +1,7 @@ (*** Interface for bounded arithmetic *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. + Require Import Crypto.Util.Tuple. Require Import Crypto.Util.AutoRewrite. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v index 33917e00d..a2c8d9de5 100644 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ b/src/LegacyArithmetic/InterfaceProofs.v @@ -1,7 +1,13 @@ (** * Alternate forms for Interface for bounded arithmetic *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.AutoRewrite. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/MontgomeryReduction.v b/src/LegacyArithmetic/MontgomeryReduction.v index c3538dd01..786e08d28 100644 --- a/src/LegacyArithmetic/MontgomeryReduction.v +++ b/src/LegacyArithmetic/MontgomeryReduction.v @@ -5,7 +5,7 @@ Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.microm Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Tactics.Test. Require Import Crypto.Util.Tactics.Not. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v index 62f1f742d..c5c69e684 100644 --- a/src/LegacyArithmetic/Pow2Base.v +++ b/src/LegacyArithmetic/Pow2Base.v @@ -1,6 +1,5 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.ZUtil. Require Import Coq.Lists.List. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index b6df85f5c..495636be7 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -2,7 +2,13 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Lists.List. Require Import Coq.funind.Recdef. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. +Require Import Crypto.Util.ListUtil Crypto.Util.NatUtil. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Shift. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.LegacyArithmetic.VerdiTactics. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.BreakMatch. @@ -282,7 +288,7 @@ Section Pow2BaseProofs. | |- _ => rewrite BaseSystemProofs.set_higher | |- _ => rewrite nth_default_base | |- _ => rewrite IHi - | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds) + | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; Z.zero_bounds) | |- context[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) | |- context[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 | |- _ => solve [auto] @@ -452,7 +458,7 @@ Section UniformBase. intros; apply Z.eq_le_incl. f_equal; auto. + apply nth_default_preserves_properties_length_dep; - try solve [apply nth_default_preserves_properties; split; zero_bounds; rewrite limb_widths_uniform; auto || omega]. + try solve [apply nth_default_preserves_properties; split; Z.zero_bounds; rewrite limb_widths_uniform; auto || omega]. intros; apply nth_default_preserves_properties_length_dep; try solve [intros; omega]. let x := fresh "x" in intro x; intros; replace x with width; try symmetry; auto. diff --git a/src/LegacyArithmetic/ZBounded.v b/src/LegacyArithmetic/ZBounded.v index bccbf7428..2eec4122b 100644 --- a/src/LegacyArithmetic/ZBounded.v +++ b/src/LegacyArithmetic/ZBounded.v @@ -2,7 +2,7 @@ (** This file specifies a ℤ-like type of bounded integers, with operations for Montgomery Reduction and Barrett Reduction. *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v index fef654f47..2943598c1 100644 --- a/src/LegacyArithmetic/ZBoundedZ.v +++ b/src/LegacyArithmetic/ZBoundedZ.v @@ -1,7 +1,9 @@ (*** ℤ can be a bounded ℤ-Like type *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. |