control flow in PLONK (if/else)

[mimoo]

I find it annoying that I can't easily write if/else blocks, or even early returns. I think the notion of blocks/branches/control flow in PLONK would be really nice to have.

I drafted a documentation that talks about that here

I guess now that Github supports LaTex I should be able to copy/paste it here:

Control flow in PLONK

Problem: Circuits making use of branches (for example, using if/else and early returns) are notoriously hard to encode in PLONK.

Proposition: Introduce an extra control-flow witness fg to enable the notion of blocks (i.e. sets of continuous statements that are executed, or not).

High-level explanation

We implement the special fg witness following 4 ideas.

1. fg is multiplied to all gates. This is the main technique, which allows us to cancel rows that are not executed/ran during runtime (and thus we don't have to figure out a way to make them "work" when running the prover).

2. fg is constrained to be either a boolean. Blocks are either enabled ($1$) or disabled ($0$) (TODO: is this necessary?)

3. fg is constrained to be 1 for essential rows. At compile time, we ensure that we can constrain the fg column to "activate" essential rows:

• top level rows: rows that are in the main block or flow (TODO: is top level a good term?)
• control rows: rows that create the control cells, which are cells that indicate if a block should be executed (e.g. the boolean x in if x then ...)

We can do this by:

• creating an fg_selector selector column at compile time
• setting fg_selector to $1$ in rows where fg must be enabled
• adding the following constraint (which must not be multiplied to fg) : $(\text{fg} - \text{fg_selector}) \cdot \text{fg_selector} = 0$

4.fg's consistency is checked at runtime via the permutation argument. This is the second technique, this allows us to wire its values to the booleans cells (see 3)

Control rows

When entering an if condition, a control row is created to enable or disable the associated block. That row simply stores the boolean in a register (and can constrain that it is a boolean).

When entering an if/else condition, two control rows are created to store both cond and not_cond = 1 - cond. Then wiring is used to constrain fg = cond in rows associated to the first block and fg = not_cond in rows associated to the second block.

Note that early returns can be seen as an if/else. For example, the following pseudo code:

if x {
   return true;
}

return false;

can be transpiled as:

if x {
	return true;
} else {
	return false;
}

Nested blocks

Nested blocks are also activated via control cells. A control cell for a nested block is constructed differently though: it is the AND bitwise operation of its own variable with all the parent control cells.

For example, in the following pseudo-code:

if x {
	// 1
	if y {
		// 2
		if z {
			// 3			
		}
	}
}

the control cell control_z that represents z must be constrained as

$$ \text{control\_z} = z \land y \land x $$

Note: this means that the control cell might be constructed over several control rows! And all control rows are essential rows that MUST be enabled by the fg_selector selector column.

As such, if branch 1 is not taken, then both control_y and control_z will be constrained to be $0$ (as x will be $0$).

Note: it is possible that the rows that create y and z are disabled, and as such the prover could place any value there. This does not matter as the AND will take care of making sure that the end value (control_z) is still $0$.

How to apply the technique on the execution trace table

Here's a high-level diagram that shows how if/else and nested if/else work:

How does this change impact the protocol?

We added two things:

• an additional witness column fg.
  • we need to randomize and commit to this column. So the proof will grow in size.
  • we need to multiply this witness with all other gates, so the composition polynomial (the polynomial that combines all constraints) will have a bigger degree (TODO: how does this impact our implementation?)
• a selector fg_selector.
  • we need to create a constraint associated to that. The constraint is of low degree so it is not a big deal.
  • we need to add it to the prover and verifier keys.

Note: If we're going the route of evaluating all polynomials, then we should also evaluate both of these polynomials as part of the protocol.

[mimoo]

I think @mrmr1993 had some thoughts about using dynamic coefficients instead of increasing the degree of all of the gates.

As an aside: what is the issue in increasing the degree of all the gates? I always have a hard time remembering.

I think the poseidon gate is annoying because there's an $w^7(x)$, which makes the gate degree $d = 7 deg(w_i) = 7 n$ which is the same for any $i$ and with $n$ the size of the domain minus 1.

Also, that's multiplied with the poseidon selector polynomial which is also of degree $n$... so the degree of that thing is $7 n^2$

And multiplied with our new selector that'd be $7 n^3$.

The degree of these polynomials impact two things:

1. when we handle the gate on the prover side we need a large domain to store enough evaluations to represent that large degree polynomial (exactly d + 1 evaluations needed, hence the d8 domain we use).
2. when we split the quotient polynomial in 7 parts, if we increased that degree we'd have to split it into more parts

My proposal shouldn't increase the domain size we need to handle the poseidon gate (or other gates) because we'd evaluate the new selector polynomial. For the same reason, it shouldn't increase the degree in (2). (This is effectively working in the same way as the poseidon selector polynomial not affecting both of these points.)

[mimoo]

/!\ actually, this comment should be wrong, as we do need more evaluations to handle something that's of higher degree.

[mimoo]

one question @mrmr1993 asked me is how to deal with the permutation. I can see two problems:

1. the branch that's not taken is still enabled in the permutation
2. two mutually exclusive branches might want to return an output or mutate a variable in a higher-level language

Here's an example that meets both problems (in some rust-like DSL):

if cond {
  x = x + 1 
} else {
  x = x + 2
}

1. The non-active branch will create a generic gate, which will have a left input wired to the cell that contains the value of x (before the if/else.
2. Both branches will wire the output of their generic gate to all cells making use of x after the if/else statement.

Hope this example illustrates the issue.

before I talk about solutions, remember that in the non-active rows, we are free to assign arbitrary values to the cells of the execution trace (as no constraints will be imposed).

solution to the first problem. I think there's two ways to tackle that problem, one over-engineered way would be to modify the permutation argument to cancel terms dynamically if they're in a non-active rows. I haven't thought much about that, but I don't think it's necessary. The easy solution is to simply write the expected values in the cells of non-active rows. That is, if a cell is wired to some cell in an active-row, just have that cell store the same value as the same in the active row.

solution to the second problem. The problem can be solved in the same manner. If the output or the reassignment needs to be the value 6, for example, because that's what the active branch says; then the non-active branch can store the value 6 in the cell implicated in the output/reassignment.

This might not be really clear, and I probably need to draw a diagram or do a better job at explaining what's happening, but basically the idea is to fill the non-active rows with values that make sense with what's happening in the active rows and the permutation (not values that make sense in the non-active rows).

One problem I can imagine: there's a contradiction in the values we use to solve problem 1, and the values we use to solve problem 2. In other word, in the system of equations that we need to solve to fill the cells of the non-active rows (of the permutation columns) might not have a solution. Is this true in practice? I don't think so, or at least I can't find an example where this would be a problem.

Worst case we have a solution that is not complete, and we can test it with a number of use-cases and see if we often run into issues like the one I described.

[mimoo]

Interestingly, Noir also supports if/else statements, might be a good idea to see what they're doing there.

[mimoo]

Another way is to make all the gate selector polynomials masked runtime polynomials. (Thanks to @mrmr1993 for the idea again)

Let me explain using a fictive custom gate which has been assigned the selector polynomial cg(x) at compile time.

Instead of multiplying the custom gate equation with cg(x), we multiply it with cg'(x) which is a polynomial given to us at runtime by the prover.

We also apply the following constraints:fg(x) * (cg'(x) - cg(x)) = 0

This constraint makes sure that:

• in rows taken by the program (fg is set to 1), cg' must be equal to cg (the dynamic custom gate selector polynomial must be equal the original one)
• in rows not taken by the program (fg is set to 0), cg'can be equal 0 (to cancel the row). I don't think we need to enforce thatcg'` is 0, we don't care what they're doing because we don't want to enforce anything in the row.

With this approach, we need to pay the cost of X additional cg' polynomials in the proof (for X types of gates). We also need to wire an additional fg polynomial, which would increase the size of the permutation. That being said, do we actually use all 7 columns of the permutation?

[mimoo]

(or we could use that technique only for poseidon, which is the gate we don't want to increase the degree of)

[mimoo]

A not-so-well-thought-idea: maybe we don't need to use the permutation for cf. Maybe we can use turboplonk to tell it (via another selector polynomial) on every row to:

• take the same value as the previous row (no change of block)
• or take the value 1 - prev_row (reach a mutually exclusive branch)
• or take the value 1 (reset)

and add a constraint to ensure that it starts with the value 1 (similar to the permutation)