I noticed that left shifts by a constant are not being marked as bounded by prove. Prove consults ft.limits, but ft.limits doesn't contain limits for constants. Something similar happens for some other ops with easy limits.
This is pretty straightforward to fix: Write a wrapper around ft.limits accesses that generates limits in cases like these.
I have a prototype CL of this, and it mostly helps. But before it can be mailed, I need to investigate and fix a few more minor regressions from it. (The compiler is quite sensitive to the order in which optimizations occur.)
And before doing that, I wanted to check in about whether this was even the right kind of fix here.