Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | WIP better square | Jason Gross | 2018-07-03 | |
| | ||||
* | Fix missing arg | Jason Gross | 2018-07-03 | |
| | ||||
* | Add missing space | Jason Gross | 2018-07-03 | |
| | ||||
* | Add support for annotating generated C functions with comments | Jason Gross | 2018-07-03 | |
| | | | | As requested by @davidben (though I haven't yet written any comments for the functions) | |||
* | Synthesize selectznz | Jason Gross | 2018-07-03 | |
| | ||||
* | Correctly reify match on prod | Jason Gross | 2018-07-03 | |
| | ||||
* | Add select | Jason Gross | 2018-07-03 | |
| | ||||
* | Comment out some code that's too slow | Jason Gross | 2018-07-03 | |
| | ||||
* | Allow passing functions to synthesize on the command line, and scmul for 25519 | Jason Gross | 2018-07-03 | |
| | ||||
* | Pull out *2 in square, don't turn *2 into <<1 | Jason Gross | 2018-07-03 | |
| | ||||
* | No subst01 in mulmod | Jason Gross | 2018-07-03 | |
| | ||||
* | Start with a better template for carry_square | Jason Gross | 2018-07-03 | |
| | ||||
* | Don't subst01 in square | Jason Gross | 2018-07-03 | |
| | ||||
* | synthesize square | Jason Gross | 2018-07-03 | |
| | ||||
* | static in c | Jason Gross | 2018-07-03 | |
| | ||||
* | static void | Jason Gross | 2018-07-03 | |
| | ||||
* | WIP | Jason Gross | 2018-07-03 | |
| | ||||
* | Add ZUtil, list lemmas | Jason Gross | 2018-07-02 | |
| | ||||
* | Fix a notation issue in previous commit | Jason Gross | 2018-07-02 | |
| | ||||
* | Add more ListUtil proofs | Jason Gross | 2018-07-02 | |
| | ||||
* | Add some list lemmas | Jason Gross | 2018-07-02 | |
| | ||||
* | Make all parameters implicit | Jasper Hugunin | 2018-07-02 | |
| | ||||
* | Prefer relations of the form [eq ==> eq ==> ... ==> eq] in setoids | Jason Gross | 2018-07-01 | |
| | | | | Also make it easy to redeclare such instances. | |||
* | Add useful list lemmas | Jason Gross | 2018-06-29 | |
| | ||||
* | Add ZUtil.Sorting | Jason Gross | 2018-06-29 | |
| | ||||
* | Revert "Add more schemes for prod" | Jason Gross | 2018-06-28 | |
| | | | | | | This reverts commit 5d38a03f5a9f69a78a582cc9cc1c350dc6596cd3. Some of these already exist in Datatypes | |||
* | Add more schemes for prod | Jason Gross | 2018-06-28 | |
| | ||||
* | Remove useless Requires | Jason Gross | 2018-06-28 | |
| | ||||
* | Try out stronger land, lor bounds | Jason Gross | 2018-06-27 | |
| | ||||
* | Add is_tighter_than_bool lemmas | Jason Gross | 2018-06-27 | |
| | ||||
* | Add lnot mod pull/push lemmas | Jason Gross | 2018-06-27 | |
| | ||||
* | Add missing Z.lnot_0 hints | Jason Gross | 2018-06-27 | |
| | ||||
* | Add more Z const hints | Jason Gross | 2018-06-27 | |
| | ||||
* | Remove lneg in favor of lnot_modulo (lneg was wrong) | Jason Gross | 2018-06-27 | |
| | ||||
* | Add some Z.land, Z.lor hints | Jason Gross | 2018-06-27 | |
| | ||||
* | Add a couple of zrange lemmas | Jason Gross | 2018-06-26 | |
| | ||||
* | Add specialize_all_ways, fix a proof in ↵ | Jason Gross | 2018-06-26 | |
| | | | | src/Compilers/Z/ArithmeticSimplifierInterp.v | |||
* | Add Z.bneg, Z.lneg | Jason Gross | 2018-06-26 | |
| | ||||
* | Slightly better definitions of some ZUtil functions | Jason Gross | 2018-06-26 | |
| | | | | | This way we can just directly reify most of the primitives we care about. | |||
* | Add list_beq | Jason Gross | 2018-06-22 | |
| | ||||
* | Add Option.List.bind_list | Jason Gross | 2018-06-21 | |
| | ||||
* | Add [freeze] to Arithmetic | Jason Gross | 2018-06-21 | |
| | ||||
* | Add extend_to_length for non-uniform-length add, sub | Jason Gross | 2018-06-19 | |
| | ||||
* | Add seq_add, seq_len_0 | Jason Gross | 2018-06-19 | |
| | ||||
* | Add a comment about sub | Jason Gross | 2018-06-18 | |
| | ||||
* | More compact printing of ASTs in errors | Jason Gross | 2018-06-18 | |
| | ||||
* | Add another prime example | Jason Gross | 2018-06-18 | |
| | ||||
* | Fix a typo in to-C shifts | Jason Gross | 2018-06-18 | |
| | ||||
* | Don't duplicate error message printing in OCaml | Jason Gross | 2018-06-18 | |
| | ||||
* | Pass around lists of strings for error messages | Jason Gross | 2018-06-17 | |
| | | | | | | | | | | This allows us to get back an error message in Saturated Solinas in OCaml on P256 x32 in reasonable time without blowing the stack. There's the slight oddity that the list of string in the success case is joined by the empty string, but the list of string in the error case is joined by newline. Probably meanas that I chose the wrong abstraction barrier somewhere. |