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
/
AbstractInterpretation.v
Commit message (
Expand
)
Author
Age
*
Fix some bounds analysis
Jason Gross
2018-08-13
*
Fix a wrong bound computation (on negatives), fix a proof
Jason Gross
2018-08-13
*
Factor through is_tighter_than_bool, add is_bounded_by_bool_Proper_if_sumbool...
Jason Gross
2018-08-13
*
Don't guarantee anything about casting outside of range
Jason Gross
2018-08-10
*
Don't fuse annotations
Jason Gross
2018-08-09
*
Push back admits in interp lemmas
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
*
Remove fastpath for Zcast in absint
Jason Gross
2018-08-06
*
Remove thunking from abstract interpretation
Jason Gross
2018-08-06
*
Allow proving force ∘ thunk = id extensionally
Jason Gross
2018-07-30
*
Support reification of firstn, skipn
Jason Gross
2018-07-18
*
Allow reification of nat_rect (fun _ => _ -> _)
Jason Gross
2018-07-15
*
Correctly reify match on prod
Jason Gross
2018-07-03
*
WIP
Jason Gross
2018-07-03
*
New pipeline, split among files
Jason Gross
2018-06-17