Carry around bounds on variables

[morganthomas]

Attach a bound to each variable at each step of arithmetization up to but not necessarily including the arithmetic circuit, so that in logic circuits to arithmetic circuits, we know how many elements we need in the byte decomposition or if we can get away with a simple range check.

[morganthomas]

These upper bounds are fixed (constant) and not required to be tight. We do not have to enforce them in the constraints. The quantifier bounds are variable and enforced. These bounds are for informational purposes so that we know how many bytes we need in a byte decomposition or if a simple range check suffices.