feat: sanity check lookup bitwidths

[DavePearce]

Overview

Consider the following example:

(defcolumns (X :i16) (Y :i16) (Z :i16))

(deflookup test (Z) (- X Y))

From a field agnostic perspective, this example is problematic. Specifically, we cannot determine a suitable bitwidth for the source column because it can be negative. In order to implement lookups correctly, we must know the bitwidth of both the target and source column for each pair (see examples below for more details why).

Therefore the purpose of this issue is to report an error when the bitwidth of a source or target column in a lookup cannot be determined.

Approach

Machinery for determining the necessary bitwidth of an MIR expression already exists within go-corset. More specifically, the ValueRange() function is implemented by all IR expressions and is part of the ir.Term[T] interface:

	// ValueRange returns the interval of values that this term can evaluate to.
	// For terms accessing registers, this is determined by the declared width of
	// the register.
	ValueRange(module schema.Module) *math.Interval

Using this function, it is possible to determine the interval of values in which any evaluation of the given term lies. In particular, using this we can easily tell when a negative value is possible.

Therefore the suggested approach is to use this method in corset/compiler/translator.go to look for negative values and, if detected, to report a suitable SyntaxError.

Notes

• (Conditional Lookups) For conditional lookups, we additionally expect that the selector expression is within the range 0..1. Hence, a similar check for this would make sense.
• (Range Constraints) A similar check can also be made for definrange constraints, and perhaps even defcomputed.

[DavePearce]

these illustrate why we must be able to determine the bitwidth of lookup columns

Example 1

Consider the following example:

(defcolumns (X :i128) (Y :i64))
(deflookup l1 (X) (Y))

This constraint is valid in the current environment, but is somewhat problematic in a field agnostic setting. Specifically, since we are looking up a u64 value into a u128 column, its not clear what should happen with the most significant 64bits. In particular, observe that for e.g. Koala Bear, column X will actually correspond with say 5 limbs whilst column Y will have 3 limbs.

Solution. The obvious approach here would be fill them out with 0 [that seems fine]. Thus, the final lookup is:

(defcolumns 
    (X'0 :i128) (X'1 :i128) (X'2 :i128) (X'3 :i128) (X'4 :i128) 
    (Y'0 :i64) (Y'1 :i64) (Y'2 :i64))

(deflookup l1 
    (X'0) (X'1) (X'2) (X'3) (X'4) 
    (Y'0) (Y'1) (Y'2)  0       0)

Example 2

Consider the opposite case:

(defcolumns (X :i64) (Y :i128))
(deflookup l1 (X) (Y))

Again, we can pad out the lookup with 0 to ensure matching numbers of columns.