Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | alternative signing derivation | 2016-09-22 | |
| | | | | cleanup | ||
* | Derive EdDSA.verify from equational specification | 2016-09-16 | |
| | | | | Experiments/SpecEd25519 will come back soon | ||
* | ModularArithmetic: conversions between [F] and [nat] | 2016-09-16 | |
| | |||
* | Fully qualify [Require]s | 2016-09-08 | |
| | | | | This way they won't become ambiguous if we add new files | ||
* | remove eq_dec from Monoid | 2016-08-23 | |
| | |||
* | [cbv beta] in the beginning of Obligation Tactic for 8.5 | 2016-08-08 | |
| | |||
* | [F] has its own module now | 2016-08-05 | |
| | | | | | | [ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem] | ||
* | Refactor ModularArithmetic into Zmod, expand Decidable | 2016-08-04 | |
| | | | | | | | | | | | | ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1 | ||
* | compute on [F q]! | 2016-07-20 | |
| | |||
* | 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 | |
| |