bound inference

This commit is most clear about what bound inference is doing.

If we only need symbolic expression of loop bounds, I think PassDown is sufficient. Need to figure out what PassUp does additionally.