aboutsummaryrefslogtreecommitdiff
path: root/src/Curves
Commit message (Expand)AuthorAge
...
* 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
* refactor point formats to use modules and prove some lemmasGravatar Andres Erbsen2015-10-07
* in case of not-on-curve points, extended coordinate addition and twisted coor...Gravatar Andres Erbsen2015-09-21
* montgomery ladder definitionGravatar Andres Erbsen2015-09-21
* make ring decidable + define constantsGravatar Robert Sloan2015-09-19
* Curves: elliptic curve point format record declarations and some invariantsGravatar Andres Erbsen2015-09-18
* fix module structure + add assembly placeholderGravatar Robert Sloan2015-09-17
* redo module structure + init curve25519Gravatar Robert Sloan2015-09-16
* init our centralized repoGravatar Robert Sloan2015-09-10