Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | 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 | |
| | ||||
* | Fix notations to not conflict with bbv | Jason Gross | 2018-05-06 | |
| | ||||
* | More reserved notations | Jason Gross | 2018-05-06 | |
| | ||||
* | Add another notation | Jason Gross | 2018-05-06 | |
| | ||||
* | Fix a typo in last commit | Jason Gross | 2018-05-06 | |
| | ||||
* | Add a reserved notation for #v | Jason Gross | 2018-05-06 | |
| | ||||
* | Don't use vm_compute with existentials | Jason Gross | 2018-05-05 | |
| | ||||
* | Update comment | Jason Gross | 2018-05-05 | |
| | ||||
* | Fully finish flat_map | Jason Gross | 2018-05-05 | |
| | ||||
* | Fix flat_map | Jason Gross | 2018-05-05 | |
| | ||||
* | WIP on lists as cons cells | Jason Gross | 2018-05-05 | |
| | ||||
* | Remove vinterp_arrow function | Jason Gross | 2018-05-05 | |
| | ||||
* | Revert "WIP on inductive base_value" | Jason Gross | 2018-05-05 | |
| | | | | This reverts commit e38faaac1d3996c61d396144e20b8bb41809a253. | |||
* | WIP on inductive base_value | Jason Gross | 2018-05-05 | |
| | ||||
* | Revert "WIP with andres, not working pattern language" | Jason Gross | 2018-05-05 | |
| | | | | This reverts commit 2fcf4cd6aabebb3b68cc0a807e5d7c78e9142cb5. | |||
* | WIP with andres, not working pattern language | Jason Gross | 2018-05-05 | |
| | ||||
* | Add comment about leaky abstraction | Jason Gross | 2018-05-05 | |
| | ||||
* | Split off specialization to base types from specialization to idents | Jason Gross | 2018-05-05 | |
| | ||||
* | Add type variables / substitutions | Jason Gross | 2018-05-05 | |
| | | | | This allows more genericness in the ident-specific code | |||
* | Change some notations for more readability by Andres | Jason Gross | 2018-05-05 | |
| | ||||
* | Update cast -> annotate | Jason Gross | 2018-05-05 | |
| | ||||
* | Parameterize over types and identifiers | Jason Gross | 2018-05-05 | |
| | ||||
* | Add notes | Jason Gross | 2018-05-05 | |
| | ||||
* | Add partial evaluation | Jason Gross | 2018-05-05 | |
| |