aboutsummaryrefslogtreecommitdiff
path: root/src/Curves
Commit message (Expand)AuthorAge
* parenthesize proofs in Weierstrass.Projective (closes #456)Gravatar Andres Erbsen2018-11-11
* Adapt to Coq's PR#8555Gravatar Maxime Dénès2018-10-02
* Import prim token notations before using themGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Compatibility after Coq PR#262.Gravatar Hugo Herbelin2018-05-14
* Generalize Jacobian.v over all a.Gravatar David Benjamin2018-04-25
* move Loops from Experiments to UtilGravatar Andres Erbsen2018-03-27
* cleanup2Gravatar Andres Erbsen2018-03-27
* Combine the zero and non-zero cases together.Gravatar David Benjamin2018-01-15
* Factor out fsatz lemmasGravatar Jason Gross2018-01-09
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
* Massively speed up JacobianGravatar Jason Gross2018-01-09
* Revert "Replace char_ge_12 with char_ge_3"Gravatar Jason Gross2018-01-09
* Replace char_ge_12 with char_ge_3Gravatar Jason Gross2018-01-09
* Jabobian.v: par -> allGravatar Andres Erbsen2018-01-09
* src/Curves/Weierstrass/Jacobian.v: specialized destruct_head_*Gravatar Andres Erbsen2018-01-09
* @davidben merged Jacobian+affine into Jacobian+JacobianGravatar Andres Erbsen2018-01-09
* Jacobian coordinatesGravatar Andres Erbsen2018-01-09
* Prove montladder correct in the zero case.Gravatar David Benjamin2018-01-08
* restore fastpath logic in Curves.Montgomery.XZProofsGravatar Andres Erbsen2017-12-22
* prove montgomery ladder for non-zero inputsGravatar Andres Erbsen2017-12-22
* Montgomery.XZ, Loops: montladder proof scaffoldingGravatar Andres Erbsen2017-12-22
* specialized destruct_head'_* in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
* expose missing proof in src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
* clean up src/Curves/Montgomery/XZProofs.vGravatar Andres Erbsen2017-12-22
* Curves.Montgomery.XZ: add+check boringssl ladderstep (#278)Gravatar Andres Erbsen2017-12-05
* projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptionalGravatar Andres Erbsen2017-10-18
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
* match C code in Jacobian additionGravatar Andres Erbsen2017-06-27
* Weierstrass Jacobian mixed additionGravatar Andres Erbsen2017-06-23
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
* 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
* use ladderstep from donna (2% faster?)Gravatar Andres Erbsen2017-05-15
* Prove relationship between `xzladderstep` and M.add (#162)Gravatar Andres Erbsen2017-04-28
* clean elliptic curve proofs, use par: in WeierstrassAffineProofsGravatar Andres Erbsen2017-04-28
* Respond to code review commentsGravatar Jason Gross2017-04-17
* Use the for-loop notation in Montgomery.XZGravatar Jason Gross2017-04-17
* lemmas about ladderstep on zeroGravatar Andres Erbsen2017-04-14
* stronger ladderstep correctness proof courtesy TeoGravatar Andres Erbsen2017-04-14
* rename-everythingGravatar Andres Erbsen2017-04-06
* Finish seperating our specs: remove old non-specified codeGravatar Andres Erbsen2016-02-15
* port some edwards curve theoremsGravatar Andres Erbsen2016-02-12
* removed lingering Check/SearchAbout statementsGravatar Jade Philipoom2016-02-07
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-02-07
|\
* | EdDSA25519 : wrote and proved optimized PointEncoding, which encodes y and th...Gravatar Jade Philipoom2016-02-07
| * PointFormats: prove dangling admitGravatar Andres Erbsen2016-02-07
|/
* PointFOrmats,EdDSA: remove redundant axiomsGravatar Andres Erbsen2016-01-16
* remove duplicate axiomGravatar Andres Erbsen2016-01-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 10:56:13 +0000