aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Review comments.Gravatar David Benjamin2018-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 bitsGravatar David Benjamin2018-03-09
|
* Prove another Barrett reduction variant.Gravatar David Benjamin2018-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 ZUtilGravatar Jason Gross2018-03-07
|
* Add comments about [refresh] failingGravatar Jason Gross2018-03-07
|
* actually reprint montgomery and uncomment a couple notations -- should have ↵Gravatar Jade Philipoom2018-03-07
| | | | been in last commit
* fix a typo, some comments, and notationsGravatar Jade Philipoom2018-03-07
|
* make Montgomery do associational carries in a generalized wayGravatar Jade Philipoom2018-03-07
|
* remove special-case convert-mul-convert implementation and use generalized ↵Gravatar Jade Philipoom2018-03-07
| | | | one in Montgomery example
* remove unneeded, commented-out codeGravatar Jade Philipoom2018-03-07
|
* Add a dummy length argument to make partial evaluation work (see #321) and ↵Gravatar Jade Philipoom2018-03-07
| | | | fixed up Montgomery notations
* factor out convert-mul-convert and prove correctnessGravatar Jade Philipoom2018-03-07
|
* git submodule update --remote --recursiveGravatar Andres Erbsen2018-02-24
|
* coqprime in COQPATH (closes #269)Gravatar Andres Erbsen2018-02-24
|
* Add ZRange.intersectionGravatar Jason Gross2018-02-23
|
* Fix a typoGravatar Jason Gross2018-02-23
|
* Add some bounds operations to ZRangeGravatar Jason Gross2018-02-23
|
* Add ZRange.oppGravatar Jason Gross2018-02-23
|
* Make the Montgomery reduction test case use 128-bit multiplications andGravatar Jade Philipoom2018-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 %RTGravatar Jade Philipoom2018-02-23
|
* Get bounds analysis workingGravatar Jade Philipoom2018-02-23
|
* fixed inlining of opaque pairs as per Jason's recommendationGravatar Jade Philipoom2018-02-23
|
* rename compact_digit to flatten_columnGravatar Jade Philipoom2018-02-23
|
* make compact_digit consume a bound argument rather than a weight-function indexGravatar Jade Philipoom2018-02-23
|
* use Z.div and Z.modulo in saturated arith, since we can now change to ↵Gravatar Jade Philipoom2018-02-23
| | | | bitshifts reflectively
* remove leftover [Eval compute] and extra spaceGravatar Jade Philipoom2018-02-23
|
* Fix naming issueGravatar Jade Philipoom2018-02-23
|
* move things from ZUtil.v into Div.vGravatar Jade Philipoom2018-02-23
|
* define mul and add placeholders for new operations in bounds partsGravatar Jade Philipoom2018-02-23
|
* Add non-CPS version of Saturated/CoreGravatar Jade Philipoom2018-02-23
|
* add three proofs to ZUtilGravatar Jade Philipoom2018-02-23
|
* add two proofs about listsGravatar Jade Philipoom2018-02-23
|
* Add non-CPS version of associational multiplication with mul_splitGravatar Jade Philipoom2018-02-23
|
* preliminary version of Montgomery reduce in new pipeline; includes adding ↵Gravatar Jade Philipoom2018-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_moduloGravatar Jade Philipoom2018-02-23
|
* add equivalence proof for Montgomery reduce_via_partial_altGravatar Jade Philipoom2018-02-23
|
* create rewrite database for saturated operations on ZGravatar Jade Philipoom2018-02-23
|
* Add new modular addition operation on ZGravatar Jade Philipoom2018-02-23
|
* Fix balance on subGravatar Jason Gross2018-02-19
| | | | | | | With some help from @jadephilipoom Previously, the carrying was removing the effect of `coef`, and we were getting too small a balance.
* A bit more uniformity in handling the prime, implicitsGravatar Jason Gross2018-02-19
|
* [experiments] Fill in opp and subGravatar Jason Gross2018-02-19
|
* Remove the mod on eval_addGravatar Jason Gross2018-02-19
|
* Remove runtime_scopeGravatar Jason Gross2018-02-19
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/315#discussion_r169085799
* [experiments] Add some more arithmetic operationsGravatar Jason Gross2018-02-19
|
* NumTheoryUtil: make coqprime dependencies explicitGravatar Andres Erbsen2018-02-19
|
* Take in n, compute limbwidthGravatar Jason Gross2018-02-18
|
* Rename type_descr to second_order, as per PR requestGravatar Jason Gross2018-02-18
|
* Rename AutoReifyGravatar Jason Gross2018-02-18
|
* Speed up the pipeline by 3x, restoring previous performanceGravatar Jason Gross2018-02-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | Apparently using `refine eq_refl` rather than `subst <name for evar>; reflexivity` was resulting in βδ reduction of `chained_carries` in `carry_mulmod`. The β reduction resulted in us getting a different cps'd term. I do not know why this particular β reduction resulted in a 3x slowdown in partial reduction; it seems like anything that cared about sharing should either get sharing from the top-level in `carry_mulmod`, or should have no difference in sharing between the terms ```coq (fun n s c p idxs => fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs)) n s c p idxs ``` and ```coq fold_right (fun a b => @carry_reduce n s c a b) p (rev idxs)) ``` This feels fragile, and I am mystified. Note for the future: I went about debugging this by integrating little bits of this PR one by one, seeing which one caused the slowdown, and then, when I realized it was use of `carry_mulmod`, I took the reified terms and made a goal asserting their equality, and then took the terms apart with `f_equal` and `extensionality` until I found the difference.
* Remove mul_rargs recordGravatar Jason Gross2018-02-18
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 22:42:26 +0000