Start instantiating boundedness things

1 files changed, 34 insertions, 33 deletions

diff --git a/_CoqProject b/_CoqProject
index 69c197695..f687ed0ff 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,35 +3,37 @@
 Bedrock/Nomega.v
 Bedrock/Word.v
 src/Algebra.v
+src/BaseSystem.v
+src/BaseSystemProofs.v
+src/EdDSARepChange.v
+src/Testbit.v
 src/Assembly/Bounded.v
 src/Assembly/Bounds.v
 src/Assembly/Compile.v
 src/Assembly/Conversions.v
 src/Assembly/Evaluables.v
 src/Assembly/GF25519.v
+src/Assembly/GF25519BoundedInstantiation.v
 src/Assembly/HL.v
 src/Assembly/LL.v
 src/Assembly/PhoasCommon.v
 src/Assembly/Pipeline.v
+src/Assembly/Qhasm.v
 src/Assembly/QhasmCommon.v
 src/Assembly/QhasmEvalCommon.v
 src/Assembly/QhasmUtil.v
-src/Assembly/Qhasm.v
 src/Assembly/State.v
 src/Assembly/StringConversion.v
 src/Assembly/WordizeUtil.v
-src/BaseSystemProofs.v
-src/BaseSystem.v
-src/BoundedArithmetic/ArchitectureToZLikeProofs.v
 src/BoundedArithmetic/ArchitectureToZLike.v
-src/BoundedArithmetic/DoubleBoundedProofs.v
+src/BoundedArithmetic/ArchitectureToZLikeProofs.v
 src/BoundedArithmetic/DoubleBounded.v
-src/BoundedArithmetic/InterfaceProofs.v
+src/BoundedArithmetic/DoubleBoundedProofs.v
 src/BoundedArithmetic/Interface.v
+src/BoundedArithmetic/InterfaceProofs.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/ExtendedCoordinates.v
 src/CompleteEdwardsCurve/Pre.v
-src/EdDSARepChange.v
 src/Encoding/EncodingTheorems.v
 src/Encoding/ModularWordEncodingPre.v
 src/Encoding/ModularWordEncodingTheorems.v
@@ -39,41 +41,47 @@ src/Encoding/PointEncodingPre.v
 src/Experiments/EncodingLemmas.v
 src/Experiments/GenericFieldPow.v
 src/Experiments/MontgomeryCurve.v
-src/ModularArithmetic/BarrettReduction/ZBounded.v
-src/ModularArithmetic/BarrettReduction/ZGeneralized.v
-src/ModularArithmetic/BarrettReduction/ZHandbook.v
-src/ModularArithmetic/BarrettReduction/Z.v
-src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/ExtPow2BaseMulProofs.v
+src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/ModularArithmeticTheorems.v
-src/ModularArithmetic/ModularBaseSystemListProofs.v
+src/ModularArithmetic/ModularBaseSystem.v
 src/ModularArithmetic/ModularBaseSystemList.v
+src/ModularArithmetic/ModularBaseSystemListProofs.v
 src/ModularArithmetic/ModularBaseSystemOpt.v
 src/ModularArithmetic/ModularBaseSystemProofs.v
-src/ModularArithmetic/ModularBaseSystem.v
-src/ModularArithmetic/Montgomery/ZBounded.v
-src/ModularArithmetic/Montgomery/ZProofs.v
-src/ModularArithmetic/Montgomery/Z.v
-src/ModularArithmetic/Pow2BaseProofs.v
 src/ModularArithmetic/Pow2Base.v
+src/ModularArithmetic/Pow2BaseProofs.v
 src/ModularArithmetic/Pre.v
 src/ModularArithmetic/PrimeFieldTheorems.v
 src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
 src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/Tutorial.v
 src/ModularArithmetic/ZBounded.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/CommonSubexpressionElimination.v
 src/Reflection/Conversion.v
 src/Reflection/CountLets.v
 src/Reflection/FilterLive.v
-src/Reflection/InlineInterp.v
 src/Reflection/Inline.v
+src/Reflection/InlineInterp.v
 src/Reflection/InlineWf.v
 src/Reflection/InputSyntax.v
 src/Reflection/InterpProofs.v
-src/Reflection/LinearizeInterp.v
 src/Reflection/Linearize.v
+src/Reflection/LinearizeInterp.v
 src/Reflection/LinearizeWf.v
+src/Reflection/Reify.v
+src/Reflection/Syntax.v
+src/Reflection/TestCase.v
+src/Reflection/WfProofs.v
+src/Reflection/WfReflective.v
+src/Reflection/WfRel.v
 src/Reflection/Named/Compile.v
 src/Reflection/Named/ContextOn.v
 src/Reflection/Named/DeadCodeElimination.v
@@ -81,29 +89,22 @@ src/Reflection/Named/EstablishLiveness.v
 src/Reflection/Named/NameUtil.v
 src/Reflection/Named/RegisterAssign.v
 src/Reflection/Named/Syntax.v
-src/Reflection/Reify.v
-src/Reflection/Syntax.v
-src/Reflection/TestCase.v
-src/Reflection/WfProofs.v
-src/Reflection/WfReflective.v
-src/Reflection/WfRel.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/Ed25519.v
 src/Spec/EdDSA.v
 src/Spec/Encoding.v
-src/Specific/FancyMachine256/Barrett.v
-src/Specific/FancyMachine256/Core.v
-src/Specific/FancyMachine256/Montgomery.v
-src/Specific/GF1305.v
-src/Specific/GF25519.v
 src/Spec/ModularArithmetic.v
 src/Spec/ModularWordEncoding.v
 src/Spec/MxDH.v
 src/Spec/PointEncoding.v
 src/Spec/WeierstrassCurve.v
-src/Tactics/Algebra_syntax/Nsatz.v
+src/Specific/GF1305.v
+src/Specific/GF25519.v
+src/Specific/FancyMachine256/Barrett.v
+src/Specific/FancyMachine256/Core.v
+src/Specific/FancyMachine256/Montgomery.v
 src/Tactics/VerdiTactics.v
-src/Testbit.v
+src/Tactics/Algebra_syntax/Nsatz.v
 src/Test/Curve25519SpecTestVectors.v
 src/Util/AdditionChainExponentiation.v
 src/Util/AutoRewrite.v