Unproven Integer Type Checking

[DavePearce]

The goal here is to develop a type check for "unproven" types (e.g. i8 versus i8@prove, etc). Two approaches:

• (Simple) We could use integer range analysis, along with bounded unrolling to given a quick-and-dirty check. This would unroll a given module to some number of rows, then fill in all proven columns with their ranges and then try to deduce the rest. I don't know whether this will work well, however, for modules with CT_MAX. The problem being that these modules have variable rows per call, and this will interfere. We could hard-code knowledge of CT_MAX.
• (Non-inductive Proof) We can improve upon the above by using a simple decision procedure for inequalities and, again, unrolling to some depth.
• (Inductive Proof) Perhaps the hardest, but also the most powerful.

[DavePearce]

(see also #390)

Overview

Imagine expanding all constraints to the "balanced form" (i.e. non-negative polynomials on each side). For example, 0 == X-Y becomes X==Y. Then, increasing values for X and Y can only increase the lhs / rhs.

Therefore, consider each variable in turn whilst assuming the type of other variables. We can substitute the maximum value for each of the other variables into our constraint, thus producing a maximum possible value for the target variable.

Approach

As for field agnosticity, the presence of normalisations is a problem. Again, the easiest solution here is work in the logical form. Then, we can apply a simple decision procedure to check the bounds of the target whilst assuming those of others.

The issue of induction still remains an issue here, as we likely require to "invent" intermediate bounds (e.g. for accumulators in a byte decomposition). However, we could have a set of predefined patterns to work from.