Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | merge | 2016-07-10 | ||
|\ | ||||
* | | added proofs about addition chain exponentiation for later use in ↵ | 2016-07-10 | ||
| | | | | | | | | ModularBaseSystem [pow], which we need for sqrt and inversion. | |||
| * | Fix ListUtil for Coq 8.4 | 2016-07-10 | ||
| | | ||||
| * | Update ListUtil | 2016-07-08 | ||
| | | ||||
| * | Add useful tactics and util lemmas | 2016-07-08 | ||
| | | ||||
| * | Add a ListUtil lemma | 2016-07-08 | ||
| | | ||||
| * | Add a ListUtil lemma | 2016-07-08 | ||
| | | ||||
| * | Fix ListUtil for Coq 8.4 | 2016-07-08 | ||
| | | | | | | | | | | [rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only accepts one database in 8.4. | |||
| * | Add update_nth out of bounds | 2016-07-07 | ||
| | | ||||
| * | Add hint db in ListUtil | 2016-07-07 | ||
| | | ||||
| * | More ListUtil facts | 2016-07-07 | ||
| | | ||||
| * | Slightly better arguments in ListUtil | 2016-07-07 | ||
| | | ||||
| * | Correct hintdb names | 2016-07-07 | ||
| | | ||||
| * | Add more about firstn to listutil | 2016-07-07 | ||
| | | ||||
| * | Add more update_nth to ListUtil | 2016-07-07 | ||
| | | ||||
| * | Fix ListUtil for Coq 8.4 | 2016-07-07 | ||
|/ | ||||
* | Add [update_nth] to ListUtil, change [set_nth] | 2016-07-06 | ||
| | | | | Define [set_nth] in terms of [update_nth] | |||
* | Fix for broken 8.5 build in ListUtil | 2016-07-06 | ||
| | ||||
* | Factored out some proofs that rely only on base being powers of two, and ↵ | 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/ | 2016-06-20 | ||
| | ||||
* | Finished admits for canonicalization proofs. | 2016-06-14 | ||
| | ||||
* | progress on second stage (conditional constant-time subtraction) of ↵ | 2016-06-13 | ||
| | | | | canonicalization proofs | |||
* | starting rewrite using different definition of map | 2016-06-11 | ||
| | ||||
* | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵ | 2016-04-28 | ||
| | | | | general contexts. | |||
* | Cleanup of GF25519 | 2016-04-20 | ||
| | ||||
* | moved lemmas from ModularBaseSystemProofs to various Util files | 2016-04-20 | ||
| | ||||
* | Added lemmas to Util/ that are needed for testbit. | 2016-04-19 | ||
| | ||||
* | Finish absolutizing imports | 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 | 2016-01-06 | ||
| | ||||
* | reorganized lemmas; moved several to ListUtil and ZUtil. | 2015-11-24 | ||
| | ||||
* | Added base_succ precondition to BaseSystem to help prove carrying. | 2015-11-19 | ||
| | ||||
* | ModularBaseSystem: carry_rep has boring modular arithmetic proofs | 2015-11-17 | ||
| | ||||
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | 2015-11-17 | ||
| | ||||
* | BaseSystem: more boring | 2015-11-10 | ||
| | ||||
* | ModularBaseSystem: finished most admits for addition and multiplication, ↵ | 2015-11-09 | ||
| | | | | moved some lemmas to ListUtil. | |||
* | ModularBaseSystem: prove some admits in mase system extension | 2015-11-07 | ||
| | ||||
* | ModularBaseSystem: continuing to prove base_good. | 2015-11-07 | ||
| | ||||
* | Merge remote-tracking branch 'jadep/master' | 2015-11-06 | ||
|\ | ||||
* | | instantiate BaseSystem using base 2^ceil(25.5i) representation of GF(2^255-19) | 2015-11-06 | ||
| | | ||||
| * | Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. | 2015-11-05 | ||
| | | ||||
| * | Relocated boring tactic to ListUtil and added combine_truncate lemma. | 2015-11-04 | ||
|/ | ||||
* | set_nth_splice case coverage | 2015-11-03 | ||
| | ||||
* | more set_nth | 2015-11-03 | ||
| | ||||
* | set_nth | 2015-11-01 | ||
| | ||||
* | BaseSystem to Util.ListUtil: separate out generic list lemmas | 2015-10-29 | ||