Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Add hint db in ListUtil | Jason Gross | 2016-07-07 | |
| | | ||||
| * | More ListUtil facts | Jason Gross | 2016-07-07 | |
| | | ||||
| * | Slightly better arguments in ListUtil | Jason Gross | 2016-07-07 | |
| | | ||||
| * | Correct hintdb names | Jason Gross | 2016-07-07 | |
| | | ||||
| * | Add more about firstn to listutil | Jason Gross | 2016-07-07 | |
| | | ||||
| * | Add more update_nth to ListUtil | Jason Gross | 2016-07-07 | |
| | | ||||
| * | Fix ListUtil for Coq 8.4 | Jason Gross | 2016-07-07 | |
|/ | ||||
* | Add [update_nth] to ListUtil, change [set_nth] | Jason Gross | 2016-07-06 | |
| | | | | Define [set_nth] in terms of [update_nth] | |||
* | Fix for broken 8.5 build in ListUtil | Jason Gross | 2016-07-06 | |
| | ||||
* | Factored out some proofs that rely only on base being powers of two, and ↵ | jadep | 2016-07-06 | |
| | | | | defined conversion between two such bases. This will allow conversion between the pseudomersenne base representation and the wire format. Also relocated some lemmas to Util. | |||
* | remove trailing whitespace from src/ | Andres Erbsen | 2016-06-20 | |
| | ||||
* | Finished admits for canonicalization proofs. | jadep | 2016-06-14 | |
| | ||||
* | progress on second stage (conditional constant-time subtraction) of ↵ | jadep | 2016-06-13 | |
| | | | | canonicalization proofs | |||
* | starting rewrite using different definition of map | jadep | 2016-06-11 | |
| | ||||
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵ | jadep | 2016-04-28 | |
| | | | | general contexts. | |||
* | Cleanup of GF25519 | jadep | 2016-04-20 | |
| | ||||
* | moved lemmas from ModularBaseSystemProofs to various Util files | jadep | 2016-04-20 | |
| | ||||
* | Added lemmas to Util/ that are needed for testbit. | jadep | 2016-04-19 | |
| | ||||
* | Finish absolutizing imports | Jason Gross | 2016-03-10 | |
| | | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ``` | |||
* | fix letify to only insert a term once | Andres Erbsen | 2016-01-06 | |
| | ||||
* | reorganized lemmas; moved several to ListUtil and ZUtil. | Jade Philipoom | 2015-11-24 | |
| | ||||
* | Added base_succ precondition to BaseSystem to help prove carrying. | Jade Philipoom | 2015-11-19 | |
| | ||||
* | ModularBaseSystem: carry_rep has boring modular arithmetic proofs | Andres Erbsen | 2015-11-17 | |
| | ||||
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | Andres Erbsen | 2015-11-17 | |
| | ||||
* | BaseSystem: more boring | Andres Erbsen | 2015-11-10 | |
| | ||||
* | ModularBaseSystem: finished most admits for addition and multiplication, ↵ | Jade Philipoom | 2015-11-09 | |
| | | | | moved some lemmas to ListUtil. | |||
* | ModularBaseSystem: prove some admits in mase system extension | Andres Erbsen | 2015-11-07 | |
| | ||||
* | ModularBaseSystem: continuing to prove base_good. | Jade Philipoom | 2015-11-07 | |
| | ||||
* | Merge remote-tracking branch 'jadep/master' | Andres Erbsen | 2015-11-06 | |
|\ | ||||
* | | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19) | Andres Erbsen | 2015-11-06 | |
| | | ||||
| * | Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. | Jade Philipoom | 2015-11-05 | |
| | | ||||
| * | Relocated boring tactic to ListUtil and added combine_truncate lemma. | Jade Philipoom | 2015-11-04 | |
|/ | ||||
* | set_nth_splice case coverage | Andres Erbsen | 2015-11-03 | |
| | ||||
* | more set_nth | Andres Erbsen | 2015-11-03 | |
| | ||||
* | set_nth | Andres Erbsen | 2015-11-01 | |
| | ||||
* | BaseSystem to Util.ListUtil: separate out generic list lemmas | Andres Erbsen | 2015-10-29 | |