aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/Ed25519.v
Commit message (Expand)AuthorAge
* Fix changed qualified tactic nameGravatar Jason Gross2017-01-17
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* Filled in point/scalar encoding definitions.Gravatar jadep2016-10-10
* Ed25519: add basepoint and prove most EdDSA preconditionsGravatar Andres Erbsen2016-10-10
* Spec.Ed25519: prove that Curve25519 is an elliptic curveGravatar Andres Erbsen2016-10-10
* Spec.Ed25519: fix exponent field modulusGravatar Andres Erbsen2016-10-10
* Ed25519: use Global InstanceGravatar Andres Erbsen2016-10-03
* Spec: add ed25519Gravatar Andres Erbsen2016-10-03
* Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
* Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-04-29
* Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-04-28
* Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-04-28
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
* Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-04-25
* instantiate ed25519 sign in specGravatar Andres Erbsen2016-03-20
* Ed25519: d is nonsquareGravatar Andres Erbsen2016-03-20
* Finish absolutizing importsGravatar Jason Gross2016-03-10
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
* efficient powmodGravatar Andres Erbsen2016-02-17
* moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ...Gravatar Jade Philipoom2016-02-16
* proved most of point encoding admits, fixed some build system issues (dead im...Gravatar Jade Philipoom2016-02-16
* added point encodings; some admits remainGravatar Jade Philipoom2016-02-16
* EdDSA: tweaked l_boundGravatar Jade Philipoom2016-02-15
* mergeGravatar Jade Philipoom2016-02-15
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 13:34:22 +0000