Fold a Summation Circuit

The example extends the Quickstart by introducing a summation circuit $F(X) = X+X$.

While the quickstart features a basic identity mapping ($F(X) = X$), this example replaces it with a custom StepCircuit that performs a summation operation, offering a more practical and detailed exploration of the Sirius framework.

The entire code for this example can be found at https://github.com/snarkify/sirius-simple-example

All changes from the quickstart are captured in this commit: https://github.com/snarkify/sirius-simple-example/commit/5b3e7bd449c1e10be2f90db4762838e066c2a10f

Why Build a Simple Example?

This example demonstrates how to move beyond basic operations by implementing a circuit that actively processes inputs, specifically summing them with themselves. This approach provides a clearer understanding of how to create and configure custom circuits using Sirius, making it an ideal next step after completing the quickstart.

Understanding Gates in Halo2 Frontend

In Halo2, a gate is a core component used to enforce specific constraints in a cryptographic circuit. At a high level, a gate defines a mathematical relationship between different values within the circuit, ensuring that certain conditions are met. For example, a multiplication gate might ensure that the product of two input values equals an output value.

Gates use symbolic expressions to represent these relationships, which are later enforced during the proof generation process. These expressions are crucial in ensuring the circuit operates correctly and can be verified by both the prover and the verifier.

For more details, please check our page on PLONKish

Circuit Configuration in fn configure

In this section, we describe the specific changes made in the fn configure function within the MyStepCircuit implementation. This function is responsible for setting up the necessary components of the circuit to perform a simple summation operation.

fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config {
    let config = Self::Config {
        s: cs.selector(),
        input: cs.advice_column(),
        output: cs.advice_column(),
    };

    // Allow equality check for `input` to ensure consistency with `z_in`
    cs.enable_equality(config.input);

    // Creating a gate that enforces input + input = output
    cs.create_gate("sum", |meta| {
        let s = meta.query_selector(config.s);
        let input = meta.query_advice(config.input, Rotation::cur());
        let output = meta.query_advice(config.output, Rotation::cur());

        vec![s * (input.clone() + input - output)]
    });

    config
}

Explanation

1. Selector (s):

   • The selector s is initialized using cs.selector(). This selector is used to control when the summation gate is active, ensuring that the gate’s constraints are only enforced during the appropriate operations.

2. Advice Columns (input, output):

   • Two advice columns are introduced:

     • input: This column holds the input values, which will be used in the summation operation.

     • output: This column stores the results of the summation (input + input).

   • The equality check is enabled for the input column with cs.enable_equality(config.input), ensuring that the same value is used consistently within the circuit.

3. Gate Definition:

   • A gate named "sum" is created using cs.create_gate. This gate enforces the condition that the value in the output column must be equal to the sum of the input column value with itself (i.e., input + input).

   • The equation is constructed as s * (input.clone() + input - output), where s is the selector controlling the gate, and input and output are the values from the respective columns. This ensures that the circuit correctly performs the summation operation.

This configuration sets up the circuit to handle a simple summation operation, demonstrating how to use selectors and advice columns within the Halo2 framework.

Circuit Synthesis in fn synthesize_step

In this section, we describe the specific changes made in the fn synthesize_step function within the MyStepCircuit implementation. This function is responsible for assigning values to the circuit's cells and enforcing the constraints defined during the configuration phase.

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 output = layouter.assign_region(
        || "main",
        |mut region| {
            z_i.iter()
                .enumerate() // we need an index to use as offset
                .map(|(i, cell)| {
                    // Enable selector to trigger the gate
                    config.s.enable(&mut region, i)?;

                    // Assign the input value to the `input` column
                    let input = region.assign_advice(
                        || "input",
                        config.input,
                        i,
                        || cell.value().copied(),
                    )?;

                    // Check at the constraint system level that the cells are equal
                    region.constrain_equal(cell.cell(), input.cell())?;

                    // Perform the operation and place the result in the `output` column
                    let output = region.assign_advice(
                        || "output",
                        config.output,
                        i,
                        || input.value().copied() + input.value(),
                    )?;

                    Ok(output)
                })
                .collect::<Result<Vec<_>, _>>()
        },
    )?;

    Ok(output
        .try_into() // convert to array
        .expect("safe, because collect from input array"))
}

Explanation

1. Region Assignment:

   • The layouter.assign_region function is used to define a region in which the circuit's logic will be executed. Each iteration over z_i represents a step in the circuit, with operations performed on each input value.

2. Selector Activation:

   • The selector s is enabled for each row in the region using config.s.enable(&mut region, i). This activates the gate that enforces the summation operation defined in the configuration step. This gate will not work on the other lines. It is important that gates should be enabled regardless of the input on the same offsets.

3. Input Assignment:

   • The input value is assigned to the input column using region.assign_advice. This step copies the value from z_i into the input column, where it will be used in the summation operation.

4. Equality Constraint:

   • The region.constrain_equal(cell.cell(), input.cell()) function ensures that the original input cell (z_i) is equal to the newly assigned input cell. This check enforces consistency in the values being used across the circuit.

5. Summation and Output Assignment:

   • The summation operation is performed, and the result is placed in the output column using region.assign_advice. Specifically, the input value is doubled (input.value().copied() + input.value()) and assigned to the output column.

6. Result Collection:

   • The results from all iterations are collected into a vector and then converted into an array using try_into. This array represents the output values (z_out) of the circuit for this step.

This function synthesizes the circuit by assigning values and ensuring that all constraints are satisfied, effectively performing the summation operation defined in the configuration.

Running the Example

1. First Run

To run the example for the first time, use the following command:

cargo run --release

This will compile the project in release mode, which is optimized for speed. During this initial run, the #set-up-commitment-keys for the BN256 and Grumpkin curves will be generated and cached. This process may take some time, so running in release mode ensures it completes as quickly as possible.

2. Subsequent Runs

For subsequent runs, you can use the following command without the --release flag:

cargo run

This will reuse the previously generated commitment keys, so the process will be faster, and there’s no need to recompile in release mode unless you're making significant changes or need the performance optimization again.

3. Expected Output

When the example runs successfully, you should see output indicating that the folding steps were executed and verified successfully:

start setup primary commitment key: bn256
start setup secondary commitment key: grumpkin
ivc created
folding step 1 was successful
folding step 2 was successful
folding step 3 was successful
folding step 4 was successful
folding step 5 was successful
verification successful
success

Summary

In this section, we explored the implementation of the fn configure and fn synthesize_step functions within the MyStepCircuit in the Sirius Simple Example. These functions work together to define and synthesize a simple step circuit that performs a summation operation.

• fn configure: This function sets up the circuit by defining the necessary components, including a selector and advice columns for input and output. A custom gate is created to enforce the summation logic, where the input is doubled and stored in the output column.

• fn synthesize_step: This function assigns values to the circuit's cells and ensures that all constraints are correctly enforced. It activates the selector, assigns the input values, performs the summation, and places the result in the output column, synthesizing the circuit for each computation step.

Together, these functions illustrate how to configure and synthesize a simple custom circuit within the Sirius framework, providing a clear example of circuit creation and execution. This example helps developers understand the practical steps involved in building and running custom circuits in a cryptographic context.