Overview
The main circuit is called MainVM
. It is the one where all the main logic happens.
It consists of multiple cycles, where on each iteration we take a next opcode and try to execute it the following way:
if opcode == Add {
// do addition
}
if opcode == SRead {
// do storage read
}
...
You may notice that Add
instruction is much simpler than the SRead
one. When you work with circuits you still need
to execute every opcode.
That’s why we can use the following approach:
if opcode == Add {
// do addition
}
if opcode == SRead {
storage_queue.push((address, value));
// proof storage read in other circuit
}
...
So instead of proving SRead
we just push a proving request, that will be sent to another circuit, that will prove it.
That’s how we can make our prover structure more optimized and flexible.
For now, we have 13 base layer circuits:
- MainVM
- CodeDecommitmentsSorter
- CodeDecommitter
- LogDemuxer
- KeccakRoundFunction
- Sha256RoundFunction
- ECRecover
- RAMPermutation
- StorageSorter
- StorageApplication
- EventsSorter
- L1MessagesSorter
- L1MessagesHasher
They mostly communicate by queues (the diagram of communication is below).
Public Input Structure
Public Input (PI) is some piece of data, that is revealed to the verifier. Usually, it consists of some inputs and outputs.
The main challenge for base layer circuits is the ability to prove unlimited amount of execution. For example, our
MainVm
circuit can handle execution of opcodes. Then, if some transaction causes execution of more than
opcodes, we won’t be able to prove it. That’s why every circuit could be extended to multiple instances. So you can
always use MainVm
instances to handle up to opcode executions.
All circuits have the following PI structure:
start flag | Boolean that shows if this is the first instance of corresponding circuit type |
---|---|
finished flag | Boolean that shows if this is the last instance of corresponding circuit type |
Input | Structure that contains all inputs to this type of circuit (every instance of one circuit type has the same input) |
FSM Input and FSM Output | The field has the same structure. It represents the inner state of circuit execution (the first fsm_input is empty, the second fsm_input equals the first fsm_output and so on…) |
Output | Structure that contains all outputs of this type of circuit (the last instance contains the real output, the output field of the others is empty) |
The code implementation can be found here.
In terms of Arithmetization we don’t allocate all these fields like public input variables. A more efficient approach
would be computing commitment of type [Num<F>; 4]
with poseidon2 and then allocating these 4 variables as public
inputs.
The equality of corresponding parts in different circuits is done during aggregating base layer circuits. Aggregating is done by recursion level circuits that also verify base layer proofs. For now this is out of our scope, so we will focus only on base layer.
Overall View of Base Layer Circuits
Base Layer Circuits
There are a couple of circuits that do queue sorting. Learn more about the algorithm on Sorting.