aboutsummaryrefslogtreecommitdiff
path: root/src/Spec
Commit message (Expand)AuthorAge
* Fix changed qualified tactic nameGravatar Jason Gross2017-01-17
* Add ladderstep_other_assocGravatar Jason Gross2017-01-07
* Add more generic ladderstepGravatar Jason Gross2017-01-07
* implement X25519Gravatar Andres Erbsen2016-11-06
* move B_order_l and prime_qGravatar Andres Erbsen2016-11-06
* put EdDSA encoding sign bit at the MSBGravatar Andres Erbsen2016-11-04
* Filled in point/scalar encoding definitions.Gravatar jadep2016-10-10
* Ed25519: add basepoint and prove most EdDSA preconditionsGravatar Andres Erbsen2016-10-10
* Spec.Ed25519: prove that Curve25519 is an elliptic curveGravatar Andres Erbsen2016-10-10
* Spec.Ed25519: fix exponent field modulusGravatar Andres Erbsen2016-10-10
* Moved PointEncoding out of SpecGravatar jadep2016-10-06
* Fixed a lingering inappropriate use of Logic.eqGravatar jadep2016-10-06
* fix 8.4 buildGravatar jadep2016-10-03
* A couple hotfixes; recent commits somehow broke thingsGravatar jadep2016-10-03
* Wrote proofs necessary to fill in all point-encoding related context variable...Gravatar jadep2016-10-03
* Ed25519: use Global InstanceGravatar Andres Erbsen2016-10-03
* Spec: add ed25519Gravatar Andres Erbsen2016-10-03
* MxDH: do not depend on implicit import of list notationsGravatar Andres Erbsen2016-09-26
* add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26
* alternative signing derivationGravatar Andres Erbsen2016-09-22
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* ModularArithmetic: conversions between [F] and [nat]Gravatar Andres Erbsen2016-09-16
* Fully qualify [Require]sGravatar Jason Gross2016-09-08
* remove eq_dec from MonoidGravatar Andres Erbsen2016-08-23
* [cbv beta] in the beginning of Obligation Tactic for 8.5Gravatar Andres Erbsen2016-08-08
* [F] has its own module nowGravatar Andres Erbsen2016-08-05
* Refactor ModularArithmetic into Zmod, expand DecidableGravatar Andres Erbsen2016-08-04
* compute on [F q]!Gravatar Andres Erbsen2016-07-20
* remove field_algebraGravatar Andres Erbsen2016-07-11
* added proofs about addition chain exponentiation for later use in ModularBase...Gravatar jadep2016-07-10
* Define the spec of Weierstrass curves (#6)Gravatar Jason Gross2016-07-03
* scalarmult support; EdDSA.sign produces valid signaturesGravatar Andres Erbsen2016-06-27
* EdDSA: prove things about specGravatar Andres Erbsen2016-06-25
* EdDSA.Notations: indentationGravatar Andres Erbsen2016-06-22
* Fix broken notations (hopefully)Gravatar Jason Gross2016-06-22
* Handle renaming of NPeano.pow to Nat.pow (#3)Gravatar Jason Gross2016-06-22
* EdDSA.v: resolve ambiguity based on ed25519.pyGravatar Andres Erbsen2016-06-21
* Whitespace changeGravatar Jason Gross2016-06-21
* use Local Obligation Tactic (8.5-compat)Gravatar Andres Erbsen2016-06-21
* remove trailing whitespace from src/Gravatar Andres Erbsen2016-06-20
* Remove anything incompatible with new algebraic hierarcyGravatar Andres Erbsen2016-06-20
* Merge branch 'field-experiment'Gravatar Andres Erbsen2016-06-20
|\
| * port EdDSA specGravatar Andres Erbsen2016-06-20
| * move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheoremsGravatar Andres Erbsen2016-06-17
| * port edwards curve specGravatar Andres Erbsen2016-06-16
* | Minor 8.5 changesGravatar Jason Gross2016-06-10
* | More changes for 8.5Gravatar Jason Gross2016-06-10
| * before changing SRep from N to F lGravatar Andres Erbsen2016-05-27
|/
* Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-04-29
* Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 13:15:02 +0000