aboutsummaryrefslogtreecommitdiff
path: root/src/Spec
Commit message (Expand)AuthorAge
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* minor updates needed to make it compile with bbvGravatar Samuel Gruetter2018-02-05
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* eddsa spec fixGravatar Andres Erbsen2017-06-14
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Strip trailing whitespaceGravatar Jason Gross2017-06-02
* Support destructuring dlet and sletGravatar Jason Gross2017-05-13
* clean elliptic curve proofs, use par: in WeierstrassAffineProofsGravatar Andres Erbsen2017-04-28
* Add commented out proof of equivalence in MxDHGravatar Jason Gross2017-04-12
* rename-everythingGravatar Andres Erbsen2017-04-06
* remove Encoding stuffGravatar Andres Erbsen2017-04-06
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
* More fine-grained tactic importsGravatar Jason Gross2017-04-03
* use improved fsatz on various elliptic curve thingsGravatar Andres Erbsen2017-03-31
* make fsatz recurse when proving nonzero-ness, undo Weierstrass workaroundGravatar Andres Erbsen2017-03-30
* make 8.5 happyGravatar Andres Erbsen2017-03-02
* use [positive] for [F] modulus, char_ge_C instead of char_gt_CGravatar Andres Erbsen2017-03-02
* rewrite ExtendedCoordinates, fix Ed25519Gravatar Andres Erbsen2017-03-02
* edwards curves over isomorphic fieldsGravatar Andres Erbsen2017-03-02
* WIPGravatar Andres Erbsen2017-03-02
* address some code review commentsGravatar Andres Erbsen2017-03-02
* Weierstrass curve is a groupGravatar Andres Erbsen2017-03-02
* change weierstrass spec, prove most cases of associativityGravatar Andres Erbsen2017-03-02
* split the algebra library; use fsatz moreGravatar Andres Erbsen2017-03-02
* fsatz, nsatz_solve_nonzeroGravatar Andres Erbsen2017-03-02
* use field_nsatz in CompleteEdwardsCurve.PreGravatar Andres Erbsen2017-03-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 00:55:24 +0000