Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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. | ||
* | 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 |
| | | | | | | This bypasses universe inconsistencies that arise when trying to return continuations from other continuations, which is a scenario that comes up frequently with cpsbind. | ||
* | 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 |
| | | | | Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction | ||
* | 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 |
| | | | | | that are correct but for which bounds relaxation loses necessary information) and add explanatory comments. | ||
* | temporary workaround for #352 | Jade Philipoom | 2018-05-31 |
| | |||
* | Define machine model, write prefancy->fancy pass, and prove Montgomery code ↵ | Jade Philipoom | 2018-05-31 |
| | | | | correct | ||
* | [WIP] shifting adds | Jade Philipoom | 2018-05-31 |
| | |||
* | change order of additions so that they a) make more sense and b) are more ↵ | Jade Philipoom | 2018-05-31 |
| | | | | suited to shifting adds | ||
* | 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 |
| | |||
* | Proofs for pre-fancy pass (could use cleanup) | Jade Philipoom | 2018-05-31 |
| | |||
* | proofs for straightline pass (with admits for some depth stuff that should ↵ | Jade Philipoom | 2018-05-31 |
| | | | | be unneeded soon) | ||
* | Move function argument out of fixpoint of List.map2 | Jason Gross | 2018-05-21 |
| | | | | | This allows us to make use of nested fixpoints involving map2, because the function argument can be inlined for guard checking now. | ||
* | Compatibility after Coq PR#262. | Hugo Herbelin | 2018-05-14 |
| | | | | | | | | | Coq PR#262 makes the inference of return clauses more uniform and general but unification is sometimes not strong enough to deal with this generality. See #5107 for details. One reduces the search space for a return clause by forbidding it to be obtained by small inversion. | ||
* | finish pushing through changes to dummy and factor out identifier match | Jade Philipoom | 2018-05-07 |
| | |||
* | replace dummy_var with dummy_arrow and change style of straightline tests to ↵ | Jade Philipoom | 2018-05-07 |
| | | | | be more robust | ||
* | clean up shared notations and constant-rewriting logic for prefancy | Jade Philipoom | 2018-05-07 |
| | |||
* | prefancy now works on barrett (modulo add-opp=>sub) | Jade Philipoom | 2018-05-07 |
| | |||
* | Move straightline and prefancy stuff above barrett reduction | Jade Philipoom | 2018-05-07 |
| | |||
* | Translating to 'pre-fancy' form now works on Montgomery | Jade Philipoom | 2018-05-07 |
| | |||
* | move depth to a more sensible location | Jade Philipoom | 2018-05-07 |
| | |||
* | Translation to straightline code now works correctly on montgomery256 | Jade Philipoom | 2018-05-07 |
| | |||
* | Translation to straightline code (first attempts, mostly working) | Jade Philipoom | 2018-05-07 |
| | |||
* | fix the placement of a dlet to make more sense | Jade Philipoom | 2018-05-07 |
| | |||
* | Backtrack on moving a notation to Notations.v, to fix conflict | Jason Gross | 2018-05-06 |
| |