aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds
Commit message (Expand)AuthorAge
* Try more simplificationGravatar Jason Gross2017-06-17
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
* Add bool into P256Gravatar Jason Gross2017-06-17
* Reify Z.mul_with_split_at_bitwidthGravatar Jason Gross2017-06-13
* Handle IdWithAlt in the simplifierGravatar Jason Gross2017-06-12
* Push bounds side conditions through the pipelineGravatar Jason Gross2017-06-12
* Initial stab at id_with_altGravatar Jason Gross2017-06-11
* Add dummy version of IdWithAlt to compilersGravatar Jason Gross2017-06-11
* Be more forceful about clearing before abstract in glue codeGravatar Jason Gross2017-06-11
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
* Only use bool in freezeGravatar Jason Gross2017-05-21
* Fix extra opp in freezeGravatar Jason Gross2017-05-20
* Get sbb conversion working in the pipelineGravatar Jason Gross2017-05-20
* Add adc -> sbb to arithmetic simpliferGravatar Jason Gross2017-05-20
* Add SubWithGetBorrow to reflective machineryGravatar Jason Gross2017-05-20
* Add compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
* Allow 'bool' in outputGravatar Jason Gross2017-05-17
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Ltac scope interprets some notations as errors, so we make anf a definitionGravatar Jason Gross2017-05-17
* Fix a typo in prev commit, add convenience notationGravatar Jason Gross2017-05-17
* Allow specifying pipeline options at call-timeGravatar Jason Gross2017-05-17
* disable ANormal form, we now support expression output!Gravatar Andres Erbsen2017-05-14
* Do more arithmetic simplifyingGravatar Jason Gross2017-05-14
* Comment out CSE in pipelineGravatar Jason Gross2017-05-14
* CSE without inlining arithmetic expressionsGravatar Jason Gross2017-05-14
* Allow more transformations in pipelineGravatar Jason Gross2017-04-17
* Inline a24_sig in ladderstepGravatar Jason Gross2017-04-17
* More robust pipelineGravatar Jason Gross2017-04-15
* Generalize MapCastCorrect a bitGravatar Jason Gross2017-04-15
* Prelinearize so we can simplify more arithmetic in pipelineGravatar Jason Gross2017-04-14
* Use 128/256 in ladderstep 130Gravatar Jason Gross2017-04-14
* Split off a-normal form from flatteningGravatar Jason Gross2017-04-14
* Clean up ladderstep goal with help from AndresGravatar Jason Gross2017-04-14
* Handle implications in pipeline glueGravatar Jason Gross2017-04-13
* Finish the last of the admits in word-size-selection!Gravatar Jason Gross2017-04-09
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* More wip on boundsGravatar Jason Gross2017-04-09
* More progress on boundsGravatar Jason Gross2017-04-09
* Don't take abs in upper_lor_and_boundsGravatar Jason Gross2017-04-09
* Take more abs in Bounds.InterpretationGravatar Jason Gross2017-04-09
* Factor out Z.{lor,land} proofs a bit moreGravatar Jason Gross2017-04-09
* Finish shift cases, extract out land, lor factsGravatar Jason Gross2017-04-09
* WIP on bounds lemmaGravatar Jason Gross2017-04-08
* More WIP on PullCastGravatar Jason Gross2017-04-08
* More WIP on PullCastGravatar Jason Gross2017-04-08
* WIP on pullcastGravatar Jason Gross2017-04-08
* Work in progress on proving PullCastGravatar Jason Gross2017-04-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 07:25:21 +0000