rename-everything

207 files changed, 1161 insertions, 1143 deletions

diff --git a/_CoqProject b/_CoqProject
index 823fda21b..491ad25ca 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,180 +2,186 @@
 -R Bedrock Bedrock
 Bedrock/Nomega.v
 Bedrock/Word.v
-src/Algebra.v
-src/EdDSARepChange.v
-src/Karatsuba.v
-src/MontgomeryCurve.v
-src/MontgomeryCurveTheorems.v
-src/MontgomeryX.v
-src/MontgomeryXProofs.v
-src/MxDHRepChange.v
-src/NewBaseSystem.v
-src/SaturatedBaseSystem.v
 src/Algebra/Field.v
 src/Algebra/Field_test.v
 src/Algebra/Group.v
+src/Algebra/Hierarchy.v
 src/Algebra/IntegralDomain.v
 src/Algebra/Monoid.v
+src/Algebra/Nsatz.v
 src/Algebra/Ring.v
 src/Algebra/ScalarMult.v
-src/BoundedArithmetic/ArchitectureToZLike.v
-src/BoundedArithmetic/ArchitectureToZLikeProofs.v
-src/BoundedArithmetic/BaseSystem.v
-src/BoundedArithmetic/BaseSystemProofs.v
-src/BoundedArithmetic/Interface.v
-src/BoundedArithmetic/InterfaceProofs.v
-src/BoundedArithmetic/Pow2Base.v
-src/BoundedArithmetic/Pow2BaseProofs.v
-src/BoundedArithmetic/Double/Core.v
-src/BoundedArithmetic/Double/Proofs/BitwiseOr.v
-src/BoundedArithmetic/Double/Proofs/Decode.v
-src/BoundedArithmetic/Double/Proofs/LoadImmediate.v
-src/BoundedArithmetic/Double/Proofs/Multiply.v
-src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
-src/BoundedArithmetic/Double/Proofs/SelectConditional.v
-src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
-src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
-src/BoundedArithmetic/Double/Proofs/ShiftRight.v
-src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
-src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v
-src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
-src/CompleteEdwardsCurve/EdwardsMontgomery.v
-src/CompleteEdwardsCurve/ExtendedCoordinates.v
-src/CompleteEdwardsCurve/Pre.v
-src/ModularArithmetic/ModularArithmeticTheorems.v
-src/ModularArithmetic/Pre.v
-src/ModularArithmetic/PrimeFieldTheorems.v
-src/ModularArithmetic/ZBounded.v
-src/ModularArithmetic/ZBoundedZ.v
-src/ModularArithmetic/BarrettReduction/Z.v
-src/ModularArithmetic/BarrettReduction/ZBounded.v
-src/ModularArithmetic/BarrettReduction/ZGeneralized.v
-src/ModularArithmetic/BarrettReduction/ZHandbook.v
-src/ModularArithmetic/Montgomery/Z.v
-src/ModularArithmetic/Montgomery/ZBounded.v
-src/ModularArithmetic/Montgomery/ZProofs.v
-src/Reflection/BoundByCast.v
-src/Reflection/BoundByCastInterp.v
-src/Reflection/BoundByCastWf.v
-src/Reflection/CommonSubexpressionElimination.v
-src/Reflection/Conversion.v
-src/Reflection/CountLets.v
-src/Reflection/Equality.v
-src/Reflection/Eta.v
-src/Reflection/EtaInterp.v
-src/Reflection/EtaWf.v
-src/Reflection/ExprInversion.v
-src/Reflection/FilterLive.v
-src/Reflection/FoldTypes.v
-src/Reflection/Inline.v
-src/Reflection/InlineCast.v
-src/Reflection/InlineCastInterp.v
-src/Reflection/InlineCastWf.v
-src/Reflection/InlineInterp.v
-src/Reflection/InlineWf.v
-src/Reflection/InputSyntax.v
-src/Reflection/InterpByIso.v
-src/Reflection/InterpByIsoProofs.v
-src/Reflection/InterpProofs.v
-src/Reflection/InterpWf.v
-src/Reflection/InterpWfRel.v
-src/Reflection/Linearize.v
-src/Reflection/LinearizeInterp.v
-src/Reflection/LinearizeWf.v
-src/Reflection/Map.v
-src/Reflection/MapCast.v
-src/Reflection/MapCastByDeBruijn.v
-src/Reflection/MapCastByDeBruijnInterp.v
-src/Reflection/MapCastByDeBruijnWf.v
-src/Reflection/MapCastInterp.v
-src/Reflection/MapCastWf.v
-src/Reflection/MultiSizeTest.v
-src/Reflection/MultiSizeTest2.v
-src/Reflection/Reify.v
-src/Reflection/Relations.v
-src/Reflection/RenameBinders.v
-src/Reflection/Rewriter.v
-src/Reflection/RewriterInterp.v
-src/Reflection/RewriterWf.v
-src/Reflection/SmartBound.v
-src/Reflection/SmartBoundInterp.v
-src/Reflection/SmartBoundWf.v
-src/Reflection/SmartCast.v
-src/Reflection/SmartCastInterp.v
-src/Reflection/SmartCastWf.v
-src/Reflection/SmartMap.v
-src/Reflection/Syntax.v
-src/Reflection/TestCase.v
-src/Reflection/Tuple.v
-src/Reflection/TypeInversion.v
-src/Reflection/TypeUtil.v
-src/Reflection/Wf.v
-src/Reflection/WfInversion.v
-src/Reflection/WfProofs.v
-src/Reflection/WfReflective.v
-src/Reflection/WfReflectiveGen.v
-src/Reflection/Named/Compile.v
-src/Reflection/Named/CompileInterp.v
-src/Reflection/Named/CompileProperties.v
-src/Reflection/Named/CompileWf.v
-src/Reflection/Named/ContextDefinitions.v
-src/Reflection/Named/ContextOn.v
-src/Reflection/Named/ContextProperties.v
-src/Reflection/Named/DeadCodeElimination.v
-src/Reflection/Named/EstablishLiveness.v
-src/Reflection/Named/FMapContext.v
-src/Reflection/Named/IdContext.v
-src/Reflection/Named/InterpretToPHOAS.v
-src/Reflection/Named/InterpretToPHOASInterp.v
-src/Reflection/Named/InterpretToPHOASWf.v
-src/Reflection/Named/MapCast.v
-src/Reflection/Named/MapCastInterp.v
-src/Reflection/Named/MapCastWf.v
-src/Reflection/Named/NameUtil.v
-src/Reflection/Named/NameUtilProperties.v
-src/Reflection/Named/PositiveContext.v
-src/Reflection/Named/RegisterAssign.v
-src/Reflection/Named/SmartMap.v
-src/Reflection/Named/Syntax.v
-src/Reflection/Named/Wf.v
-src/Reflection/Named/WfInterp.v
-src/Reflection/Named/ContextProperties/NameUtil.v
-src/Reflection/Named/ContextProperties/SmartMap.v
-src/Reflection/Named/ContextProperties/Tactics.v
-src/Reflection/Named/PositiveContext/Defaults.v
-src/Reflection/Named/PositiveContext/DefaultsProperties.v
-src/Reflection/Z/ArithmeticSimplifier.v
-src/Reflection/Z/ArithmeticSimplifierInterp.v
-src/Reflection/Z/ArithmeticSimplifierUtil.v
-src/Reflection/Z/ArithmeticSimplifierWf.v
-src/Reflection/Z/BinaryNotationConstants.v
-src/Reflection/Z/CNotations.v
-src/Reflection/Z/FoldTypes.v
-src/Reflection/Z/HexNotationConstants.v
-src/Reflection/Z/Inline.v
-src/Reflection/Z/InlineInterp.v
-src/Reflection/Z/InlineWf.v
-src/Reflection/Z/JavaNotations.v
-src/Reflection/Z/MapCastByDeBruijn.v
-src/Reflection/Z/MapCastByDeBruijnInterp.v
-src/Reflection/Z/MapCastByDeBruijnWf.v
-src/Reflection/Z/OpInversion.v
-src/Reflection/Z/Reify.v
-src/Reflection/Z/Syntax.v
-src/Reflection/Z/Bounds/Interpretation.v
-src/Reflection/Z/Bounds/InterpretationLemmas.v
-src/Reflection/Z/Bounds/MapCastByDeBruijn.v
-src/Reflection/Z/Bounds/MapCastByDeBruijnInterp.v
-src/Reflection/Z/Bounds/MapCastByDeBruijnWf.v
-src/Reflection/Z/Bounds/Pipeline.v
-src/Reflection/Z/Bounds/Relax.v
-src/Reflection/Z/Bounds/Pipeline/Definition.v
-src/Reflection/Z/Bounds/Pipeline/Glue.v
-src/Reflection/Z/Bounds/Pipeline/OutputType.v
-src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
-src/Reflection/Z/Syntax/Equality.v
-src/Reflection/Z/Syntax/Util.v
+src/Arithmetic/Core.v
+src/Arithmetic/Karatsuba.v
+src/Arithmetic/ModularArithmeticPre.v
+src/Arithmetic/ModularArithmeticTheorems.v
+src/Arithmetic/PrimeFieldTheorems.v
+src/Arithmetic/Saturated.v
+src/Arithmetic/BarrettReduction/Generalized.v
+src/Arithmetic/BarrettReduction/HAC.v
+src/Arithmetic/BarrettReduction/Wikipedia.v
+src/Arithmetic/MontgomeryReduction/Definition.v
+src/Arithmetic/MontgomeryReduction/Proofs.v
+src/Compilers/BoundByCast.v
+src/Compilers/BoundByCastInterp.v
+src/Compilers/BoundByCastWf.v
+src/Compilers/CommonSubexpressionElimination.v
+src/Compilers/Conversion.v
+src/Compilers/CountLets.v
+src/Compilers/Equality.v
+src/Compilers/Eta.v
+src/Compilers/EtaInterp.v
+src/Compilers/EtaWf.v
+src/Compilers/ExprInversion.v
+src/Compilers/FilterLive.v
+src/Compilers/FoldTypes.v
+src/Compilers/Inline.v
+src/Compilers/InlineCast.v
+src/Compilers/InlineCastInterp.v
+src/Compilers/InlineCastWf.v
+src/Compilers/InlineInterp.v
+src/Compilers/InlineWf.v
+src/Compilers/InputSyntax.v
+src/Compilers/InterpByIso.v
+src/Compilers/InterpByIsoProofs.v
+src/Compilers/InterpProofs.v
+src/Compilers/InterpWf.v
+src/Compilers/InterpWfRel.v
+src/Compilers/Linearize.v
+src/Compilers/LinearizeInterp.v
+src/Compilers/LinearizeWf.v
+src/Compilers/Map.v
+src/Compilers/MapCast.v
+src/Compilers/MapCastByDeBruijn.v
+src/Compilers/MapCastByDeBruijnInterp.v
+src/Compilers/MapCastByDeBruijnWf.v
+src/Compilers/MapCastInterp.v
+src/Compilers/MapCastWf.v
+src/Compilers/MultiSizeTest.v
+src/Compilers/MultiSizeTest2.v
+src/Compilers/Reify.v
+src/Compilers/Relations.v
+src/Compilers/RenameBinders.v
+src/Compilers/Rewriter.v
+src/Compilers/RewriterInterp.v
+src/Compilers/RewriterWf.v
+src/Compilers/SmartBound.v
+src/Compilers/SmartBoundInterp.v
+src/Compilers/SmartBoundWf.v
+src/Compilers/SmartCast.v
+src/Compilers/SmartCastInterp.v
+src/Compilers/SmartCastWf.v
+src/Compilers/SmartMap.v
+src/Compilers/Syntax.v
+src/Compilers/TestCase.v
+src/Compilers/Tuple.v
+src/Compilers/TypeInversion.v
+src/Compilers/TypeUtil.v
+src/Compilers/Wf.v
+src/Compilers/WfInversion.v
+src/Compilers/WfProofs.v
+src/Compilers/WfReflective.v
+src/Compilers/WfReflectiveGen.v
+src/Compilers/Named/Compile.v
+src/Compilers/Named/CompileInterp.v
+src/Compilers/Named/CompileProperties.v
+src/Compilers/Named/CompileWf.v
+src/Compilers/Named/ContextDefinitions.v
+src/Compilers/Named/ContextOn.v
+src/Compilers/Named/ContextProperties.v
+src/Compilers/Named/DeadCodeElimination.v
+src/Compilers/Named/EstablishLiveness.v
+src/Compilers/Named/FMapContext.v
+src/Compilers/Named/IdContext.v
+src/Compilers/Named/InterpretToPHOAS.v
+src/Compilers/Named/InterpretToPHOASInterp.v
+src/Compilers/Named/InterpretToPHOASWf.v
+src/Compilers/Named/MapCast.v
+src/Compilers/Named/MapCastInterp.v
+src/Compilers/Named/MapCastWf.v
+src/Compilers/Named/NameUtil.v
+src/Compilers/Named/NameUtilProperties.v
+src/Compilers/Named/PositiveContext.v
+src/Compilers/Named/RegisterAssign.v
+src/Compilers/Named/SmartMap.v
+src/Compilers/Named/Syntax.v
+src/Compilers/Named/Wf.v
+src/Compilers/Named/WfInterp.v
+src/Compilers/Named/ContextProperties/NameUtil.v
+src/Compilers/Named/ContextProperties/SmartMap.v
+src/Compilers/Named/ContextProperties/Tactics.v
+src/Compilers/Named/PositiveContext/Defaults.v
+src/Compilers/Named/PositiveContext/DefaultsProperties.v
+src/Compilers/Z/ArithmeticSimplifier.v
+src/Compilers/Z/ArithmeticSimplifierInterp.v
+src/Compilers/Z/ArithmeticSimplifierUtil.v
+src/Compilers/Z/ArithmeticSimplifierWf.v
+src/Compilers/Z/BinaryNotationConstants.v
+src/Compilers/Z/CNotations.v
+src/Compilers/Z/FoldTypes.v
+src/Compilers/Z/HexNotationConstants.v
+src/Compilers/Z/Inline.v
+src/Compilers/Z/InlineInterp.v
+src/Compilers/Z/InlineWf.v
+src/Compilers/Z/JavaNotations.v
+src/Compilers/Z/MapCastByDeBruijn.v
+src/Compilers/Z/MapCastByDeBruijnInterp.v
+src/Compilers/Z/MapCastByDeBruijnWf.v
+src/Compilers/Z/OpInversion.v
+src/Compilers/Z/Reify.v
+src/Compilers/Z/Syntax.v
+src/Compilers/Z/Bounds/Interpretation.v
+src/Compilers/Z/Bounds/InterpretationLemmas.v
+src/Compilers/Z/Bounds/MapCastByDeBruijn.v
+src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
+src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
+src/Compilers/Z/Bounds/Pipeline.v
+src/Compilers/Z/Bounds/Relax.v
+src/Compilers/Z/Bounds/Pipeline/Definition.v
+src/Compilers/Z/Bounds/Pipeline/Glue.v
+src/Compilers/Z/Bounds/Pipeline/OutputType.v
+src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+src/Compilers/Z/Syntax/Equality.v
+src/Compilers/Z/Syntax/Util.v
+src/Curves/Edwards/AffineProofs.v
+src/Curves/Edwards/Montgomery.v
+src/Curves/Edwards/Pre.v
+src/Curves/Edwards/XYZT.v
+src/Curves/Montgomery/Affine.v
+src/Curves/Montgomery/AffineProofs.v
+src/Curves/Montgomery/XZ.v
+src/Curves/Montgomery/XZProofs.v
+src/Curves/Weierstrass/Affine.v
+src/Curves/Weierstrass/AffineProofs.v
+src/Curves/Weierstrass/Pre.v
+src/Curves/Weierstrass/Projective.v
+src/LegacyArithmetic/ArchitectureToZLike.v
+src/LegacyArithmetic/ArchitectureToZLikeProofs.v
+src/LegacyArithmetic/BarretReduction.v
+src/LegacyArithmetic/BaseSystem.v
+src/LegacyArithmetic/BaseSystemProofs.v
+src/LegacyArithmetic/Interface.v
+src/LegacyArithmetic/InterfaceProofs.v
+src/LegacyArithmetic/MontgomeryReduction.v
+src/LegacyArithmetic/Pow2Base.v
+src/LegacyArithmetic/Pow2BaseProofs.v
+src/LegacyArithmetic/VerdiTactics.v
+src/LegacyArithmetic/ZBounded.v
+src/LegacyArithmetic/ZBoundedZ.v
+src/LegacyArithmetic/Double/Core.v
+src/LegacyArithmetic/Double/Proofs/BitwiseOr.v
+src/LegacyArithmetic/Double/Proofs/Decode.v
+src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
+src/LegacyArithmetic/Double/Proofs/Multiply.v
+src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
+src/LegacyArithmetic/Double/Proofs/SelectConditional.v
+src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
+src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
+src/LegacyArithmetic/Double/Proofs/ShiftRight.v
+src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
+src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v
+src/Primitives/EdDSARepChange.v
+src/Primitives/MxDHRepChange.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/Ed25519.v
 src/Spec/EdDSA.v
@@ -183,14 +189,12 @@ src/Spec/ModularArithmetic.v
 src/Spec/MontgomeryCurve.v
 src/Spec/MxDH.v
 src/Spec/WeierstrassCurve.v
+src/Spec/Test/X25519.v
+src/Specific/ArithmeticSynthesisTest.v
 src/Specific/IntegrationTest.v
-src/Specific/NewBaseSystemTest.v
 src/Specific/FancyMachine256/Barrett.v
 src/Specific/FancyMachine256/Core.v
 src/Specific/FancyMachine256/Montgomery.v
-src/Tactics/VerdiTactics.v
-src/Tactics/Algebra_syntax/Nsatz.v
-src/Test/Curve25519SpecTestVectors.v
 src/Util/AdditionChainExponentiation.v
 src/Util/AutoRewrite.v
 src/Util/Bool.v
@@ -273,7 +277,3 @@ src/Util/Tactics/TransparentAssert.v
 src/Util/Tactics/UnifyAbstractReflexivity.v
 src/Util/Tactics/UniquePose.v
 src/Util/Tactics/VM.v
-src/WeierstrassCurve/Definitions.v
-src/WeierstrassCurve/Pre.v
-src/WeierstrassCurve/Projective.v
-src/WeierstrassCurve/WeierstrassCurveTheorems.v
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
index e71b24018..7270f6018 100644
--- a/src/Algebra/Field.v
+++ b/src/Algebra/Field.v
@@ -2,7 +2,7 @@ Require Import Crypto.Util.Relations Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.DebugPrint.
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
-Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.IntegralDomain.
 Require Coq.setoid_ring.Field_theory.
 
 Section Field.
@@ -215,14 +215,14 @@ End Homomorphism_rev.
 
 Ltac guess_field :=
   match goal with
-  | |- ?eq _ _ =>  constr:(_:Algebra.field (eq:=eq))
-  | |- not (?eq _ _) =>  constr:(_:Algebra.field (eq:=eq))
-  | [H: ?eq _ _ |- _ ] =>  constr:(_:Algebra.field (eq:=eq))
-  | [H: not (?eq _ _) |- _] =>  constr:(_:Algebra.field (eq:=eq))
+  | |- ?eq _ _ =>  constr:(_:Hierarchy.field (eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Hierarchy.field (eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Hierarchy.field (eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Hierarchy.field (eq:=eq))
   end.
 
 Ltac goal_to_field_equality fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
   match goal with
   | [ |- eq _ _] => idtac
   | [ |- not (eq ?x ?y) ] => apply not_exfalso; intro; goal_to_field_equality fld
@@ -234,10 +234,10 @@ Ltac goal_to_field_equality fld :=
   end.
 
 Ltac inequalities_to_inverse_equations fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
-  let div := match type of fld with Algebra.field(div:=?div) => div end in
-  let sub := match type of fld with Algebra.field(sub:=?sub) => sub end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
+  let div := match type of fld with Hierarchy.field(div:=?div) => div end in
+  let sub := match type of fld with Hierarchy.field(sub:=?sub) => sub end in
   repeat match goal with
          | [H: not (eq _ _) |- _ ] =>
            lazymatch type of H with
@@ -258,8 +258,8 @@ Ltac unique_pose_implication pf :=
   end.
 
 Ltac inverses_to_conditional_equations fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let inv := match type of fld with Algebra.field(inv:=?inv) => inv end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let inv := match type of fld with Hierarchy.field(inv:=?inv) => inv end in
   repeat match goal with
          | |- context[inv ?d] =>
            unique_pose_implication constr:(right_multiplicative_inverse(H:=fld) d)
@@ -268,15 +268,15 @@ Ltac inverses_to_conditional_equations fld :=
          end.
 
 Ltac clear_hypotheses_with_nonzero_requirements fld :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
   repeat match goal with
            [H: not (eq _ zero) -> _ |- _ ] => clear H
          end.
 
 Ltac forward_nonzero fld solver_tac :=
-  let eq := match type of fld with Algebra.field(eq:=?eq) => eq end in
-  let zero := match type of fld with Algebra.field(zero:=?zero) => zero end in
+  let eq := match type of fld with Hierarchy.field(eq:=?eq) => eq end in
+  let zero := match type of fld with Hierarchy.field(zero:=?zero) => zero end in
   repeat match goal with
          | [H: not (eq ?x zero) -> _ |- _ ]
            => let H' := fresh in
diff --git a/src/Algebra/Field_test.v b/src/Algebra/Field_test.v
index 0743729c2..59ca72c6b 100644
--- a/src/Algebra/Field_test.v
+++ b/src/Algebra/Field_test.v
@@ -4,7 +4,7 @@ Require Import Crypto.Algebra.Ring Crypto.Algebra.Field.
 Module _fsatz_test.
   Section _test.
     Context {F eq zero one opp add sub mul inv div}
-            {fld:@Algebra.field F eq zero one opp add sub mul inv div}
+            {fld:@Hierarchy.field F eq zero one opp add sub mul inv div}
             {eq_dec:DecidableRel eq}.
     Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
     Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
index 64e378281..8ce3e2a91 100644
--- a/src/Algebra/Group.v
+++ b/src/Algebra/Group.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms Crypto.Util.Relations (*Crypto.Util.Tactics*).
-Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 
 Section BasicProperties.
   Context {T eq op id inv} `{@group T eq op id inv}.
diff --git a/src/Algebra.v b/src/Algebra/Hierarchy.v
index 342e9feaa..342e9feaa 100644
--- a/src/Algebra.v
+++ b/src/Algebra/Hierarchy.v
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
index 4ab50c6e3..c52b4ce87 100644
--- a/src/Algebra/IntegralDomain.v
+++ b/src/Algebra/IntegralDomain.v
@@ -1,7 +1,7 @@
 Require Coq.setoid_ring.Integral_domain.
-Require Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.Factorize.
-Require Import Crypto.Algebra Crypto.Algebra.Ring.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
@@ -23,8 +23,8 @@ Module IntegralDomain.
     Section ReflectiveNsatzSideConditionProver.
       Import BinInt BinNat BinPos.
       Context {R eq zero one opp add sub mul}
-              {ring:@Algebra.ring R eq zero one opp add sub mul}
-              {zpzf:@Algebra.is_zero_product_zero_factor R eq zero mul}.
+              {ring:@Hierarchy.ring R eq zero one opp add sub mul}
+              {zpzf:@Hierarchy.is_zero_product_zero_factor R eq zero mul}.
       Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
       Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
       Local Infix "+" := add.  Local Infix "-" := sub. Local Infix "*" := mul.
@@ -198,4 +198,4 @@ Ltac dropRingSyntax :=
         Ncring.opp_notation
         Ncring.eq_notation
     ] in *.
-Ltac nsatz := Algebra_syntax.Nsatz.nsatz; dropRingSyntax.
+Ltac nsatz := Algebra.Nsatz.nsatz; dropRingSyntax.
diff --git a/src/Algebra/Monoid.v b/src/Algebra/Monoid.v
index bd15290c7..470e8df40 100644
--- a/src/Algebra/Monoid.v
+++ b/src/Algebra/Monoid.v
@@ -1,6 +1,6 @@
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Algebra.
+Require Import Crypto.Algebra.Hierarchy.
 
 Section Monoid.
   Context {T eq op id} {monoid:@monoid T eq op id}.
diff --git a/src/Tactics/Algebra_syntax/Nsatz.v b/src/Algebra/Nsatz.v
index e219bc579..2a65e7d82 100644
--- a/src/Tactics/Algebra_syntax/Nsatz.v
+++ b/src/Algebra/Nsatz.v
@@ -1,4 +1,7 @@
-(*** Tactics for manipulating polynomial equations *)
+(* This is a rewrite of the Ltac parts of standard library nsatz. We should
+  periodically check whether we still need it -- once enough bugs get fixed
+  in mailine, we hope to drop this implementation *)
+
 Require Coq.nsatz.Nsatz.
 Require Import Coq.Lists.List.
 
diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
index cff27bdb3..406706988 100644
--- a/src/Algebra/Ring.v
+++ b/src/Algebra/Ring.v
@@ -4,7 +4,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.OnSubterms.
 Require Import Crypto.Util.Tactics.Revert.
-Require Import Crypto.Algebra Crypto.Algebra.Group Crypto.Algebra.Monoid.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Group Crypto.Algebra.Monoid.
 Require Coq.ZArith.ZArith Coq.PArith.PArith.
 
 
@@ -420,7 +420,7 @@ End of_Z.
 Definition char_ge
            {R eq zero one opp add} {sub:R->R->R} {mul:R->R->R}
            C :=
-  @Algebra.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
+  @Hierarchy.char_ge R eq zero (fun p => (@of_Z R zero one opp add) (BinInt.Z.pos p)) C.
 Existing Class char_ge.
 
 (*** Tactics for ring equations *)
diff --git a/src/Algebra/ScalarMult.v b/src/Algebra/ScalarMult.v
index 5c17a6bb5..f52fc93ee 100644
--- a/src/Algebra/ScalarMult.v
+++ b/src/Algebra/ScalarMult.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Algebra Crypto.Algebra.Monoid.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Monoid.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.
diff --git a/src/ModularArithmetic/BarrettReduction/ZGeneralized.v b/src/Arithmetic/BarrettReduction/Generalized.v
index 596c8e5f9..76058463c 100644
--- a/src/ModularArithmetic/BarrettReduction/ZGeneralized.v
+++ b/src/Arithmetic/BarrettReduction/Generalized.v
@@ -9,7 +9,7 @@
     base ([b]), exponent ([k]), and the [offset] than those given in
     the HAC. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch Crypto.Algebra.
+Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
 
diff --git a/src/ModularArithmetic/BarrettReduction/ZHandbook.v b/src/Arithmetic/BarrettReduction/HAC.v
index 8962a997f..70661ee96 100644
--- a/src/ModularArithmetic/BarrettReduction/ZHandbook.v
+++ b/src/Arithmetic/BarrettReduction/HAC.v
@@ -9,7 +9,7 @@
     have to carry around extra precision), but requires more stringint
     conditions on the base ([b]), exponent ([k]), and the [offset]. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch Crypto.Algebra.
+Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch.
 
 Local Open Scope Z_scope.
 
diff --git a/src/ModularArithmetic/BarrettReduction/Z.v b/src/Arithmetic/BarrettReduction/Wikipedia.v
index 69ce10c4b..69ce10c4b 100644
--- a/src/ModularArithmetic/BarrettReduction/Z.v
+++ b/src/Arithmetic/BarrettReduction/Wikipedia.v
diff --git a/src/NewBaseSystem.v b/src/Arithmetic/Core.v
index 4611cf6ed..2613765d0 100644
--- a/src/NewBaseSystem.v
+++ b/src/Arithmetic/Core.v
@@ -244,11 +244,11 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.omega.Omega.
 Require Import Coq.ZArith.BinIntDef.
 Local Open Scope Z_scope.
 
-Require Import Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Import Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.Decidable Crypto.Util.LetIn.
 Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil Crypto.Util.Sigma.
 Require Import Crypto.Util.CPSUtil Crypto.Util.Prod.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.VM.
diff --git a/src/Karatsuba.v b/src/Arithmetic/Karatsuba.v
index 8e88d64c3..0f20bb238 100644
--- a/src/Karatsuba.v
+++ b/src/Arithmetic/Karatsuba.v
@@ -1,5 +1,5 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Tactics.Algebra_syntax.Nsatz.
+Require Import Crypto.Algebra.Nsatz.
 Require Import Crypto.Util.ZUtil.
 Local Open Scope Z_scope.
 
diff --git a/src/ModularArithmetic/Pre.v b/src/Arithmetic/ModularArithmeticPre.v
index c8b5a9740..b27ffd16d 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/Arithmetic/ModularArithmeticPre.v
@@ -3,7 +3,6 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Coq.Logic.EqdepFacts.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.NumTheoryUtil.
-Require Import Crypto.Tactics.VerdiTactics.
 Require Export Crypto.Util.FixCoqMistakes.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
@@ -18,7 +17,7 @@ Lemma exist_reduced_eq: forall (m : Z) (a b : Z), a = b -> forall pfa pfb,
     exist (fun z : Z => z = z mod m) b pfb.
 Proof.
   intuition; simpl in *; try congruence.
-  subst_max.
+  subst.
   f_equal.
   eapply UIP_dec, Z.eq_dec.
 Qed.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v
index 9cd211943..990aa9dc8 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/Arithmetic/ModularArithmeticTheorems.v
@@ -1,12 +1,12 @@
 Require Import Coq.omega.Omega.
 Require Import Crypto.Spec.ModularArithmetic.
-Require Import Crypto.ModularArithmetic.Pre.
+Require Import Crypto.Arithmetic.ModularArithmeticPre.
 
 Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac.
 
-Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field.
 Require Import Crypto.Util.Decidable Crypto.Util.ZUtil.
 Require Export Crypto.Util.FixCoqMistakes.
 
@@ -22,7 +22,7 @@ Module F.
   Global Instance eq_dec {m} : DecidableRel (@eq (F m)). pose proof dec_eq_Z. exact _. Defined.
   
   Global Instance commutative_ring_modulo m
-    : @Algebra.commutative_ring (F m) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul.
+    : @Algebra.Hierarchy.commutative_ring (F m) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul.
   Proof.
     repeat (split || intro); unwrap_F;
       autorewrite with zsimplify; solve [ exact _ | auto with zarith | congruence].
@@ -211,13 +211,13 @@ Module F.
     Proof using Type.
       destruct (pow_spec x) as [HO HS]; intros.
       destruct n; auto; unfold id.
-      rewrite Pre.N_pos_1plus at 1.
+      rewrite ModularArithmeticPre.N_pos_1plus at 1.
       rewrite HS.
       simpl.
       induction p using Pos.peano_ind.
-      - simpl. rewrite HO. apply Algebra.right_identity.
+      - simpl. rewrite HO. apply Algebra.Hierarchy.right_identity.
       - rewrite (@pow_pos_succ (F m) (@F.mul m) eq _ _ associative x).
-        rewrite <-IHp, Pos.pred_N_succ, Pre.N_pos_1plus, HS.
+        rewrite <-IHp, Pos.pred_N_succ, ModularArithmeticPre.N_pos_1plus, HS.
         trivial.
     Qed.
 
diff --git a/src/ModularArithmetic/Montgomery/Z.v b/src/Arithmetic/MontgomeryReduction/Definition.v
index 78d3c037f..78d3c037f 100644
--- a/src/ModularArithmetic/Montgomery/Z.v
+++ b/src/Arithmetic/MontgomeryReduction/Definition.v
diff --git a/src/ModularArithmetic/Montgomery/ZProofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v
index 2d8f6155d..d5de00213 100644
--- a/src/ModularArithmetic/Montgomery/ZProofs.v
+++ b/src/Arithmetic/MontgomeryReduction/Proofs.v
@@ -3,7 +3,7 @@
     Reduction, and Montgomery Multiplication on [Z].  We follow
     Wikipedia. *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Structures.Equalities.
-Require Import Crypto.ModularArithmetic.Montgomery.Z.
+Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SimplifyRepeatedIfs.
@@ -34,13 +34,13 @@ Section montgomery.
 
   Lemma to_from_montgomery_naive x : to_montgomery_naive (from_montgomery_naive x) ≡ x.
   Proof using R'_good.
-    unfold Z.to_montgomery_naive, Z.from_montgomery_naive.
+    unfold to_montgomery_naive, from_montgomery_naive.
     rewrite <- Z.mul_assoc, R'_good'.
     autorewrite with zsimplify; reflexivity.
   Qed.
   Lemma from_to_montgomery_naive x : from_montgomery_naive (to_montgomery_naive x) ≡ x.
   Proof using R'_good.
-    unfold Z.to_montgomery_naive, Z.from_montgomery_naive.
+    unfold to_montgomery_naive, from_montgomery_naive.
     rewrite <- Z.mul_assoc, R'_good.
     autorewrite with zsimplify; reflexivity.
   Qed.
@@ -52,19 +52,19 @@ Section montgomery.
     Local Infix "*" := (mul_naive R') : montgomery_scope.
 
     Lemma add_correct_naive x y : from_montgomery_naive (x + y) = from_montgomery_naive x + from_montgomery_naive y.
-    Proof using Type. unfold Z.from_montgomery_naive, add; lia. Qed.
+    Proof using Type. unfold from_montgomery_naive, add; lia. Qed.
     Lemma add_correct_naive_to x y : to_montgomery_naive (x + y) = (to_montgomery_naive x + to_montgomery_naive y)%montgomery.
-    Proof using Type. unfold Z.to_montgomery_naive, add; autorewrite with push_Zmul; reflexivity. Qed.
+    Proof using Type. unfold to_montgomery_naive, add; autorewrite with push_Zmul; reflexivity. Qed.
     Lemma sub_correct_naive x y : from_montgomery_naive (x - y) = from_montgomery_naive x - from_montgomery_naive y.
-    Proof using Type. unfold Z.from_montgomery_naive, sub; lia. Qed.
+    Proof using Type. unfold from_montgomery_naive, sub; lia. Qed.
     Lemma sub_correct_naive_to x y : to_montgomery_naive (x - y) = (to_montgomery_naive x - to_montgomery_naive y)%montgomery.
-    Proof using Type. unfold Z.to_montgomery_naive, sub; autorewrite with push_Zmul; reflexivity. Qed.
+    Proof using Type. unfold to_montgomery_naive, sub; autorewrite with push_Zmul; reflexivity. Qed.
 
     Theorem mul_correct_naive x y : from_montgomery_naive (x * y) = from_montgomery_naive x * from_montgomery_naive y.
-    Proof using Type. unfold Z.from_montgomery_naive, mul_naive; lia. Qed.
+    Proof using Type. unfold from_montgomery_naive, mul_naive; lia. Qed.
     Theorem mul_correct_naive_to x y : to_montgomery_naive (x * y) ≡ (to_montgomery_naive x * to_montgomery_naive y)%montgomery.
     Proof using R'_good.
-      unfold Z.to_montgomery_naive, mul_naive.
+      unfold to_montgomery_naive, mul_naive.
       rewrite <- !Z.mul_assoc, R'_good.
       autorewrite with zsimplify; apply (f_equal2 Z.modulo); lia.
     Qed.
@@ -98,7 +98,7 @@ Section montgomery.
       Lemma prereduce_correct : prereduce T ≡ T * R'.
       Proof using N'_good N'_in_range N_reasonable R'_good.
         transitivity ((T + m * N) * R').
-        { unfold Z.prereduce.
+        { unfold prereduce.
           autorewrite with zstrip_div; push_Zmod.
           rewrite N'_good'_alt.
           autorewrite with zsimplify pull_Zmod.
@@ -131,7 +131,7 @@ Section montgomery.
         : 0 <= N
           -> 0 <= T <= R * B
           -> 0 <= prereduce T < B + N.
-        Proof using N_reasonable m_small. unfold Z.prereduce; auto with zarith nia. Qed.
+        Proof using N_reasonable m_small. unfold prereduce; auto with zarith nia. Qed.
       End generic.
 
       Section N_very_small.
@@ -170,7 +170,7 @@ Section montgomery.
             -> 0 <= reduce N R N' T < R.
         Proof using N_reasonable N_small_enough m_small.
           intro H; pose proof (prereduce_in_range_small_enough H).
-          unfold reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia.
+          unfold reduce, prereduce in *; break_match; Z.ltb_to_lt; nia.
         Qed.
 
         Lemma partial_reduce_in_range_R
@@ -178,7 +178,7 @@ Section montgomery.
             -> 0 <= partial_reduce N R N' T < R.
         Proof using N_reasonable N_small_enough m_small.
           intro H; pose proof (prereduce_in_range_small_enough H).
-          unfold partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia.
+          unfold partial_reduce, prereduce in *; break_match; Z.ltb_to_lt; nia.
         Qed.
 
         Lemma reduce_via_partial_in_range_R
@@ -186,7 +186,7 @@ Section montgomery.
             -> 0 <= reduce_via_partial N R N' T < R.
         Proof using N_reasonable N_small_enough m_small.
           intro H; pose proof (prereduce_in_range_small_enough H).
-          unfold reduce_via_partial, partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia.
+          unfold reduce_via_partial, partial_reduce, prereduce in *; break_match; Z.ltb_to_lt; nia.
         Qed.
       End N_small_enough.
 
@@ -201,7 +201,7 @@ Section montgomery.
           -> 0 <= reduce N R N' T < N.
         Proof using N_reasonable m_small.
           intro H; pose proof (prereduce_in_range H).
-          unfold reduce, Z.prereduce in *; break_match; Z.ltb_to_lt; nia.
+          unfold reduce, prereduce in *; break_match; Z.ltb_to_lt; nia.
         Qed.
 
         Lemma partial_reduce_in_range
@@ -209,7 +209,7 @@ Section montgomery.
           -> Z.min 0 (R - N) <= partial_reduce N R N' T < 2 * N.
         Proof using N_reasonable m_small.
           intro H; pose proof (prereduce_in_range H).
-          unfold partial_reduce, Z.prereduce in *; break_match; Z.ltb_to_lt;
+          unfold partial_reduce, prereduce in *; break_match; Z.ltb_to_lt;
             apply Z.min_case_strong; nia.
         Qed.
 
@@ -235,7 +235,7 @@ Section montgomery.
           assert (T + m * N < R * R -> (T + m * N) / R < R) by auto with zarith.
           assert (H' : (T + m * N) mod (R * R) = if R * R <=? T + m * N then T + m * N - R * R else T + m * N)
             by (break_match; Z.ltb_to_lt; autorewrite with zsimplify; lia).
-          unfold partial_reduce, partial_reduce_alt, Z.prereduce.
+          unfold partial_reduce, partial_reduce_alt, prereduce.
           rewrite H'; clear H'.
           simplify_repeated_ifs.
           set (m' := m) in *.
@@ -253,7 +253,7 @@ Section montgomery.
       Local Notation from_montgomery := (from_montgomery N R N').
       Lemma to_from_montgomery a : to_montgomery (from_montgomery a) ≡ a.
       Proof using N'_good N'_in_range N_reasonable R'_good.
-        unfold Z.to_montgomery, Z.from_montgomery.
+        unfold to_montgomery, from_montgomery.
         transitivity ((a * 1) * 1); [ | apply f_equal2; lia ].
         rewrite <- !R'_good, !reduce_correct.
         unfold Z.equiv_modulo; push_Zmod; pull_Zmod.
@@ -261,7 +261,7 @@ Section montgomery.
       Qed.
       Lemma from_to_montgomery a : from_montgomery (to_montgomery a) ≡ a.
       Proof using N'_good N'_in_range N_reasonable R'_good.
-        unfold Z.to_montgomery, Z.from_montgomery.
+        unfold to_montgomery, from_montgomery.
         rewrite !reduce_correct.
         transitivity (a * ((R * (R * R' mod N) * R') mod N)).
         { unfold Z.equiv_modulo; push_Zmod; pull_Zmod.
@@ -274,12 +274,12 @@ Section montgomery.
 
       Theorem mul_correct x y : from_montgomery (x * y) ≡ from_montgomery x * from_montgomery y.
       Proof using N'_good N'_in_range N_reasonable R'_good.
-        unfold Z.from_montgomery, mul.
+        unfold from_montgomery, mul.
         rewrite !reduce_correct; apply f_equal2; lia.
       Qed.
       Theorem mul_correct_to x y : to_montgomery (x * y) ≡ (to_montgomery x * to_montgomery y)%montgomery.
       Proof using N'_good N'_in_range N_reasonable R'_good.
-        unfold Z.to_montgomery, mul.
+        unfold to_montgomery, mul.
         rewrite !reduce_correct.
         transitivity (x * y * R * 1 * 1 * 1);
           [ rewrite <- R'_good at 1
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v
index eba1af740..c253752c5 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/Arithmetic/PrimeFieldTheorems.v
@@ -1,10 +1,10 @@
-Require Export Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.ModularArithmeticTheorems.
+Require Export Crypto.Spec.ModularArithmetic.
+Require Export Crypto.Arithmetic.ModularArithmeticTheorems.
 Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
 
 Require Import Coq.nsatz.Nsatz.
-Require Import Crypto.ModularArithmetic.Pre.
+Require Import Crypto.Arithmetic.ModularArithmeticPre.
 Require Import Crypto.Util.NumTheoryUtil.
-Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
 Require Import Coq.Logic.Eqdep_dec.
@@ -12,7 +12,7 @@ Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
-Require Crypto.Algebra Crypto.Algebra.Field.
+Require Crypto.Algebra.Hierarchy Crypto.Algebra.Field.
 
 Existing Class prime.
 Local Open Scope F_scope.
@@ -27,7 +27,7 @@ Module F.
     Lemma inv_0 : F.inv 0%F = F.of_Z q 0. Proof using Type. destruct inv_spec; auto. Qed.
     Lemma inv_nonzero (x:F q) : (x <> 0 -> F.inv x * x%F = 1)%F. Proof using Type*. destruct inv_spec; auto. Qed.
 
-    Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul F.inv F.div.
+    Global Instance field_modulo : @Algebra.Hierarchy.field (F q) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul F.inv F.div.
     Proof using Type*.
       repeat match goal with
              | _ => solve [ solve_proper
@@ -107,7 +107,7 @@ Module F.
              | |- _ => progress rewrite <-?Z2N.inj_0, <-?Z2N.inj_add by zero_bounds
              | |- _ => rewrite <-@euler_criterion by auto
              | |- ?x ^ (?f _) = ?a <-> ?x ^ (?f _) = ?a => do 3 f_equiv; [ ]
-             | |- _ => rewrite !Zmod_odd in *; repeat break_if; omega
+             | |- _ => rewrite !Zmod_odd in *; repeat (break_match; break_match_hyps); omega
              | |- _ => rewrite Z.rem_mul_r in * by omega
              | |- (exists x, _) <-> ?B => assert B by field; solve [intuition eauto]
              | |- (?x ^ Z.to_N ?a = 1) <-> _ =>
@@ -214,16 +214,16 @@ Module F.
         repeat match goal with
              | |- _ => progress subst
              | |- _ => progress rewrite ?F.pow_0_l
-             | |- _ => break_if
-             | |- (exists x, _) <-> ?B => assert B by field; solve [intuition eauto]
              | |- (_ <> _)%N => rewrite <-Z2N.inj_0, Z2N.inj_iff by zero_bounds
              | |- (?a <> 0)%Z => assert (0 < a) by zero_bounds; omega
              | |- _ => congruence
              end.
+        break_match;
+          match goal with |- _ <-> ?G => assert G by field end; intuition eauto.
       } {
         rewrite eq_b4_a2_iff by auto.
         rewrite !@F.pow_2_r in *.
-        break_if.
+        break_match.
         intuition (f_equal; eauto).
         split; intro A. {
           destruct (Field.only_two_square_roots_choice _ x (x * x) A eq_refl) as [B | B];
@@ -258,11 +258,11 @@ Module F.
       Definition div x y := mul (inv y) x.
       
       Lemma ring :
-        @Algebra.ring H eq zero one opp add sub mul
+        @Algebra.Hierarchy.ring H eq zero one opp add sub mul
         /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi
         /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'.
       Proof using phi'_add phi'_iff phi'_mul phi'_one phi'_opp phi'_phi phi'_sub phi'_zero. eapply @Ring.ring_by_isomorphism; assumption || exact _. Qed.
-      Local Instance _iso_ring : Algebra.ring := proj1 ring.
+      Local Instance _iso_ring : Algebra.Hierarchy.ring := proj1 ring.
       Local Instance _iso_hom1 : Ring.is_homomorphism := proj1 (proj2 ring).
       Local Instance _iso_hom2 : Ring.is_homomorphism := proj2 (proj2 ring).
 
@@ -279,12 +279,12 @@ Module F.
       Let div_proof : forall a b : H, phi' (mul (inv b) a) = phi' a / phi' b.
       Proof.
         intros.
-        rewrite phi'_mul, inv_proof, Algebra.field_div_definition, Algebra.commutative.
+        rewrite phi'_mul, inv_proof, Algebra.Hierarchy.field_div_definition, Algebra.Hierarchy.commutative.
         reflexivity.
       Qed.
 
       Lemma field_and_iso :
-        @Algebra.field H eq zero one opp add sub mul inv div
+        @Algebra.Hierarchy.field H eq zero one opp add sub mul inv div
         /\ @Ring.is_homomorphism (F q) Logic.eq F.one F.add F.mul H eq one add mul phi
         /\ @Ring.is_homomorphism H eq one add mul (F q) Logic.eq F.one F.add F.mul phi'.
       Proof using Type*. eapply @Field.field_and_homomorphism_from_redundant_representation;
diff --git a/src/SaturatedBaseSystem.v b/src/Arithmetic/Saturated.v
index cddb9797d..cb37fb1f9 100644
--- a/src/SaturatedBaseSystem.v
+++ b/src/Arithmetic/Saturated.v
@@ -3,8 +3,8 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Lists.List.
 Local Open Scope Z_scope.
 
-Require Import Crypto.Tactics.Algebra_syntax.Nsatz.
-Require Import Crypto.NewBaseSystem.
+Require Import Crypto.Algebra.Nsatz.
+Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil.
 Require Import Crypto.Util.Tuple Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
diff --git a/src/Reflection/BoundByCast.v b/src/Compilers/BoundByCast.v
index d65e67919..3a7bf143a 100644
--- a/src/Reflection/BoundByCast.v
+++ b/src/Compilers/BoundByCast.v
@@ -1,11 +1,11 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartBound.
-Require Import Crypto.Reflection.InlineCast.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Reflection.MapCast.
-Require Import Crypto.Reflection.Eta.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartBound.
+Require Import Crypto.Compilers.InlineCast.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Inline.
+Require Import Crypto.Compilers.Linearize.
+Require Import Crypto.Compilers.MapCast.
+Require Import Crypto.Compilers.Eta.
 
 Local Open Scope expr_scope.
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/BoundByCastInterp.v b/src/Compilers/BoundByCastInterp.v
index 46a50fd42..77496659b 100644
--- a/src/Reflection/BoundByCastInterp.v
+++ b/src/Compilers/BoundByCastInterp.v
@@ -1,20 +1,20 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.InterpWfRel.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.BoundByCast.
-Require Import Crypto.Reflection.SmartBound.
-Require Import Crypto.Reflection.SmartBoundInterp.
-Require Import Crypto.Reflection.SmartBoundWf.
-Require Import Crypto.Reflection.InlineCastInterp.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.InlineInterp.
-Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.MapCastInterp.
-Require Import Crypto.Reflection.MapCastWf.
-Require Import Crypto.Reflection.EtaInterp.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InterpWfRel.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.BoundByCast.
+Require Import Crypto.Compilers.SmartBound.
+Require Import Crypto.Compilers.SmartBoundInterp.
+Require Import Crypto.Compilers.SmartBoundWf.
+Require Import Crypto.Compilers.InlineCastInterp.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.InlineInterp.
+Require Import Crypto.Compilers.LinearizeInterp.
+Require Import Crypto.Compilers.LinearizeWf.
+Require Import Crypto.Compilers.MapCastInterp.
+Require Import Crypto.Compilers.MapCastWf.
+Require Import Crypto.Compilers.EtaInterp.
 
 Local Open Scope expr_scope.
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/BoundByCastWf.v b/src/Compilers/BoundByCastWf.v
index cc60f14b1..d03ec1359 100644
--- a/src/Reflection/BoundByCastWf.v
+++ b/src/Compilers/BoundByCastWf.v
@@ -1,11 +1,11 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.BoundByCast.
-Require Import Crypto.Reflection.EtaWf.
-Require Import Crypto.Reflection.InlineCastWf.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.SmartBoundWf.
-Require Import Crypto.Reflection.MapCastWf.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.BoundByCast.
+Require Import Crypto.Compilers.EtaWf.
+Require Import Crypto.Compilers.InlineCastWf.
+Require Import Crypto.Compilers.LinearizeWf.
+Require Import Crypto.Compilers.SmartBoundWf.
+Require Import Crypto.Compilers.MapCastWf.
 
 Local Open Scope expr_scope.
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Compilers/CommonSubexpressionElimination.v
index 6d3921aa6..73df034a6 100644
--- a/src/Reflection/CommonSubexpressionElimination.v
+++ b/src/Compilers/CommonSubexpressionElimination.v
@@ -1,7 +1,7 @@
 (** * Common Subexpression Elimination for PHOAS Syntax *)
 Require Import Coq.Lists.List.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Bool.
 
 Local Open Scope list_scope.
diff --git a/src/Reflection/Conversion.v b/src/Compilers/Conversion.v
index bd0f4f695..29874c96f 100644
--- a/src/Reflection/Conversion.v
+++ b/src/Compilers/Conversion.v
@@ -1,6 +1,6 @@
 (** * Convert between interpretations of types *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Map.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Map.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 
diff --git a/src/Reflection/CountLets.v b/src/Compilers/CountLets.v
index 64c46d58a..4810162c8 100644
--- a/src/Reflection/CountLets.v
+++ b/src/Compilers/CountLets.v
@@ -1,6 +1,6 @@
 (** * Counts how many binders there are *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Reflection/Equality.v b/src/Compilers/Equality.v
index ad642fe2d..8e2b44de8 100644
--- a/src/Reflection/Equality.v
+++ b/src/Compilers/Equality.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.FixCoqMistakes.
 
diff --git a/src/Reflection/Eta.v b/src/Compilers/Eta.v
index d40267858..9ca778f15 100644
--- a/src/Reflection/Eta.v
+++ b/src/Compilers/Eta.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/EtaInterp.v b/src/Compilers/EtaInterp.v
index deb551d7d..f59024b98 100644
--- a/src/Reflection/EtaInterp.v
+++ b/src/Compilers/EtaInterp.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 
diff --git a/src/Reflection/EtaWf.v b/src/Compilers/EtaWf.v
index 240f5a1e3..e8dd2f846 100644
--- a/src/Reflection/EtaWf.v
+++ b/src/Compilers/EtaWf.v
@@ -1,9 +1,9 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.EtaInterp.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.WfInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.EtaInterp.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.WfInversion.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SplitInContext.
diff --git a/src/Reflection/ExprInversion.v b/src/Compilers/ExprInversion.v
index 645555cb5..a1d2587f5 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Compilers/ExprInversion.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/FilterLive.v b/src/Compilers/FilterLive.v
index 68144c0f7..5f3f0156d 100644
--- a/src/Reflection/FilterLive.v
+++ b/src/Compilers/FilterLive.v
@@ -1,8 +1,8 @@
 (** * Computes a list of live variables *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.CountLets.
 Require Import Crypto.Util.ListUtil.
 
 Local Notation eta x := (fst x, snd x).
diff --git a/src/Reflection/FoldTypes.v b/src/Compilers/FoldTypes.v
index d5d62a3aa..0b923fcc9 100644
--- a/src/Reflection/FoldTypes.v
+++ b/src/Compilers/FoldTypes.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.SmartMap.
 
 Section language.
   Context {base_type_code} {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
diff --git a/src/Reflection/Inline.v b/src/Compilers/Inline.v
index 74abeef10..d2aa44520 100644
--- a/src/Reflection/Inline.v
+++ b/src/Compilers/Inline.v
@@ -1,6 +1,6 @@
 (** * Inline: Remove some [Let] expressions *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Reflection/InlineCast.v b/src/Compilers/InlineCast.v
index d3e85d02d..675835760 100644
--- a/src/Reflection/InlineCast.v
+++ b/src/Compilers/InlineCast.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartCast.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartCast.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/InlineCastInterp.v b/src/Compilers/InlineCastInterp.v
index f885fbd16..2b2e08b4d 100644
--- a/src/Reflection/InlineCastInterp.v
+++ b/src/Compilers/InlineCastInterp.v
@@ -1,14 +1,14 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.InlineCast.
-Require Import Crypto.Reflection.InlineInterp.
-Require Import Crypto.Reflection.SmartCast.
-Require Import Crypto.Reflection.SmartCastInterp.
-Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.InlineCast.
+Require Import Crypto.Compilers.InlineInterp.
+Require Import Crypto.Compilers.SmartCast.
+Require Import Crypto.Compilers.SmartCastInterp.
+Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
diff --git a/src/Reflection/InlineCastWf.v b/src/Compilers/InlineCastWf.v
index a61455c4f..f2d3cc84f 100644
--- a/src/Reflection/InlineCastWf.v
+++ b/src/Compilers/InlineCastWf.v
@@ -1,13 +1,13 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.WfInversion.
-Require Import Crypto.Reflection.InlineCast.
-Require Import Crypto.Reflection.InlineWf.
-Require Import Crypto.Reflection.SmartCast.
-Require Import Crypto.Reflection.SmartCastWf.
-Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.InlineCast.
+Require Import Crypto.Compilers.InlineWf.
+Require Import Crypto.Compilers.SmartCast.
+Require Import Crypto.Compilers.SmartCastWf.
+Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
diff --git a/src/Reflection/InlineInterp.v b/src/Compilers/InlineInterp.v
index cb9276d9a..5ec549054 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Compilers/InlineInterp.v
@@ -1,10 +1,10 @@
 (** * Inline: Remove some [Let] expressions *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.InlineWf.
-Require Import Crypto.Reflection.InterpProofs.
-Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.InlineWf.
+Require Import Crypto.Compilers.InterpProofs.
+Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Util.Sigma Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
diff --git a/src/Reflection/InlineWf.v b/src/Compilers/InlineWf.v
index 20ae25010..a0d77471c 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Compilers/InlineWf.v
@@ -1,11 +1,11 @@
 (** * Inline: Remove some [Let] expressions *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.WfInversion.
-Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
diff --git a/src/Reflection/InputSyntax.v b/src/Compilers/InputSyntax.v
index 123e4f851..22f7cdd61 100644
--- a/src/Reflection/InputSyntax.v
+++ b/src/Compilers/InputSyntax.v
@@ -1,9 +1,9 @@
 (** * PHOAS Representation of Gallina which allows exact denotation *)
 Require Import Coq.Strings.String.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.InterpProofs.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.InterpProofs.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Notations.
diff --git a/src/Reflection/InterpByIso.v b/src/Compilers/InterpByIso.v
index a971b8e88..a2263364b 100644
--- a/src/Reflection/InterpByIso.v
+++ b/src/Compilers/InterpByIso.v
@@ -1,7 +1,7 @@
 (** * PHOAS interpretation function for any retract of [var:=interp_base_type] *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.SmartMap.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/InterpByIsoProofs.v b/src/Compilers/InterpByIsoProofs.v
index 07ad8ed62..98e700738 100644
--- a/src/Reflection/InterpByIsoProofs.v
+++ b/src/Compilers/InterpByIsoProofs.v
@@ -1,10 +1,10 @@
 (** * PHOAS interpretation function for any retract of [var:=interp_base_type] *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.InterpByIso.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.InterpByIso.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.RewriteHyp.
diff --git a/src/Reflection/InterpProofs.v b/src/Compilers/InterpProofs.v
index 5d8322441..5ea1a99a4 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Compilers/InterpProofs.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.WfProofs.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.WfProofs.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Sigma Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.RewriteHyp.
diff --git a/src/Reflection/InterpWf.v b/src/Compilers/InterpWf.v
index 5f76e0791..e1572ceed 100644
--- a/src/Reflection/InterpWf.v
+++ b/src/Compilers/InterpWf.v
@@ -1,7 +1,7 @@
 Require Import Coq.Strings.String Coq.Classes.RelationClasses.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/InterpWfRel.v b/src/Compilers/InterpWfRel.v
index 40288232a..46be4220d 100644
--- a/src/Reflection/InterpWfRel.v
+++ b/src/Compilers/InterpWfRel.v
@@ -1,7 +1,7 @@
 Require Import Coq.Strings.String Coq.Classes.RelationClasses.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Linearize.v b/src/Compilers/Linearize.v
index 9fc45c798..fc6957bf4 100644
--- a/src/Reflection/Linearize.v
+++ b/src/Compilers/Linearize.v
@@ -1,6 +1,6 @@
 (** * Linearize: Place all and only operations in let binders *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 (*Require Import Crypto.Util.Tactics.*)
 
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/LinearizeInterp.v b/src/Compilers/LinearizeInterp.v
index 293d80a34..6451431fa 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Compilers/LinearizeInterp.v
@@ -1,10 +1,10 @@
 (** * Linearize: Place all and only operations in let binders *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.InterpProofs.
-Require Import Crypto.Reflection.Linearize.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.LinearizeWf.
+Require Import Crypto.Compilers.InterpProofs.
+Require Import Crypto.Compilers.Linearize.
 Require Import Crypto.Util.Sigma Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
diff --git a/src/Reflection/LinearizeWf.v b/src/Compilers/LinearizeWf.v
index b12e83b56..073137fd4 100644
--- a/src/Reflection/LinearizeWf.v
+++ b/src/Compilers/LinearizeWf.v
@@ -1,8 +1,8 @@
 (** * Linearize: Place all and only operations in let binders *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.Linearize.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.Linearize.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sigma.
 
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/Map.v b/src/Compilers/Map.v
index 9faa69eb9..9fe9f7011 100644
--- a/src/Reflection/Map.v
+++ b/src/Compilers/Map.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/MapCast.v b/src/Compilers/MapCast.v
index 56736fa20..0cb453b00 100644
--- a/src/Reflection/MapCast.v
+++ b/src/Compilers/MapCast.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/MapCastByDeBruijn.v b/src/Compilers/MapCastByDeBruijn.v
index 68eb06a54..0964847a6 100644
--- a/src/Reflection/MapCastByDeBruijn.v
+++ b/src/Compilers/MapCastByDeBruijn.v
@@ -1,11 +1,11 @@
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.MapCast.
-Require Import Crypto.Reflection.Named.InterpretToPHOAS.
-Require Import Crypto.Reflection.Named.Compile.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.MapCast.
+Require Import Crypto.Compilers.Named.InterpretToPHOAS.
+Require Import Crypto.Compilers.Named.Compile.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
+Require Import Crypto.Compilers.Syntax.
 
 (** N.B. This procedure only works when there are no nested lets,
     i.e., nothing like [let x := let y := z in w] in the PHOAS syntax
diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v
index 90cbad00c..5d8156f09 100644
--- a/src/Reflection/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/MapCastByDeBruijnInterp.v
@@ -1,18 +1,18 @@
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.MapCastInterp.
-Require Import Crypto.Reflection.Named.MapCastWf.
-Require Import Crypto.Reflection.Named.InterpretToPHOASInterp.
-Require Import Crypto.Reflection.Named.CompileInterp.
-Require Import Crypto.Reflection.Named.CompileWf.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
-Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.MapCastByDeBruijn.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.MapCastInterp.
+Require Import Crypto.Compilers.Named.MapCastWf.
+Require Import Crypto.Compilers.Named.InterpretToPHOASInterp.
+Require Import Crypto.Compilers.Named.CompileInterp.
+Require Import Crypto.Compilers.Named.CompileWf.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
+Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.MapCastByDeBruijn.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v
index 4fd3975f7..7bc58042f 100644
--- a/src/Reflection/MapCastByDeBruijnWf.v
+++ b/src/Compilers/MapCastByDeBruijnWf.v
@@ -1,16 +1,16 @@
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.MapCastWf.
-Require Import Crypto.Reflection.Named.InterpretToPHOASWf.
-Require Import Crypto.Reflection.Named.CompileWf.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
-Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.MapCastByDeBruijn.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.MapCastWf.
+Require Import Crypto.Compilers.Named.InterpretToPHOASWf.
+Require Import Crypto.Compilers.Named.CompileWf.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
+Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.MapCastByDeBruijn.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
diff --git a/src/Reflection/MapCastInterp.v b/src/Compilers/MapCastInterp.v
index 528e69e12..bbf4581b5 100644
--- a/src/Reflection/MapCastInterp.v
+++ b/src/Compilers/MapCastInterp.v
@@ -1,11 +1,11 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.MapCast.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.WfInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.MapCast.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.WfInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/MapCastWf.v b/src/Compilers/MapCastWf.v
index 54e8d0020..2961b9426 100644
--- a/src/Reflection/MapCastWf.v
+++ b/src/Compilers/MapCastWf.v
@@ -1,10 +1,10 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.MapCast.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.WfInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.MapCast.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.WfInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/MultiSizeTest.v b/src/Compilers/MultiSizeTest.v
index 2c7975113..fab0c65d8 100644
--- a/src/Reflection/MultiSizeTest.v
+++ b/src/Compilers/MultiSizeTest.v
@@ -1,5 +1,5 @@
 Require Import Coq.omega.Omega.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.SmartMap.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Compilers/MultiSizeTest2.v
index 4bac3d14c..eac196510 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Compilers/MultiSizeTest2.v
@@ -1,7 +1,7 @@
 Require Import Coq.omega.Omega.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.BoundByCast.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.BoundByCast.
 
 (** * Preliminaries: bounded and unbounded number types *)
 
diff --git a/src/Reflection/Named/Compile.v b/src/Compilers/Named/Compile.v
index 55f4aba70..bee71cea5 100644
--- a/src/Reflection/Named/Compile.v
+++ b/src/Compilers/Named/Compile.v
@@ -1,7 +1,7 @@
 (** * PHOAS → Named Representation of Gallina *)
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Syntax.
 
 Local Notation eta x := (fst x, snd x).
 
diff --git a/src/Reflection/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v
index 100d53aa3..1c7e42258 100644
--- a/src/Reflection/Named/CompileInterp.v
+++ b/src/Compilers/Named/CompileInterp.v
@@ -1,13 +1,13 @@
 (** * PHOAS → Named Representation of Gallina *)
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Named.NameUtilProperties.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.NameUtil.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Named.Compile.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Named.NameUtilProperties.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.NameUtil.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Named.Compile.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Decidable.
diff --git a/src/Reflection/Named/CompileProperties.v b/src/Compilers/Named/CompileProperties.v
index 357004197..9803946b2 100644
--- a/src/Reflection/Named/CompileProperties.v
+++ b/src/Compilers/Named/CompileProperties.v
@@ -1,11 +1,11 @@
 Require Import Coq.omega.Omega.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Named.NameUtilProperties.
-Require Import Crypto.Reflection.Named.Compile.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Named.NameUtilProperties.
+Require Import Crypto.Compilers.Named.Compile.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.CountLets.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Named/CompileWf.v b/src/Compilers/Named/CompileWf.v
index 5fb17b18d..aea8cb2b1 100644
--- a/src/Reflection/Named/CompileWf.v
+++ b/src/Compilers/Named/CompileWf.v
@@ -1,14 +1,14 @@
 (** * PHOAS → Named Representation of Gallina *)
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.NameUtil.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Named.NameUtilProperties.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Named.Compile.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.NameUtil.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Named.NameUtilProperties.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Named.Compile.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v
index c63142de6..6e1a3e64a 100644
--- a/src/Reflection/Named/ContextDefinitions.v
+++ b/src/Compilers/Named/ContextDefinitions.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Decidable.
 
diff --git a/src/Reflection/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v
index d32911283..6c06d3fbe 100644
--- a/src/Reflection/Named/ContextOn.v
+++ b/src/Compilers/Named/ContextOn.v
@@ -1,5 +1,5 @@
 (** * Transfer [Context] across an injection *)
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 
 Section language.
   Context {base_type_code Name1 Name2 : Type}
diff --git a/src/Reflection/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v
index c031d0af2..c2a9ca828 100644
--- a/src/Reflection/Named/ContextProperties.v
+++ b/src/Compilers/Named/ContextProperties.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.Tactics.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.Tactics.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
diff --git a/src/Reflection/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v
index 4853f9a41..96653ac99 100644
--- a/src/Reflection/Named/ContextProperties/NameUtil.v
+++ b/src/Compilers/Named/ContextProperties/NameUtil.v
@@ -1,13 +1,13 @@
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.FixCoqMistakes.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Named.NameUtilProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.Tactics.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Named.NameUtilProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.Tactics.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Named/ContextProperties/SmartMap.v b/src/Compilers/Named/ContextProperties/SmartMap.v
index 89d0d1c5d..7cf761a34 100644
--- a/src/Reflection/Named/ContextProperties/SmartMap.v
+++ b/src/Compilers/Named/ContextProperties/SmartMap.v
@@ -1,10 +1,10 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.Tactics.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.Tactics.
 Require Import Crypto.Util.Decidable.
 
 Section with_context.
diff --git a/src/Reflection/Named/ContextProperties/Tactics.v b/src/Compilers/Named/ContextProperties/Tactics.v
index 91d6d20d2..9616725d6 100644
--- a/src/Reflection/Named/ContextProperties/Tactics.v
+++ b/src/Compilers/Named/ContextProperties/Tactics.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v
index d97c36742..312370834 100644
--- a/src/Reflection/Named/DeadCodeElimination.v
+++ b/src/Compilers/Named/DeadCodeElimination.v
@@ -1,12 +1,12 @@
 (** * PHOAS → Named Representation of Gallina *)
 Require Import Coq.PArith.BinPos Coq.Lists.List.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Compile.
-Require Import Crypto.Reflection.Named.RegisterAssign.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.EstablishLiveness.
-Require Import Crypto.Reflection.CountLets.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Compile.
+Require Import Crypto.Compilers.Named.RegisterAssign.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.EstablishLiveness.
+Require Import Crypto.Compilers.CountLets.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.LetIn.
 
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Compilers/Named/EstablishLiveness.v
index 7509d5f7a..5d1255af3 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Compilers/Named/EstablishLiveness.v
@@ -1,9 +1,9 @@
 (** * Compute a list of liveness values for each binding *)
 Require Import Coq.Lists.List.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.CountLets.
 Require Import Crypto.Util.ListUtil.
 
 Local Notation eta x := (fst x, snd x).
diff --git a/src/Reflection/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v
index e01186f2c..1ea45cbbe 100644
--- a/src/Reflection/Named/FMapContext.v
+++ b/src/Compilers/Named/FMapContext.v
@@ -1,8 +1,8 @@
 Require Import Coq.Bool.Sumbool.
 Require Import Coq.FSets.FMapInterface.
 Require Import Coq.FSets.FMapFacts.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Equality.
 
diff --git a/src/Reflection/Named/IdContext.v b/src/Compilers/Named/IdContext.v
index c2a6936f8..5ed1e7cf2 100644
--- a/src/Reflection/Named/IdContext.v
+++ b/src/Compilers/Named/IdContext.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 
 Section language.
   Context {base_type_code Name}
diff --git a/src/Reflection/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v
index a9a44a93f..dc737a38d 100644
--- a/src/Reflection/Named/InterpretToPHOAS.v
+++ b/src/Compilers/Named/InterpretToPHOAS.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.PointedProp.
 
 Local Notation eta_and x := (conj (let (a, b) := x in a) (let (a, b) := x in b)).
diff --git a/src/Reflection/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v
index 4f66e94d4..0772721f6 100644
--- a/src/Reflection/Named/InterpretToPHOASInterp.v
+++ b/src/Compilers/Named/InterpretToPHOASInterp.v
@@ -1,10 +1,10 @@
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.InterpretToPHOAS.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.InterpretToPHOAS.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/Named/InterpretToPHOASWf.v b/src/Compilers/Named/InterpretToPHOASWf.v
index daab24b62..c0e59d10e 100644
--- a/src/Reflection/Named/InterpretToPHOASWf.v
+++ b/src/Compilers/Named/InterpretToPHOASWf.v
@@ -1,11 +1,11 @@
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.SmartMap.
-Require Import Crypto.Reflection.Named.InterpretToPHOAS.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
+Require Import Crypto.Compilers.Named.InterpretToPHOAS.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/Named/MapCast.v b/src/Compilers/Named/MapCast.v
index a0b161a0a..83c477765 100644
--- a/src/Reflection/Named/MapCast.v
+++ b/src/Compilers/Named/MapCast.v
@@ -1,7 +1,7 @@
 Require Import Coq.Bool.Sumbool.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 
 Local Open Scope nexpr_scope.
 Section language.
diff --git a/src/Reflection/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v
index b7afa1494..f3842e691 100644
--- a/src/Reflection/Named/MapCastInterp.v
+++ b/src/Compilers/Named/MapCastInterp.v
@@ -1,13 +1,13 @@
 Require Import Coq.Bool.Sumbool.
 Require Import Coq.Logic.Eqdep_dec.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.SmartMap.
-Require Import Crypto.Reflection.Named.MapCast.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
+Require Import Crypto.Compilers.Named.MapCast.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Option.
diff --git a/src/Reflection/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v
index f05df34c1..cd8a2e720 100644
--- a/src/Reflection/Named/MapCastWf.v
+++ b/src/Compilers/Named/MapCastWf.v
@@ -1,14 +1,14 @@
 Require Import Coq.Bool.Sumbool.
 Require Import Coq.Logic.Eqdep_dec.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.ContextDefinitions.
-Require Import Crypto.Reflection.Named.ContextProperties.
-Require Import Crypto.Reflection.Named.ContextProperties.SmartMap.
-Require Import Crypto.Reflection.Named.Wf.
-Require Import Crypto.Reflection.Named.MapCast.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.ContextDefinitions.
+Require Import Crypto.Compilers.Named.ContextProperties.
+Require Import Crypto.Compilers.Named.ContextProperties.SmartMap.
+Require Import Crypto.Compilers.Named.Wf.
+Require Import Crypto.Compilers.Named.MapCast.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
diff --git a/src/Reflection/Named/NameUtil.v b/src/Compilers/Named/NameUtil.v
index 5356cd132..8b099ffdf 100644
--- a/src/Reflection/Named/NameUtil.v
+++ b/src/Compilers/Named/NameUtil.v
@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 
 Local Open Scope core_scope.
 Local Notation eta x := (fst x, snd x).
diff --git a/src/Reflection/Named/NameUtilProperties.v b/src/Compilers/Named/NameUtilProperties.v
index 9a52ff49d..d2791a5ea 100644
--- a/src/Reflection/Named/NameUtilProperties.v
+++ b/src/Compilers/Named/NameUtilProperties.v
@@ -1,9 +1,9 @@
 Require Import Coq.omega.Omega.
 Require Import Coq.Arith.Arith.
 Require Import Coq.Lists.List.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.CountLets.
-Require Import Crypto.Reflection.Named.NameUtil.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.CountLets.
+Require Import Crypto.Compilers.Named.NameUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.SplitInContext.
diff --git a/src/Reflection/Named/PositiveContext.v b/src/Compilers/Named/PositiveContext.v
index 4356a174a..8291c8acf 100644
--- a/src/Reflection/Named/PositiveContext.v
+++ b/src/Compilers/Named/PositiveContext.v
@@ -1,6 +1,6 @@
 Require Import Coq.FSets.FMapPositive.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.FMapContext.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.FMapContext.
 
 Module PositiveContext := FMapContext PositiveMap.
 Notation PositiveContext := PositiveContext.FMapContext.
diff --git a/src/Reflection/Named/PositiveContext/Defaults.v b/src/Compilers/Named/PositiveContext/Defaults.v
index 34ce169f2..7e0c011f1 100644
--- a/src/Reflection/Named/PositiveContext/Defaults.v
+++ b/src/Compilers/Named/PositiveContext/Defaults.v
@@ -1,8 +1,8 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.CountLets.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/Named/PositiveContext/DefaultsProperties.v b/src/Compilers/Named/PositiveContext/DefaultsProperties.v
index 435a4c74c..2b46de136 100644
--- a/src/Reflection/Named/PositiveContext/DefaultsProperties.v
+++ b/src/Compilers/Named/PositiveContext/DefaultsProperties.v
@@ -1,10 +1,10 @@
 Require Import Coq.Lists.List.
 Require Import Coq.Numbers.BinNums.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.CountLets.
-Require Import Crypto.Reflection.Named.NameUtil.
-Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.CountLets.
+Require Import Crypto.Compilers.Named.NameUtil.
+Require Import Crypto.Compilers.Named.PositiveContext.Defaults.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.NatUtil.
diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Compilers/Named/RegisterAssign.v
index 18e15519a..d1e871fd0 100644
--- a/src/Reflection/Named/RegisterAssign.v
+++ b/src/Compilers/Named/RegisterAssign.v
@@ -1,8 +1,8 @@
 (** * Reassign registers *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.NameUtil.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.NameUtil.
 Require Import Crypto.Util.Decidable.
 
 Local Notation eta x := (fst x, snd x).
diff --git a/src/Reflection/Named/SmartMap.v b/src/Compilers/Named/SmartMap.v
index 3cacf7a1b..76b2eec58 100644
--- a/src/Reflection/Named/SmartMap.v
+++ b/src/Compilers/Named/SmartMap.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Syntax.
 
 Module Export Named.
   Section language.
diff --git a/src/Reflection/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index b4846be9a..c58fcc9d1 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -1,7 +1,7 @@
 (** * Named Representation of Gallina *)
 Require Import Coq.Classes.RelationClasses.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tuple.
 (*Require Import Crypto.Util.Tactics.*)
diff --git a/src/Reflection/Named/Wf.v b/src/Compilers/Named/Wf.v
index 6b1e68e65..df2213b21 100644
--- a/src/Reflection/Named/Wf.v
+++ b/src/Compilers/Named/Wf.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Util.PointedProp.
 
 Module Export Named.
diff --git a/src/Reflection/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v
index c5fe2bb3a..b44811b06 100644
--- a/src/Reflection/Named/WfInterp.v
+++ b/src/Compilers/Named/WfInterp.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
diff --git a/src/Reflection/Reify.v b/src/Compilers/Reify.v
index adc3feec8..bfe94d857 100644
--- a/src/Reflection/Reify.v
+++ b/src/Compilers/Reify.v
@@ -2,9 +2,9 @@
 (** The reification procedure goes through [InputSyntax], which allows
     judgmental equality of the denotation of the reified term. *)
 Require Import Coq.Strings.String.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.InputSyntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.InputSyntax.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.DebugPrint.
 (*Require Import Crypto.Util.Tactics.PrintContext.*)
@@ -17,7 +17,7 @@ Require Import Crypto.Util.Tactics.TransparentAssert.
     more debugging. *)
 Ltac reify_debug_level := constr:(0).
 Module Import ReifyDebugNotations.
-  Export Reflection.Syntax.Notations.
+  Export Compilers.Syntax.Notations.
   Export Util.LetIn.
   Open Scope string_scope.
 End ReifyDebugNotations.
diff --git a/src/Reflection/Relations.v b/src/Compilers/Relations.v
index 9a927243d..27a101e4f 100644
--- a/src/Reflection/Relations.v
+++ b/src/Compilers/Relations.v
@@ -1,7 +1,7 @@
 Require Import Coq.Lists.List Coq.Classes.RelationClasses Coq.Classes.Morphisms.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SplitInContext.
diff --git a/src/Reflection/RenameBinders.v b/src/Compilers/RenameBinders.v
index cd40e4366..7be603cbe 100644
--- a/src/Reflection/RenameBinders.v
+++ b/src/Compilers/RenameBinders.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
 
 Ltac uncurry_f f :=
   let t := type of f in
diff --git a/src/Reflection/Rewriter.v b/src/Compilers/Rewriter.v
index b53d0903d..a23627480 100644
--- a/src/Reflection/Rewriter.v
+++ b/src/Compilers/Rewriter.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/RewriterInterp.v b/src/Compilers/RewriterInterp.v
index 4a18c0a47..1f9fa5bed 100644
--- a/src/Reflection/RewriterInterp.v
+++ b/src/Compilers/RewriterInterp.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Rewriter.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Rewriter.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 
 Section language.
diff --git a/src/Reflection/RewriterWf.v b/src/Compilers/RewriterWf.v
index a7ac86851..0dfdbaab6 100644
--- a/src/Reflection/RewriterWf.v
+++ b/src/Compilers/RewriterWf.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfInversion.
-Require Import Crypto.Reflection.Rewriter.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.Rewriter.
 
 Section language.
   Context {base_type_code : Type}
diff --git a/src/Reflection/SmartBound.v b/src/Compilers/SmartBound.v
index 56014c7b6..39fd34dd7 100644
--- a/src/Reflection/SmartBound.v
+++ b/src/Compilers/SmartBound.v
@@ -1,8 +1,8 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.SmartCast.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.SmartCast.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/SmartBoundInterp.v b/src/Compilers/SmartBoundInterp.v
index 0262ef615..bd43f36a8 100644
--- a/src/Reflection/SmartBoundInterp.v
+++ b/src/Compilers/SmartBoundInterp.v
@@ -1,20 +1,20 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.InterpWfRel.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.SmartMap.
-(*Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.BoundByCast.*)
-Require Import Crypto.Reflection.SmartBound.
-Require Import Crypto.Reflection.ExprInversion.
-(*Require Import Crypto.Reflection.SmartBoundWf.
-Require Import Crypto.Reflection.InlineCastInterp.
-Require Import Crypto.Reflection.InlineInterp.
-Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.MapCastInterp.
-Require Import Crypto.Reflection.MapCastWf.
-Require Import Crypto.Reflection.EtaInterp.*)
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InterpWfRel.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.SmartMap.
+(*Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.BoundByCast.*)
+Require Import Crypto.Compilers.SmartBound.
+Require Import Crypto.Compilers.ExprInversion.
+(*Require Import Crypto.Compilers.SmartBoundWf.
+Require Import Crypto.Compilers.InlineCastInterp.
+Require Import Crypto.Compilers.InlineInterp.
+Require Import Crypto.Compilers.LinearizeInterp.
+Require Import Crypto.Compilers.LinearizeWf.
+Require Import Crypto.Compilers.MapCastInterp.
+Require Import Crypto.Compilers.MapCastWf.
+Require Import Crypto.Compilers.EtaInterp.*)
 Require Import Crypto.Util.Tactics.DestructHead.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/SmartBoundWf.v b/src/Compilers/SmartBoundWf.v
index 72c5c1475..ae7f2c81f 100644
--- a/src/Reflection/SmartBoundWf.v
+++ b/src/Compilers/SmartBoundWf.v
@@ -1,12 +1,12 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.SmartBound.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.SmartCastWf.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.SmartBound.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.SmartCastWf.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
 
diff --git a/src/Reflection/SmartCast.v b/src/Compilers/SmartCast.v
index ee3712954..237907e9c 100644
--- a/src/Reflection/SmartCast.v
+++ b/src/Compilers/SmartCast.v
@@ -1,6 +1,6 @@
 Require Import Coq.Bool.Sumbool.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeUtil.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeUtil.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/SmartCastInterp.v b/src/Compilers/SmartCastInterp.v
index 92ca265e1..e755cd168 100644
--- a/src/Reflection/SmartCastInterp.v
+++ b/src/Compilers/SmartCastInterp.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.SmartCast.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.SmartCast.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/SmartCastWf.v b/src/Compilers/SmartCastWf.v
index 4c5601669..8ff630b77 100644
--- a/src/Reflection/SmartCastWf.v
+++ b/src/Compilers/SmartCastWf.v
@@ -1,8 +1,8 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfProofs.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.SmartCast.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfProofs.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.SmartCast.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Notations.
diff --git a/src/Reflection/SmartMap.v b/src/Compilers/SmartMap.v
index 934497f65..5dfa38a1a 100644
--- a/src/Reflection/SmartMap.v
+++ b/src/Compilers/SmartMap.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Notations.
diff --git a/src/Reflection/Syntax.v b/src/Compilers/Syntax.v
index d8b88e560..d8b88e560 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Compilers/Syntax.v
diff --git a/src/Reflection/TestCase.v b/src/Compilers/TestCase.v
index cf759d7e9..241fbd34b 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -1,18 +1,18 @@
 Require Import Coq.omega.Omega Coq.micromega.Psatz.
 Require Import Coq.PArith.BinPos Coq.Lists.List.
-Require Import Crypto.Reflection.Named.Syntax.
-Require Import Crypto.Reflection.Named.Compile.
-Require Import Crypto.Reflection.Named.RegisterAssign.
-Require Import Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Equality.
-Require Export Crypto.Reflection.Reify.
-Require Import Crypto.Reflection.InputSyntax.
-Require Import Crypto.Reflection.CommonSubexpressionElimination.
-Require Crypto.Reflection.Linearize Crypto.Reflection.Inline.
-Require Import Crypto.Reflection.WfReflective.
-Require Import Crypto.Reflection.Conversion.
+Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Compile.
+Require Import Crypto.Compilers.Named.RegisterAssign.
+Require Import Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Equality.
+Require Export Crypto.Compilers.Reify.
+Require Import Crypto.Compilers.InputSyntax.
+Require Import Crypto.Compilers.CommonSubexpressionElimination.
+Require Crypto.Compilers.Linearize Crypto.Compilers.Inline.
+Require Import Crypto.Compilers.WfReflective.
+Require Import Crypto.Compilers.Conversion.
 Require Import Crypto.Util.NatUtil.
 
 Import ReifyDebugNotations.
diff --git a/src/Reflection/Tuple.v b/src/Compilers/Tuple.v
index 519325b82..0ee0d8ae2 100644
--- a/src/Reflection/Tuple.v
+++ b/src/Compilers/Tuple.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Util.Tuple.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Reflection/TypeInversion.v b/src/Compilers/TypeInversion.v
index 2138a3788..ab00a1dc5 100644
--- a/src/Reflection/TypeInversion.v
+++ b/src/Compilers/TypeInversion.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.FixCoqMistakes.
 
 Section language.
diff --git a/src/Reflection/TypeUtil.v b/src/Compilers/TypeUtil.v
index 8f7661bde..050374562 100644
--- a/src/Reflection/TypeUtil.v
+++ b/src/Compilers/TypeUtil.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.Notations.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/Wf.v b/src/Compilers/Wf.v
index 91a99b150..f3f653696 100644
--- a/src/Reflection/Wf.v
+++ b/src/Compilers/Wf.v
@@ -1,5 +1,5 @@
 Require Import Coq.Lists.List.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.Notations.
 
 Create HintDb wf discriminated.
diff --git a/src/Reflection/WfInversion.v b/src/Compilers/WfInversion.v
index d76fd90f4..79869e554 100644
--- a/src/Reflection/WfInversion.v
+++ b/src/Compilers/WfInversion.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Equality.
diff --git a/src/Reflection/WfProofs.v b/src/Compilers/WfProofs.v
index ca1f50478..ea06c8b89 100644
--- a/src/Reflection/WfProofs.v
+++ b/src/Compilers/WfProofs.v
@@ -1,8 +1,8 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfInversion.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.ExprInversion.
 Require Import Crypto.Util.Sigma Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.RewriteHyp.
diff --git a/src/Reflection/WfReflective.v b/src/Compilers/WfReflective.v
index c54537fa2..4ba6d7a53 100644
--- a/src/Reflection/WfReflective.v
+++ b/src/Compilers/WfReflective.v
@@ -48,10 +48,10 @@
       -> reified_Prop] *)
 
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.EtaWf.
-Require Import Crypto.Reflection.WfReflectiveGen.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.EtaWf.
+Require Import Crypto.Compilers.WfReflectiveGen.
 Require Import Crypto.Util.Notations Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
diff --git a/src/Reflection/WfReflectiveGen.v b/src/Compilers/WfReflectiveGen.v
index 23cdd8691..4de378451 100644
--- a/src/Reflection/WfReflectiveGen.v
+++ b/src/Compilers/WfReflectiveGen.v
@@ -48,10 +48,10 @@
       -> option pointed_Prop] *)
 
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
-Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Util.Notations Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
 Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Compilers.Wf.
 Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *)
 Require Export Crypto.Util.FixCoqMistakes.
 
diff --git a/src/Reflection/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 821ef8459..b2621c625 100644
--- a/src/Reflection/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -1,8 +1,8 @@
 (** * SimplifyArith: Remove things like (_ * 1), (_ + 0), etc *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Rewriter.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Rewriter.
+Require Import Crypto.Compilers.Z.Syntax.
 
 Section language.
   Local Notation exprf := (@exprf base_type op).
diff --git a/src/Reflection/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index 0c77d8179..6eec2f2a4 100644
--- a/src/Reflection/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -1,14 +1,14 @@
 Require Import Coq.micromega.Psatz.
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.RewriterInterp.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.OpInversion.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifier.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifierUtil.
-Require Import Crypto.Reflection.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.RewriterInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.OpInversion.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/Z/ArithmeticSimplifierUtil.v b/src/Compilers/Z/ArithmeticSimplifierUtil.v
index 10cf87eaa..49d3a2257 100644
--- a/src/Reflection/Z/ArithmeticSimplifierUtil.v
+++ b/src/Compilers/Z/ArithmeticSimplifierUtil.v
@@ -1,5 +1,5 @@
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifier.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
 
 (** ** Equality for [inverted_expr] *)
 Section inverted_expr.
diff --git a/src/Reflection/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index 70e47f24f..24a9b4d23 100644
--- a/src/Reflection/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -1,13 +1,13 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfInversion.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.ExprInversion.
-Require Import Crypto.Reflection.RewriterWf.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.OpInversion.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifier.
-Require Import Crypto.Reflection.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfInversion.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.ExprInversion.
+Require Import Crypto.Compilers.RewriterWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.OpInversion.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sum.
diff --git a/src/Reflection/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 32a993e08..f26364329 100644
--- a/src/Reflection/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -1,5 +1,5 @@
-Require Export Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
 Require Export Bedrock.Word.
 Require Export Crypto.Util.Notations.
 
diff --git a/src/Reflection/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index 69670bee0..b9880f097 100644
--- a/src/Reflection/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -1,12 +1,12 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.Tactics.DestructHead.
-Export Reflection.Syntax.Notations.
+Export Compilers.Syntax.Notations.
 
 Local Notation eta x := (fst x, snd x).
 Local Notation eta3 x := (eta (fst x), snd x).
diff --git a/src/Reflection/Z/Bounds/InterpretationLemmas.v b/src/Compilers/Z/Bounds/InterpretationLemmas.v
index 11a6ea91e..7a1c2bc73 100644
--- a/src/Reflection/Z/Bounds/InterpretationLemmas.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas.v
@@ -1,10 +1,10 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Psatz.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.FixedWordSizesEquality.
diff --git a/src/Reflection/Z/Bounds/MapCastByDeBruijn.v b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v
index d99133e51..45b084566 100644
--- a/src/Reflection/Z/Bounds/MapCastByDeBruijn.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijn.v
@@ -1,8 +1,8 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.MapCastByDeBruijn.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 
 Section language.
   Context {t : type base_type}.
diff --git a/src/Reflection/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
index a7dc016bd..46f472311 100644
--- a/src/Reflection/Z/Bounds/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
@@ -1,13 +1,13 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Z.MapCastByDeBruijnInterp.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.Z.Bounds.InterpretationLemmas.
-Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.
+Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
 
 Lemma MapCastCorrect
       {t} (e : Expr base_type op t)
diff --git a/src/Reflection/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
index 57b45f68a..04d1f964e 100644
--- a/src/Reflection/Z/Bounds/MapCastByDeBruijnWf.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
@@ -1,13 +1,13 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.Z.MapCastByDeBruijnWf.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.Z.Bounds.InterpretationLemmas.
-Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Z.MapCastByDeBruijnWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.
+Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
 
 Definition Wf_MapCast
            {t} (e : Expr base_type op t)
diff --git a/src/Reflection/Z/Bounds/Pipeline.v b/src/Compilers/Z/Bounds/Pipeline.v
index 11bce1444..6c9cda840 100644
--- a/src/Reflection/Z/Bounds/Pipeline.v
+++ b/src/Compilers/Z/Bounds/Pipeline.v
@@ -1,6 +1,6 @@
 (** * Reflective Pipeline *)
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.Glue.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.ReflectiveTactics.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.Glue.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.ReflectiveTactics.
 (** This file combines the various PHOAS modules in tactics,
     culminating in a tactic [refine_reflectively], which solves a goal of the form
 <<
diff --git a/src/Reflection/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index 98d3078c3..ae3401b78 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -1,7 +1,7 @@
 (** * Reflective Pipeline: Main Pipeline Definition *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.OutputType.
 (** This file contains the definitions of the assembling of the
     various transformations that are used in the pipeline.  There are
     two stages to the reflective pipeline, with different
@@ -24,10 +24,10 @@ Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
 
 (** ** Pre-Wf Stage *)
 (** *** Pre-Wf Pipeline Imports *)
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.EtaInterp.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifier.
-Require Import Crypto.Reflection.Z.ArithmeticSimplifierInterp.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.EtaInterp.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifier.
+Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp.
 
 (** *** Definition of the Pre-Wf Pipeline *)
 (** Do not change the name or the type of this definition *)
@@ -51,17 +51,17 @@ Qed.
 
 (** ** Post-Wf Stage *)
 (** *** Post-Wf Pipeline Imports *)
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.EtaWf.
-Require Import Crypto.Reflection.Z.Inline.
-Require Import Crypto.Reflection.Z.InlineInterp.
-Require Import Crypto.Reflection.Z.InlineWf.
-Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijn.
-Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnInterp.
-Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnWf.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.EtaWf.
+Require Import Crypto.Compilers.Z.Inline.
+Require Import Crypto.Compilers.Z.InlineInterp.
+Require Import Crypto.Compilers.Z.InlineWf.
+Require Import Crypto.Compilers.Linearize.
+Require Import Crypto.Compilers.LinearizeInterp.
+Require Import Crypto.Compilers.LinearizeWf.
+Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp.
+Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf.
 Require Import Crypto.Util.Sigma.MapProjections.
 
 (** *** Definition of the Post-Wf Pipeline *)
@@ -85,10 +85,10 @@ Definition PostWfPipeline
 
 (** *** Correctness proof of the Pre-Wf Pipeline *)
 (** Do not change the statement of this lemma. *)
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.Equality.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Z.Syntax.Util.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.Equality.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Z.Syntax.Util.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Compilers/Z/Bounds/Pipeline/Glue.v
index 8219a6fb6..5aa22e106 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Glue.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Glue.v
@@ -1,12 +1,12 @@
 (** * Reflective Pipeline: Glue Code *)
 (** This file defines the tactics that transform a non-reflective goal
     into a goal the that the reflective machinery can handle. *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Reify.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Reify.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Reify.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Reify.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Curry.
 Require Import Crypto.Util.FixedWordSizes.
@@ -20,7 +20,7 @@ Require Import Crypto.Util.Tactics.PrintContext.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 
 Module Export Exports.
-  Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
+  Export Crypto.Compilers.Z.Reify. (* export for the tactic redefinitions *)
 End Exports.
 
 (** ** [reassoc_sig_and_eexists] *)
diff --git a/src/Reflection/Z/Bounds/Pipeline/OutputType.v b/src/Compilers/Z/Bounds/Pipeline/OutputType.v
index 301ee9e9c..8205ef70c 100644
--- a/src/Reflection/Z/Bounds/Pipeline/OutputType.v
+++ b/src/Compilers/Z/Bounds/Pipeline/OutputType.v
@@ -1,10 +1,10 @@
 (** * Definition of the output type of the post-Wf pipeline *)
 (** Do not change these definitions unless you're hacking on the
     entire reflective pipeline tactic automation. *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
 Local Notation pick_typeb := Bounds.bounds_to_base_type (only parsing).
diff --git a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index b082353da..3586cc78d 100644
--- a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -10,19 +10,19 @@
     reflective machinery itself, or if you find bugs or slowness. *)
 (** ** Preamble *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfReflective.
-Require Import Crypto.Reflection.RenameBinders.
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.EtaInterp.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.Z.Bounds.Relax.
-Require Import Crypto.Reflection.Reify.
-Require Import Crypto.Reflection.Z.Reify.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfReflective.
+Require Import Crypto.Compilers.RenameBinders.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.EtaInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Z.Bounds.Relax.
+Require Import Crypto.Compilers.Reify.
+Require Import Crypto.Compilers.Z.Reify.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.SubstLet.
 Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity.
@@ -44,9 +44,9 @@ Require Import Bedrock.Word.
     v)] which has been transformed by the reflective pipeline. *)
 
 Module Export Exports.
-  Export Crypto.Reflection.Reify. (* export for the instances for recursing under binders *)
-  Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
-  Export Crypto.Reflection.Z.Bounds.Pipeline.Definition.Exports.
+  Export Crypto.Compilers.Reify. (* export for the instances for recursing under binders *)
+  Export Crypto.Compilers.Z.Reify. (* export for the tactic redefinitions *)
+  Export Crypto.Compilers.Z.Bounds.Pipeline.Definition.Exports.
 End Exports.
 
 (** ** Reification *)
@@ -129,21 +129,21 @@ Ltac unify_abstract_cbv_interp_rhs_reflexivity :=
     and add extra equality hypotheses to minimize the work we have to
     do in Ltac. *)
 (** *** Gallina assembly imports *)
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.WfReflectiveGen.
-Require Import Crypto.Reflection.WfReflective.
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.EtaWf.
-Require Import Crypto.Reflection.EtaInterp.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Equality.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
-Require Import Crypto.Reflection.Z.Bounds.Relax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.WfReflectiveGen.
+Require Import Crypto.Compilers.WfReflective.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.EtaWf.
+Require Import Crypto.Compilers.EtaInterp.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.OutputType.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Z.Bounds.Relax.
 Require Import Crypto.Util.PartiallyReifiedProp.
 Require Import Crypto.Util.Equality.
 
diff --git a/src/Reflection/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v
index e77ef423a..40b678071 100644
--- a/src/Reflection/Z/Bounds/Relax.v
+++ b/src/Compilers/Z/Bounds/Relax.v
@@ -1,13 +1,13 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Equality.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.Z.Bounds.Interpretation.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.Z.Bounds.Interpretation.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.BreakMatch.
diff --git a/src/Reflection/Z/CNotations.v b/src/Compilers/Z/CNotations.v
index 77220a7bf..8ec885db3 100644
--- a/src/Reflection/Z/CNotations.v
+++ b/src/Compilers/Z/CNotations.v
@@ -1,6 +1,6 @@
-Require Export Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Export Crypto.Reflection.Z.HexNotationConstants.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Export Crypto.Compilers.Z.HexNotationConstants.
 Require Export Crypto.Util.Notations.
 
 Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T  x  =  A ; '//' b").
diff --git a/src/Reflection/Z/FoldTypes.v b/src/Compilers/Z/FoldTypes.v
index 776f000f5..fc6aa9406 100644
--- a/src/Reflection/Z/FoldTypes.v
+++ b/src/Compilers/Z/FoldTypes.v
@@ -1,7 +1,7 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.FoldTypes.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.FoldTypes.
 
 Section min_or_max.
   Context (f : base_type -> base_type -> base_type)
diff --git a/src/Reflection/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 8c03945cb..a5fb9b757 100644
--- a/src/Reflection/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -1,6 +1,6 @@
 Require Import Coq.ZArith.ZArith.
-Require Export Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
 Require Export Bedrock.Word.
 Require Export Crypto.Util.Notations.
 
diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v
new file mode 100644
index 000000000..8a8bea98b
--- /dev/null
+++ b/src/Compilers/Z/Inline.v
@@ -0,0 +1,7 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Inline.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+
+Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t
+  := @InlineConst base_type op (is_const) t e.
diff --git a/src/Reflection/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v
index e3fc9b45d..c02197331 100644
--- a/src/Reflection/Z/InlineInterp.v
+++ b/src/Compilers/Z/InlineInterp.v
@@ -1,8 +1,8 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.InlineInterp.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Inline.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Inline.
 
 Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e)
   : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x
diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v
new file mode 100644
index 000000000..32b84aa1f
--- /dev/null
+++ b/src/Compilers/Z/InlineWf.v
@@ -0,0 +1,11 @@
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.InlineWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Inline.
+
+Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
+  : Wf (InlineConst e)
+  := @Wf_InlineConst _ _ _ t e Hwf.
+
+Hint Resolve Wf_InlineConst : wf.
diff --git a/src/Reflection/Z/JavaNotations.v b/src/Compilers/Z/JavaNotations.v
index 0a28387df..bab120b0a 100644
--- a/src/Reflection/Z/JavaNotations.v
+++ b/src/Compilers/Z/JavaNotations.v
@@ -1,6 +1,6 @@
-Require Export Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Export Crypto.Reflection.Z.HexNotationConstants.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Export Crypto.Compilers.Z.HexNotationConstants.
 Require Export Crypto.Util.Notations.
 
 Reserved Notation "T x = A ; b" (at level 200, b at level 200, format "T  x  =  A ; '//' b").
diff --git a/src/Reflection/Z/MapCastByDeBruijn.v b/src/Compilers/Z/MapCastByDeBruijn.v
index 4ccfe6d2d..1985653d4 100644
--- a/src/Reflection/Z/MapCastByDeBruijn.v
+++ b/src/Compilers/Z/MapCastByDeBruijn.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.MapCastByDeBruijn.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Z.Syntax.
 
 Section language.
   Context {interp_base_type_bounds : base_type -> Type}
diff --git a/src/Reflection/Z/MapCastByDeBruijnInterp.v b/src/Compilers/Z/MapCastByDeBruijnInterp.v
index 6e57136ab..cd145c6fa 100644
--- a/src/Reflection/Z/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/MapCastByDeBruijnInterp.v
@@ -1,10 +1,10 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.MapCastByDeBruijnInterp.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.MapCastByDeBruijnInterp.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
 
 Section language.
   Context {interp_base_type_bounds : base_type -> Type}
diff --git a/src/Reflection/Z/MapCastByDeBruijnWf.v b/src/Compilers/Z/MapCastByDeBruijnWf.v
index 1173d8186..cce16e5fe 100644
--- a/src/Reflection/Z/MapCastByDeBruijnWf.v
+++ b/src/Compilers/Z/MapCastByDeBruijnWf.v
@@ -1,10 +1,10 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Relations.
-Require Import Crypto.Reflection.MapCastByDeBruijnWf.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.MapCastByDeBruijn.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.MapCastByDeBruijnWf.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.MapCastByDeBruijn.
 
 Section language.
   Context {interp_base_type_bounds : base_type -> Type}
diff --git a/src/Reflection/Z/OpInversion.v b/src/Compilers/Z/OpInversion.v
index 6b2cdd85b..58b00c538 100644
--- a/src/Reflection/Z/OpInversion.v
+++ b/src/Compilers/Z/OpInversion.v
@@ -1,6 +1,6 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.Z.Syntax.
 
 Ltac invert_one_op e :=
   preinvert_one_type e;
diff --git a/src/Compilers/Z/Reify.v b/src/Compilers/Z/Reify.v
new file mode 100644
index 000000000..44ac44a03
--- /dev/null
+++ b/src/Compilers/Z/Reify.v
@@ -0,0 +1,50 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Compilers.InputSyntax.
+Require Import Crypto.Compilers.Z.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.Equality.
+Require Import Crypto.Compilers.Z.Syntax.Util.
+Require Import Crypto.Compilers.WfReflective.
+Require Import Crypto.Compilers.Reify.
+Require Import Crypto.Compilers.Inline.
+Require Import Crypto.Compilers.InlineInterp.
+Require Import Crypto.Compilers.Linearize.
+Require Import Crypto.Compilers.LinearizeInterp.
+Require Import Crypto.Compilers.Eta.
+Require Import Crypto.Compilers.EtaInterp.
+
+Ltac base_reify_op op op_head extra ::=
+     lazymatch op_head with
+     | @Z.add => constr:(reify_op op op_head 2 (Add TZ TZ TZ))
+     | @Z.mul => constr:(reify_op op op_head 2 (Mul TZ TZ TZ))
+     | @Z.sub => constr:(reify_op op op_head 2 (Sub TZ TZ TZ))
+     | @Z.shiftl => constr:(reify_op op op_head 2 (Shl TZ TZ TZ))
+     | @Z.shiftr => constr:(reify_op op op_head 2 (Shr TZ TZ TZ))
+     | @Z.land => constr:(reify_op op op_head 2 (Land TZ TZ TZ))
+     | @Z.lor => constr:(reify_op op op_head 2 (Lor TZ TZ TZ))
+     | @Z.opp => constr:(reify_op op op_head 1 (Opp TZ TZ))
+     end.
+Ltac base_reify_type T ::=
+     lazymatch T with
+     | Z => TZ
+     end.
+Ltac Reify' e := Compilers.Reify.Reify' base_type interp_base_type op e.
+Ltac Reify e :=
+  let v := Compilers.Reify.Reify base_type interp_base_type op make_const e in
+  constr:(ExprEta v).
+Ltac prove_ExprEta_Compile_correct :=
+  fun _
+  => intros;
+     rewrite ?InterpExprEta;
+     prove_compile_correct_using ltac:(fun _ => apply make_const_correct) ().
+
+Ltac Reify_rhs :=
+ Compilers.Reify.Reify_rhs_gen Reify prove_ExprEta_Compile_correct interp_op ltac:(fun tac => tac ()).
+
+Ltac prereify_context_variables :=
+ Compilers.Reify.prereify_context_variables interp_base_type.
+Ltac reify_context_variable :=
+ Compilers.Reify.reify_context_variable base_type interp_base_type op.
+Ltac lazy_reify_context_variable :=
+ Compilers.Reify.lazy_reify_context_variable base_type interp_base_type op.
+Ltac reify_context_variables :=
+ Compilers.Reify.reify_context_variables base_type interp_base_type op.
diff --git a/src/Reflection/Z/Syntax.v b/src/Compilers/Z/Syntax.v
index 58c55bc06..754b3fb5a 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Compilers/Z/Syntax.v
@@ -1,9 +1,9 @@
 (** * PHOAS Syntax for expression trees on ℤ *)
 Require Import Coq.ZArith.ZArith.
 Require Import Bedrock.Word.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeUtil.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeUtil.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.NatUtil. (* for nat_beq for equality schemes *)
diff --git a/src/Reflection/Z/Syntax/Equality.v b/src/Compilers/Z/Syntax/Equality.v
index 17822d7ec..10cd287be 100644
--- a/src/Reflection/Z/Syntax/Equality.v
+++ b/src/Compilers/Z/Syntax/Equality.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.Equality.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.Equality.
+Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.PartiallyReifiedProp.
 Require Import Crypto.Util.HProp.
diff --git a/src/Reflection/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index b5862c72f..6cf54a99c 100644
--- a/src/Reflection/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -1,9 +1,9 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.SmartMap.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.TypeUtil.
-Require Import Crypto.Reflection.TypeInversion.
-Require Import Crypto.Reflection.Z.Syntax.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Wf.
+Require Import Crypto.Compilers.TypeUtil.
+Require Import Crypto.Compilers.TypeInversion.
+Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Util.FixedWordSizesEquality.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.HProp.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/Curves/Edwards/AffineProofs.v
index d5fa958b4..2d1db7126 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/Curves/Edwards/AffineProofs.v
@@ -1,7 +1,6 @@
 Require Export Crypto.Spec.CompleteEdwardsCurve.
 
-Require Import Crypto.Algebra Crypto.Algebra Crypto.Util.Decidable.
-Require Import Crypto.CompleteEdwardsCurve.Pre.
+Require Import Crypto.Algebra.Hierarchy Crypto.Util.Decidable.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Relations.Relation_Definitions.
@@ -224,7 +223,7 @@ Module E.
             {nonsquare_d : forall x, not (Feq (Fmul x x) Fd)}.
 
     Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
-            {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
+            {fieldK: @Algebra.Hierarchy.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
             {Keq_dec:DecidableRel Keq}.
     Context {FtoK:F->K} {HFtoK:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                                      K Keq Kone Kadd Kmul FtoK}.
diff --git a/src/CompleteEdwardsCurve/EdwardsMontgomery.v b/src/Curves/Edwards/Montgomery.v
index f5a30ff88..d274356c9 100644
--- a/src/CompleteEdwardsCurve/EdwardsMontgomery.v
+++ b/src/Curves/Edwards/Montgomery.v
@@ -1,16 +1,16 @@
-Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurveTheorems.
-Require Import Crypto.MontgomeryCurve.
+Require Import Crypto.Curves.Edwards.AffineProofs.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.AffineProofs.
+Require Import Crypto.Curves.Montgomery.Affine.
 
 Require Import Crypto.Util.Notations Crypto.Util.Decidable.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Sum Crypto.Util.Prod.
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Import BinNums.
 
 Module E.
   Section EdwardsMontgomery.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {char_ge_28 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}
             {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -20,9 +20,9 @@ Module E.
     Local Notation "x ^ 2" := (x*x).
 
     Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
-    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
     Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
 
     Context {a d: F}
             {nonzero_a : a <> 0}
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/Curves/Edwards/Pre.v
index 4dfd01cfd..244acc9b5 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/Curves/Edwards/Pre.v
@@ -1,11 +1,11 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid Crypto.Util.Relations.
-Require Import Crypto.Algebra Crypto.Algebra.Ring Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.Ring Crypto.Algebra.Field.
 Require Import Crypto.Util.Notations Crypto.Util.Decidable (*Crypto.Util.Tactics*).
 Require Import Coq.PArith.BinPos.
 
 Section Edwards.
   Context {F eq zero one opp add sub mul inv div}
-          {field:@Algebra.field F eq zero one opp add sub mul inv div}
+          {field:@Algebra.Hierarchy.field F eq zero one opp add sub mul inv div}
           {eq_dec:DecidableRel eq}.
 
   Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/Curves/Edwards/XYZT.v
index f05a1d997..160866b64 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/Curves/Edwards/XYZT.v
@@ -1,17 +1,17 @@
 Require Import Coq.Classes.Morphisms.
 
-Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Import Crypto.Spec.CompleteEdwardsCurve Crypto.Curves.Edwards.AffineProofs.
 
-Require Import Crypto.Algebra Crypto.Algebra.
 Require Import Crypto.Util.Notations Crypto.Util.GlobalSettings.
 Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.UniquePose.
 
 Module Extended.
   Section ExtendedCoordinates.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
             {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -107,11 +107,11 @@ Module Extended.
         end.
       Next Obligation. pose proof (E.denominator_nonzero _ nonzero_a square_a _ nonsquare_d _ _ (proj2_sig (to_twisted P1))  _ _  (proj2_sig (to_twisted P2))); t. Qed.
 
-      Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : group /\ _ /\ _ :=
+      Program Definition _group_proof nonzero_a' square_a' nonsquare_d' : Algebra.Hierarchy.group /\ _ /\ _ :=
                  @Group.group_from_redundant_representation
                    _ _ _ _ _
                    ((E.edwards_curve_abelian_group(a:=a)(d:=d)(nonzero_a:=nonzero_a')(square_a:=square_a')
-                                                  (nonsquare_d:=nonsquare_d')).(abelian_group_group))
+                                                  (nonsquare_d:=nonsquare_d')).(Algebra.Hierarchy.abelian_group_group))
                    _
                    eq
                    m1add
@@ -130,7 +130,7 @@ Module Extended.
       Next Obligation. cbv [to_twisted opp]. t. Qed.
       Next Obligation. cbv [to_twisted zero]. t. Qed.
       Global Instance group x y z
-        : group := proj1 (_group_proof x y z).
+        : Algebra.Hierarchy.group := proj1 (_group_proof x y z).
       Global Instance homomorphism_from_twisted x y z :
         Monoid.is_homomorphism := proj1 (proj2 (_group_proof x y z)).
       Global Instance homomorphism_to_twisted x y z :
diff --git a/src/MontgomeryCurve.v b/src/Curves/Montgomery/Affine.v
index a04701ed5..721908a6a 100644
--- a/src/MontgomeryCurve.v
+++ b/src/Curves/Montgomery/Affine.v
@@ -1,4 +1,4 @@
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings.
 Require Import Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -8,7 +8,7 @@ Module M.
   Section MontgomeryCurve.
     Import BinNat.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
             {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/MontgomeryCurveTheorems.v b/src/Curves/Montgomery/AffineProofs.v
index 7f7ad5bdf..a83109a55 100644
--- a/src/MontgomeryCurveTheorems.v
+++ b/src/Curves/Montgomery/AffineProofs.v
@@ -1,22 +1,23 @@
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings.
 Require Import Crypto.Util.Sum Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
-Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions.
-Require Import Crypto.WeierstrassCurve.WeierstrassCurveTheorems.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine.
+Require Import Crypto.Curves.Weierstrass.AffineProofs.
 
 Module M.
   Section MontgomeryCurve.
     Import BinNat.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
             {char_ge_28:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 28}.
     Let char_ge_12 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12.
-    Proof. eapply char_ge_weaken; eauto. vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto. vm_decide. Qed.
     Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
       
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
@@ -63,7 +64,7 @@ Module M.
     Program Definition _MW (discr_nonzero:id _) : _ /\ _ /\ _ :=
       @Group.group_from_redundant_representation
         Wpoint W.eq Wadd W.zero Wopp
-        (abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero)))
+        (Algebra.Hierarchy.abelian_group_group (W.commutative_group(char_ge_12:=char_ge_12)(discriminant_nonzero:=discr_nonzero)))
         (@M.point F Feq Fadd Fmul a b) M.eq (M.add(char_ge_3:=char_ge_3)(b_nonzero:=b_nonzero)) M.zero (M.opp(b_nonzero:=b_nonzero))
         (M.of_Weierstrass(b_nonzero:=b_nonzero))
         (M.to_Weierstrass(b_nonzero:=b_nonzero))
@@ -75,7 +76,7 @@ Module M.
     Next Obligation. Proof. t; fsatz. Qed.
     Next Obligation. Proof. t; fsatz. Qed.
 
-    Global Instance group discr_nonzero : Algebra.group := proj1 (_MW discr_nonzero).
+    Global Instance group discr_nonzero : Algebra.Hierarchy.group := proj1 (_MW discr_nonzero).
     Global Instance homomorphism_of_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.of_Weierstrass) := proj1 (proj2 (_MW discr_nonzero)).
     Global Instance homomorphism_to_Weierstrass discr_nonzero : Monoid.is_homomorphism(phi:=M.to_Weierstrass) := proj2 (proj2 (_MW discr_nonzero)).
   End MontgomeryCurve.
diff --git a/src/MontgomeryX.v b/src/Curves/Montgomery/XZ.v
index 6cb5b2387..60020827c 100644
--- a/src/MontgomeryX.v
+++ b/src/Curves/Montgomery/XZ.v
@@ -1,13 +1,14 @@
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.GlobalSettings Crypto.Util.Notations.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
 
 Module M.
   Section MontgomeryCurve.
     Import BinNat.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
             {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -30,7 +31,7 @@ Module M.
       end.
 
     Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
-    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
 
     (* From Curve25519 paper by djb, appendix B. Credited to Montgomery *)
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
diff --git a/src/MontgomeryXProofs.v b/src/Curves/Montgomery/XZProofs.v
index f3f0346c9..d24d1398c 100644
--- a/src/MontgomeryXProofs.v
+++ b/src/Curves/Montgomery/XZProofs.v
@@ -1,12 +1,13 @@
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn.
-Require Import Crypto.Spec.MontgomeryCurve Crypto.MontgomeryCurve.
-Require Import Crypto.MontgomeryX BinPos.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Spec.MontgomeryCurve Crypto.Curves.Montgomery.Affine.
+Require Import Crypto.Curves.Montgomery.XZ BinPos.
 
 Module M.
   Section MontgomeryCurve.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
             {char_ge_5:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 5}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -17,7 +18,7 @@ Module M.
     Local Notation "( x , y )" := (inl (pair x y)).
 
     Let char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two)).
-    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
 
     Context {a b: F} {b_nonzero:b <> 0}.
     Context {a24:F} {a24_correct:(1+1+1+1)*a24 = a-(1+1)}.
diff --git a/src/WeierstrassCurve/Definitions.v b/src/Curves/Weierstrass/Affine.v
index fb400d8c8..90bb3bdbc 100644
--- a/src/WeierstrassCurve/Definitions.v
+++ b/src/Curves/Weierstrass/Affine.v
@@ -1,11 +1,11 @@
 Require Import Crypto.Spec.WeierstrassCurve.
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
 
 Module W.
   Section W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:DecidableRel Feq}.
 
     Program Definition opp (P:@W.point F Feq Fadd Fmul a b) : @W.point F Feq Fadd Fmul a b
diff --git a/src/WeierstrassCurve/WeierstrassCurveTheorems.v b/src/Curves/Weierstrass/AffineProofs.v
index bfc07814f..81583d88f 100644
--- a/src/WeierstrassCurve/WeierstrassCurveTheorems.v
+++ b/src/Curves/Weierstrass/AffineProofs.v
@@ -1,18 +1,18 @@
 Require Import Coq.Numbers.BinNums.
 Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Spec.WeierstrassCurve Crypto.WeierstrassCurve.Definitions.
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Spec.WeierstrassCurve Crypto.Curves.Weierstrass.Affine.
+Require Import Crypto.Algebra.Field Crypto.Algebra.Hierarchy.
 Require Import Crypto.Util.Decidable Crypto.Util.Tactics.DestructHead Crypto.Util.Tactics.BreakMatch.
 Require Import Coq.PArith.BinPos.
 
 Module W.
   Section W.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:DecidableRel Feq}
             {char_ge_12:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 12%positive}. (* FIXME: shouldn't need we need 4, not 12? *)
     Let char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul 3.
-    Proof. eapply char_ge_weaken; eauto; vm_decide. Qed.
+    Proof. eapply Algebra.Hierarchy.char_ge_weaken; eauto; vm_decide. Qed.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "-" := Fsub. Local Infix "*" := Fmul.
diff --git a/src/WeierstrassCurve/Pre.v b/src/Curves/Weierstrass/Pre.v
index 3b12bcfe1..6647d8e76 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/Curves/Weierstrass/Pre.v
@@ -1,5 +1,5 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
-Require Import Crypto.Algebra Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Field.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Notations.
@@ -10,7 +10,7 @@ Local Open Scope core_scope.
 
 Section Pre.
   Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-          {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+          {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
           {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
           {eq_dec: DecidableRel Feq}.
   Local Infix "=" := Feq. Local Notation "a <> b" := (not (a = b)).
diff --git a/src/WeierstrassCurve/Projective.v b/src/Curves/Weierstrass/Projective.v
index f07be0f36..20866ca5d 100644
--- a/src/WeierstrassCurve/Projective.v
+++ b/src/Curves/Weierstrass/Projective.v
@@ -10,7 +10,7 @@ Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.Sigma.
 Module Projective.
   Section Projective.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {a b:F}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}
             {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/BoundedArithmetic/ArchitectureToZLike.v b/src/LegacyArithmetic/ArchitectureToZLike.v
index b9e7109b9..19450f831 100644
--- a/src/BoundedArithmetic/ArchitectureToZLike.v
+++ b/src/LegacyArithmetic/ArchitectureToZLike.v
@@ -1,8 +1,8 @@
 (*** Implementing ℤ-Like via Architecture *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.Double.Core.
+Require Import Crypto.LegacyArithmetic.ZBounded.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.LetIn.
 
diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v
index e08624274..8d4b59ceb 100644
--- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
+++ b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v
@@ -1,12 +1,12 @@
 (*** Proving ℤ-Like via Architecture *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Multiply.
-Require Import Crypto.BoundedArithmetic.ArchitectureToZLike.
-Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.InterfaceProofs.
+Require Import Crypto.LegacyArithmetic.Double.Core.
+Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub.
+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.Tactics.UniquePose.
diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/LegacyArithmetic/BarretReduction.v
index c0f50b240..1be9361ba 100644
--- a/src/ModularArithmetic/BarrettReduction/ZBounded.v
+++ b/src/LegacyArithmetic/BarretReduction.v
@@ -2,8 +2,8 @@
 (** This file implements Barrett Reduction on [ZLikeOps].  We follow
     [BarretReduction/ZHandbook.v]. *)
 Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz.
-Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook.
-Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.Arithmetic.BarrettReduction.HAC.
+Require Import Crypto.LegacyArithmetic.ZBounded.
 Require Import Crypto.Util.ZUtil.
 (*Require Import Crypto.Util.Tactics.*)
 Require Import Crypto.Util.Notations.
diff --git a/src/BoundedArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v
index e870e62fb..a54bc483f 100644
--- a/src/BoundedArithmetic/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.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.FixCoqMistakes.
 Import Nat.
diff --git a/src/BoundedArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v
index 9eb694778..9a06109d1 100644
--- a/src/BoundedArithmetic/BaseSystemProofs.v
+++ b/src/LegacyArithmetic/BaseSystemProofs.v
@@ -1,8 +1,8 @@
 Require Import Coq.Lists.List Coq.micromega.Psatz.
-Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
-Require Import Crypto.BoundedArithmetic.BaseSystem.
+Require Import Crypto.LegacyArithmetic.BaseSystem.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Notations.
 Import Morphisms.
diff --git a/src/BoundedArithmetic/Double/Core.v b/src/LegacyArithmetic/Double/Core.v
index bf4de044d..b7be2d18a 100644
--- a/src/BoundedArithmetic/Double/Core.v
+++ b/src/LegacyArithmetic/Double/Core.v
@@ -1,15 +1,15 @@
 (*** Implementing Large Bounded Arithmetic via pairs *)
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.InterfaceProofs.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.LetIn.
 Import Bug5107WorkAround.
 
-Require Crypto.BoundedArithmetic.BaseSystem.
-Require Crypto.BoundedArithmetic.Pow2Base.
+Require Crypto.LegacyArithmetic.BaseSystem.
+Require Crypto.LegacyArithmetic.Pow2Base.
 
 Local Open Scope nat_scope.
 Local Open Scope Z_scope.
diff --git a/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v
index 9d5b409f8..0f07c6299 100644
--- a/src/BoundedArithmetic/Double/Proofs/BitwiseOr.v
+++ b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+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.Tactics.BreakMatch.
 
diff --git a/src/BoundedArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v
index 04c90e835..b5b6d6623 100644
--- a/src/BoundedArithmetic/Double/Proofs/Decode.v
+++ b/src/LegacyArithmetic/Double/Proofs/Decode.v
@@ -1,14 +1,14 @@
 Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
+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.ListUtil.
 Require Import Crypto.Util.Notations.
 
-Require Crypto.BoundedArithmetic.Pow2Base.
-Require Crypto.BoundedArithmetic.Pow2BaseProofs.
+Require Crypto.LegacyArithmetic.Pow2Base.
+Require Crypto.LegacyArithmetic.Pow2BaseProofs.
 
 Local Open Scope nat_scope.
 Local Open Scope type_scope.
@@ -71,7 +71,7 @@ Section decode.
   Qed.
   Global Instance tuple_decoder_O w : tuple_decoder (k := 1) w =~> decode w.
   Proof using Type.
-    cbv [tuple_decoder BoundedArithmetic.BaseSystem.decode BoundedArithmetic.BaseSystem.decode' BoundedArithmetic.BaseSystem.accumulate Pow2Base.base_from_limb_widths repeat].
+    cbv [tuple_decoder LegacyArithmetic.BaseSystem.decode LegacyArithmetic.BaseSystem.decode' LegacyArithmetic.BaseSystem.accumulate Pow2Base.base_from_limb_widths repeat].
     simpl; hnf; lia.
   Qed.
   Global Instance tuple_decoder_m1 w : tuple_decoder (k := 0) w =~> 0.
diff --git a/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
index 9c00b728f..2c7f87dd7 100644
--- a/src/BoundedArithmetic/Double/Proofs/LoadImmediate.v
+++ b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+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.
 
 Local Open Scope Z_scope.
diff --git a/src/BoundedArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v
index 6d2f72c25..8fed917d9 100644
--- a/src/BoundedArithmetic/Double/Proofs/Multiply.v
+++ b/src/LegacyArithmetic/Double/Proofs/Multiply.v
@@ -1,10 +1,10 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.SpreadLeftImmediate.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.RippleCarryAddSub.
+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.LegacyArithmetic.Double.Proofs.SpreadLeftImmediate.
+Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.SimplifyProjections.
 Require Import Crypto.Util.Notations.
diff --git a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
index 5d9443a91..e703c2e57 100644
--- a/src/BoundedArithmetic/Double/Proofs/RippleCarryAddSub.v
+++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+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.Tuple.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
diff --git a/src/BoundedArithmetic/Double/Proofs/SelectConditional.v b/src/LegacyArithmetic/Double/Proofs/SelectConditional.v
index 8dd12e0bc..953acf056 100644
--- a/src/BoundedArithmetic/Double/Proofs/SelectConditional.v
+++ b/src/LegacyArithmetic/Double/Proofs/SelectConditional.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.Double.Core.
+Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
 
 Section select_conditional.
   Context {n W}
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
index 759c05e6e..2230e36b6 100644
--- a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftLeftRightTactic.
+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.*)
 
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
index 997fb1937..41234bf6e 100644
--- a/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
@@ -1,5 +1,5 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.Interface.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.BreakMatch.
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v
index f2509927f..16e7c5d6a 100644
--- a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftLeftRightTactic.
+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.*)
 
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
index 7e9f5ddcd..00a6d03cd 100644
--- a/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftLeftRightTactic.
+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.*)
 
diff --git a/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v
index 84f24eef5..c50d43616 100644
--- a/src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v
+++ b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v
@@ -1,8 +1,8 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
-Require Import Crypto.BoundedArithmetic.InterfaceProofs.
-Require Import Crypto.BoundedArithmetic.Double.Core.
-Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+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.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.SpecializeBy.
diff --git a/src/BoundedArithmetic/Interface.v b/src/LegacyArithmetic/Interface.v
index 4a671eb4c..4a671eb4c 100644
--- a/src/BoundedArithmetic/Interface.v
+++ b/src/LegacyArithmetic/Interface.v
diff --git a/src/BoundedArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v
index 85120f50c..9ef97fa55 100644
--- a/src/BoundedArithmetic/InterfaceProofs.v
+++ b/src/LegacyArithmetic/InterfaceProofs.v
@@ -1,6 +1,6 @@
 (** * Alternate forms for Interface for bounded arithmetic *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.Interface.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.AutoRewrite.
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/LegacyArithmetic/MontgomeryReduction.v
index 7b52ce009..c3538dd01 100644
--- a/src/ModularArithmetic/Montgomery/ZBounded.v
+++ b/src/LegacyArithmetic/MontgomeryReduction.v
@@ -2,9 +2,9 @@
 (** This file implements Montgomery Form, Montgomery Reduction, and
     Montgomery Multiplication on [ZLikeOps].  We follow [Montgomery/Z.v]. *)
 Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz.
-Require Import Crypto.ModularArithmetic.Montgomery.Z.
-Require Import Crypto.ModularArithmetic.Montgomery.ZProofs.
-Require Import Crypto.ModularArithmetic.ZBounded.
+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.Tactics.Test.
 Require Import Crypto.Util.Tactics.Not.
@@ -37,7 +37,7 @@ Section montgomery.
   Definition partial_reduce : forall v : LargeT,
       { partial_reduce : SmallT
       | large_valid v
-        -> decode_small partial_reduce = Montgomery.Z.partial_reduce modulus small_bound (decode_small modulus') (decode_large v)
+        -> decode_small partial_reduce = MontgomeryReduction.Definition.partial_reduce modulus small_bound (decode_small modulus') (decode_large v)
            /\ small_valid partial_reduce }.
   Proof.
     intro T. evar (pr : SmallT); exists pr. intros T_valid.
@@ -48,7 +48,7 @@ Section montgomery.
     assert (0 <= modulus) by apply (modulus_nonneg _).
     assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega).
     rewrite <- partial_reduce_alt_eq by omega.
-    cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce].
+    cbv [MontgomeryReduction.Definition.partial_reduce MontgomeryReduction.Definition.partial_reduce_alt MontgomeryReduction.Definition.prereduce].
     pull_zlike_decode.
     cse.
     subst pr; split; [ reflexivity | exact _ ].
@@ -57,7 +57,7 @@ Section montgomery.
   Definition reduce_via_partial : forall v : LargeT,
       { reduce : SmallT
       | large_valid v
-        -> decode_small reduce = Montgomery.Z.reduce_via_partial modulus small_bound (decode_small modulus') (decode_large v)
+        -> decode_small reduce = MontgomeryReduction.Definition.reduce_via_partial modulus small_bound (decode_small modulus') (decode_large v)
            /\ small_valid reduce }.
   Proof.
     intro T. evar (pr : SmallT); exists pr. intros T_valid.
@@ -69,7 +69,7 @@ Section montgomery.
     assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega).
     unfold reduce_via_partial.
     rewrite <- partial_reduce_alt_eq by omega.
-    cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce].
+    cbv [MontgomeryReduction.Definition.partial_reduce MontgomeryReduction.Definition.partial_reduce_alt MontgomeryReduction.Definition.prereduce].
     pull_zlike_decode.
     cse.
     subst pr; split; [ reflexivity | exact _ ].
diff --git a/src/BoundedArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v
index 62f1f742d..62f1f742d 100644
--- a/src/BoundedArithmetic/Pow2Base.v
+++ b/src/LegacyArithmetic/Pow2Base.v
diff --git a/src/BoundedArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v
index fcb453ea6..8a38275dd 100644
--- a/src/BoundedArithmetic/Pow2BaseProofs.v
+++ b/src/LegacyArithmetic/Pow2BaseProofs.v
@@ -3,18 +3,18 @@ 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.Tactics.VerdiTactics.
+Require Import Crypto.LegacyArithmetic.VerdiTactics.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.BoundedArithmetic.Pow2Base.
+Require Import Crypto.LegacyArithmetic.Pow2Base.
 Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.Bool.
 Require Export Crypto.Util.FixCoqMistakes.
 Local Open Scope Z_scope.
 
-Require Crypto.BoundedArithmetic.BaseSystemProofs.
+Require Crypto.LegacyArithmetic.BaseSystemProofs.
 
 Create HintDb simpl_add_to_nth discriminated.
 Create HintDb push_upper_bound discriminated.
diff --git a/src/LegacyArithmetic/README.md b/src/LegacyArithmetic/README.md
new file mode 100644
index 000000000..b0137664c
--- /dev/null
+++ b/src/LegacyArithmetic/README.md
@@ -0,0 +1,3 @@
+The development of this directory predates `src/Arithmetic`, and should probably
+be considered to be superseded by it. The p256 Montgomery reduction for
+a 128-bit cpu synthesized here still works.
diff --git a/src/Tactics/VerdiTactics.v b/src/LegacyArithmetic/VerdiTactics.v
index 4060fc675..4060fc675 100644
--- a/src/Tactics/VerdiTactics.v
+++ b/src/LegacyArithmetic/VerdiTactics.v
diff --git a/src/ModularArithmetic/ZBounded.v b/src/LegacyArithmetic/ZBounded.v
index bccbf7428..bccbf7428 100644
--- a/src/ModularArithmetic/ZBounded.v
+++ b/src/LegacyArithmetic/ZBounded.v
diff --git a/src/ModularArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v
index fd004451b..fef654f47 100644
--- a/src/ModularArithmetic/ZBoundedZ.v
+++ b/src/LegacyArithmetic/ZBoundedZ.v
@@ -1,6 +1,6 @@
 (*** ℤ can be a bounded ℤ-Like type *)
 Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.LegacyArithmetic.ZBounded.
 Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.LetIn.
diff --git a/src/EdDSARepChange.v b/src/Primitives/EdDSARepChange.v
index 0a214dc88..1ad4611be 100644
--- a/src/EdDSARepChange.v
+++ b/src/Primitives/EdDSARepChange.v
@@ -1,7 +1,7 @@
 Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions.
-Require Import Crypto.Algebra. Import Monoid Group ScalarMult.
+Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.ScalarMult.
 Require Import Crypto.Util.Decidable Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.SetEvars.
 Require Import Crypto.Util.Tactics.SubstEvars.
@@ -10,7 +10,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Coq.omega.Omega.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Option Crypto.Util.Logic Crypto.Util.Relations Crypto.Util.WordUtil Util.LetIn Util.NatUtil.
-Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Spec.ModularArithmetic Crypto.Arithmetic.PrimeFieldTheorems.
 Import NPeano.
 
 Import Notations.
@@ -102,7 +102,7 @@ Section EdDSA.
   Proof using Type*. exact (proj2_sig verify'_sig). Qed.
 
   Section ChangeRep.
-    Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@group Erep ErepEq ErepAdd ErepId ErepOpp}.
+    Context {Erep ErepEq ErepAdd ErepId ErepOpp} {Agroup:@Algebra.Hierarchy.group Erep ErepEq ErepAdd ErepId ErepOpp}.
     Context {EToRep} {Ahomom:@is_homomorphism E Eeq Eadd Erep ErepEq ErepAdd EToRep}.
 
     Context {ERepEnc : Erep -> word b}
diff --git a/src/MxDHRepChange.v b/src/Primitives/MxDHRepChange.v
index ef2d06f5f..9f0276ef8 100644
--- a/src/MxDHRepChange.v
+++ b/src/Primitives/MxDHRepChange.v
@@ -1,12 +1,12 @@
 Require Import Crypto.Spec.MxDH.
-Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field.
+Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field.
 Require Import Crypto.Util.Tuple Crypto.Util.Prod.
 Require Import Crypto.Util.Tactics.DestructHead.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
 Section MxDHRepChange.
-  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {Fcswap:bool->F*F->F*F->(F*F)*(F*F)} {Fa24:F} {tb1:nat->bool}.
-  Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {impl_field:@Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Keq_dec:Decidable.DecidableRel Keq} {Kcswap:bool->K*K->K*K->(K*K)*(K*K)} {Ka24:K} {tb2:nat->bool}.
+  Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {Fcswap:bool->F*F->F*F->(F*F)*(F*F)} {Fa24:F} {tb1:nat->bool}.
+  Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {impl_field:@Algebra.Hierarchy.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv} {Keq_dec:Decidable.DecidableRel Keq} {Kcswap:bool->K*K->K*K->(K*K)*(K*K)} {Ka24:K} {tb2:nat->bool}.
 
   Context {FtoK} {homom:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                               K Keq Kone Kadd Kmul FtoK}.
diff --git a/src/Reflection/Z/Inline.v b/src/Reflection/Z/Inline.v
deleted file mode 100644
index 989286232..000000000
--- a/src/Reflection/Z/Inline.v
+++ /dev/null
@@ -1,7 +0,0 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-
-Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t
-  := @InlineConst base_type op (is_const) t e.
diff --git a/src/Reflection/Z/InlineWf.v b/src/Reflection/Z/InlineWf.v
deleted file mode 100644
index 5d5eb0617..000000000
--- a/src/Reflection/Z/InlineWf.v
+++ /dev/null
@@ -1,11 +0,0 @@
-Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Wf.
-Require Import Crypto.Reflection.InlineWf.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Inline.
-
-Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
-  : Wf (InlineConst e)
-  := @Wf_InlineConst _ _ _ t e Hwf.
-
-Hint Resolve Wf_InlineConst : wf.
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
deleted file mode 100644
index 439a1df8c..000000000
--- a/src/Reflection/Z/Reify.v
+++ /dev/null
@@ -1,50 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Reflection.InputSyntax.
-Require Import Crypto.Reflection.Z.Syntax.
-Require Import Crypto.Reflection.Z.Syntax.Equality.
-Require Import Crypto.Reflection.Z.Syntax.Util.
-Require Import Crypto.Reflection.WfReflective.
-Require Import Crypto.Reflection.Reify.
-Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Reflection.InlineInterp.
-Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.Eta.
-Require Import Crypto.Reflection.EtaInterp.
-
-Ltac base_reify_op op op_head extra ::=
-     lazymatch op_head with
-     | @Z.add => constr:(reify_op op op_head 2 (Add TZ TZ TZ))
-     | @Z.mul => constr:(reify_op op op_head 2 (Mul TZ TZ TZ))
-     | @Z.sub => constr:(reify_op op op_head 2 (Sub TZ TZ TZ))
-     | @Z.shiftl => constr:(reify_op op op_head 2 (Shl TZ TZ TZ))
-     | @Z.shiftr => constr:(reify_op op op_head 2 (Shr TZ TZ TZ))
-     | @Z.land => constr:(reify_op op op_head 2 (Land TZ TZ TZ))
-     | @Z.lor => constr:(reify_op op op_head 2 (Lor TZ TZ TZ))
-     | @Z.opp => constr:(reify_op op op_head 1 (Opp TZ TZ))
-     end.
-Ltac base_reify_type T ::=
-     lazymatch T with
-     | Z => TZ
-     end.
-Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e.
-Ltac Reify e :=
-  let v := Reflection.Reify.Reify base_type interp_base_type op make_const e in
-  constr:(ExprEta v).
-Ltac prove_ExprEta_Compile_correct :=
-  fun _
-  => intros;
-     rewrite ?InterpExprEta;
-     prove_compile_correct_using ltac:(fun _ => apply make_const_correct) ().
-
-Ltac Reify_rhs :=
-  Reflection.Reify.Reify_rhs_gen Reify prove_ExprEta_Compile_correct interp_op ltac:(fun tac => tac ()).
-
-Ltac prereify_context_variables :=
-  Reflection.Reify.prereify_context_variables interp_base_type.
-Ltac reify_context_variable :=
-  Reflection.Reify.reify_context_variable base_type interp_base_type op.
-Ltac lazy_reify_context_variable :=
-  Reflection.Reify.lazy_reify_context_variable base_type interp_base_type op.
-Ltac reify_context_variables :=
-  Reflection.Reify.reify_context_variables base_type interp_base_type op.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index daaa2ed74..83e5645d5 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -1,4 +1,4 @@
-Require Crypto.CompleteEdwardsCurve.Pre.
+Require Crypto.Curves.Edwards.Pre.
 Require Crypto.Util.Decidable.
 
 Module E.
@@ -10,7 +10,7 @@ Module E.
     *)
 
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {char_ge_3 : @Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos BinNat.N.two)}
             {Feq_dec:Decidable.DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/Spec/Ed25519.v b/src/Spec/Ed25519.v
index 2a2847a31..b8526bb0e 100644
--- a/src/Spec/Ed25519.v
+++ b/src/Spec/Ed25519.v
@@ -2,7 +2,8 @@ Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.Spec.CompleteEdwardsCurve.
 Require Import Crypto.Spec.EdDSA.
 
-Require ModularArithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *)
+Require Crypto.Arithmetic.PrimeFieldTheorems. (* to know that Z mod p is a field *)
+Require Crypto.Curves.Edwards.AffineProofs.
 
 (* these 2 proofs can be generated using https://github.com/andres-erbsen/safecurves-primes *)
 Axiom prime_q : Znumtheory.prime (2^255-19). Global Existing Instance prime_q.
@@ -83,7 +84,7 @@ Section Ed25519.
 
   Definition ed25519 (l_order_B: E.eq(F:=Fq)(Fone:=F.one) (mul (BinInt.Z.to_nat l) B)%E zero) :
     EdDSA (E:=E) (Eadd:=add) (Ezero:=zero) (EscalarMult:=mul) (B:=B)
-          (Eopp:=Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *)
+          (Eopp:=Crypto.Curves.Edwards.AffineProofs.E.opp(nonzero_a:=nonzero_a)) (* TODO: move defn *)
           (Eeq:=E.eq) (* TODO: move defn *)
           (l:=l) (b:=b) (n:=n) (c:=c)
           (Eenc:=Eenc) (Senc:=Senc) (H:=SHA512).
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index 67a1014f6..82a9ba6cc 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -1,7 +1,7 @@
 Require Bedrock.Word Crypto.Util.WordUtil.
 Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
-Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
+Require Crypto.Algebra.ScalarMult.
 
 Require Import Omega. (* TODO: remove this import when we drop 8.4 *)
 
@@ -41,7 +41,7 @@ Section EdDSA.
         {Senc : F l -> Word.word b} (* normative encoding of scalars *)
     :=
       {
-        EdDSA_group:@Algebra.group E Eeq Eadd Ezero Eopp;
+        EdDSA_group:@Algebra.Hierarchy.group E Eeq Eadd Ezero Eopp;
         EdDSA_scalarmult:@Algebra.ScalarMult.is_scalarmult E Eeq Eadd Ezero EscalarMult;
 
         EdDSA_c_valid : c = 2 \/ c = 3;
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index ed6a0c4a2..cb57b4547 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -1,6 +1,6 @@
 Require Coq.ZArith.Znumtheory Coq.Numbers.BinNums.
 
-Require Crypto.ModularArithmetic.Pre.
+Require Crypto.Arithmetic.ModularArithmeticPre.
 
 Delimit Scope positive_scope with positive.
 Bind Scope positive_scope with BinPos.positive.
@@ -33,7 +33,7 @@ Global Set Printing Coercions.
 
 Module F.
   Definition F (m : BinPos.positive) := { z : BinInt.Z | z = z mod m }.
-  Local Obligation Tactic := cbv beta; auto using Pre.Z_mod_mod.
+  Local Obligation Tactic := cbv beta; auto using ModularArithmeticPre.Z_mod_mod.
   Program Definition of_Z  m  (a:BinNums.Z) : F m := a mod m.
   Definition to_Z {m} (a:F m) : BinNums.Z := proj1_sig a.
 
@@ -51,14 +51,14 @@ Module F.
                                | inv zero = zero
                                  /\ ( Znumtheory.prime m ->
                                       forall a, a <> zero -> mul (inv a) a = one )
-                               } := Pre.inv_impl.
+                               } := ModularArithmeticPre.inv_impl.
     Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec.
     Definition div (a b:F m) : F m := mul a (inv b).
 
     Definition pow_with_spec : { pow : F m -> BinNums.N -> F m
                                | forall a, pow a 0%N = one
                                            /\ forall x, pow a (1 + x)%N = mul a (pow a x)
-                               } := Pre.pow_impl.
+                               } := ModularArithmeticPre.pow_impl.
     Definition pow : F m -> BinNums.N -> F m := Eval hnf in proj1_sig pow_with_spec.
   End FieldOperations.
 
diff --git a/src/Spec/MontgomeryCurve.v b/src/Spec/MontgomeryCurve.v
index e5ed281f9..ff6d3a080 100644
--- a/src/Spec/MontgomeryCurve.v
+++ b/src/Spec/MontgomeryCurve.v
@@ -1,4 +1,4 @@
-Require Crypto.Algebra Crypto.Algebra.Field.
+Require Crypto.Algebra.Field.
 Require Crypto.Util.GlobalSettings.
 Require Crypto.Util.Tactics.DestructHead Crypto.Util.Sum Crypto.Util.Prod.
 
@@ -6,7 +6,7 @@ Module M.
   Section MontgomeryCurve.
     Import BinNat.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
+            {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
             {Feq_dec:Decidable.DecidableRel Feq}
             {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/Spec/MxDH.v b/src/Spec/MxDH.v
index 27f5f9a7f..d70521581 100644
--- a/src/Spec/MxDH.v
+++ b/src/Spec/MxDH.v
@@ -1,9 +1,9 @@
-Require Crypto.Algebra.
+Require Crypto.Algebra.Hierarchy.
 Require Import Crypto.Util.Notations.
 
 Module MxDH. (* from RFC7748 *)
   Section MontgomeryLadderKeyExchange.
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
diff --git a/src/Test/Curve25519SpecTestVectors.v b/src/Spec/Test/X25519.v
index 15ca468c1..15ca468c1 100644
--- a/src/Test/Curve25519SpecTestVectors.v
+++ b/src/Spec/Test/X25519.v
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index eebc79df4..226ec6616 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -1,4 +1,4 @@
-Require Crypto.WeierstrassCurve.Pre.
+Require Crypto.Curves.Weierstrass.Pre.
 
 Module W.
   Section WeierstrassCurves.
@@ -9,7 +9,7 @@ Module W.
      * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79)
      *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.Hierarchy.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq} {char_ge_3:@Ring.char_ge F Feq Fzero Fone Fopp Fadd Fsub Fmul (BinNat.N.succ_pos (BinNat.N.two))}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope.
     Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope.
diff --git a/src/Specific/NewBaseSystemTest.v b/src/Specific/ArithmeticSynthesisTest.v
index 8cbb8a596..257de7e95 100644
--- a/src/Specific/NewBaseSystemTest.v
+++ b/src/Specific/ArithmeticSynthesisTest.v
@@ -1,7 +1,7 @@
 Require Import Coq.ZArith.ZArith Coq.ZArith.BinIntDef.
 Require Import Coq.Lists.List. Import ListNotations.
-Require Import Crypto.NewBaseSystem. Import B.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Arithmetic.Core. Import B.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import (*Crypto.Util.Tactics*) Crypto.Util.Decidable.
 Require Import Crypto.Util.LetIn Crypto.Util.ZUtil.
 Require Crypto.Util.Tuple.
diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index b87a9a0bc..263bc82ba 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Specific.FancyMachine256.Core.
-Require Import Crypto.ModularArithmetic.BarrettReduction.ZBounded.
-Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook.
+Require Import LegacyArithmetic.BarretReduction.
+Require Import Crypto.Arithmetic.BarrettReduction.HAC.
 
 (** Useful for arithmetic in the field of integers modulo the order of the curve25519 base point *)
 Section expression.
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 6ea614936..900ac92a9 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -3,22 +3,22 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Coq.PArith.BinPos Coq.micromega.Psatz.
 Require Export Coq.ZArith.ZArith Coq.Lists.List.
 Require Import Crypto.Util.Decidable.
-Require Export Crypto.BoundedArithmetic.Interface.
-Require Export Crypto.BoundedArithmetic.ArchitectureToZLike.
-Require Export Crypto.BoundedArithmetic.ArchitectureToZLikeProofs.
+Require Export Crypto.LegacyArithmetic.Interface.
+Require Export Crypto.LegacyArithmetic.ArchitectureToZLike.
+Require Export Crypto.LegacyArithmetic.ArchitectureToZLikeProofs.
 Require Export Crypto.Util.Tuple.
 Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod.
-Require Export Crypto.Reflection.Named.Syntax.
-Require Export Crypto.Reflection.Named.PositiveContext.
-Require Import Crypto.Reflection.Named.DeadCodeElimination.
-Require Import Crypto.Reflection.CountLets.
-Require Import Crypto.Reflection.Named.ContextOn.
-Require Import Crypto.Reflection.Named.Wf.
-Require Export Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Reflection.Inline.
-Require Import Crypto.Reflection.CommonSubexpressionElimination.
-Require Export Crypto.Reflection.Reify.
+Require Export Crypto.Compilers.Named.Syntax.
+Require Export Crypto.Compilers.Named.PositiveContext.
+Require Import Crypto.Compilers.Named.DeadCodeElimination.
+Require Import Crypto.Compilers.CountLets.
+Require Import Crypto.Compilers.Named.ContextOn.
+Require Import Crypto.Compilers.Named.Wf.
+Require Export Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Linearize.
+Require Import Crypto.Compilers.Inline.
+Require Import Crypto.Compilers.CommonSubexpressionElimination.
+Require Export Crypto.Compilers.Reify.
 Require Export Crypto.Util.ZUtil.
 Require Export Crypto.Util.Option.
 Require Export Crypto.Util.Notations.
@@ -245,7 +245,7 @@ Section assemble.
     := invert_Some (@Named.interp base_type interp_base_type op Register RegisterContext interp_op empty t e v).
 End assemble.
 
-Export Reflection.Named.Syntax.
+Export Compilers.Named.Syntax.
 Open Scope nexpr_scope.
 Open Scope ctype_scope.
 Open Scope type_scope.
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index f052cd548..e6af32aab 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Specific.FancyMachine256.Core.
-Require Import Crypto.ModularArithmetic.Montgomery.ZBounded.
-Require Import Crypto.ModularArithmetic.Montgomery.ZProofs.
+Require Import Crypto.LegacyArithmetic.MontgomeryReduction.
+Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs.
 
 Section expression.
   Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops) (modulus : Z) (m' : Z) (Hm : modulus <> 0) (H : 0 <= modulus < 2^256) (Hm' : 0 <= m' < 2^256).
@@ -48,7 +48,7 @@ Section expression.
              v
              Hv
     : fancy_machine.decode (expression v) = _
-    := @ZBounded.reduce_via_partial_correct (2^256) modulus _ (props' _ _ eq_refl eq_refl) (ldi' m') I Hm R' HR0 HR1 (fst v, snd v) I Hv.
+    := @Crypto.LegacyArithmetic.MontgomeryReduction.reduce_via_partial_correct (2^256) modulus _ (props' _ _ eq_refl eq_refl) (ldi' m') I Hm R' HR0 HR1 (fst v, snd v) I Hv.
 End expression.
 
 Section reflected.
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v
index 81a3ff0a3..937b5125f 100644
--- a/src/Specific/IntegrationTest.v
+++ b/src/Specific/IntegrationTest.v
@@ -2,17 +2,16 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Lists.List.
 Local Open Scope Z_scope.
 
-Require Import Crypto.Algebra.
-Require Import Crypto.NewBaseSystem.
+Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Util.FixedWordSizes.
-Require Import Crypto.Specific.NewBaseSystemTest.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.Specific.ArithmeticSynthesisTest.
+Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.MoveLetIn.
 Import ListNotations.
 
-Require Import Crypto.Reflection.Z.Bounds.Pipeline.
+Require Import Crypto.Compilers.Z.Bounds.Pipeline.
 
 Section BoundedField25p5.
   Local Coercion Z.of_nat : nat >-> Z.
diff --git a/src/SpecificGen/2213_32.json b/src/SpecificGen/2213_32.json
deleted file mode 100644
index fe000da25..000000000
--- a/src/SpecificGen/2213_32.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 221,
-        "c" : 3,
-        "n" : 8,
-        "w" : 32,
-        "ch" : "[0;1;2;3;4;5;6;7;0;1]"
-}
diff --git a/src/SpecificGen/2519_32.json b/src/SpecificGen/2519_32.json
deleted file mode 100644
index f2aabdb70..000000000
--- a/src/SpecificGen/2519_32.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 251,
-        "c" : 9,
-        "n" : 10,
-        "w" : 32,
-        "ch" : "[0;1;2;3;4;5;6;7;8;9;0;1]"
-}
diff --git a/src/SpecificGen/25519_32.json b/src/SpecificGen/25519_32.json
deleted file mode 100644
index 383c03531..000000000
--- a/src/SpecificGen/25519_32.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 255,
-        "c" : 19,
-        "n" : 10,
-        "w" : 32,
-        "ch" : "[0;1;2;3;4;5;6;7;8;9;0;1]"
-}
diff --git a/src/SpecificGen/25519_64.json b/src/SpecificGen/25519_64.json
deleted file mode 100644
index b4acfda31..000000000
--- a/src/SpecificGen/25519_64.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 255,
-        "c" : 19,
-        "n" : 5,
-        "w" : 64,
-        "ch" : "[0;1;2;3;4;0;1]"
-}
diff --git a/src/SpecificGen/41417_32.json b/src/SpecificGen/41417_32.json
deleted file mode 100644
index 0a55e4c0b..000000000
--- a/src/SpecificGen/41417_32.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 414,
-        "c" : 17,
-        "n" : 18,
-        "w" : 32,
-        "ch" : "[0;1;2;3;4;5;6;7;8;9;10;11;12;13;14;15;16;17;0;1]"
-}
diff --git a/src/SpecificGen/5211_32.json b/src/SpecificGen/5211_32.json
deleted file mode 100644
index dc43b67b7..000000000
--- a/src/SpecificGen/5211_32.json
+++ /dev/null
@@ -1,7 +0,0 @@
-{
-        "k" : 521,
-        "c" : 1,
-        "n" : 20,
-        "w" : 32,
-        "ch" : "[0;1;2;3;4;5;6;7;8;9;10;11;12;13;14;15;16;17;18;19;0;1]"
-}
diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
index 110a756ea..e03b2e36f 100644
--- a/src/Util/AdditionChainExponentiation.v
+++ b/src/Util/AdditionChainExponentiation.v
@@ -1,7 +1,7 @@
 Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations.
 Require Import Coq.Numbers.BinNums Coq.NArith.BinNat.
 Require Import Crypto.Util.ListUtil.
-Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
+Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
@@ -28,7 +28,7 @@ Section AddChainExp.
   (0, 6)] (* 31 = 30 + 1 *)
   [1] = 31. reflexivity. Qed.
 
-  Context {G eq op id} {monoid:@Algebra.monoid G eq op id}.
+  Context {G eq op id} {monoid:@Algebra.Hierarchy.monoid G eq op id}.
   Context {scalarmult} {is_scalarmult:@ScalarMult.is_scalarmult G eq op id scalarmult}.
   Local Infix "=" := eq : type_scope.
   Local Open Scope N_scope.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 2fd7f8adc..e4f9dde08 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -1,7 +1,7 @@
 Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Classes.Equivalence.
 Require Import Coq.NArith.NArith Coq.PArith.BinPosDef.
 Require Import Coq.Numbers.Natural.Peano.NPeano.
-Require Import Crypto.Algebra Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
+Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult.
 Require Import Crypto.Util.NUtil.
 Require Import Crypto.Util.Tactics.BreakMatch.
 
@@ -9,7 +9,7 @@ Local Open Scope equiv_scope.
 
 Generalizable All Variables.
 Section IterAssocOp.
-  Context {T eq op id} {moinoid : @monoid T eq op id} (testbit : nat -> bool).
+  Context {T eq op id} {moinoid : @Algebra.Hierarchy.monoid T eq op id} (testbit : nat -> bool).
   Local Infix "===" := eq. Local Infix "===" := eq : type_scope.
 
   Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)).
@@ -26,12 +26,12 @@ Section IterAssocOp.
 
   Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a).
   Proof using Type*.
-   induction p; intros; simpl; rewrite ?associative, ?IHp; reflexivity.
+   induction p; intros; simpl; rewrite ?Algebra.Hierarchy.associative, ?IHp; reflexivity.
   Qed.
 
   Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a  === op a (N_iter_op n a).
   Proof using Type*.
-    destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?right_identity; reflexivity.
+    destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?Algebra.Hierarchy.right_identity; reflexivity.
   Qed.
 
   Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a.
diff --git a/synthesis-parameters.txt b/synthesis-parameters.txt
new file mode 100644
index 000000000..2140cebf0
--- /dev/null
+++ b/synthesis-parameters.txt
@@ -0,0 +1,53 @@
+==> src/SpecificGen/2213_32.json <==
+{
+        "k" : 221,
+        "c" : 3,
+        "n" : 8,
+        "w" : 32,
+        "ch" : "[0;1;2;3;4;5;6;7;0;1]"
+}
+
+==> src/SpecificGen/2519_32.json <==
+{
+        "k" : 251,
+        "c" : 9,
+        "n" : 10,
+        "w" : 32,
+        "ch" : "[0;1;2;3;4;5;6;7;8;9;0;1]"
+}
+
+==> src/SpecificGen/25519_32.json <==
+{
+        "k" : 255,
+        "c" : 19,
+        "n" : 10,
+        "w" : 32,
+        "ch" : "[0;1;2;3;4;5;6;7;8;9;0;1]"
+}
+
+==> src/SpecificGen/25519_64.json <==
+{
+        "k" : 255,
+        "c" : 19,
+        "n" : 5,
+        "w" : 64,
+        "ch" : "[0;1;2;3;4;0;1]"
+}
+
+==> src/SpecificGen/41417_32.json <==
+{
+        "k" : 414,
+        "c" : 17,
+        "n" : 18,
+        "w" : 32,
+        "ch" : "[0;1;2;3;4;5;6;7;8;9;10;11;12;13;14;15;16;17;0;1]"
+}
+
+==> src/SpecificGen/5211_32.json <==
+{
+        "k" : 521,
+        "c" : 1,
+        "n" : 20,
+        "w" : 32,
+        "ch" : "[0;1;2;3;4;5;6;7;8;9;10;11;12;13;14;15;16;17;18;19;0;1]"
+}