Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Add shiftl notation | 2018-03-19 | ||
| | ||||
* | Update printing | 2018-03-19 | ||
| | ||||
* | Move relax_zrange to a separate phase | 2018-03-19 | ||
| | ||||
* | WIP cast | 2018-03-19 | ||
| | ||||
* | Update montred to newish pipeline, revive DCE | 2018-03-19 | ||
| | | | | | | | | | - Update the style of montred snythesis to match the changes in the pipeline - Bring back non-quadratic dead code elimination and make use of it for montgomery reduction - Update partial reduction to inline "var-like" things (fst, snd, pair applied to var) | |||
* | Add a ring goal | 2018-03-19 | ||
| | | | | Unfortunately, the ring proofs are a bit messy. | |||
* | subsetoid_ring: don't ask for false things | 2018-03-12 | ||
| | | | | | We can't actually prove the previous okness lemmas in SimplyTypedArithmetic, so we instead ask for exactly what we need. | |||
* | Add Algebra.SubsetoidRing | 2018-03-12 | ||
| | ||||
* | make update-_CoqProject | 2018-03-10 | ||
| | ||||
* | Bump coqprime for .gitignore | 2018-03-10 | ||
| | ||||
* | Review comments. | 2018-03-09 | ||
| | | | | | | | Major change is porting everything to Z and using Z.div_mod_to_quot_rem which is a handy sledgehammer. Z is also a nice simplification. Dealing with subtraction is tidier, though I do have 0 <= x goals everywhere as a result. | |||
* | easy bits | 2018-03-09 | ||
| | ||||
* | Prove another Barrett reduction variant. | 2018-03-09 | ||
| | | | | | | | | | | This variant comes from http://www.ridiculousfish.com/blog/posts/labor-of-division-episode-i.html. It was useful for https://boringssl-review.googlesource.com/#/c/boringssl/+/25887. TODO - Talk to Andres to figure out all the ways this could be done more cleanly. It was originally a standalone file. | |||
* | Don't use deprecated compat notations in ZUtil | 2018-03-07 | ||
| | ||||
* | Add comments about [refresh] failing | 2018-03-07 | ||
| | ||||
* | actually reprint montgomery and uncomment a couple notations -- should have ↵ | 2018-03-07 | ||
| | | | | been in last commit | |||
* | fix a typo, some comments, and notations | 2018-03-07 | ||
| | ||||
* | make Montgomery do associational carries in a generalized way | 2018-03-07 | ||
| | ||||
* | remove special-case convert-mul-convert implementation and use generalized ↵ | 2018-03-07 | ||
| | | | | one in Montgomery example | |||
* | remove unneeded, commented-out code | 2018-03-07 | ||
| | ||||
* | Add a dummy length argument to make partial evaluation work (see #321) and ↵ | 2018-03-07 | ||
| | | | | fixed up Montgomery notations | |||
* | factor out convert-mul-convert and prove correctness | 2018-03-07 | ||
| | ||||
* | Add stuff to author-blacklist for bbv | 2018-02-28 | ||
| | ||||
* | git submodule update --remote --recursive | 2018-02-24 | ||
| | ||||
* | coqprime in COQPATH (closes #269) | 2018-02-24 | ||
| | ||||
* | Add ZRange.intersection | 2018-02-23 | ||
| | ||||
* | Fix a typo | 2018-02-23 | ||
| | ||||
* | Add some bounds operations to ZRange | 2018-02-23 | ||
| | ||||
* | Add ZRange.opp | 2018-02-23 | ||
| | ||||
* | Make the Montgomery reduction test case use 128-bit multiplications and | 2018-02-23 | ||
| | | | | | | | | Columns arithmetic. This includes: - writing flatten_column in terms of list_rect instead of matches, so it can be reified - adding list_rect, shiftl, and List.length to various IRs - dead code elimination | |||
* | fix leftover %RT | 2018-02-23 | ||
| | ||||
* | Get bounds analysis working | 2018-02-23 | ||
| | ||||
* | fixed inlining of opaque pairs as per Jason's recommendation | 2018-02-23 | ||
| | ||||
* | rename compact_digit to flatten_column | 2018-02-23 | ||
| | ||||
* | make compact_digit consume a bound argument rather than a weight-function index | 2018-02-23 | ||
| | ||||
* | use Z.div and Z.modulo in saturated arith, since we can now change to ↵ | 2018-02-23 | ||
| | | | | bitshifts reflectively | |||
* | remove leftover [Eval compute] and extra space | 2018-02-23 | ||
| | ||||
* | Fix naming issue | 2018-02-23 | ||
| | ||||
* | move things from ZUtil.v into Div.v | 2018-02-23 | ||
| | ||||
* | define mul and add placeholders for new operations in bounds parts | 2018-02-23 | ||
| | ||||
* | Add non-CPS version of Saturated/Core | 2018-02-23 | ||
| | ||||
* | add three proofs to ZUtil | 2018-02-23 | ||
| | ||||
* | add two proofs about lists | 2018-02-23 | ||
| | ||||
* | Add non-CPS version of associational multiplication with mul_split | 2018-02-23 | ||
| | ||||
* | preliminary version of Montgomery reduce in new pipeline; includes adding ↵ | 2018-02-23 | ||
| | | | | support for Z.leb and several saturated-arith operations (add_get_carry, add_with_get_carry, sub_get_borrow, mul_split, zselect, and add_modulo) | |||
* | add proof about Z.equiv_modulo | 2018-02-23 | ||
| | ||||
* | add equivalence proof for Montgomery reduce_via_partial_alt | 2018-02-23 | ||
| | ||||
* | create rewrite database for saturated operations on Z | 2018-02-23 | ||
| | ||||
* | Add new modular addition operation on Z | 2018-02-23 | ||
| | ||||
* | Change Implicit Arguments to Arguments in coqprime | 2018-02-23 | ||
| |