Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Reserve a notatoin for ;; | 2018-06-16 | |
| | |||
* | Add zrange equality | 2018-06-15 | |
| | |||
* | Add ErrorT monad, and Show class | 2018-06-15 | |
| | |||
* | Add decimal_string_of_Z | 2018-06-15 | |
| | |||
* | Add some lemmas and defs to ListUtil.FoldBool | 2018-06-14 | |
| | |||
* | Set universe polymorphism in CPSNotations | 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 | 2018-06-14 | |
| | |||
* | Actually use primitive projections in PrimitiveHList | 2018-06-13 | |
| | |||
* | Minor refactoring | 2018-06-13 | |
| | | | | Note that List.repeat (ListUtil.List.repeat) rather than repeat (Coq.Lists.List.repeat) was interfering with extraction | ||
* | Add PrimitiveHList, PrimitiveProd | 2018-06-13 | |
| | |||
* | Move Option.List.map to OptionList.map to fix name clashes in Tuple | 2018-06-04 | |
| | |||
* | Add Option.List.map | 2018-06-04 | |
| | |||
* | Move cps notations into a scope | 2018-06-01 | |
| | |||
* | Add more bind reserved notations | 2018-05-31 | |
| | |||
* | fix over-indented line | 2018-05-31 | |
| | |||
* | prove prefancy->fancy for barrett special case | 2018-05-31 | |
| | |||
* | move around some Lets so that 8.8 doesn't error | 2018-05-31 | |
| | |||
* | relocate ok_expr tactics and fix an admit with a silly bounds relaxation hack | 2018-05-31 | |
| | |||
* | Proved pre-fancy barrett reduction correct (except 1 admit for bounds | 2018-05-31 | |
| | | | | | that are correct but for which bounds relaxation loses necessary information) and add explanatory comments. | ||
* | temporary workaround for #352 | 2018-05-31 | |
| | |||
* | Define machine model, write prefancy->fancy pass, and prove Montgomery code ↵ | 2018-05-31 | |
| | | | | correct | ||
* | [WIP] shifting adds | 2018-05-31 | |
| | |||
* | change order of additions so that they a) make more sense and b) are more ↵ | 2018-05-31 | |
| | | | | suited to shifting adds | ||
* | tweak binders so that shifts from base conversion get inlined | 2018-05-31 | |
| | |||
* | remove unneeded comment and extra whitespace | 2018-05-31 | |
| | |||
* | end-to-end proof for montgomery | 2018-05-31 | |
| | |||
* | Proofs for pre-fancy pass (could use cleanup) | 2018-05-31 | |
| | |||
* | proofs for straightline pass (with admits for some depth stuff that should ↵ | 2018-05-31 | |
| | | | | be unneeded soon) | ||
* | Move function argument out of fixpoint of List.map2 | 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. | 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 | 2018-05-07 | |
| | |||
* | replace dummy_var with dummy_arrow and change style of straightline tests to ↵ | 2018-05-07 | |
| | | | | be more robust | ||
* | clean up shared notations and constant-rewriting logic for prefancy | 2018-05-07 | |
| | |||
* | prefancy now works on barrett (modulo add-opp=>sub) | 2018-05-07 | |
| | |||
* | Move straightline and prefancy stuff above barrett reduction | 2018-05-07 | |
| | |||
* | Translating to 'pre-fancy' form now works on Montgomery | 2018-05-07 | |
| | |||
* | move depth to a more sensible location | 2018-05-07 | |
| | |||
* | Translation to straightline code now works correctly on montgomery256 | 2018-05-07 | |
| | |||
* | Translation to straightline code (first attempts, mostly working) | 2018-05-07 | |
| | |||
* | fix the placement of a dlet to make more sense | 2018-05-07 | |
| | |||
* | Backtrack on moving a notation to Notations.v, to fix conflict | 2018-05-06 | |
| | |||
* | Fix notations to not conflict with bbv | 2018-05-06 | |
| | |||
* | More reserved notations | 2018-05-06 | |
| | |||
* | Add another notation | 2018-05-06 | |
| | |||
* | Fix a typo in last commit | 2018-05-06 | |
| | |||
* | Add a reserved notation for #v | 2018-05-06 | |
| | |||
* | Don't use vm_compute with existentials | 2018-05-05 | |
| | |||
* | Update comment | 2018-05-05 | |
| | |||
* | Fully finish flat_map | 2018-05-05 | |
| | |||
* | Fix flat_map | 2018-05-05 | |
| |