From c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Thu, 6 Apr 2017 22:53:07 -0400 Subject: rename-everything --- _CoqProject | 350 ++++++++++++++++++++++++++++++------------------------------ 1 file changed, 175 insertions(+), 175 deletions(-) (limited to '_CoqProject') 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 -- cgit v1.2.3