aboutsummaryrefslogtreecommitdiff
path: root/src/Curves
Commit message (Expand)AuthorAge
* 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
* PointFormats: extended coordinates equivalence proofsGravatar Andres Erbsen2016-01-16
* fix merge conflicts + PointFormats proofsGravatar Robert Sloan2016-01-14
|\
* | assumption lemmas in PointFormatsGravatar Rob Sloan2016-01-11
* | simple refactor of makefile; commentsGravatar varomodt2016-01-09
| * cleanupGravatar Andres Erbsen2016-01-08
|/
* PointFormats: factor out admitsGravatar Andres Erbsen2016-01-08
* PointFormats: no zero denominators in Edwards additionGravatar Andres Erbsen2016-01-08
* PointFormats: addition produces points on curveGravatar Andres Erbsen2016-01-07
* Start writing PointFormats field proofsGravatar Andres Erbsen2016-01-07
* PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing...Gravatar Jade Philipoom2016-01-05
* PointFormats : removed reliance on Pos.size_nat; doubleAndAdd now takes an ar...Gravatar Jade Philipoom2015-12-28
* PointFormats : changed iter_op to allow overestimating bitlength of argument.Gravatar Jade Philipoom2015-12-26
* Removed OpWithZero typeclass in favor of explicit arguments.Gravatar Jade Philipoom2015-12-25
* PointFormats: completed remaining admits for non-destruction doubleAndAdd.Gravatar Jade Philipoom2015-12-24
* PointFormats: implemented doubleAndAdd without destructing scalar and proved ...Gravatar Jade Philipoom2015-12-24
* PointFormats: wrote and proved equivalent a double-and-add implementation of ...Gravatar Jade Philipoom2015-12-20
* PointFormats: all Edwards25519 points are onCurveGravatar Andres Erbsen2015-12-15
* EdDSA: mostly-complete spec and preliminary structure.Gravatar Jade Philipoom2015-12-12
* More improved structure for EdDSA and PointFormats.Gravatar Jade Philipoom2015-12-10
* More refacoring PointFormats.Gravatar Jade Philipoom2015-12-09
* Rewrote PointFormats to be parameterized by modulus; reformatting of EdDSA.Gravatar Jade Philipoom2015-12-09
* scalar multiplicationGravatar Andres Erbsen2015-11-25
* remove resolved todoGravatar Andres Erbsen2015-10-28
* Tiny module-system tweaks in PointFormatsGravatar Adam Chlipala2015-10-28
* fix the makefile to not rebuild + module renamingGravatar Robert Sloan2015-10-22
|\
* | fix the makefile to not rebuild + module renamingGravatar Robert Sloan2015-10-22
| * disable Curve25519 until PointFormats is parametric or we give up and retryGravatar Andres Erbsen2015-10-22
| * refactor pointformats to use have a module type of correct implementationsGravatar Andres Erbsen2015-10-22
|/
* pull changes from desktopGravatar Robert Sloan2015-10-19
* pull changes from desktopGravatar Robert Sloan2015-10-19
* Small PointFormats tweaks while reading throughGravatar Adam Chlipala2015-10-12
* comment out edwards<->montgomery conversionGravatar Andres Erbsen2015-10-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 05:46:26 +0000