Fold the zkevm-circuits

In previous section, we have illustrate how to use Sirius to fold user defined circuits. While these example serves a good start, they are more like toy examples. In this section, we will explain how to use Sirius to fold one important real-world application: zkEVM.

The EVM can be modeled as a state transition function. It specifies a transition function F that, given an initial world state S and a transaction T, outputs a new world state S’: f(S,T) = S'. This fits into the realm of IVC perfectly. In zkEVM circuit, we process the transactions as well as other blockchain data into circuit witness. The super_circuit proves that the state root is updated correctly.

zkEVM circuit is co-authored by PSE and Scroll using halo2 library. It has very complex structures that contains multiple sub-circuits and their interactions. These sub-circuits is put together into a giant halo2 circuit called super_circuit. This is the user defined step circuit that Sirius will fold. It turned out this is made possible by about 400 lines of codes. We will describe how to turn the super_circuit into a step circuit.

Transform zkEVM into step circuit

Circuit modification

In order to make zkEVM circuit as a step circuit, we just need to implement the StepCircuit trait. This trait is very similar to the halo2's Circuit trait except that the synthesize method is replaced with synthesize_step where we must expose z_in and z_out.

The most natural way is to define the prev_state_root as z_in, witness as auxiliary inputs, cur_state_root as z_out. i.e. we have z_out = F(w,z_in) . In sub-circuit pi_circuit (pi stands for public input), prev_state_root and cur_state_root are calculated and assigned, and there is no need to modify the circuit layout. By slightly modify the internal functions, the pi_circuit will expose them to super_circuit . Then next thing is to adapt the super_circuit configuration and synthesize methods, which is straightforward and most of the code can be reused.

Code snippet

All major changes are from zkevm-circuits repo and can be found in this PR. Some minor changes to the entry point is also necessary, which can be found in this PR.

Here we will highlight a few important modifications on zkemv-circuits

Step 1

Add prev_state_cells and last_state_cells in PiCircuit so that we can expose them in super_circuit later.

#[derive(Clone, Debug)]
pub struct PiCircuit<F: Field> {
    /// PublicInputs data known by the verifier
    pub public_data: PublicData,
    _marker: PhantomData<F>,

    connections: RefCell<Option<Connections<F>>>,
    tx_value_cells: RefCell<Option<Vec<AssignedCell<F, F>>>>,

    prev_state_cells: RefCell<Option<Vec<AssignedCell<F, F>>>>,
    last_state_cells: RefCell<Option<Vec<AssignedCell<F, F>>>>,
}

Step 2

Expose (prev_state_root, last_state_root) in fn assign_pi_bytes. By directly modify the following code, we avoid modifying the existing pi_circuit structure. In the return of assign_pi_bytes , we have both pi_hash_cells which is last_state_cells as well as newly added prev_state_cells

fn assign_pi_bytes() {
   // skip codes
   
   // Added the return of rpi_byte_cells, it includes prev_state_root to be exposed
   // last_state_root is already exposed by this function as pi_hash_cells
    let (rpi_cells, rpi_byte_cells): (Vec<AssignedCell<F, F>>, Vec<Vec<AssignedCell<F, F>>>) =
            [
                public_data.chain_id.to_be_bytes().to_vec(),
                public_data.prev_state_root.to_fixed_bytes().to_vec(),
                public_data.next_state_root.to_fixed_bytes().to_vec(),
                public_data.withdraw_trie_root.to_fixed_bytes().to_vec(),
            ].iter() // skip the rest of code for simplicity
     let prev_state_cells = rpi_byte_cells[1].clone();
     
     // skip codes
     
     // we expose pi_hash_cells (i.e. last_state_cells) as well as prev_state_cells
     Ok(((pi_hash_cells, prev_state_cells), connections))
}

Step 3

Add a helper function to export state root cells. This is z_in and z_out when we turn the super_circuit into a step_circuit

/// (3) export state root cells for step circuit z_in and z_out
pub fn export_io(&self) -> StepCircuitIO<F> {
    (self.prev_state_cells, self.last_state_cells)
}

Step 4

With all the preparations of previous steps, we can implement the required Sirius::StepCircuit trait with slightly modification from the implementation of halo2::Circuit trait. Usually, when we convert a halo2 circuit into Sirius step circuit, fn configuration stays the same. The logic of fn synthesize_step will be very similar to fn synthesize except that in fn synthesize_step accept the z_in as parameter.

More precisely, the input z_in is an array of fixed length assigned cells, these cells located in the "outer" of step circuit. We use copy constraint to assign them inside step circuit region. The rest of the logic is same as synthesize . At the end of function, we return the assigned cells z_out so that the "outer" circuit can use it later on.

/// (4) Implement StepCircuit trait for SuperCircuit
impl SuperCircuit // skip generics for simplicity
{
    // exactly same as `fn configure` in halo2::Circuit
    // so we skip paste it here
    fn configure();
    
    /// Helper function
    /// almost the same as synthesize_sub of super_circuit
    fn synthesize_sub_with_io(
        &self,
        config: &SuperCircuitConfig<Fr>,
        challenges: &crate::util::Challenges<Value<Fr>>,
        layouter: &mut impl Layouter<Fr>,
    ) -> Result<StepCircuitIO, Error> {
        // skip codes
        // in the end return z_in and z_out
        Ok(self.pi_circuit.export_io())
    }
    
     // this is the key function of StepCircuit trait
     // very similar to synthesize function
     fn synthesize_step(
        &self,
        (config, challenges): Self::Config,
        layouter: &mut impl Layouter<Fr>,
        z_i: &[AssignedCell<Fr, Fr>; ARITY],
    ) -> Result<[AssignedCell<Fr, Fr>; ARITY], SynthesisError> {
        let challenges = challenges.values(layouter);

        config.u8_table.load(layouter)?;
        config.u16_table.load(layouter)?;
        
        // the key difference here is that the super_circuit now
        // is part of Sirius's ivc folding circuit
        // Sirius is responsible to pass the input z_in to super_circuit
        // and get the z_out from super_circuit (i.e. by copy constraints)
        let (z_in, z_out) = self.synthesize_sub_with_io(&config, &challenges, layouter)?;

        assert_eq!(z_i.len(), z_in.len());

        z_i.iter().zip(z_in).try_for_each(|(lhs, rhs)| {
            layouter.assign_region(
                || "constrain step circuit z_in",
                move |mut region| region.constrain_equal(lhs.cell(), rhs.cell()),
            )?;
            Ok::<(), Error>(())
        })?;

        Ok(z_out
            .try_into()
            .unwrap_or_else(|v: Vec<AssignedCell<Fr, Fr>>| {
                panic!("ARITY {} must be equal {}", v.len(), ARITY)
        }))
    }
}

Check it out

You can try it out here:

// checkout the repo
git clone https://github.com/snarkify/scroll-prover;
cd scroll-prover;

// run the example
TRACE_PATH="tests/extra_traces/batch_495/chunk_495" make test-fold-prove;

This repo is just the entry point which depends on our modified zkevm-circuits repo.

Currently, it can be compiled successfully. However, it will have runtime error like this:

thread 'test_fold_prove' panicked at /Users/chao/.cargo/git/checkouts/sirius-fc7a02d83db739dc/30174b4/src/ivc/step_folding_circuit.rs:242:13:
You can't use instance column

This is because we are still missing several features to fully support the folding zkevm circuit. We listed a few important features in the following sub-section.

Challenges

Although we only have about 400 lines to modify the circuits as well as adding the folding prover. There are some challenges during this process. To solve these challenges, we need implement several new features. Here we list important ones.

Folding of public inputs

During the folding of zkevm circuit, the prover treats witness data as private inputs, after folding of multiple steps, the verifier is unable to verify the data source. The normal way of accumulate the public input of each step will not work well because during folding we use random linear combination to accumulate the public inputs. The random number depends on the commitment of witness of each step. The final verifier (i.e. decider) doesn't have access. Thus, the decider cannot compute the accumulated public inputs offline without knowing these challenges from each step.

Thus, the prover must accumulate the public IO of each step in a way such that the verifier can easily compute and verify it at the end. To the best of our knowledge, this part is neither clearly documented nor enforcized in existing literature or libraries. We added this feature in Sirius to accumulate step circuit's public IO so that the verifier can easily verify.

Large number of gates

super_circuit has about 2000+ custom gates. If we use powers of random linear number to combine them together as expression, the degree of the combined polynomial will be too high to deal with. Instead, we use Protogalaxy to evaluate each of them separately and combine their values together.

Large number of columns

super_circuit has about 800+ columns. In folding, we try to minimize the total number of commitments. To do this, we usually concatenate all the columns into one big vector and use a large commitment key (larger than the key for each column). However, with 800+ columns, it means the key size is increased by about 2^10.

The tradeoff is to make some balance between the size of commitment key and the number of commitments to be folded.

Compare with proof aggregation

The zkEVM prover first parses the execution trace from geth into a vector of Block which serves as the circuit inputs. Then feed the inputs into the super_circuit. Then the prover can synthesize the circuit and create a proof. However, when the number of blocks is too large to fit into a single circuit, prover has to split the execution traces into multiple chunks and aggregate them recursively into one final proof.

In Scroll's current design, zkEVM prover used 4-layers aggregation architecture. The first layer is to create one proof per chunk. After that, each layer consists of either compressing or aggregating proofs from previous layer. It worth to emphasize that the prover has to create a fully workable proof in order to move to next layer.

With Sirius folding scheme, the prover directly folds each chunk into accumulate instance per step. The total number of folding steps is specified by prover's choice. At the last step, prover uses decider to prove the accumulated instance. This approach eliminates the need of layered architecture as well as the individual proofs created by each layer.