Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Merge of fixedlength and master | jadep | 2016-07-11 | |
|\ | ||||
* | | ported Specific files to use ModularBaseSystemInterface | jadep | 2016-07-11 | |
| | | ||||
| * | s/conservative_common_denominator/common_denominator/g | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | rename [common_denominator] to [field_simplify_if_div] | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | remove field_algebra | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | port CompleteEdwardsCurveTheorems (builds again) | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | pose proof fails where specialize works (typeclass resolution / unification?) | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | wrap nsatz in Algebra | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | [congruence] is more powerful in 8.5 than in 8.4 | Andres Erbsen | 2016-07-11 | |
| | | ||||
| * | merge | jadep | 2016-07-10 | |
| |\ | ||||
| * | | added proofs about addition chain exponentiation for later use in ↵ | jadep | 2016-07-10 | |
| | | | | | | | | | | | | ModularBaseSystem [pow], which we need for sqrt and inversion. | |||
| | * | Fix ListUtil for Coq 8.4 | Jason Gross | 2016-07-10 | |
| | | | ||||
| | * | Update ListUtil | Jason Gross | 2016-07-08 | |
| | | | ||||
| | * | Fix NatUtil for 8.4 | Jason Gross | 2016-07-08 | |
| | | | ||||
| | * | Add useful tactics and util lemmas | Jason Gross | 2016-07-08 | |
| | | | ||||
* | | | proved correctness of [add] operation in ModularBaseSystemInterface | jadep | 2016-07-08 | |
| | | | ||||
* | | | defined some group operations, stated group lemma for tuple-based [add] (in ↵ | jadep | 2016-07-08 | |
| | | | | | | | | | | | | terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor | |||
* | | | added a few length proofs to ModularBaseSystemProofs to help with tuple ↵ | jadep | 2016-07-08 | |
| | | | | | | | | | | | | conversion | |||
| | * | Add a NatUtil lemma and db | Jason Gross | 2016-07-08 | |
| | | | ||||
| | * | Add a ListUtil lemma | Jason Gross | 2016-07-08 | |
| | | | ||||
| | * | Add a ListUtil lemma | Jason Gross | 2016-07-08 | |
| | | | ||||
| | * | Add Z.div_0_l to ZUtil | Jason Gross | 2016-07-08 | |
| | | | ||||
* | | | unstuck carry_mul_opt_cps using from_list_default | jadep | 2016-07-08 | |
| | | | ||||
| | * | Fix ListUtil for Coq 8.4 | Jason Gross | 2016-07-08 | |
| | | | | | | | | | | | | | | | [rewrite_strat] ignores [using tac] sometimes, and [Hint Rewrite] only accepts one database in 8.4. | |||
* | | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | jadep | 2016-07-08 | |
| | | | | | | | | | | | | length equality | |||
| * | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | jadep | 2016-07-08 | |
| | | | | | | | | | | | | length equality | |||
| * | | Added mod case to zero_bounds | jadep | 2016-07-08 | |
| | | | ||||
| | * | Add update_nth out of bounds | Jason Gross | 2016-07-07 | |
| | | | ||||
| | * | 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 pow2_mod to ZUtil | Jason Gross | 2016-07-07 | |
| |/ | ||||
| * | Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility. | jadep | 2016-07-07 | |
| | | ||||
| * | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-07-07 | |
| |\ | ||||
| | * | Fix notations, add & | Jason Gross | 2016-07-06 | |
| | | | ||||
| | * | Add [update_nth] to ListUtil, change [set_nth] | Jason Gross | 2016-07-06 | |
| | | | | | | | | | | | | Define [set_nth] in terms of [update_nth] | |||
| | * | Add notations for Z.shift{r,l} to ZUtil | Jason Gross | 2016-07-06 | |
| | | | ||||
| | * | Improve some reserved notations | Jason Gross | 2016-07-06 | |
| | | | | | | | | | | | | Compatibility with theories/Numbers/NatInt/NZBits.v | |||
| | * | Add a TODO comment | Jason Gross | 2016-07-06 | |
| | | | | | | | | | | | | For jadep, or for me, after the 8.5 build is fixed. | |||
| * | | Proved lingering lemmas in PointEncodingPre. | jadep | 2016-07-06 | |
| | | | ||||
| | * | Fix for broken 8.5 build in ListUtil | Jason Gross | 2016-07-06 | |
| |/ | ||||
| * | fixed indentation for new lemmas in ZUtil | jadep | 2016-07-06 | |
| | | ||||
| * | Merged changes, including new ZUtil conventions. | jadep | 2016-07-06 | |
| |\ | ||||
| * \ | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | jadep | 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. | |||
* | | | | stuck trying to figure out dependently typed continuation passing style | Andres Erbsen | 2016-07-06 | |
| | | | |