aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/Ed25519.v
Commit message (Expand)AuthorAge
* Remove EdDSAGravatar Benjamin Barenblat2019-04-26
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* eddsa spec fixGravatar Andres Erbsen2017-06-14
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* rename-everythingGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* 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-05-06 04:32:39 +0000