Foreword

These docs aim to give a brief overview of what this repo is for, what it solves, and how it does so. For a deeper understanding, we recommend reading the source code: we hope it is declarative enough and that the comments are helpful.

General overview

The path from writing a Noir program and verifying a Plonky2 proof has many steps. This repo aims to touch only some of those, since the modularity provided by Aztec's stack allows it. We want to create a new backend for Noir using Plonky2 prover instead of Barretenberg. Essentially, these are the steps:

Read the ACIR circuit and the trace that solves it. These are the outputs of compiling and executing a Noir program with nargo execute.
Create a Plonky2 circuit equivalent to the ACIR circuit.
Provide concrete values to the Plonky2 circuit and generate the proof.

The ACIR circuit is composed by Opcodes, a set of abstract operations over variables. These variables are called witnesses in this context.

As for now, the backend as an executable has 3 operations:

prove
write_vk
verify

All the mentioned steps are performed in the prove command. The write_vk and verify mimics Barretenberg's behaviour:

write_vk should generate, serialize and persist the verification key so that the verify command can consume it.
verify should read the verification key and the proof and use the Plonky2 API to verify the proof.

Equivalence between ACIR Witnesses and Plonky2 Targets

In an ACIR circuit we have the concept of Witness. We can think of a witness as an inmutable variable in the circuit. All the opcodes operate over these witnesses, and they are numbered from 0 to N. On the other hand, Plonky2 circuits operate over the concept of Targets. You can think of Targets as the input and output wires that are connected to the operations in the arithmetic circuit. These targets are the skeleton of the circuit, and we cannot talk about this targets holding values while building the circuit, since the Targets will only be associated to values once the circuit is executing.

Throughout the construction of the Plonky2 circuit we'll need a mapping between Witnesses and some Targets, more specifically we'll need an injective function F: Witness -> Targets. Why? Because two different opcodes can refer to the same witness, and in those cases we'll want to refer to the same targets while we're building the circuit. Besides, to generate the Plonky2 proof we need to provide some concrete values to the input targets.

Opcodes

Opcodes are the basic elements that make the ACIR abstraction. An Abstract Circuit Intermediate Representation (ACIR) is a set of opcodes of different kinds (AssertZero, MemoryInit, MemoryOp, BlackBoxFunction, BrilligCall). These opcodes take different forms and talk about witnesses (inmutable variables in the circuit) and their main function is to establish restrictions over these witnesses.

AssertZero

AssertZero is the main opcode in almost any circuit: it allows arithmetic operations over an arbitrary set of variables. This arithmetic operations are represented through equations that must hold throughout the program. For example, if we want to say

x := y*y + z - 2

we should express it like an equation

y*y + z - x - 2 == 0

that ultimately will translate into an AssertZero opcode of the form

#![allow(unused)]
fn main() {
{
    quadratic_terms: [(1,y,y)]
    linear_combinations: [(1,z), (-1, x)]
    constant: -2
}
}

Any assignment of a variable done in Noir, or any comparison by equality will end up being an AssertZero opcode.

Equivalence in Plonky2

Plonky2 has an ArithmeticGate that we can access through the CircuitBuilder API. There are some methods that we can use to facilitate the translation without the need of using the gate directly:

add(t1: Target, t2: Target)
mul(t1: Target, t2: Target)
mul_const(t1: Target, c: FieldElement)
assert_zero(t: Target) -> Restricts the value being held by the target to equal 0.

The ArithmeticGate accepts equations of the form

k_0 * x * y + k_1 * z

so to translate a single AssertZero we need to generate a Plonky2 circuit that potentially uses many Arithmetic Gates. So, to sum it up, a single AssertZero opcode might be translated to many arithmetic operations.

Memory Operations

There are 2 memory operations: MemoryInit and MemoryOp (read or write). This opcode exists to handle the case where we read or write values from arrays with an unknown position in circuit-building time. For example, the Noir program...

fn main(array: [Field; 5]) -> pub Field {
    array[3]
}

...resolves to AssertZero opcodes, since the input Witness are w0, w1, w2, w3 & w4, the output witness is w5, and the code just makes an AssertZero to ensure that w3 is equal to w5. Instead, when the Noir code looks like this...

fn main(array: [Field; 5], index: Field) -> pub Field {
    array[index]
}

...then we're making a random access into an array in a position unknown at the time the circuit is being built. This requires the concept of Memory blocks (or memory arrays).

MemoryInit

It represents the creation of an array in memory. What does this mean for a prover? Well, it depends on the prover. This opcode will be translated into a set of constraints that will be used to generate the Plonky2 circuit. It has 2 fields:

block_id: the memory block index that is being created. This index will be global within our program. It's numbered from 0 to N.
witnesses: an array of the witnesses that hold the initial values of the memory block.

Our way of translating this to Plonky2 was simply creating a global mapping between indexes and arrays of Plonky2 targets, like HashMap<usize,Vec<Target>>.

MemoryOp

It represents either a memory read operation or a memory write operation.

Memory Read

The opcode has the following fields:

block_id: the index of the memory block we're reading from.
index: witness that holds the value of the index where we want to read from. It's like array[index].
value: witness where the value of the memory read will be stored. It's like value = array[index].

To implement this we used the Plonky2 RandomAccessMemory gate through the CircuitBuilder's random_access() method.

Memory Write

The opcode has the following fields:

block_id: the memory block index we're writing into.
index: witness that holds the value of the index we want to write into.
value: witness that holds the value we want to write. Assume we have a value = w_1.

This would be equivalent as doing array[index] = value.

Now, this operation is a bit tricky since we don't know the position we're writing while building the circuit. During the circuit construction, we have arrays of targets representing our memory blocks, and these targets have unchangeable values during circuit execution. We need to create a static circuit, but any slot's value could change. Therefore, we need to create an entirely new array and constrain its values to be the same as the previous ones, except for the position we're changing. As you can imagine, this operation is rather expensive.

To visualize this: imagine we need to write position 2 with some value v. Then we'll need to create a new set of targets and attach them to the corresponding value.

Previous memory block: | t0 | t1 | t2 | t3 | t4 | ↓ ↓ ↓ ↓ New memory block: | t0' | t1' | t2' | t3' | t4' | ↑ New value: v

We iterate over all the targets, using the CircuitBuilder's is_equal() method to figure out which position are we changing. If the position doesn't match the index, we link it to the target in the previous version of the memory block on the same position. If the position matches the index, then we create a new target with the value we want to write and link it to the new memory array.

BrilligCall Opcode

In Noir there are explicit unconstrained functions like the ones we define with the unconstrained keyword. This means that the return values of this functions will not be constrained, they will be like clues to the circuit provided through the Witness values. There are also implicit brillig calls like when we try to find the inverse of a field element. We can ignore these opcodes because their only purpose is to notify that some calculations were made that will not be constrained on the same way they were performed. The implicit brillig calls usually come with some assertZero opcodes that assert that the RESULT of the calculation is correct, like when we make a division.

It's important to remark that the "clues" provided in the witness as a result of a BrilligCall should be passed over to the prover (just like we do with the input values) since there is no way the Plonky2 execution can figure out these values on its own.

BlackBoxFunction opcode

This opcode is different from Brillig Opcode. The idea is similar, but in this case we do want to constrain the calculations, and that's the key difference. The idea behind blackbox functions is to delegate to the proving backend the responsibility of how that calculation should be represented within its paradigm, so it can produce an optimal circuit. There are lots of blackbox functions. The ones done so far for Plonky2 are:

Docs