| Commit message (Expand) | Author | Age |
* | Do less reduction in split_in_context | Jason Gross | 2018-08-29 |
* | Fix proofs broken by changes to cc_m proofs | Jason Gross | 2018-08-24 |
* | Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtil | Jason Gross | 2018-08-23 |
* | Make Z.div_mod_to_quot_rem stronger | Jason Gross | 2018-07-10 |
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 |
* | Minor refactoring | Jason Gross | 2018-06-13 |
* | 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 |
* | temporary workaround for #352 | Jade Philipoom | 2018-05-31 |
* | Define machine model, write prefancy->fancy pass, and prove Montgomery code c... | Jade Philipoom | 2018-05-31 |
* | [WIP] shifting adds | Jade Philipoom | 2018-05-31 |
* | change order of additions so that they a) make more sense and b) are more sui... | Jade Philipoom | 2018-05-31 |
* | 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 be... | Jade Philipoom | 2018-05-31 |
* | 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 |
* | 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 |
* | un-hardcode # of reductions | Jade Philipoom | 2018-04-30 |
* | print saturated mulmod for p192 on 32-bit, add note about p256 | Jade Philipoom | 2018-04-30 |
* | fixed too-many-additions problem by fixing number of limbs in from_associational | Jade Philipoom | 2018-04-30 |
* | Fix some carry logic | Jade Philipoom | 2018-04-30 |
* | First stab at generating code for saturated solinas modular | Jade Philipoom | 2018-04-30 |
* | fix comment | Jade Philipoom | 2018-04-30 |
* | Fix bounds analysis for saturated ops and remove unneeded comment | Jade Philipoom | 2018-04-30 |
* | first stab at reifying barrett | Jade Philipoom | 2018-04-30 |
* | fix definitions of saturated operations to avoid unnecessary work, and make M... | Jade Philipoom | 2018-04-30 |
* | tweak definition of flatten to use an index rather than check the length of t... | Jade Philipoom | 2018-04-30 |
* | fix the placement of a dlet to make more sense | Jade Philipoom | 2018-04-30 |
* | In reassocation, don't reassociate additions | Jason Gross | 2018-04-26 |
* | Fix a printout | Jason Gross | 2018-04-26 |
* | Revert most of "Make reassociation optional" | Jason Gross | 2018-04-26 |
* | Make reassociation optional | Jason Gross | 2018-04-26 |
* | Compute tight bounds in a different way | Jason Gross | 2018-04-26 |
* | Don't introduce extra lambdas and apps in uncurry | Jason Gross | 2018-04-26 |
* | Add some Positional Hint Rewrites | Jason Gross | 2018-04-26 |
* | pass-through after Jason's review | Jade Philipoom | 2018-04-19 |
* | add instructions cc_m, rshi, and sub_with_get_borrow to pipeline in preparati... | Jade Philipoom | 2018-04-19 |