Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add a distr_length database | 2016-07-19 | |
| | |||
* | Add a lemma about sum_firstn | 2016-07-18 | |
| | |||
* | Add a ListUtil lemma | 2016-07-18 | |
| | |||
* | Fix for Coq 8.4 (missing lemmas) | 2016-07-18 | |
| | |||
* | Fix some typos in the previous commit | 2016-07-18 | |
| | |||
* | Add some lemmas about nth_default in bounds | 2016-07-18 | |
| | |||
* | Added lemmas to ZUtil and NatUtil (for Testbit) | 2016-07-18 | |
| | |||
* | 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 | |
| |