aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add another reserved notation for App_fstGravatar Jason Gross2018-03-21
|
* s/partial reduction/partial evaluation/Gravatar Jason Gross2018-03-21
|
* Don't inline var nodes on the first pass through partial evaluationGravatar Jason Gross2018-03-21
|
* Let-bind placeGravatar Jason Gross2018-03-21
| | | | | This allows vm_compute to run in 300 seconds on the from_associational pipeline.
* [experiments] Thunk the eliminator casesGravatar Jason Gross2018-03-20
| | | | | This allows us to remove the special case for `bool_rect`, and is a step towards targeting `vm_compute` rather than `lazy`.
* Remove some dead codeGravatar Jason Gross2018-03-19
|
* Fix for Coq <= 8.7Gravatar Jason Gross2018-03-19
|
* Add support for Z*Z casts, get montred workingGravatar Jason Gross2018-03-19
|
* Split up the two calls to `lazy`Gravatar Jason Gross2018-03-19
| | | | It was too slow to do `lazy -[Let_In]` in montgomery reduction.
* Fix some bugs in cachingGravatar Jason Gross2018-03-19
| | | | Also adapt to the lack of `'` notation in master for `Z.pos`.
* Add comments explaining the various [interp] functionsGravatar Jason Gross2018-03-19
|
* Add commented out example of using the full end-to-end lemma inlineGravatar Jason Gross2018-03-19
|
* Add end-to-end correctness lemmaGravatar Jason Gross2018-03-19
|
* Unify cache and nocacheGravatar Jason Gross2018-03-19
|
* Add alternate tactics for handling the all-in-one-derive caseGravatar Jason Gross2018-03-19
|
* Clean and simplify some codeGravatar Jason Gross2018-03-19
|
* WIP with Andres on cleaning boilerplateGravatar Jason Gross2018-03-19
|
* Partial fix for montredGravatar Jason Gross2018-03-19
| | | | Still need to insert casts for operations returning two values
* Speed up the final pipeline by about 2xGravatar Jason Gross2018-03-19
| | | | | | | | | | | | | | | | | As the comment says, doing `lazy` is twice as slow as doing `lazy -[Let_In]; lazy`. This is because the bounds pipeline does `dlet E : Expr := (reduced thing) in let b := extract_bounds E in ...`. If we allow `lazy` to unfold `Let_In` before it fully reduces the function (function, because `Expr := forall var, @expr var`), then there is no sharing between the partial reduction in bounds extraction and the partial reduction in the return value. So we force `lazy` to fully reduce the argument first, and only then permit `lazy` to inline it. This is slightly slower than doing bounds analysis in a non-PHOAS representation; we spend about 3%-5% of the overall time doing bounds extraction, and fully reducing the bounds extraction expression before plugging in arguments costs a bit more. However, it's still reasonably fast, and the code is much simpler when `Interp` always succeeds rather than returning `option`.
* Insert missing commentGravatar Jason Gross2018-03-19
|
* Remove dead bounds analysis codeGravatar Jason Gross2018-03-19
|
* Move the ring goal upGravatar Jason Gross2018-03-19
|
* Add shiftl notationGravatar Jason Gross2018-03-19
|
* Update printingGravatar Jason Gross2018-03-19
|
* Move relax_zrange to a separate phaseGravatar Jason Gross2018-03-19
|
* WIP castGravatar Jason Gross2018-03-19
|
* Update montred to newish pipeline, revive DCEGravatar Jason Gross2018-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 goalGravatar Jason Gross2018-03-19
| | | | Unfortunately, the ring proofs are a bit messy.
* subsetoid_ring: don't ask for false thingsGravatar Jason Gross2018-03-12
| | | | | We can't actually prove the previous okness lemmas in SimplyTypedArithmetic, so we instead ask for exactly what we need.
* Add Algebra.SubsetoidRingGravatar Jason Gross2018-03-12
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 04:34:53 +0000