Regions in Halo2

Okay, circuits have chips, right?, oh! and regions!

Up until this point we have had a single large region, although this is a useful technique because it allows easy "repeating" computation by referring to neighboring cells, it would be a hard way to build circuits in general: normally, we like to compartmentalize and compose smaller things into larger things. Whether in software engineering or hardware design, this is a common pattern, and Halo2 circuit development is no different.

Using (multiple) regions will allow us to create distinct "logical" units that we can compose. In fact, what people usually refer to as a "gate" in regular circuits (think addition/multiplication gates) are in fact more analogous to regions with certain gates enabled in Halo2. This will enable us to create more complex circuits in a more modular way by building up a library of "gadgets" which we can compose to obtain more and more complex behavior.

Another Gate

Okay, new gate time...

Change the configure function into:

    fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
        let q_enable = meta.complex_selector();
        let advice = meta.advice_column();

        // define a new gate:
        meta.create_gate("vertical-mul", |meta| {
            let w0 = meta.query_advice(advice, Rotation(0));
            let w1 = meta.query_advice(advice, Rotation(1));
            let w3 = meta.query_advice(advice, Rotation(2));
            let q_enable = meta.query_selector(q_enable);
            vec![q_enable * (w0 * w1 - w3)]
        });

        TestConfig {
            _ph: PhantomData,
            q_mul: q_enable,
            advice,
        }
    }

To ease the creation of the multiplication gate, we will add a function that allocates a new separate region for a multiplication gate:

impl<F: Field> TestCircuit<F> {
    /// This region occupies 3 rows.
    fn mul(
        config: &<Self as Circuit<F>>::Config,
        layouter: &mut impl Layouter<F>,
        lhs: AssignedCell<F, F>,
        rhs: AssignedCell<F, F>,
    ) -> Result<AssignedCell<F, F>, Error> {
        layouter.assign_region(
            || "mul",
            |mut region| {
                let v0 = lhs.value().cloned();
                let v1 = rhs.value().cloned();
                let v2 =
                    v0 //
                        .and_then(|v0| v1.and_then(|v1| Value::known(v0 * v1)));

                let w0 = region.assign_advice(
                    || "assign w0", //
                    config.advice,
                    0,
                    || v0,
                )?;

                let w1 = region.assign_advice(
                    || "assign w1", //
                    config.advice,
                    1,
                    || v1,
                )?;

                let w2 = region.assign_advice(
                    || "assign w2", //
                    config.advice,
                    2,
                    || v2,
                )?;

                // turn on the gate
                config.q_mul.enable(&mut region, 0)?;
                Ok(w2)
            },
        )
    }
}

This function:

• Takes two assigned cells.
• Assigns the offset = 0 cell to the value of the lhs cell.
• Assigns the offset = 1 cell to the value of the rhs cell.
• Assigns the offset = 2 cell to the product of the two inputs.
• Turns on the vertical-mul gate.

Finally, it returns the offset = 2 cell: the product of the two inputs.

In order to use this function, we will also need some way to create assigned cells. To do this we create a function which allocates a small (1 row) region, enables no gates and simply returns the cell:

#![allow(unused)]
fn main() {
impl<F: Field> TestCircuit<F> {
    /// This region occupies 1 row.
    fn unconstrained(
        config: &<Self as Circuit<F>>::Config,
        layouter: &mut impl Layouter<F>,
        value: Value<F>,
    ) -> Result<AssignedCell<F, F>, Error> {
        layouter.assign_region(
            || "free variable",
            |mut region| {
                region.assign_advice(
                    || "assign w0", //
                    config.advice,
                    0,
                    || value,
                )
            },
        )
    }
}
}

With this we can start writing circuits in style:

    fn synthesize(
        &self,
        config: Self::Config, //
        mut layouter: impl Layouter<F>,
    ) -> Result<(), Error> {
        // create a new free variable
        let a = TestCircuit::<F>::unconstrained(
            &config, //
            &mut layouter,
            self.secret.clone(),
        )?;

        // do a few multiplications
        let a2 = TestCircuit::<F>::mul(
            &config, //
            &mut layouter,
            a.clone(),
            a.clone(),
        )?;
        let a3 = TestCircuit::<F>::mul(
            &config, //
            &mut layouter,
            a2.clone(),
            a.clone(),
        )?;
        let _a5 = TestCircuit::<F>::mul(
            &config, //
            &mut layouter,
            a3.clone(),
            a2.clone(),
        )?;

        Ok(())
    }

So far this circuit is not that useful: we are not checking the result of the multiplications against anything. We will get to that in the next couple of sections.

The Issue

As hinted at in the warning, this code is not safe!

The problem is that equality is not enforced between:

• The assigned cells lhs/rhs
• The assigned cells w0/w1

A malicious prover could set w0 and w1 to arbitrary values not related to the inputs of lhs and rhs. To fix this, we are going to need equality constraints, which we will explore in the next section.

Exercises