merge rsloan-phoas refactors into master

1 files changed, 34 insertions, 4 deletions

diff --git a/_CoqProject b/_CoqProject
index f40ae6199..757d85fe7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,6 +7,7 @@ src/Assembly/Bounds.v
 src/Assembly/Compile.v
 src/Assembly/Conversions.v
 src/Assembly/Evaluables.v
+src/Assembly/GF25519BoundedInstantiation.v
 src/Assembly/GF25519.v
 src/Assembly/HL.v
 src/Assembly/LL.v
@@ -23,10 +24,33 @@ src/BaseSystemProofs.v
 src/BaseSystem.v
 src/BoundedArithmetic/ArchitectureToZLikeProofs.v
 src/BoundedArithmetic/ArchitectureToZLike.v
-src/BoundedArithmetic/DoubleBoundedProofs.v
-src/BoundedArithmetic/DoubleBounded.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/ShiftLeftRightTactic.v
+src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
+src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
+src/BoundedArithmetic/Double/Proofs/ShiftRight.v
+src/BoundedArithmetic/Double/Proofs/SpreadLeftImmediate.v
+src/BoundedArithmetic/Double/Repeated/Core.v
+src/BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr.v
+src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
+src/BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate.v
+src/BoundedArithmetic/Double/Repeated/Proofs/Multiply.v
+src/BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub.v
+src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v
+src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
+src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
+src/BoundedArithmetic/Eta.v
 src/BoundedArithmetic/InterfaceProofs.v
 src/BoundedArithmetic/Interface.v
+src/BoundedArithmetic/StripCF.v
+src/BoundedArithmetic/X86ToZLikeProofs.v
+src/BoundedArithmetic/X86ToZLike.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
 src/CompleteEdwardsCurve/ExtendedCoordinates.v
 src/CompleteEdwardsCurve/Pre.v
@@ -35,13 +59,15 @@ src/Encoding/EncodingTheorems.v
 src/Encoding/ModularWordEncodingPre.v
 src/Encoding/ModularWordEncodingTheorems.v
 src/Encoding/PointEncodingPre.v
-src/Experiments/EncodingLemmas.v
+src/Encoding/PointEncoding.v
+src/Experiments/Ed25519.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/Conversion.v
 src/ModularArithmetic/ExtendedBaseVector.v
 src/ModularArithmetic/ExtPow2BaseMulProofs.v
 src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -61,6 +87,7 @@ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
 src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/Tutorial.v
 src/ModularArithmetic/ZBounded.v
+src/ModularArithmetic/ZBoundedZ.v
 src/Reflection/CommonSubexpressionElimination.v
 src/Reflection/Conversion.v
 src/Reflection/CountLets.v
@@ -73,6 +100,7 @@ src/Reflection/InterpProofs.v
 src/Reflection/LinearizeInterp.v
 src/Reflection/Linearize.v
 src/Reflection/LinearizeWf.v
+src/Reflection/MapInterp.v
 src/Reflection/Named/Compile.v
 src/Reflection/Named/ContextOn.v
 src/Reflection/Named/DeadCodeElimination.v
@@ -94,11 +122,13 @@ src/Specific/FancyMachine256/Barrett.v
 src/Specific/FancyMachine256/Core.v
 src/Specific/FancyMachine256/Montgomery.v
 src/Specific/GF1305.v
+src/Specific/GF25519BoundedCommon.v
+src/Specific/GF25519Bounded.v
 src/Specific/GF25519.v
+src/Specific/SC25519.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/Tactics/VerdiTactics.v