Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | ScalarMult: Z -> G -> G (closes #193) | 2017-06-14 | |
| | |||
* | rename-everything | 2017-04-06 | |
| | |||
* | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | 2017-03-02 | |
| | |||
* | alternative signing derivation | 2016-09-22 | |
| | | | | cleanup | ||
* | Derive EdDSA.verify from equational specification | 2016-09-16 | |
| | | | | Experiments/SpecEd25519 will come back soon | ||
* | Fully qualify [Require]s | 2016-09-08 | |
| | | | | This way they won't become ambiguous if we add new files | ||
* | added proofs about addition chain exponentiation for later use in ↵ | 2016-07-10 | |
| | | | | ModularBaseSystem [pow], which we need for sqrt and inversion. | ||
* | scalarmult support; EdDSA.sign produces valid signatures | 2016-06-27 | |
| | |||
* | EdDSA: prove things about spec | 2016-06-25 | |
| | |||
* | EdDSA.Notations: indentation | 2016-06-22 | |
| | |||
* | Handle renaming of NPeano.pow to Nat.pow (#3) | 2016-06-22 | |
| | | | | We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5 | ||
* | EdDSA.v: resolve ambiguity based on ed25519.py | 2016-06-21 | |
| | |||
* | Whitespace change | 2016-06-21 | |
| | |||
* | remove trailing whitespace from src/ | 2016-06-20 | |
| | |||
* | port EdDSA spec | 2016-06-20 | |
| | |||
* | before changing SRep from N to F l | 2016-05-27 | |
| | |||
* | Changed name of Encoding to CanonicalEncoding, and changed notation to match. | 2016-04-29 | |
| | |||
* | consolidate and rename Edwards curve lemmas | 2016-04-25 | |
| | |||
* | point_eq_dec | 2016-04-22 | |
| | |||
* | ed25519 derivation: pair programming with jgross... slow progress | 2016-03-24 | |
| | |||
* | nicer verify() derivation starter | 2016-03-21 | |
| | |||
* | Finish absolutizing imports | 2016-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 WordUtil | 2016-02-25 | |
| | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵ | 2016-02-15 | |
| | | | | the commit looks huge) | ||
* | Spec/EdDSA: comments, remove prehashing | 2016-02-13 | |
| | |||
* | Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v | 2016-02-13 | |
| | |||
* | EdDSA spec ported over to new field implementation | 2016-02-13 | |