diff options
author | Robert Sloan <varomodt@gmail.com> | 2016-06-22 14:06:28 -0400 |
---|---|---|
committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 14:06:28 -0400 |
commit | 2f44fe53e1a598b524e11cda3dc9ce7a04534247 (patch) | |
tree | 47a77eb4ed8fea3ac5ec99c5bf5ad9131ba44fd9 /_CoqProject | |
parent | e101fc5dd8783d029d7a4933c7ccca4a67ed3874 (diff) | |
parent | 3d8afe1c9bd905e3a62523e87a2aa7e5d9f5093d (diff) |
Merge with plv/master
Diffstat (limited to '_CoqProject')
-rw-r--r-- | _CoqProject | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/_CoqProject b/_CoqProject index c92f9481c..567860b25 100644 --- a/_CoqProject +++ b/_CoqProject @@ -1,22 +1,21 @@ -R src Crypto --R Coqprime/Coqprime Coqprime +-R Bedrock Bedrock +Bedrock/Nomega.v +Bedrock/Word.v +src/Algebra.v src/BaseSystem.v src/BaseSystemProofs.v -src/EdDSAProofs.v -src/Rep.v src/Testbit.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v -src/CompleteEdwardsCurve/DoubleAndAdd.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v -src/Encoding/PointEncodingPre.v -src/Encoding/PointEncodingTheorems.v +src/Experiments/DerivationsOptionRectLetInEncoding.v +src/Experiments/GenericFieldPow.v +src/Experiments/SpecEd25519.v src/ModularArithmetic/ExtendedBaseVector.v -src/ModularArithmetic/FField.v -src/ModularArithmetic/FNsatz.v src/ModularArithmetic/ModularArithmeticTheorems.v src/ModularArithmetic/ModularBaseSystem.v src/ModularArithmetic/ModularBaseSystemOpt.v @@ -28,15 +27,13 @@ src/ModularArithmetic/PseudoMersenneBaseParams.v src/ModularArithmetic/PseudoMersenneBaseRep.v src/ModularArithmetic/Tutorial.v src/Spec/CompleteEdwardsCurve.v -src/Spec/Ed25519.v src/Spec/EdDSA.v src/Spec/Encoding.v src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v -src/Spec/PointEncoding.v -src/Specific/Ed25519.v src/Specific/GF1305.v src/Specific/GF25519.v +src/Tactics/Nsatz.v src/Tactics/VerdiTactics.v src/Util/CaseUtil.v src/Util/IterAssocOp.v @@ -44,6 +41,7 @@ src/Util/ListUtil.v src/Util/NatUtil.v src/Util/NumTheoryUtil.v src/Util/Tactics.v +src/Util/Tuple.v src/Util/WordUtil.v src/Util/ZUtil.v src/Assembly/QhasmCommon.v |