aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Review comments.Gravatar David Benjamin2018-03-09
* easy bitsGravatar David Benjamin2018-03-09
* Prove another Barrett reduction variant.Gravatar David Benjamin2018-03-09
* 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 b...Gravatar Jade Philipoom2018-03-07
* 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 on...Gravatar Jade Philipoom2018-03-07
* remove unneeded, commented-out codeGravatar Jade Philipoom2018-03-07
* Add a dummy length argument to make partial evaluation work (see #321) and fi...Gravatar Jade Philipoom2018-03-07
* 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
* 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 bitshif...Gravatar Jade Philipoom2018-02-23
* 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 sup...Gravatar Jade Philipoom2018-02-23
* 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
* 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
* [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
* Remove mul_rargs recordGravatar Jason Gross2018-02-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 10:07:06 +0000