major refactoring, respect C semantics for int sizes.
Previously, all computations were on Integers.  If there were overflows in the program,
the constant folder could have a different result.
verified verification conditions for overflow checks.
Proof script also checked in.
wibbles.