aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Tiny module-system tweaks in PointFormatsGravatar Adam Chlipala2015-10-28
* pos_pow_nat_posGravatar Andres Erbsen2015-10-25
* nth_tacGravatar Andres Erbsen2015-10-25
* slight refactoring of BaseSystemGravatar Andres Erbsen2015-10-25
* bounds checksGravatar Andres Erbsen2015-10-25
* positional number system equivalence transcribed from pencil-and-paper proofs...Gravatar Andres Erbsen2015-10-25
* primitive positional numeral system definition on top of ZGravatar Andres Erbsen2015-10-24
* add morphism-based field implGravatar Robert Sloan2015-10-22
* 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
|/
* word equivGravatar Robert Sloan2015-10-20
* pull changes from desktopGravatar Robert Sloan2015-10-19
* pull changes from desktopGravatar Robert Sloan2015-10-19
* pull changes from desktopGravatar Robert Sloan2015-10-19
* gfPlus abstractionGravatar Robert Sloan2015-10-16
* 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
* Galois: add broken testGravatar Andres Erbsen2015-09-22
* 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
* remove broken codeGravatar Robert Sloan2015-09-20
* merge with masterGravatar Robert Sloan2015-09-19
|\
* | make ring decidable + define constantsGravatar Robert Sloan2015-09-19
| * make `field` work when GaloisField and GaloisFieldTheory are imported at the ...Gravatar Andres Erbsen2015-09-18
|/
* Curves: elliptic curve point format record declarations and some invariantsGravatar Andres Erbsen2015-09-18
* GaloisFieldTheory: add scope delimiterGravatar Andres Erbsen2015-09-18
* GaloisFieldTheory: scoped notation that coincides with ZGravatar Andres Erbsen2015-09-18
* overlflow-checking ZToGF functionGravatar Andres Erbsen2015-09-17
* import VerdiTacticsGravatar Andres Erbsen2015-09-17
* Removed dependency on proof irrelevance (it turns out we had a redundant exis...Gravatar Adam Chlipala2015-09-17
* Beautified remaining GaloisFieldTheory proofsGravatar Adam Chlipala2015-09-17
* Got most of the way through new GaloisField codeGravatar Adam Chlipala2015-09-17
* fix module structure + add assembly placeholderGravatar Robert Sloan2015-09-17
* redo module structure + init curve25519Gravatar Robert Sloan2015-09-16
* Basic Galois Field Theory ModulesGravatar Robert Sloan2015-09-16
* init our centralized repoGravatar Robert Sloan2015-09-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 17:05:29 +0000