# Fold a Summation Circuit The example extends the [quickstart](https://docs.snarkify.io/sirius-folding/quickstart "mention") 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 All changes from the quickstart are captured in this commit: **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](https://docs.snarkify.io/terminologies#plonkish "mention") #### 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. ```rust fn configure(cs: &mut ConstraintSystem) -> 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. ```rust fn synthesize_step( &self, config: Self::Config, layouter: &mut impl Layouter, z_i: &[AssignedCell; A], ) -> Result<[AssignedCell; 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::, _>>() }, )?; 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: ```bash 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](#set-up-commitment-keys "mention") 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: ```bash 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.