diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-05-24 00:32:09 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-05-24 00:32:09 -0400 |
| commit | de5416133dc67dcd2729d4c7448991ab2672782a (patch) | |
| tree | 51e77dc33a19560b10719da49544ec6822627071 /_CoqProject | |
| parent | 7fcbb62c515ad973f43a43a73f8ea821e63e3ff6 (diff) | |
F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more broken...
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/_CoqProject b/_CoqProject index 1046bef3c..416b29176 100644 --- a/_CoqProject +++ b/_CoqProject @@ -2,6 +2,8 @@ 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 @@ -10,6 +12,7 @@ src/Encoding/EncodingTheorems.v src/Encoding/ModularWordEncodingPre.v src/Encoding/ModularWordEncodingTheorems.v src/Encoding/PointEncodingPre.v +src/Encoding/PointEncodingTheorems.v src/ModularArithmetic/ExtendedBaseVector.v src/ModularArithmetic/FField.v src/ModularArithmetic/FNsatz.v @@ -31,10 +34,9 @@ src/Spec/ModularArithmetic.v src/Spec/ModularWordEncoding.v src/Spec/PointEncoding.v src/Specific/Ed25519.v -src/Specific/GF25519.v src/Specific/GF1305.v +src/Specific/GF25519.v src/Tactics/VerdiTactics.v -src/Testbit.v src/Util/CaseUtil.v src/Util/IterAssocOp.v src/Util/ListUtil.v |