diff options
author | Robert Sloan <varomodt@google.com> | 2016-10-13 11:45:20 -0700 |
---|---|---|
committer | Robert Sloan <varomodt@google.com> | 2016-10-13 11:45:20 -0700 |
commit | f33a97192cf426a4e0aa11ae2639b881ae1abc51 (patch) | |
tree | 5940d6b7f07ab434238430a5b96134495222507c /_CoqProject | |
parent | d9d0cdd73d3b92b662bdf1af82f37b13c25e5c1e (diff) |
Minor refactors waiting for the code generation to finish
Diffstat (limited to '_CoqProject')
-rw-r--r-- | _CoqProject | 71 |
1 files changed, 34 insertions, 37 deletions
diff --git a/_CoqProject b/_CoqProject index f724f229f..a9ed35505 100644 --- a/_CoqProject +++ b/_CoqProject @@ -3,10 +3,7 @@ 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 @@ -15,74 +12,67 @@ 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/BoundedArithmetic/ArchitectureToZLike.v +src/BaseSystemProofs.v +src/BaseSystem.v src/BoundedArithmetic/ArchitectureToZLikeProofs.v -src/BoundedArithmetic/DoubleBounded.v +src/BoundedArithmetic/ArchitectureToZLike.v src/BoundedArithmetic/DoubleBoundedProofs.v -src/BoundedArithmetic/Interface.v +src/BoundedArithmetic/DoubleBounded.v src/BoundedArithmetic/InterfaceProofs.v +src/BoundedArithmetic/Interface.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 src/Encoding/PointEncodingPre.v src/Experiments/EncodingLemmas.v src/Experiments/GenericFieldPow.v -<<<<<<< HEAD src/Experiments/MontgomeryCurve.v -======= -src/Experiments/SpecEd25519.v ->>>>>>> bd40805a09cc060531c5a1e7a69329255150f991 -src/ModularArithmetic/ExtPow2BaseMulProofs.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/ModularArithmeticTheorems.v -src/ModularArithmetic/ModularBaseSystem.v -src/ModularArithmetic/ModularBaseSystemList.v src/ModularArithmetic/ModularBaseSystemListProofs.v +src/ModularArithmetic/ModularBaseSystemList.v src/ModularArithmetic/ModularBaseSystemOpt.v src/ModularArithmetic/ModularBaseSystemProofs.v -src/ModularArithmetic/Pow2Base.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/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/Inline.v src/Reflection/InlineInterp.v +src/Reflection/Inline.v src/Reflection/InlineWf.v src/Reflection/InputSyntax.v src/Reflection/InterpProofs.v -src/Reflection/Linearize.v src/Reflection/LinearizeInterp.v +src/Reflection/Linearize.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 @@ -90,22 +80,29 @@ 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/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/Tactics/Algebra_syntax/Nsatz.v +src/Tactics/VerdiTactics.v +src/Testbit.v src/Test/Curve25519SpecTestVectors.v src/Util/AdditionChainExponentiation.v src/Util/AutoRewrite.v |