avoiding constraining the same things in snarky

[mimoo]

Currently in snarky we build a small AST when operating on field vars (called Cvars). The AST looks like this:

pub enum CVar<F>
where
    F: PrimeField,
{
    /// A constant.
    Constant(F),

    /// A variable that can be refered to via a `usize`.
    Var(usize),

    /// The addition of two other [CVar]s.
    Add(Box<CVar<F>>, Box<CVar<F>>),

    /// Scaling of a [CVar].
    Scale(F, Box<CVar<F>>),
}

I believe this was used when snarky was targeting R1CS, and it was useful because additions are for free. But in Plonk it seems less useful. Worse, it seems like this might lead us to constrain the same things several times.

For example, this pseudo-code would constrain the additions in x twice as z would contain the entire AST contained in x:

let x = x1 + x2 + x3 + x4 + ...;
let z = y + x;
assert_eq(x, 3);
assert_eq(z, 4);

There's three ways to solve this, that I can think of:

1. let the user manually decide when to reduce the AST of a variable. This is what we do in pickles and snarkyjs with the seal function IIUC
2. remove the AST and always create constraints right away when we add or scale. This might prevent us from optimizing the generic constraint. It seems like sometimes we can merge two generic constraints in one if we're clever. I actually haven't thought much about when this case arise, it'd be good to write an example
3. keep a hashmap of AST to already-constrained variables

Solution 3 seems interesting. When reducing an AST, the algorithm could hash the entire AST and see if it was already constrained, and if so what the result variable is. If it wasn't, step in the AST and do the same, rinse and repeat. This might the best solution to implement?

cc @imeckler @mitschabaude

[mimoo]

I guess one optimization for 2. I can think of is the boolean constraint: x ( x - 1) = x^2 - x = 0 which you can write with two generic gates naively, but can also write as a single generic gate by setting:

• left input = right input = x (with the wiring)
• left coefficient = -1
• mul coefficient = 1

which gives us:

c_l * l + c_r * r + c_o * o + c_m * l * r + c_c = 
-1 * l + 0 * r + 0 * o + 1 * l * r + 0 =
-l + l * r = 
x * x - x = 0

[mitschabaude]

(3) would be a great solution! We should go for it. I also think the existing system (1) -- keeping the AST around without reusing intermediate sealed variables -- leads to less efficient user code than the simpler (2) / sealing variables eagerly.

To support doing something about this, I can give an example of user code that I saw several times, which is very inefficient just because we keep the AST around. A common pattern is to "select" a single variable out of an array x[0], x[1], ..., x[n-1], by computing some boolean b[i] for each i which will be 1 for only one of the i. Users tend to write this as a series of Circuit.if statements:

let x = Field.zero;
for (let i=0; i<n; i++) {
  x = Circuit.if(b[i], x[i], x);
}
// if exactly one of the b[i] was 1, and the others 0, then x === x[i] now

Now consider that Circuit.if is implemented as follows:

Circuit.if(b, x, y) === b*(x - y) + y  // x if b=1=true, y else

Note here that if y is an addition AST of length i, then b*(x - y) + y is an addition AST of length (i+1).

So in the example user code above, x = Circuit.if(b[i], x[i], x), x becomes a bigger AST in every iteration, and the multiplication by b[i] reduces that AST to a different variable every time. In the last iteration, x is an AST of length n-1, and the sealing + multiplication in this last step alone creates O(n) generic gates! The entire loop creates O(n^2) generic gates, while even the most naive approach involving eagerly creating gates leads to O(n) gates.

I believe such pathological inefficiencies are easy to create, and educating users about the low-level details and how they can use seal in the right places is not a viable option (I don't want to think about "sealing" when writing application code). Therefore, we need to get rid of the current system!

[mitschabaude]

@mimoo, thinking about your example with the boolean constraint, I wonder if we can do this optimization automatically. Just keeping a hashmap of constrained variables doesn't solve it: When multiplying x by (1-x), I'm afraid our algorithm would treat (1-x) as a separate variable y and create two generic gates, x + y + (-1) = 0 (constraining y) and x*y = 0.

[mitschabaude]

We could track for each variable whether it can be written as a polynomial of degree 2 in one or two other variables. So every variable could keep track of a representation of the form $a_0 + a_x x + a_y y + a_{xy} x y$ where $x, y$ are two other variables (or zero). When adding or multiplying variables, we can first check if the two representations can again be merged into a single degree 2 polynomial. If yes, we're fine because the result still fits into an unfinalized generic gate. If not, we create one or two new sealed variables, which get their own generic gates and are stored in our hashmap.

In the boolean example, we would recognize that the product of $x$ and $1 - x$ can be represented as $x - x^2$, and not finalize a gate. If another $c x$ is added, it would become $(c - 1) x - x^2$ and still not finalized. If then another $y$ is added, we would finalize $z = (c - 1) x - x^2$ into a generic gate and store a new degree 2 representation $y + z$.

Can this be improved further?

[mitschabaude]

I wonder how hard it is to simply keep track of everything and reduce it to generic gates in the most optimal way. Is there prior art on this?