| Commit message (Expand) | Author | Age |
|---|
| * | 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 src/Compilers/Z/ArithmeticSimplifierI... | Jason Gross | 2018-06-26 |
| * | Add Z.bneg, Z.lneg | Jason Gross | 2018-06-26 |
| * | Slightly better definitions of some ZUtil functions | Jason Gross | 2018-06-26 |
| * | 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 |
| * | Add ShowLines | Jason Gross | 2018-06-17 |
| * | New pipeline, split among files | Jason Gross | 2018-06-17 |
| * | Reserve a notatoin for ;; | Jason Gross | 2018-06-16 |
| * | Add zrange equality | Jason Gross | 2018-06-15 |
| * | Add ErrorT monad, and Show class | Jason Gross | 2018-06-15 |
| * | Add decimal_string_of_Z | Jason Gross | 2018-06-15 |
| * | Add some lemmas and defs to ListUtil.FoldBool | Jason Gross | 2018-06-14 |
| * | Set universe polymorphism in CPSNotations | Jason Gross | 2018-06-14 |
| * | Add notations for cpsbind, cps_option_bind | Jason Gross | 2018-06-14 |
| * | Actually use primitive projections in PrimitiveHList | Jason Gross | 2018-06-13 |
| * | Minor refactoring | Jason Gross | 2018-06-13 |
| * | Add PrimitiveHList, PrimitiveProd | Jason Gross | 2018-06-13 |
| * | Move Option.List.map to OptionList.map to fix name clashes in Tuple | Jason Gross | 2018-06-04 |
| * | Add Option.List.map | Jason Gross | 2018-06-04 |
| * | Move cps notations into a scope | Jason Gross | 2018-06-01 |
| * | Add more bind reserved notations | Jason Gross | 2018-05-31 |
| * | fix over-indented line |  Jade Philipoom | 2018-05-31 |
| * | prove prefancy->fancy for barrett special case | Jade Philipoom | 2018-05-31 |
| * | move around some Lets so that 8.8 doesn't error | Jade Philipoom | 2018-05-31 |
| * | relocate ok_expr tactics and fix an admit with a silly bounds relaxation hack | Jade Philipoom | 2018-05-31 |
| * | Proved pre-fancy barrett reduction correct (except 1 admit for bounds | Jade Philipoom | 2018-05-31 |
| * | temporary workaround for #352 | Jade Philipoom | 2018-05-31 |
| * | Define machine model, write prefancy->fancy pass, and prove Montgomery code c... | Jade Philipoom | 2018-05-31 |
| * | [WIP] shifting adds | Jade Philipoom | 2018-05-31 |
| * | change order of additions so that they a) make more sense and b) are more sui... | Jade Philipoom | 2018-05-31 |
| * | tweak binders so that shifts from base conversion get inlined | Jade Philipoom | 2018-05-31 |
| * | remove unneeded comment and extra whitespace | Jade Philipoom | 2018-05-31 |
| * | end-to-end proof for montgomery | Jade Philipoom | 2018-05-31 |
Jason Gross
Jason Gross
Jade Philipoom