Combine constraints generated by selector expressions

[bobbinth]

Currently, constraints generated for enf match expressions are not combined in any way. This results in a large number of constraints which will significantly impact verifier performance. There are two ways of combining constraints for enf match:

1. A relatively straight-forward way described in Add support for selectors #125 (comment).
2. A more sophisticated way which would give us a near-ideal result. This approach is described below.

A simple example

Let's say we have the following enf match statement:

enf match:
    case c: op_add(s[0..3])
    case !c: op_mul(s[0..3])

ev op_add([s[3])
  enf s[0]' = s[0] + s[1]
  enf s[1]' = s[2]

ev op_mul([s[3])
  enf s[1]' = s[2]
  enf s[0]' = s[0] * s[1]

Currently, this will be reduced to 4 individual constraints:

$$ c \cdot (s_0' - s_0 - s_1) = 0 $$

$$ c \cdot (s_1' - s_2) = 0 $$

$$ (1 - c) \cdot (s_0' - s_0 \cdot s_1) = 0 $$

$$ (1 - c) \cdot (s_1' - s_2) = 0 $$

But we'd like to reduce it to two constraints which are much simpler:

$$ c \cdot (s_0' - s_0 - s_1) + (1 - c) \cdot (s_0' - s_0 \cdot s_1) = 0 $$

$$ (c + 1 - c) \cdot (s_1' - s_2) = 0 $$

It is easy to see that the second constraint is just $s_1' - s_2 = 0$, but we'll leave this optimization for later.

General methodology

The key tool we'll use in this methodology is evaluation at a random point to test for equivalence between constraints. This works in our case because we deal with bounded-degree polynomials, and if we evaluate on a large enough domain, the probability that two distinct polynomials will evaluate to the same value is negligible. For us, I think degree 2 extension of our base field should be sufficiently large, but we can also go to degree 3 extension to be extra safe.

Let's say we have the following enf match statement:

enf match:
  s0: a, b, c, d
  s1: e, f, g
  s2: h, i

Where s0, s1, s2 are selectors and a, .., h are individual constraints.

Let's also say that when evaluated at a random point, we get the following values for each constraint:

• a, c, and f evaluate to r0.
• b evaluates to r1
• d evaluates to r2
• e evaluates to r3
• g, h evaluate to r4.
• i evaluates to r5

Then, we start processing arms of enf match statement one-by-one, keeping track of aggregated results. We want to do the following two things:

1. Eliminate equivalent constraints in the same arm (e.g., a and c).
2. Establish links between equivalent constraints across different arms (e.g., a and f).

At the end of the process we want to end up with a data structure which records the following:

r0: (a, s0), (f, s1)
r1: (b, s0)
r2: (d, s0)
r3: (e, s1)
r4: (g, s1), (h, s2)
r5: (i, s2)

Then, we combine thee expressions together in a way that each constraint ends up having distinct selectors. Strategies for this could be different. One result could look like so:

(a, s0), (f, s1), (i, s2)
(b, s0), (e, s1)
(d, s0), (g, s1), (h, s2)

And then, in the end, we get 3 constraints which look like so:

a * (s0 + s1) + s2 * i = 0
s0 * b + s1 * e = 0
s0 * d + g * (s1 + s2) = 0

Notice that f and h are eliminated because they are the same constraints as a and g respectively.

[Al-Kindi-0]

Great write-up, thank you!
As for evaluating at a random point, I think that we can just evaluate twice (or three times depending on the degree and number of variables) over the base field in order to drive the soundness error down.

[tohrnii]

@bitwalker also suggested an alternate way by using E-graphs to check if two constraints are equivalent.