Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix changed qualified tactic name | Jason Gross | 2017-01-17 |
| | |||
* | Add ladderstep_other_assoc | Jason Gross | 2017-01-07 |
| | |||
* | Add more generic ladderstep | Jason Gross | 2017-01-07 |
| | |||
* | implement X25519 | Andres Erbsen | 2016-11-06 |
| | |||
* | move B_order_l and prime_q | Andres Erbsen | 2016-11-06 |
| | |||
* | put EdDSA encoding sign bit at the MSB | Andres Erbsen | 2016-11-04 |
| | |||
* | Filled in point/scalar encoding definitions. | jadep | 2016-10-10 |
| | |||
* | Ed25519: add basepoint and prove most EdDSA preconditions | Andres Erbsen | 2016-10-10 |
| | |||
* | Spec.Ed25519: prove that Curve25519 is an elliptic curve | Andres Erbsen | 2016-10-10 |
| | |||
* | Spec.Ed25519: fix exponent field modulus | Andres Erbsen | 2016-10-10 |
| | |||
* | Moved PointEncoding out of Spec | jadep | 2016-10-06 |
| | |||
* | Fixed a lingering inappropriate use of Logic.eq | jadep | 2016-10-06 |
| | |||
* | fix 8.4 build | jadep | 2016-10-03 |
| | |||
* | A couple hotfixes; recent commits somehow broke things | jadep | 2016-10-03 |
| | |||
* | Wrote proofs necessary to fill in all point-encoding related context ↵ | jadep | 2016-10-03 |
| | | | | variables in EdDSARepChange.v | ||
* | Ed25519: use Global Instance | Andres Erbsen | 2016-10-03 |
| | |||
* | Spec: add ed25519 | Andres Erbsen | 2016-10-03 |
| | |||
* | MxDH: do not depend on implicit import of list notations | Andres Erbsen | 2016-09-26 |
| | |||
* | add Montgomery x-coordinate Diffie-Hellman and Curve25519 | Andres Erbsen | 2016-09-26 |
| | |||
* | alternative signing derivation | Andres Erbsen | 2016-09-22 |
| | | | | cleanup | ||
* | Derive EdDSA.verify from equational specification | Andres Erbsen | 2016-09-16 |
| | | | | Experiments/SpecEd25519 will come back soon | ||
* | ModularArithmetic: conversions between [F] and [nat] | Andres Erbsen | 2016-09-16 |
| | |||
* | Fully qualify [Require]s | Jason Gross | 2016-09-08 |
| | | | | This way they won't become ambiguous if we add new files | ||
* | remove eq_dec from Monoid | Andres Erbsen | 2016-08-23 |
| | |||
* | [cbv beta] in the beginning of Obligation Tactic for 8.5 | Andres Erbsen | 2016-08-08 |
| | |||
* | [F] has its own module now | Andres Erbsen | 2016-08-05 |
| | | | | | | [ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem] | ||
* | Refactor ModularArithmetic into Zmod, expand Decidable | Andres Erbsen | 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]! | 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 |
| |