index
:
fiat-crypto
master
fast, formally verified cryptography
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
Experiments
/
NewPipeline
/
AbstractInterpretationProofs.v
Commit message (
Expand
)
Author
Age
*
Refactor/generalize some pipeline definitions/proofs
Jason Gross
2018-10-30
*
Guarantee that casting always returns inrange
Jason Gross
2018-10-12
*
Finish interp proof of abstract interpretation
Jason Gross
2018-09-14
*
Add more operation-specific proofs
Jason Gross
2018-08-21
*
Do most of abs-int interp proofs
Jason Gross
2018-08-21
*
Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...
Jason Gross
2018-08-13
*
Don't fuse annotations
Jason Gross
2018-08-09
*
Push back admits in interp lemmas
Jason Gross
2018-08-08
*
Add some partial interp proofs for abs-int
Jason Gross
2018-08-08
*
Finish relax interp proofs
Jason Gross
2018-08-07
*
Add another GeneralizeVar pass to add support for using Wf3
Jason Gross
2018-08-07
*
Start setting up abs-int interp proofs
Jason Gross
2018-08-06
*
Remove fastpath for Zcast in absint
Jason Gross
2018-08-06
*
Remove thunking from abstract interpretation
Jason Gross
2018-08-06
*
Finish AbsInt Wf proofs
Jason Gross
2018-08-04
*
Generalize type.eqv a bit
Jason Gross
2018-07-30
*
Integrate Wf and Interp proofs
Jason Gross
2018-07-30
*
New pipeline, split among files
Jason Gross
2018-06-17