Fold a Halo2 Circuit

You can reuse chips & gadgets from the halo2 ecosystem without restriction, as well as reuse the implementation code of the circuit itself. However, you must allocate at the logic level the part of the circuit that will be used as input and output (z_in & z_out) from the circuit, checking the consistency of steps

Suppose we have a halo2 circuit that proves opcodes for VM. Then when turning such a circuit into a step-circuit, we must represent the state of the VM-like memory into a fixed-size array (e.g. using a hash function) and check the consistency of this memory at the beginning and end of the circuit synthetize. This way, no matter how many execution steps there are, you will always get a mathematical proof that each step is consistent with the previous one.

Consider a simple case, we have a circuit proving a hash function and we want to have a step-circuit proving an arbitrary number of nested hashes for a fixed data set. Then the only task will be to take the argument of the hash function as input (z_in) and return AssignedCell representing the ready hash (z_out). Then IVC will be able to prove any number of nested hashes without overhead in the proof step.

The `ShuffleChip` Example

This section documents the iterative process of evolving a Sirius project by integrating a Halo2's ShuffleChip. The development process is captured through specific commits, each introducing new functionality or improving the existing implementation.

Initial Fork from Sirius Quickstart

The project began by forking the sirius-quickstart repository. This initial step provided a working example of a simple StepCircuit in the Sirius framework, which performed a trivial operation—returning the input unchanged over multiple folding steps.

• Commit: Sirius Quickstart Init

Key Features:

• Trivial StepCircuit: A basic StepCircuit implementation that served as the foundation for further development.

• Initial Configuration: Basic setup for primary and secondary circuits using BN256 and Grumpkin elliptic curves.

Adding Halo2's ShuffleChip

Integrating the ShuffleChip Example

In this phase, the project was extended by incorporating the ShuffleChip example from the Halo2 library. The adaptation required minimal changes—mainly making some fields public to fit the existing Sirius framework. This straightforward integration highlights how easily Halo2 components can be used within Sirius. Also at this stage, we have copied the halo2 circuit implementation inside the step circuit trait implementation without modification.

• Commit: Add ShuffleChip Example

Key Changes:

• ShuffleChip Module: Added the ShuffleChip as a module in the project.

• Minimal Adaptation: The only changes needed were making some fields public, demonstrating the seamless compatibility between Halo2 chips and Sirius.

Enhancing Circuit Logic and Input Handling

Add Consistency Between Steps

With the integration of the ShuffleChip, the next step involved refining how inputs were handled across different folding steps. The input handling was improved by moving input_0 from a simple private signal to being passed as z_in for each step. This change made the circuit consistent across all folding steps.

• Commit: Implement Step-Circuit with Enhanced Input Handling

Key Enhancements:

• Input Consistency: By tying input_0 directly to z_in, the circuit now ensures consistent data flow across folding steps, enhancing the integrity of the computation.

• Increased Commitment Key Size: The number of columns in the circuit increased, requiring a larger commitment key size to accommodate the added complexity.

• Array Usage for Inputs: Arrays replaced Vec for inputs and shuffles to guarantee consistent sizes across all steps, a necessary condition for correct step synthesis.

Code Explanation

Configuring the Circuit

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
    let input_0 = meta.advice_column();
    meta.enable_equality(input_0);
    let input_1 = meta.fixed_column();
    let shuffle_0 = meta.advice_column();
    let shuffle_1 = meta.advice_column();
    ShuffleChip::configure(meta, input_0, input_1, shuffle_0, shuffle_1)
}

Here we repeat the halo2_proofs::plonk::Circuit::configure code almost verbatim, however, we add a call to enable_equality to perform an equality check with z_in in the synthesize_step.

Synthesizing the Step-Circuit

fn synthesize_step(
    &self,
    config: Self::Config,
    layouter: &mut impl Layouter<F>,
    z_i: &[AssignedCell<F, F>; A],
) -> Result<[AssignedCell<F, F>; A], SynthesisError> {
    let ch = ShuffleChip::<F>::construct(config);

    layouter.assign_region(
        || "load inputs",
        |mut region| {
            for (i, (input_0, input_1)) in z_i.iter().zip(self.input_1.iter()).enumerate() {
                input_0.copy_advice(|| "input 0", &mut region, ch.config.input_0, i)?;

                region.assign_fixed(
                    || "input_1",
                    ch.config.input_1,
                    i,
                    || Value::known(*input_1),
                )?;
                ch.config.s_input.enable(&mut region, i)?;
            }
            Ok(())
        },
    )?;
    let z_out = layouter.assign_region(
        || "load shuffles",
        |mut region| {
            self.shuffle_0
                .iter()
                .zip(self.shuffle_1.iter())
                .enumerate()
                .map(|(i, (shuffle_0, shuffle_1))| {
                    region.assign_advice(
                        || "shuffle_1",
                        ch.config.shuffle_1,
                        i,
                        || *shuffle_1,
                    )?;
                    ch.config.s_shuffle.enable(&mut region, i)?;

                    region.assign_advice(|| "shuffle_0", ch.config.shuffle_0, i, || *shuffle_0)
                })
                .collect::<Result<Vec<_>, _>>()
        },
    )?;

    // For this commit - ignore processing of input
    Ok(z_out.try_into().unwrap())
}

Here we also repeat the code of halo2_proofs::plonk::Circuit::synthesize implementation, but there are two important differences:

• Handling the input with an equality check (copy_advice). We don't just have to switch from private input to z_in, but also add a check at the ConstraintSystem level.

• Storing shuffle_0 cells and returning them from step synthesis so that they can be reused in subsequent steps, ensuring step-circuit consistency within the IVC framework

Summary

This iterative development process highlights the flexibility of the Sirius framework in accommodating and integrating Halo2's chips, like ShuffleChip. The minimal adaptation needed for the integration demonstrates how seamlessly Sirius can work with existing cryptographic components. Each commit represents a step towards building a more complex and functional circuit, starting from a basic template to a fully integrated solution