aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* | make field on F automatically clean up the constant-vomit it expandsGravatar Andres Erbsen2016-02-11
* | port some Edwards curve stuff from GF to FGravatar Andres Erbsen2016-02-11
* | port several theorems from GF to FGravatar Andres Erbsen2016-02-11
* | Define F m, a replacement for GF with several benefits.Gravatar Andres Erbsen2016-02-11
* | fresh take at specifications using implicit arguments instead of module param...Gravatar Andres Erbsen2016-02-07
* | remove a dangling AboutGravatar Andres Erbsen2016-02-07
|/
* 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
| * Specific/GF25519: factor out lemmasGravatar Andres Erbsen2016-02-07
| * Do some work pair-programming with Andres on optsGravatar Jason Gross2016-02-05
| * Update build process to use COQPATH & _CoqProjectGravatar Jason Gross2016-02-05
* | GaloisTheory: added lemmas useful for proving Euler's Criterion with GF. NumT...Gravatar Jade Philipoom2016-02-02
* | ModualrBaseSystem: proved lingering admit in subtraction proof.Gravatar Jade Philipoom2016-01-25
|/
* NumTheoryUtil: proved Fermat's Little Theorem.Gravatar Jade Philipoom2016-01-23
* NumTheoryUtil : code cleanup; moved some lemmas to ZUtil.Gravatar Jade Philipoom2016-01-23
* Import coqprime; use it to prove Euler's criterion.Gravatar Jade Philipoom2016-01-20
* 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
|\
| * Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-13
| |\
| * | euler's criterion reduced to fermat's little theorem and two lemmas about pri...Gravatar Jade Philipoom2016-01-13
* | | simple tactic ruleGravatar Rob Sloan2016-01-11
* | | 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
* | fix field for division by constant (by dmz@mit.edu)Gravatar Andres Erbsen2016-01-07
* | fix unverified typo in fermat proofGravatar Andres Erbsen2016-01-07
* | Start writing PointFormats field proofsGravatar Andres Erbsen2016-01-07
* | Merge branch 'specific-rewrite'Gravatar Andres Erbsen2016-01-06
|\ \ | |/ |/|
| * fix letify to only insert a term onceGravatar Andres Erbsen2016-01-06
* | Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar Jade Philipoom2016-01-05
|\ \
* | | Specific/EdDSA25519: created most of specific instantiation of EdDSA; still m...Gravatar Jade Philipoom2016-01-05
* | | PointFormats/EdDSA: scoping tweaks in PointFormats, small changes of phrasing...Gravatar Jade Philipoom2016-01-05
* | | Util: added util lemmas needed to instantiate EdDSA25519.Gravatar Jade Philipoom2016-01-05
| * | remove commentGravatar Andres Erbsen2016-01-04
| | * prettier GF25519 derivation that runs out of memoryGravatar Andres Erbsen2016-01-04
| | * UNTESTED simplification of specific GF25519 derivationGravatar Andres Erbsen2016-01-02
| |/
| * draft of Fermat's Little TheoremGravatar Andres Erbsen2015-12-31
|/
* Code-reviewing EdDSAGravatar Adam Chlipala2015-12-29
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 15:53:37 +0000