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