aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
* Finish interp proof of abstract interpretationGravatar Jason Gross2018-09-14
* Add more operation-specific proofsGravatar Jason Gross2018-08-21
* Do most of abs-int interp proofsGravatar Jason Gross2018-08-21
* Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...Gravatar Jason Gross2018-08-13
* Don't fuse annotationsGravatar Jason Gross2018-08-09
* Push back admits in interp lemmasGravatar Jason Gross2018-08-08
* Add some partial interp proofs for abs-intGravatar Jason Gross2018-08-08
* Finish relax interp proofsGravatar Jason Gross2018-08-07
* Add another GeneralizeVar pass to add support for using Wf3Gravatar Jason Gross2018-08-07
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Remove fastpath for Zcast in absintGravatar Jason Gross2018-08-06
* Remove thunking from abstract interpretationGravatar Jason Gross2018-08-06
* Finish AbsInt Wf proofsGravatar Jason Gross2018-08-04
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 05:37:51 +0000