aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Collapse)AuthorAge
* reorganized lemmas; moved several to ListUtil and ZUtil.Gravatar Jade Philipoom2015-11-24
|
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17
|
* Merge remote-tracking branch 'jadep/master'Gravatar Andres Erbsen2015-11-06
|\
* | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19)Gravatar Andres Erbsen2015-11-06
|/
* Beautified BinGF.splitWordsGravatar Adam Chlipala2015-10-30
|
* word bound propagation examplesGravatar Andres Erbsen2015-10-30
|
* BaseSystem to Util.ListUtil: separate out generic list lemmasGravatar Andres Erbsen2015-10-29
|
* Merge branch 'master' of github.mit.edu:rsloan/fiat-cryptoGravatar Andres Erbsen2015-10-29
|\
| * patches for galoisGravatar Robert Sloan2015-10-27
| |
* | positional number system equivalence transcribed from pencil-and-paper ↵Gravatar Andres Erbsen2015-10-25
|/ | | | proofs by <jadep@mit.edu>
* add morphism-based field implGravatar Robert Sloan2015-10-22
|
* fix the makefile to not rebuild + module renamingGravatar Robert Sloan2015-10-22
|
* pull changes from desktopGravatar Robert Sloan2015-10-19
|
* gfPlus abstractionGravatar Robert Sloan2015-10-16
|
* make ring decidable + define constantsGravatar Robert Sloan2015-09-19
|
* makefile dependency orderGravatar Andres Erbsen2015-09-18
|
* Curves: elliptic curve point format record declarations and some invariantsGravatar Andres Erbsen2015-09-18
|
* import VerdiTacticsGravatar Andres Erbsen2015-09-17
|
* redo module structure + init curve25519Gravatar Robert Sloan2015-09-16
|
* init our centralized repoGravatar Robert Sloan2015-09-10