Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | ed25519 spec: small cleanup | 2016-07-21 | |
| | |||
* | compute on [F q]! | 2016-07-20 | |
| | |||
* | experiments wd25519: simplify proof for a | 2016-07-20 | |
| | |||
* | Remove a nested proof | 2016-07-18 | |
| | | | | | Fix for Warning: Nested proofs are deprecated and will stop working in a future Coq version [deprecated-nested-proofs,deprecated] | ||
* | EdDSA: prove things about spec | 2016-06-25 | |
| | |||
* | Remove anything incompatible with new algebraic hierarcy | 2016-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 |