Custom gates

The goal of this section is to draw the connections between the practical aspect of designing custom gates and the theory behind it.

First, suppose we had the following layout of gates. This means that our circuit has four gates: a (single) generic gate, a (non-optimized) complete add, and then two different Example gates that we just make up for the example; ExamplePairs and ExampleTriples.

rowGateType::01234567891011121314
0Genericlro
1CompleteAddx1y1x2y2x3y3infsame_xsinf_zx21_inv
2ExamplePairsaeiouy
3ExampleTriplesabcdefghijklmno

The most important aspect to take into account when you are designing a new custom gate is writing the actual description of the new functionality. For this, we are using the Expression framework that allows us to write equations generically by representing each column of the table (wire) as a variable. Then we can write operations between them and define the gate constraints. From a mathematical perspective, these will have the shape of multivariate polynomials of as many variables as columns in the table (currently 15 for Kimchi) that is constrained to equal 0.

In our example, we would define equations that represent the operations carried out by each of the gates. In the following equations we use the variable names that we wrote in the cells above, and we don’t imply that the same name in a different row correspond to the same value (we are not imposing equalities between gates yet):

Generic:

  1. l r o l r

CompleteAdd:

  1. x21_inv x2 x1 same_x
  2. same_x x2 x1
  3. same_x s y1 x1 same_x x2 x1 s y2 + y1
  4. x1 x2 x3 s
  5. s x1 x3 y1 y3
  6. y2 y1 same_x inf
  7. y2 y1 inf_z inf

ExamplePairs:

  1. a e
  2. i o
  3. u y

ExampleTriples:

  1. a b c
  2. d e f
  3. g h i
  4. j k l
  5. m n o

Nonetheless, when we write these constraints in proof-systems, we use a shared framework that helps us use the columns in each row as placeholders. For example, the i-th column of the current row Curr is represented as:

#![allow(unused)]
fn main() {
E::<F>::cell(Column::Witness(i), CurrOrNext::Curr)
}

where the E type is a shorthand for Expr<ConstantExpr>. More succinctly, we refer to the above simply as:

#![allow(unused)]
fn main() {
witness_curr(i)
}

For readability, let’s just refer to them here as w0..w14. Then, the above constraints would look like the following:

Generic:

  1. w0 w1 w2 w0 w1

CompleteAdd:

  1. w10 w2 w0 w7
  2. w7 w2 w0
  3. w7 w8 w1 w0 w7 w2 w0 w8 w3 + w1
  4. w0 w2 w4 w8
  5. w8 w0 w4 w1 w4
  6. w3 w1 w7 w6
  7. w3 w1 w9 w6

ExamplePairs:

  1. w0 w1
  2. w2 w3
  3. w4 w5

ExampleTriples:

  1. w0 w1 w2
  2. w3 w4 w5
  3. w6 w7 w8
  4. w9 w10 w11
  5. w12 w13 w14

Looking at the list of equations, each of them look like polynomials in the variables w0..w14, constrained to zero. But so far, the type of equations we had studied were univariate (i.e. rather than ). But this will not be a problem, since these multivariate equations will soon become univariate with a simple trick: interpolation. Right now, we are describing the gate constraints row-wise (i.e. horizontally). But as we said before, our domain will be determined by the number of rows; we will transform these equations to a vertical and univariate behaviour. The strategy to follow will be obtaining witness polynomials that evaluate to the cells of the execution trace.

First, note that so far we didn’t mention any values for the w0..w14 terms, but instead they are placeholders for what is yet to come. And what is this you may ask: the witness of the relation. Put it another way, the witness will be the instantiation of the cells of the table that will make all of the above constraints hold. And where do we get these values from? Well, the prover will know or will compute them.

Second, we count the number of rows that we ended up with: here it’s four (conveniently, a power of two). What we want to do is to create as many witness polynomials as the number of columns in the execution trace. These polynomials, that we can call , must be design to evaluate to the cells of the trace. Formally we define each as:

Meaning that returns the -th column of the -th row of the execution trace. And how can we create such polynomials? We will use interpolation, which can be efficiently computed over power-of-two-sized groups, as it is the case in the example. Recalling Lagrangian terms, they act like linearly independent selectors over a set, in particular:

Let be a multiplicative group formed by the powers of a generator . Given any element in the group, the -th Lagrangian term evaluates to iff and iff .

Given that our group has size , the number of rows (ignoring ZK for now), will be the set . This means that we can build such witness polynomials as:

Then, the above constraints will become the following equations using our univariate witness polynomials:

Generic:

CompleteAdd:

ExamplePairs:

ExampleTriples:

These are the constraints that will need to be satisfied by a correct witness for the relation. We already know how to check many equations at once (combining them with powers of alpha), and how to check that the above holds for the full domain (by providing the quotient polynomial of the huge equation after dividing by the vanishing polynomial on ). All there’s left to do is making a correspondence between the constraints that need to be satisfied, and the particular row in the execution trace to which they apply. This implies, that before even aggregating the constraints into a single one, we need to impose this restriction.

In proof-systems, we represent this restriction with the GateType selector. In particular, we would multiply each of the constraints above by the Expr terms: Index(GateType::YourType), which will be transformed (again) into mutually exclusive selector polynomials. This means, that each row can only have one of these polynomials being nonzero (equal to ), whereas the evaluation of all of the other selector polynomials for the given row should be . These polynomials are known by the verifier, who could check that this is indeed the case.

But what will these polynomials look like? I am sure the above paragraph is familiar for you already. Once again, we will be able to build them using interpolation with our Lagrangian terms for . In our example: will equal when and otherwise; will equal when and otherwise; will equal when and otherwise; and will equal when and otherwise. These polynomials are, in fact, a description of the circuit.

Note that we managed to make constraints for different gates already independent from each other (thanks to the mutually exclusivity). Nonetheless, granting independence within the gate is still needed. Here’s where we will be using the powers of alpha: within a gate the powers cannot be repeated, but they can be reused among gates. Then, we will need different powers of alpha for this stage of the protocol, as this is the largest number of different constraints within the same gate.

Putting all of the above together, this means that our LONG and single constraint will look like:

Finally, providing and performing the check on a random \ would give the verifier the assurance of the following:

The prover knows a polynomial that equals zero on any .

Nonetheless, it would still remain to verify that actually corresponds to the encoding of the actual constraints. Meaning, checking that this polynomial encodes the column witnesses, and the agreed circuit. So instead of providing just (actually, a commitment to it), the prover can send commitments to each of the witness polynomials, so that the verifier can reconstruct the huge constraint using the encodings of the circuit (which is known ahead).