rename-everything

1 files changed, 175 insertions, 175 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