aboutsummaryrefslogtreecommitdiff
path: root/src/Spec/Ed25519.v
Commit message (Collapse)AuthorAge
* Remove EdDSAGravatar Benjamin Barenblat2019-04-26
| | | | | Remove Spec/EdDSA.v and its reverse dependencies Spec/Ed25519.v and Primitives/EdDSARepChange.v. This code is no longer in use.
* Import prim token notations before using themGravatar Jason Gross2018-08-24
| | | | | | | | | | | This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362 Almost all changes were made via https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
* 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
| | | | | | | With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ```
* rename-everythingGravatar Andres Erbsen2017-04-06
|
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
| | | | | | | | This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
* 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
| | | | | | - PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway
* 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 ↵Gravatar jadep2016-04-28
| | | | general contexts.
* Completed encoding reorganization; factored sign_bit out of PointEncodings ↵Gravatar jadep2016-04-28
| | | | and finished encoding admits.
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
|
* Reorganization and revision of Encoding code and redefinition of sign_bit ↵Gravatar jadep2016-04-25
| | | | function.
* instantiate ed25519 sign in specGravatar Andres Erbsen2016-03-20
|
* Ed25519: d is nonsquareGravatar Andres Erbsen2016-03-20
|
* Finish absolutizing importsGravatar Jason Gross2016-03-10
| | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* Factor out some bedrock dependencies into WordUtilGravatar Jason Gross2016-02-25
| | | | Also move a definition about words, with a TODO about location, into WordUtil.
* efficient powmodGravatar Andres Erbsen2016-02-17
|
* moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵Gravatar Jade Philipoom2016-02-16
| | | | CompleteEdwardsCurve, where the precondition is not in scope.
* proved most of point encoding admits, fixed some build system issues (dead ↵Gravatar Jade Philipoom2016-02-16
| | | | imports of PointFormats and Galois things)
* 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-19 06:17:00 +0000