Fold a Fibonacci Circuit

Realization of a Fibonacci step circuit

This example builds upon the Quickstart by introducing a more complex and meaningful circuit $F([X_i, X_{i+1}]) = [X_{i+N}, X_{i+1+N}]$, where $X_i = X_{i-2} + X_{i-1}$. While the Quickstart features a basic identity mapping, this example demonstrates how to compute Fibonacci numbers iteratively using the Sirius framework, offering a deeper exploration of the framework's capabilities.

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

All changes from the Quickstart are captured in this commit: https://github.com/snarkify/sirius-fibonacci-example/commit/484209062c8bf184e491982647d751393b66e1e8

Why Build a Fibonacci Example?

This example demonstrates how to implement and configure a circuit that calculates Fibonacci numbers across multiple folding steps. It provides a more detailed understanding of the Sirius framework's flexibility and power, making it an ideal next step after completing the Quickstart.

Understanding Gates in Halo2 Frontend

Circuit Configuration in fn configure

In this section, we describe the specific changes made in the fn configure function within the FibonacciCircuit implementation. This function sets up the necessary components of the circuit to compute Fibonacci numbers.

/// Configure the step circuit. This method initializes necessary
/// fixed columns and advice columns
fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config {
    let config = Self::Config {
        s: cs.selector(),
        e: cs.advice_column(),
    };
                                                                  
    cs.enable_equality(config.e);
                                                                  
    cs.create_gate("fibo-block", |meta| {
        let s = meta.query_selector(config.s);
                                                                  
        let e1 = meta.query_advice(config.e, Rotation(-2));
        let e2 = meta.query_advice(config.e, Rotation(-1));
        let e3 = meta.query_advice(config.e, Rotation(0));
                                                                  
        vec![s * (e1 + e2 - e3)]
    });
                                                                  
    config
}

Explanation

• Selector (s): The selector s is initialized using cs.selector(). This selector controls when the Fibonacci gate is active, ensuring that the constraints are enforced only when necessary.

• Advice Column (e): An advice column is introduced to store the Fibonacci numbers as they are computed. The column is enabled for equality checks to ensure that values are coKnsistent across the circuit.

• Gate Definition: A gate named "fibo-block" is created using cs.create_gate. This gate enforces the Fibonacci relation $a_n = a_{n-2} + a_{n-1}$​, ensuring that each output value is correctly computed as the sum of the previous two inputs.

This configuration prepares the circuit to handle the iterative computation of Fibonacci numbers, demonstrating how to use selectors and advice columns in the Halo2 frontend.

Circuit Synthesis in fn synthesize_step

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

/// Sythesize the circuit for a computation step and return variable
/// that corresponds to the output of the step z_{i+1}
/// this method will be called when we synthesize the IVC_Circuit
///
/// Return `z_out` result
fn synthesize_step(
    &self,
    config: Self::Config,
    layouter: &mut impl Layouter<F>,
    z_i: &[AssignedCell<F, F>; 2],
) -> Result<[AssignedCell<F, F>; 2], SynthesisError> {
    let z_out = layouter.assign_region(
        || "main",
        |mut region| {
            let [a, b] = z_i;
                                                                                              
            FibonacciIter(a.value().copied(), b.value().copied())
                .enumerate()
                .map(|(offset, value)| {
                    let assigned = region.assign_advice(
                        || "element of sequence",
                        config.e,
                        offset,
                        || value,
                    )?;
                                                                                              
                    // Enforce equality constraints on the first two elements.
                    //
                    // For all other - enable gate with check. Note that the gate starts work
                    // at index 2, because the gate references the -2 cell internally
                    match offset {
                        0 => {
                            region.constrain_equal(a.cell(), assigned.cell())?;
                        }
                        1 => {
                            region.constrain_equal(b.cell(), assigned.cell())?;
                        }
                        _ => {
                            config.s.enable(&mut region, offset)?;
                        }
                    }
                                                                                              
                    Ok(assigned)
                })
                .take(N + A1)
                .skip(N) // We only need the last two elements (A1 := 2)
                .collect::<Result<Vec<_>, _>>()
        },
    )?;
                                                                                              
    Ok(z_out.try_into().unwrap())
}

Explanation

• Region Assignment: The layouter.assign_region function defines a region where the circuit logic is executed. Each iteration over z_i represents a computation step, with operations performed to generate the next Fibonacci number.

• Selector Activation: The selector s is enabled for each relevant row in the region using config.s.enable(&mut region, offset). This ensures that the Fibonacci relation is enforced only at the correct positions in the sequence.

• Input and Equality Constraint: The input values are assigned to the advice column a, and equality constraints are enforced to maintain consistency with the previous step's outputs.

• Summation and Output Assignment: The Fibonacci numbers are computed by summing the previous two values, and the results are stored in the advice column.

• Result Collection: The results are collected into an array, representing the output values (z_out) for this computation step.

This function synthesizes the circuit by assigning values and ensuring that all constraints are satisfied, effectively computing the Fibonacci sequence as 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, optimizing for speed. During the initial run, the setup for 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 quickly.

2. Subsequent Runs

For subsequent runs, use the following command:

cargo run

This command reuses the previously generated commitment keys, making the process faster. There's no need to recompile in release mode unless you make significant changes or need performance optimization again.

3. Expected Output

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

textCopy codestart 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 FibonacciCircuit in the Sirius Fibonacci Example. These functions work together to define and synthesize a circuit that computes Fibonacci numbers iteratively.

• fn configure: This function sets up the circuit by defining the necessary components, including a selector and an advice column. A custom gate is created to enforce the Fibonacci relation.

• 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, computes the Fibonacci numbers, and places the results in the output column.

Together, these functions illustrate how to configure and synthesize a more complex custom circuit within the Sirius framework, providing a clear example of how to build and execute iterative computations in a cryptographic context.