Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Slightly better type for Interp_InterpToPHOAS | 2017-05-16 | |
| | |||
* | Add Named.ExprInversion | 2017-05-15 | |
| | |||
* | Add Wf_from_unit | 2017-05-15 | |
| | | | | | This one is much easier to compute with, and it means we can get rid of a lot of pesky Named.wff proofs. | ||
* | Add more pointed prop lemmas | 2017-05-15 | |
| | |||
* | Add src/Compilers/Z/Named/DeadCodeEliminationInterp.v | 2017-05-15 | |
| | |||
* | Add DeadCodeEliminationInterp | 2017-05-15 | |
| | |||
* | Add a stronger lemma to registerassigninterp | 2017-05-15 | |
| | |||
* | use ladderstep from donna (2% faster?) | 2017-05-15 | |
| | |||
* | disable ANormal form, we now support expression output! | 2017-05-14 | |
| | |||
* | Add reserved java notation | 2017-05-14 | |
| | |||
* | Add a reserved C notation | 2017-05-14 | |
| | |||
* | update c.sh for new return notation | 2017-05-14 | |
| | |||
* | Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ↵ | 2017-05-14 | |
|\ | | | | | | | return-notation | ||
* | | Add GetNames | 2017-05-14 | |
| | | |||
* | | Add Named.default_names_for | 2017-05-14 | |
| | | |||
| * | make display (for return statement) | 2017-05-14 | |
| | | |||
| * | Stick 'return' at the end of printed functions | 2017-05-14 | |
|/ | |||
* | make display again (really not sure what's up) | 2017-05-14 | |
| | |||
* | make display | 2017-05-14 | |
| | | | | Not quite sure what changed.... | ||
* | Add Named.CountLets | 2017-05-14 | |
| | |||
* | force carry intermediates to be bound early | 2017-05-14 | |
| | |||
* | make display (ladderstep with specialize square) | 2017-05-14 | |
| | |||
* | Use specialized square in ladderstep | 2017-05-14 | |
| | |||
* | Make proj1_sig square_sig take only one argument | 2017-05-14 | |
| | |||
* | Add Z/Named/DeadCodeElimination.v | 2017-05-14 | |
| | |||
* | Split off EliminateDeadCode | 2017-05-14 | |
| | |||
* | make display without 0x0 * _ | 2017-05-14 | |
| | |||
* | Do more arithmetic simplifying | 2017-05-14 | |
| | | | | Needed to remove some multiplication by 0 | ||
* | specialize squaring earlier | 2017-05-14 | |
| | |||
* | preserve common subexpressions in donna-derived code | 2017-05-14 | |
| | |||
* | Add support for more constants | 2017-05-14 | |
| | |||
* | applied micro-optimizations from donna with [transitivity] and [ring] (as ↵ | 2017-05-14 | |
| | | | | per #176) | ||
* | Add constant, support pair-returning assignment | 2017-05-14 | |
| | |||
* | More debug info in reification | 2017-05-14 | |
| | |||
* | remove lingering [About] | 2017-05-14 | |
| | |||
* | remove redundant definition | 2017-05-14 | |
| | |||
* | make freeze use the correct versions of add_get_carry and zselect | 2017-05-14 | |
| | |||
* | add wrapper for add_get_carry and proofs for add_get_carry and zselect | 2017-05-14 | |
| | |||
* | Add lemma justifying compiler optimization for adc | 2017-05-14 | |
| | |||
* | Fix notation binding levels so types work in nlet | 2017-05-14 | |
| | |||
* | Add some reserved notations | 2017-05-14 | |
| | |||
* | Ooops, I mixed up Bind Scope and Delimit Scope | 2017-05-14 | |
| | |||
* | Fix some scoping | 2017-05-14 | |
| | |||
* | Allow specifying type in nlet | 2017-05-14 | |
| | |||
* | Comment out CSE in pipeline | 2017-05-14 | |
| | |||
* | CSE without inlining arithmetic expressions | 2017-05-14 | |
| | | | | | | | | | | This takes care of most of #158. The remaining bits are reworking the Wf and interpretation lemmas to actually work. (The former needs a only bit of rethinking and rephrasing to handle the fact that sometimes we change the stored symbolic expression from a complicated one to a fresh variable, while the latter needs major surgery, which Adam tells me is easy, and this is a note that when I come back to it, I should look at the email thread with Adam about CSE from last summer.) | ||
* | Add Z.div_le_mono_nonneg | 2017-05-13 | |
| | |||
* | Add mod_bound_min_max | 2017-05-13 | |
| | |||
* | Add proper lemma for add_with_carry | 2017-05-13 | |
| | |||
* | Change definition of add_get_carry | 2017-05-13 | |
| | | | | | The new definition is judgmentally equal to the old one, but is slightly easier to reify. |