Terminologies

ZKP

In the context of Zero-Knowledge Proofs (ZKP), a circuit is a mathematical representation of a computation. It is a structured way to encode logical and arithmetic operations that need to be verified. In essence, a circuit in ZKP serves as the blueprint for proving that a particular computation was carried out correctly without revealing the inputs or intermediate steps.

Key Concepts:

• Arithmetic Circuits: These are circuits that represent computations over finite fields. They consist of gates that perform basic operations like addition and multiplication. The wires connecting the gates represent variables or values.

• Constraints: Circuits are composed of constraints that must be satisfied for the computation to be considered valid. In ZKP, these constraints are often represented as polynomial equations over a finite field.

• Witness: The witness refers to the private inputs to the circuit that the prover uses to demonstrate that they know a valid solution to the circuit’s constraints.

• Public Inputs and Outputs: These are the values that are known to both the prover and verifier. The circuit ensures that the outputs are correctly computed from the inputs according to the circuit's logic.

• Prover and Verifier: In a ZKP system, the prover uses the circuit to demonstrate that a computation is correct, while the verifier checks the proof without needing to know the private inputs (witness).

Circuit

In ZKP systems, circuits are used to express complex computations that can be verified succinctly. The circuit breaks down the computation into small, verifiable steps, ensuring that every operation adheres to the defined constraints. This allows the verifier to be confident that the prover has correctly executed the computation, even without seeing the actual inputs or the complete computation process.

For example, in recursive proof systems like Nova, circuits are used to represent each step of an incremental computation. These circuits ensure that every step is independently verifiable, allowing for the entire computation to be verified incrementally.

Understanding the concept of a circuit is fundamental to grasping how ZKP systems function, as it forms the backbone of how computations are encoded, verified, and proven.

Step Circuit

Check Circuit first.

StepCircuit

The StepCircuit trait is a core component in the `IVC` struct. It represents a single step in an incremental computation process, providing the necessary structure for handling inputs, configuring the step-circuit, and producing outputs at each step.

Why `Step`?

The Step prefix denotes the fact that this circuit will be called at each step of the folding, rather than once. This also adds the concept of fixed-size input and output. That is, unlike a regular circuit, Sirius also have a mechanism for linking circuit states between steps.

PLONKish

Within the Sirius framework, we use PLONKish. For a mathematical description of the arithmetic, please refer to https://zcash.github.io/halo2/concepts/arithmetization.html

Within this constraint system, we have a matrix over a field (each matrix element is a finite field element over a prime number.

Phases

As part of the step-circuit implementation in Sirius, we have two phases:

• Configuration, when we set the circuit constraint strcuture, we create a matrix over the field that we will populate. This phase should not depend on the circuit-input in any way.

• Synthesis, when we fill the table and check if the generated witness falls under the constraints

API

For more details check Quickstart

#[derive(Debug, Clone)]
struct MyConfig {}
struct MyStepCircuit {}

impl<const A: usize, F: PrimeField> StepCircuit<A, F> for MyStepCircuit {
    /// This is a configuration object that stores things like columns.
    type Config = MyConfig;

    /// Configure the step circuit. This method initializes necessary
    /// fixed columns and advice columns
    fn configure(_cs: &mut ConstraintSystem<F>) -> Self::Config {
        todo!("impl `configure`")
    }

    /// 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>; A],
    ) -> Result<[AssignedCell<F, F>; A], SynthesisError> {
        todo!("impl `synthesize_step`")
    }
}

Columns

• Fixed (this also includes Selector & TableColumn) - immutable constants

• Instance - inputs to the circuit (provided externally)

• Advice - values depending on inputs

API

use sirius::halo2_proofs::plonk::{Advice, Column, Fixed, Instance, Selector, TableColumn};
struct Config {
    selector: Selector,
    advice: Column<Advice>,
    fixed: Column<Fixed>,
    instance: Column<Instance>,
    table_column: TableColumn,
}

Column Relationships (Gates)

Example: "5th column plus 4th column minus 9th column should equal 0"'

API

From Fold a Summation Circuit:

fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config {
    ...
                                                                        
    // Creating a gate that reflects the sum
    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)]
    });
                                                                        
    ...
}

Allowed Values for Relationships (Lookup)

Example: "5th column plus 4th column minus 9th column should be something from 1st column"

API

fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config {
    ...
                                                                  
    let allowed = cs.lookup_table_column();
    let advice = cs.advice_column();
                                                                  
    cs.lookup("main", |table| {
        let advice = table.query_advice(advice, Rotation::cur());
                                                                  
        vec![(advice, allowed)]
    });
                                                                  
    ...
}

Equalities Between Cells (Copy-Constraint)

Simply put, this is the only type of relationship not between columns but between cells.

API

From Fold a Summation Circuit

fn configure(cs: &mut ConstraintSystem<F>) -> Self::Config {
    ...
                                                                     
    // Allow equality check for `input`
    // for check consistency with `z_in`
    cs.enable_equality(config.input);
                                                                     
    ...
}
                                                                     
/// 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>; A],
) -> Result<[AssignedCell<F, F>; A], SynthesisError> {
    ...
    // Check at the constraint system level that the cells are equal
    region.constrain_equal(cell.cell(), input.cell())?;
    ...
}

IVC

Incrementally Verifiable Computation (IVC) allows the creation of proofs for each step of a computation incrementally, meaning proofs are generated as the computation progresses. This approach is efficient for long-running or stateful processes, as it avoids the need to re-compute the entire proof from scratch. IVC is particularly useful in blockchain and other systems where verifying sequential computations without re-running them is crucial. It supports efficient and scalable verification by enabling step-by-step proof generation and later combining these into a single proof.