# Halo2 Circuits

## Groth16 Uses R1CS Arithmetization

R1CS encodes an arithmetic computation (addition and multiplication).

$\text{Public Inputs: } (1, x_1, \dots, x_m)$
$\text{Private Inputs: } (x_{m + 1}, \dots, x_n)$
$\text{Constraints: }(A_1B_1 = C_1, \dots, A_kB_k = C_k)$

**Variables** $x_i$ are stored in two vectors (public and private).

A **constraint** is a degree-1 or degree-2 polynomial equation: $\text{polynomial}_A * \text{polynomial}_B = \text{polynomial}_C$

$A_j, B_j, C_j$ are each a linear combination (degree-0 or degree-1 polynomial) of the constraint system variables $x_i$: $A_j, B_j, C_j = \sum_{i \in [1, n]}c_ix_i$.

$A_jB_j$ is a degree-1 or degree-2 polynomial.

**Addition** is encoded as a degree-1 constraint:
$$(x_1 + x_2) * (1) = (x_3)$$

**Linear combinations** are encoded as a degree-1 constraint:
$$(x_1 + 2x_2 + 3x_3) * (1) = (x_4)$$

**Multiplication** is encoded as a degree-1 constraint:
$$
(x_1) * (x_2) = (x_3) \\
(x_1 + x_2) * (2x_3 + 3x_4) = (x_5)
$$

## Halo2 uses Plonk Arithmetization

Plonk encodes an arithmetic computation plus variable copying and lookup tables.

Variables are laid out in a **matrix** and can have one of three types:
- **Advice** - private input
- **Instance** - public input
- **Fixed** - constant value

Each **column** in a matrix stores variables of a single type.


</br>

Halo2/Plonk use **custom constraints** - each constraint defines an arithmetic operation/operations on the matrix values which is not limited to the R1CS form $AB = C$.

Example custom constraints:
$$
x_1^{(i)} + x_2^{(i)} = x_3^{(i)} \\
x_1^{(i)} + x_2^{(i)} = x_1^{(i + 1)} \\
3x_1^{(i)} + 5x_2^{(i)}x_2^{(i)}x_3^{(i)} = \text{pi}^{(i)}
$$
Note that constraints can have degree greater than 2 (e.g. $x_1x_1x_1$) and variables are identified using there position in the matrix (e.g. $x_1^{(i)}$ is the variable in row $i$ of column $1$).

</br>

The Halo2 **constraint system** defines the matrix and custom constraints.

Each constraint $j$ is associated with a **selector** $s_j$ whose value in each row $s_j^{(i)} \in \{0, 1\}$ turns constraint $j$ on/off.

Each constraint $j$ is associated with a **fixed column** in the matrix $(s_j^{(1)}, \dots, s_j^{(n)})$ which determines whether the constraint is enabled/disabled in each matrix row.

Each circuit's constraint system must be **configured** before you can synthesize its values:
- Define columns
- Define constraints
- Define value copies
- Define lookup tables

// Circuit stores public and private inputs.
struct MyCircuit {
    pub_inputs: PublicInputs,
    priv_inputs: PrivateInputs,
}

// Circuit has two private inputs.
struct PrivateInputs {
    a: Value,
    b: Value,
}

// Circuit has no public inputs.
struct PublicInputs;

// `MyCircuit`'s configuration.
struct MyConfig {
    // Two advice columns.
    advice: [Column<Advice>; 2],
    // One constraint (addition).
    s_add: Selector,
}

impl Circuit for MyCircuit {
    type Config = MyConfig;
    type FloorPlanner = SimpleFloorPlanner;
    
    fn configure(cs: &mut ConstraintSystem) -> Self::Config {
        // Create columns:
        let a_1 = cs.advice_column();
        let a_2 = cs.advice_column();
        
        // Create constraints:
        let s_add = cs.selector();
        cs.create_gate("add", |cs| {
            // `Rotation::cur` is the row where `s_add` is enabled.
            let a = cs.query_advice(a_1, Rotation::cur());
            let b = cs.query_advice(a_2, Rotation::cur());
            
            // `Rotation::next` is the next row.
            let c = cs.query_advice(a_1, Rotation::next());
            
            // `a + b - c = 0`
            Constraints::with_selector(s_add, a + b - c)
        });
        
        MyConfig {
            advice: [a_1, a_2],
            s_add,
        }
    }
    
    fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter) -> Result<(), Error> {
        let [col_1, col_2] = config.advice;

        let _c = layouter.assign_region("a + b = c", |mut region| {
            // Row where `s_add` is enabled has a relative row index of `0` in the region.
            let offset = 0;
            
            // Turn addition constraint on using `s_add` selector.
            config.s_add.enable(region, offset)?;
            
            // Allocate values.
            let a = region.assign_advice("a", config.advice[0], offset, || self.priv_inputs.a)?;
            let b = region.assign_advice("b", config.advice[1], offset, || self.priv_inputs.b)?;
            region.assign_advice("c", config.advice[0], offset + 1, || {
                a.value().zip(b.value()).map(|(a, b)| a + b)
            })
        })?;
        
        Ok(())
    }
}