diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2017-03-29 00:27:15 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2017-03-31 10:36:51 -0400 |
| commit | e97200ea903c57574026c6b6d0be73ad0bfed991 (patch) | |
| tree | 862f46df6f671d912ab6c62a695f241146b35c69 /_CoqProject | |
| parent | 686fcbced2b0fb0b35fa6ad5aa71dd6924aee459 (diff) | |
use improved fsatz on various elliptic curve things
partial correctness of projective addition
stronger projective addition proof
fixup
Diffstat (limited to '_CoqProject')
| -rw-r--r-- | _CoqProject | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index d546a6f66..57df4d61f 100644 --- a/_CoqProject +++ b/_CoqProject @@ -7,6 +7,8 @@ src/BaseSystem.v src/BaseSystemProofs.v src/EdDSARepChange.v src/Karatsuba.v +src/MontgomeryCurveTheorems.v +src/MontgomeryX.v src/MxDHRepChange.v src/NewBaseSystem.v src/SaturatedBaseSystem.v @@ -64,6 +66,7 @@ src/BoundedArithmetic/Double/Repeated/Proofs/SelectConditional.v src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +src/CompleteEdwardsCurve/EdwardsMontgomery.v src/CompleteEdwardsCurve/ExtendedCoordinates.v src/CompleteEdwardsCurve/Pre.v src/Encoding/EncodingTheorems.v @@ -519,4 +522,5 @@ src/Util/Tactics/SplitInContext.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v src/WeierstrassCurve/Pre.v +src/WeierstrassCurve/Projective.v src/WeierstrassCurve/WeierstrassCurveTheorems.v |