| Commit message (Collapse) | Author | Age | ||
|---|---|---|---|---|
| ... | ||||
| * | Add DeadCodeEliminationInterp |  Jason Gross | 2017-05-15 | |
| | | ||||
| * | Add a stronger lemma to registerassigninterp | Jason Gross | 2017-05-15 | |
| | | ||||
| * | use ladderstep from donna (2% faster?) |  Andres Erbsen | 2017-05-15 | |
| | | ||||
| * | disable ANormal form, we now support expression output! | Andres Erbsen | 2017-05-14 | |
| | | ||||
| * | Add reserved java notation | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Add a reserved C notation | Jason Gross | 2017-05-14 | |
| | | ||||
| * | update c.sh for new return notation | Andres Erbsen | 2017-05-14 | |
| | | ||||
| * | Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ↵ | Andres Erbsen | 2017-05-14 | |
| |\ | | | | | | | return-notation | |||
| * | | Add GetNames | Jason Gross | 2017-05-14 | |
| | | | ||||
| * | | Add Named.default_names_for | Jason Gross | 2017-05-14 | |
| | | | ||||
| | * | make display (for return statement) | Jason Gross | 2017-05-14 | |
| | | | ||||
| | * | Stick 'return' at the end of printed functions | Jason Gross | 2017-05-14 | |
| |/ | ||||
| * | make display again (really not sure what's up) | Jason Gross | 2017-05-14 | |
| | | ||||
| * | make display | Jason Gross | 2017-05-14 | |
| | | | | | Not quite sure what changed.... | |||
| * | Add Named.CountLets | Jason Gross | 2017-05-14 | |
| | | ||||
| * | force carry intermediates to be bound early | Andres Erbsen | 2017-05-14 | |
| | | ||||
| * | make display (ladderstep with specialize square) | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Use specialized square in ladderstep | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Make proj1_sig square_sig take only one argument | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Add Z/Named/DeadCodeElimination.v | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Split off EliminateDeadCode | Jason Gross | 2017-05-14 | |
| | | ||||
| * | make display without 0x0 * _ | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Do more arithmetic simplifying | Jason Gross | 2017-05-14 | |
| | | | | | Needed to remove some multiplication by 0 | |||
| * | specialize squaring earlier | Andres Erbsen | 2017-05-14 | |
| | | ||||
| * | preserve common subexpressions in donna-derived code | Andres Erbsen | 2017-05-14 | |
| | | ||||
| * | Add support for more constants | Jason Gross | 2017-05-14 | |
| | | ||||
| * | applied micro-optimizations from donna with [transitivity] and [ring] (as ↵ |  jadep | 2017-05-14 | |
| | | | | | per #176) | |||
| * | Add constant, support pair-returning assignment | Jason Gross | 2017-05-14 | |
| | | ||||
| * | More debug info in reification | Jason Gross | 2017-05-14 | |
| | | ||||
| * | remove lingering [About] | jadephilipoom | 2017-05-14 | |
| | | ||||
| * | remove redundant definition | jadep | 2017-05-14 | |
| | | ||||
| * | make freeze use the correct versions of add_get_carry and zselect | jadep | 2017-05-14 | |
| | | ||||
| * | add wrapper for add_get_carry and proofs for add_get_carry and zselect | jadep | 2017-05-14 | |
| | | ||||
| * | Add lemma justifying compiler optimization for adc | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Fix notation binding levels so types work in nlet | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Add some reserved notations | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Ooops, I mixed up Bind Scope and Delimit Scope | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Fix some scoping | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Allow specifying type in nlet | Jason Gross | 2017-05-14 | |
| | | ||||
| * | Comment out CSE in pipeline | Jason Gross | 2017-05-14 | |
| | | ||||
| * | CSE without inlining arithmetic expressions | Jason Gross | 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 | Jason Gross | 2017-05-13 | |
| | | ||||
| * | Add mod_bound_min_max | Jason Gross | 2017-05-13 | |
| | | ||||
| * | Add proper lemma for add_with_carry | Jason Gross | 2017-05-13 | |
| | | ||||
| * | Change definition of add_get_carry | Jason Gross | 2017-05-13 | |
| | | | | | | The new definition is judgmentally equal to the old one, but is slightly easier to reify. | |||
| * | Add definitions for zselect and add_get_carry | Jason Gross | 2017-05-13 | |
| | | | | | In ZUtil/Definitions.v | |||
| * | Add flatten_binding_list_SmartVarfMap2_pair_in_generalize2 | Jason Gross | 2017-05-13 | |
| | | ||||
| * | Support destructuring dlet and slet | Jason Gross | 2017-05-13 | |
| | | | | | | The current way to support it is a kludge around the fact that `x binder` only works for recursive notations | |||
| * | Add Zdiv_0_r to zsimplify | Jason Gross | 2017-05-13 | |
| | | ||||
| * | Split off pull_Zmod, push_Zmod from ZUtil | Jason Gross | 2017-05-13 | |
| | | ||||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |