aboutsummaryrefslogtreecommitdiff
path: root/src/CompleteEdwardsCurve
Commit message (Expand)AuthorAge
* extended coordinates setoid boilerplateGravatar Andres Erbsen2016-06-22
* Finish absolutizing importsGravatar Jason Gross2016-06-22
* Remove [Admitted]; [Qed] is now under a secondGravatar Jason Gross2016-06-22
* CompleteEdwardsCurveTheorems: associativity proof that times out on QedGravatar Andres Erbsen2016-06-22
* ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoo...Gravatar Andres Erbsen2016-06-22
* moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...Gravatar Jade Philipoom2016-06-22
* cleaned up and ported definition to solve for x ^ 2 in the curve equationGravatar Jade Philipoom2016-06-22
* remove CheckGravatar Andres Erbsen2016-06-22
* port bounded iter_op and Edwards doubleAndAddGravatar Andres Erbsen2016-06-22
* CompleteEdwardsCurve: unifiedAddM1: Closed Under Global ContextGravatar Andres Erbsen2016-06-22
* ported some of EdDSA25519 to new field frameworkGravatar Jade Philipoom2016-06-22
* EdDSA spec ported over to new field implementationGravatar Jade Philipoom2016-06-22
* workaround field with typeclass modulusGravatar Andres Erbsen2016-06-22
* fix importsGravatar Andres Erbsen2016-06-22
* document field issue re-appearingGravatar Andres Erbsen2016-06-22
* port some edwards curve theoremsGravatar Andres Erbsen2016-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 01:53:50 +0000