Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | Merge pull request #22 from mit-plv/wrap-nsatz | 2016-07-11 | ||
| |\ | | | | | | | stop using raw nsatz, field_algebra, common_denominator | |||
| | * | s/conservative_common_denominator/common_denominator/g | 2016-07-11 | ||
| | | | ||||
| | * | rename [common_denominator] to [field_simplify_if_div] | 2016-07-11 | ||
| | | | ||||
| | * | remove field_algebra | 2016-07-11 | ||
| | | | ||||
| | * | port CompleteEdwardsCurveTheorems (builds again) | 2016-07-11 | ||
| | | | ||||
| | * | pose proof fails where specialize works (typeclass resolution / unification?) | 2016-07-11 | ||
| | | | ||||
| | * | wrap nsatz in Algebra | 2016-07-11 | ||
| |/ | ||||
| * | [congruence] is more powerful in 8.5 than in 8.4 | 2016-07-11 | ||
| | | ||||
| * | Add 8.5pl2 to travis | 2016-07-11 | ||
| | | ||||
| * | 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. | |||
| | * | Update .gitignore | 2016-07-10 | ||
| | | | ||||
| | * | Fix ListUtil for Coq 8.4 | 2016-07-10 | ||
| | | | ||||
| | * | Update ListUtil | 2016-07-08 | ||
| | | | ||||
| | * | Fix NatUtil for 8.4 | 2016-07-08 | ||
| | | | ||||
| | * | Add useful tactics and util lemmas | 2016-07-08 | ||
| | | | ||||
* | | | proved correctness of [add] operation in ModularBaseSystemInterface | 2016-07-08 | ||
| | | | ||||
* | | | defined some group operations, stated group lemma for tuple-based [add] (in ↵ | 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 ↵ | 2016-07-08 | ||
| | | | | | | | | | | | | conversion | |||
| | * | Add a NatUtil lemma and db | 2016-07-08 | ||
| | | | ||||
| | * | Add a ListUtil lemma | 2016-07-08 | ||
| | | | ||||
| | * | Add a ListUtil lemma | 2016-07-08 | ||
| | | | ||||
| | * | Add Z.div_0_l to ZUtil | 2016-07-08 | ||
| | | | ||||
* | | | unstuck carry_mul_opt_cps using from_list_default | 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. | |||
* | | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | 2016-07-08 | ||
| | | | | | | | | | | | | length equality | |||
| * | | Util/Tuple: added a version of from_list that doesn't require a proof of ↵ | 2016-07-08 | ||
| | | | | | | | | | | | | length equality | |||
| * | | Added mod case to zero_bounds | 2016-07-08 | ||
| | | | ||||
| | * | 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 pow2_mod to ZUtil | 2016-07-07 | ||
| |/ | ||||
| * | Changed [auto]s to [eauto]s in ModularBaseSystemProofs for 8.5 compatibility. | 2016-07-07 | ||
| | | ||||
| * | Merge branch 'master' of github.com:mit-plv/fiat-crypto | 2016-07-07 | ||
| |\ | ||||
| | * | Fix notations, add & | 2016-07-06 | ||
| | | | ||||
| | * | Add [update_nth] to ListUtil, change [set_nth] | 2016-07-06 | ||
| | | | | | | | | | | | | Define [set_nth] in terms of [update_nth] | |||
| | * | Add notations for Z.shift{r,l} to ZUtil | 2016-07-06 | ||
| | | | ||||
| | * | Improve some reserved notations | 2016-07-06 | ||
| | | | | | | | | | | | | Compatibility with theories/Numbers/NatInt/NZBits.v | |||
| | * | Add a TODO comment | 2016-07-06 | ||
| | | | | | | | | | | | | For jadep, or for me, after the 8.5 build is fixed. | |||
| * | | Proved lingering lemmas in PointEncodingPre. | 2016-07-06 | ||
| | | | ||||
| | * | Clean up the makefile a bit | 2016-07-06 | ||
| | | | ||||
| | * | Fix coqprime clean, install targets, add cleanall | 2016-07-06 | ||
| | | | ||||
| | * | Fix for broken 8.5 build in ListUtil | 2016-07-06 | ||
| |/ | ||||
| * | fixed indentation for new lemmas in ZUtil | 2016-07-06 | ||
| | | ||||
| * | Merged changes, including new ZUtil conventions. | 2016-07-06 | ||
| |\ |