Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | compute on [F q]! | Andres Erbsen | 2016-07-20 |
| | |||
* | remove field_algebra | Andres Erbsen | 2016-07-11 |
| | |||
* | added proofs about addition chain exponentiation for later use in ↵ | jadep | 2016-07-10 |
| | | | | ModularBaseSystem [pow], which we need for sqrt and inversion. | ||
* | Define the spec of Weierstrass curves (#6) | Jason Gross | 2016-07-03 |
| | | | | | Define the spec of Weierstrass curves This is the start of work on P256. | ||
* | scalarmult support; EdDSA.sign produces valid signatures | Andres Erbsen | 2016-06-27 |
| | |||
* | EdDSA: prove things about spec | Andres Erbsen | 2016-06-25 |
| | |||
* | EdDSA.Notations: indentation | Andres Erbsen | 2016-06-22 |
| | |||
* | Fix broken notations (hopefully) | Jason Gross | 2016-06-22 |
| | |||
* | Handle renaming of NPeano.pow to Nat.pow (#3) | Jason Gross | 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 | Andres Erbsen | 2016-06-21 |
| | |||
* | Whitespace change | Jason Gross | 2016-06-21 |
| | |||
* | use Local Obligation Tactic (8.5-compat) | Andres Erbsen | 2016-06-21 |
| | |||
* | remove trailing whitespace from src/ | Andres Erbsen | 2016-06-20 |
| | |||
* | Remove anything incompatible with new algebraic hierarcy | Andres Erbsen | 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 | ||
* | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
|\ | | | | | | | includes broken files to be removed in next commit | ||
| * | port EdDSA spec | Andres Erbsen | 2016-06-20 |
| | | |||
| * | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | Andres Erbsen | 2016-06-17 |
| | | |||
| * | port edwards curve spec | Andres Erbsen | 2016-06-16 |
| | | |||
* | | Minor 8.5 changes | Jason Gross | 2016-06-10 |
| | | |||
* | | More changes for 8.5 | Jason Gross | 2016-06-10 |
| | | | | | | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior | ||
| * | before changing SRep from N to F l | Andres Erbsen | 2016-05-27 |
|/ | |||
* | Changed name of Encoding to CanonicalEncoding, and changed notation to match. | jadep | 2016-04-29 |
| | |||
* | Moved sign_bit definition to Spec. | jadep | 2016-04-29 |
| | |||
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵ | jadep | 2016-04-28 |
| | | | | general contexts. | ||
* | Completed encoding reorganization; factored sign_bit out of PointEncodings ↵ | jadep | 2016-04-28 |
| | | | | and finished encoding admits. | ||
* | consolidate and rename Edwards curve lemmas | Andres Erbsen | 2016-04-25 |
| | |||
* | Reorganization and revision of Encoding code and redefinition of sign_bit ↵ | jadep | 2016-04-25 |
| | | | | function. | ||
* | point_eq_dec | Andres Erbsen | 2016-04-22 |
| | |||
* | ed25519: continue derivation | Andres Erbsen | 2016-04-08 |
| | |||
* | Drop second projections in Ed25519 | Jason Gross | 2016-03-29 |
| | |||
* | ed25519 derivation: pair programming with jgross... slow progress | Andres Erbsen | 2016-03-24 |
| | |||
* | nicer verify() derivation starter | Andres Erbsen | 2016-03-21 |
| | |||
* | instantiate ed25519 sign in spec | Andres Erbsen | 2016-03-20 |
| | |||
* | Ed25519: d is nonsquare | Andres Erbsen | 2016-03-20 |
| | |||
* | Finish absolutizing imports | Jason Gross | 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 | Jason Gross | 2016-02-25 |
| | | | | Also move a definition about words, with a TODO about location, into WordUtil. | ||
* | efficient powmod | Andres Erbsen | 2016-02-17 |
| | |||
* | removed Print Assumptions | Jade Philipoom | 2016-02-16 |
| | |||
* | moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵ | Jade Philipoom | 2016-02-16 |
| | | | | CompleteEdwardsCurve, where the precondition is not in scope. | ||
* | proved most of point encoding admits, fixed some build system issues (dead ↵ | Jade Philipoom | 2016-02-16 |
| | | | | imports of PointFormats and Galois things) | ||
* | added point encodings; some admits remain | Jade Philipoom | 2016-02-16 |
| | |||
* | EdDSA: tweaked l_bound | Jade Philipoom | 2016-02-15 |
| | |||
* | merge | Jade Philipoom | 2016-02-15 |
|\ | |||
* | | instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵ | Jade Philipoom | 2016-02-15 |
| | | | | | | | | the commit looks huge) | ||
* | | added generic encoding spec | Jade Philipoom | 2016-02-15 |
| | | |||
| * | Finish seperating our specs: remove old non-specified code | Andres Erbsen | 2016-02-15 |
|/ | |||
* | ported some of EdDSA25519 to new field framework | Jade Philipoom | 2016-02-15 |
| | |||
* | update F Coercions and tutorial | Andres Erbsen | 2016-02-14 |
| | |||
* | Spec/EdDSA: comments, remove prehashing | Andres Erbsen | 2016-02-13 |
| | |||
* | Spec/EdDSA: cleanup; refactor lemmas to src/EdDSAProofs.v | Andres Erbsen | 2016-02-13 |
| |