Halo 2 for Dummies

Halo 2 is succint non-interactive zero-knowledge argument of knowledge (zkSNARK) library for developing applications with an associated zkSNARK in order to prove their honesty in computing the programs. In this chapter, I present a simple implementation of a program, under the form of a $2$ -variable polynomial, by using Halo 2.

Author(s): khaihanhtang

PLONKish Arithemetization

We recommend readers who are not familiar with PlonK's arithmetization to read the article PlonK's Arithmetization. In this chapter, we further discuss a more customized version of PlonK's arithmetization, namely, PLONKish arithmetization. Customization aims to handle more general gates with more complicated structures rather than employing only multiplication, addition, multiplication with constants and addition with constants gates.

PLONKish arithmetization can be pictured as a table of the following types of columns:

Constant columns for putting constants,
Instant columns for putting public inputs,
Advice columns for putting private inputs, literally known as witnesses,
Selector columns for putting selectors.

For simplicity, in this section, we present a transformation from a program, represented by an arithmetic circuit, to the form of PLONKish arithmetization. This transformation can be showed by an example that proves the knowledge of a $2$ -variable polynomial specified in A Simple Arithmetic Circuit. Then, we explain the method for transforming this polynomial to the form of PLONKish arithmetization in Transforming to PLONKish Arithmetization and programming in A Simple Halo 2 Program.

A Simple Arithmetic Circuit

Let $\mathbb{F}$ be some finite field. We would like to show in this section the transformation from the program computing polynomial $f(u, v) = u^2 + 3uv + v + 5$ where $u, v \in \mathbb{F}$ . With inputs $u, v \in \mathbb{F}$ , the arithmetic circuit for this polynomial is equivalently represented by topologically following the sequence of computations below.

Compute $u^2$ .
Compute $uv$ .
Compute $3uv$ .
Compute $u^2 + 3uv$ .
Compute $u^2 + 3uv + v$ .
Compute $u^2 + 3uv + v + 5$ .

Transforming to PLONKish Arithmetization

To setup the above sequence of computations, in A Simple Arithmetic Circuit, into PLONKish arithmetization, we specify a table to contain all possible variables appeared during the computing the arithmetic circuit for $f(u,v) = u^2 + 3uv + v + 5$ . Then, for each row, we setup a the set gates, or equivalently gate constraints, that applies to the row.

Specifying columns

We define the following tuple of columns

(\mathsf{advice} _0, \mathsf{advice} _1, \mathsf{advice} _2, \mathsf{constant}, \mathsf{selector} _{\mathsf{add}}, \mathsf{selector} _{\mathsf{mul}}, \mathsf{selector} _{\mathsf{addc}}, \mathsf{selector} _{\mathsf{mulc}})

where

$\mathsf{advice}_0, \mathsf{advice}_1, \mathsf{advice}_2$ are columns containing private inputs, i.e., values belonging to these columns are hidden to any verifier,
$\mathsf{constant}$ is the column containing public constants appearing during the computation,
$\mathsf{selector} _{\mathsf{add}}, \mathsf{selector} _{\mathsf{mul}}, \mathsf{selector} _{\mathsf{addc}}, \mathsf{selector} _{\mathsf{mulc}}$ contain public selectors corresponding to addition, multiplication, addition with constant, multiplication with constant, respectively, gates.

Transforming to Constraints and Meaning of Columns

We now explain the intuition to the above setting of columns. To do this, we need to transform the sequence of computations in A Simple Arithmetic Circuit into $2$ parts, namely, gate constraints (or gate identities) and wire constraints (or wire identities). In particular, we transform

\begin{align} t^{(1)} &= u^2, &t^{(3)} &= t^{(2)} \cdot 3 = 3uv, & t^{(5)} &= t^{(4)} + v = u^2 + 3uv + v,\\\\ t^{(2)} &= u v, & t^{(4)} &= t^{(1)} + t^{(3)} = u^2 + 3uv, &t^{(6)} &= t^{(5)} + 5 = u^2 + 3uv + v + 5 \end{align}

to gate constraints

\begin{align} x ^{(1)} _{c} &= x ^{(1)} _{a} \cdot x ^{(1)} _{b}, & x ^{(3)} _{c} &= x ^{(3)} _{a} \cdot 3, & x ^{(5)} _{c} &= x ^{(5)} _{a} + x ^{(5)} _{b},\\\\ x ^{(2)} _{c} &= x ^{(2)} _{a} \cdot x ^{(2)} _{b}, & x ^{(4)} _{c} &= x ^{(4)} _{a} + x ^{(4)} _{b}, & x ^{(6)} _{c} &= x ^{(6)} _{a} + 5 \end{align}

and wire constraints

\begin{align} u &= x_{a}^{(1)} = x_{a}^{(2)} = x_{b}^{(1)}, &t^{(1)} &= x_{a}^{(4)} = x_{c}^{(1)}, &t^{(3)} &= x_{b}^{(4)} = x_{c}^{(3)}, &t^{(5)} &= x_{a}^{(6)} = x_{c}^{(5)},\\\\ v &= x_{b}^{(2)} = x_{b}^{(5)}, &t^{(2)} &= x_{a}^{(3)} = x_{c}^{(2)}, &t^{(4)} &= x_{a}^{(5)} = x_{c}^{(4)}, &t^{(6)} &= x_{c}^{(6)}. \end{align}

We note that $x_b^{(3)}, x_b^{(6)}$ are not set. To deal with these values, we simple set them to be equal to any random vales, since they do not affect the constraints defined above.

Notice that each equation in gate constrains receives either $2$ secret inputs or $1$ secret input and $1$ constant and returns $1$ secret output. Therefore, we use $2$ columns, namely, $\mathsf{advice}_0$ and $\mathsf{advice}_1$ , to contain the secret inputs and $1$ column, namely, $\mathsf{advice}_2$ , to contain the secret output. Moreover, we also use the column $\mathsf{constant}$ to contain possible public constants.

The remaining columns, namely, $\mathsf{selector} _{\mathsf{add}}, \mathsf{selector} _{\mathsf{mul}}, \mathsf{selector} _{\mathsf{addc}}, \mathsf{selector} _{\mathsf{mulc}}$ , are employed to contain the selectors indicating the required constraints for each row, which corresponds to a constraint in the set of gate constraints specified above. We now clarify the employment of selectors to guarantee the correctness of gate constraints.

Specifying Table Values and Gate Constraints

For each row $i \in \\{1, \dots, 6\\}$ of the table, we denote by the tuple

(x_{a}^{(i)}, x_{b}^{(i)}, x_{c}^{(i)}, c^{(i)}, s_{\mathsf{add}}^{(i)}, s_{\mathsf{mul}}^{(i)}, s_{\mathsf{addc}}^{(i)}, s_{\mathsf{mulc}}^{(i)})

corresponding to the tuple of columns

(\mathsf{advice} _0, \mathsf{advice} _1, \mathsf{advice} _2, \mathsf{constant}, \mathsf{selector} _{\mathsf{add}}, \mathsf{selector} _{\mathsf{mul}}, \mathsf{selector} _{\mathsf{addc}}, \mathsf{selector} _{\mathsf{mulc}})

devised above.

For each row $i \in \\{1,\dots, 6\\}$ , we set the following $4$ constraints

\begin{align} s_\mathsf{add}^{(i)}\cdot (x_{a}^{(i)} + x_{b}^{(i)} - x_{c}^{(i)}) &= 0, & s_\mathsf{mul}^{(i)}\cdot (x_{a}^{(i)} \cdot x_{b}^{(i)} - x_{c}^{(i)}) &= 0,\\\\ s_\mathsf{addc}^{(i)}\cdot (x_{a}^{(i)} + c^{(i)} - x_{c}^{(i)}) &= 0, & s_\mathsf{mulc}^{(i)}\cdot (x_{a}^{(i)} \cdot c^{(i)} - x_{c}^{(i)}) &= 0. \end{align}

Example. Assume that the $i$ -th row corresponds to a multiplication gate. Hence, in this case, we set $(s_{\mathsf{add}}^{(i)}, s_{\mathsf{mul}}^{(i)}, s_{\mathsf{addc}}^{(i)}, s_{\mathsf{mulc}}^{(i)}) = (0, 1, 0, 0)$ . We can see that only $s_{\mathsf{mul}}^{(i)} = 1$ while remaining selectors are set to $0$ .

Therefore, whatever the values $x_{a}^{(i)}, x_{b}^{(i)}, x_{c}^{(i)}, c^{(i)}$ are set, the results always hold with respect to the gates $s_\mathsf{add}^{(i)}\cdot (x_{a}^{(i)} + x_{b}^{(i)} - x_{c}^{(i)}) = 0, s_\mathsf{addc}^{(i)}\cdot (x_{a}^{(i)} + c^{(i)} - x_{c}^{(i)}) = 0$ and $s_\mathsf{mulc}^{(i)}\cdot (x_{a}^{(i)} \cdot c^{(i)} - x_{c}^{(i)}) = 0$ .

However, since $s_{\mathsf{mul}}^{(i)} = 1$ , we can see that the gate $s_\mathsf{mul}^{(i)}\cdot (x_{a}^{(i)} \cdot x_{b}^{(i)} - x_{c}^{(i)}) = 0$ must guarantee $x_{a}^{(i)} \cdot x_{b}^{(i)} = x_{c}^{(i)}$ .

A Simple Halo 2 Program

Based on the specifications in Transforming to PLONKish Arithmetization, we now show an implementation in Rust for proving knowledge of input of $f(u, v) = u^2 + 3uv + v + 5$ mentioned in A Simple Arithmetic Circuit. The implementation can be found in Example of Halo2-PSE.

The following are a recommended for setting up a Rust implementation for Halo 2.

In Cargo.toml, specify the dependency

[dependencies]
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git" }

In main.rs, we implement step-by-step as follows:

Specify columns by putting all possible columns into a custom struct MyConfig.

#[derive(Clone, Debug)]
struct MyConfig {
    advice: [Column<Advice>; 3],
    instance: Column<Instance>,
    constant: Column<Fixed>,

    // selectors
    s_add: Selector,
    s_mul: Selector,
    s_add_c: Selector,
    s_mul_c: Selector,
}

Define gates based on elements of the above defined struct.

impl<Field: FieldExt> FChip<Field> {
    fn configure(
        meta: &mut ConstraintSystem<Field>,
        advice: [Column<Advice>; 3],
        instance: Column<Instance>,
        constant: Column<Fixed>,
    ) -> <Self as Chip<Field>>::Config {
        // specify columns used for proving copy constraints
        meta.enable_equality(instance);
        meta.enable_constant(constant);
        for column in &advice {
            meta.enable_equality(*column);
        }

        // extract columns with respect to selectors
        let s_add = meta.selector();
        let s_mul = meta.selector();
        let s_add_c = meta.selector();
        let s_mul_c = meta.selector();

        // define addition gate
        meta.create_gate("add", |meta| {
            let s_add = meta.query_selector(s_add);
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let rhs = meta.query_advice(advice[1], Rotation::cur());
            let out = meta.query_advice(advice[2], Rotation::cur());
            vec![s_add * (lhs + rhs - out)]
        });

        // define multiplication gate
        meta.create_gate("mul", |meta| {
            let s_mul = meta.query_selector(s_mul);
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let rhs = meta.query_advice(advice[1], Rotation::cur());
            let out = meta.query_advice(advice[2], Rotation::cur());
            vec![s_mul * (lhs * rhs - out)]
        });

        // define addition with constant gate
        meta.create_gate("add with constant", |meta| {
            let s_add_c = meta.query_selector(s_add_c);
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let fixed = meta.query_fixed(constant, Rotation::cur());
            let out = meta.query_advice(advice[2], Rotation::cur());
            vec![s_add_c * (lhs + fixed - out)]
        });

        // define multiplication with constant gate
        meta.create_gate("mul with constant", |meta| {
            let s_mul_c = meta.query_selector(s_mul_c);
            let lhs = meta.query_advice(advice[0], Rotation::cur());
            let fixed = meta.query_fixed(constant, Rotation::cur());
            let out = meta.query_advice(advice[2], Rotation::cur());
            vec![s_mul_c * (lhs * fixed - out)]
        });

        MyConfig {
            advice,
            instance,
            constant,
            s_add,
            s_mul,
            s_add_c,
            s_mul_c,
        }
    }
}

Put values to the table and define wire constraints.

impl<Field: FieldExt> Circuit<Field> for MyCircuit<Field> {
    type Config = MyConfig;
    type FloorPlanner = SimpleFloorPlanner;

    fn without_witnesses(&self) -> Self {
        Self::default()
    }

    fn configure(meta: &mut ConstraintSystem<Field>) -> Self::Config {
        let advice = [meta.advice_column(), meta.advice_column(), meta.advice_column()];
        let instance = meta.instance_column();
        let constant = meta.fixed_column();
        FChip::configure(meta, advice, instance, constant)
    }

    fn synthesize(
        &self, config: Self::Config, mut layouter: impl Layouter<Field>
    ) -> Result<(), Error> {
        // handling multiplication region
        let t1 = self.u * self.u;
        let t2 = self.u * self.v;
        let t3 = t2 * Value::known(Field::from(3));

        // define multiplication region
        let (
            (x_a1, x_b1, x_c1),
            (x_a2, x_b2, x_c2),
            (x_a3, x_c3)
        ) = layouter.assign_region(
            || "multiplication region",
            |mut region| {
                // first row
                config.s_mul.enable(&mut region, 0)?;
                let x_a1 = region.assign_advice(|| "x_a1",
                    config.advice[0].clone(), 0, || self.u)?;
                let x_b1 = region.assign_advice(|| "x_b1",
                    config.advice[1].clone(), 0, || self.u)?;
                let x_c1 = region.assign_advice(|| "x_c1",
                    config.advice[2].clone(), 0, || t1)?;

                // second row
                config.s_mul.enable(&mut region, 1)?;
                let x_a2 = region.assign_advice(|| "x_a2",
                    config.advice[0].clone(), 1, || self.u)?;
                let x_b2 = region.assign_advice(|| "x_b2",
                    config.advice[1].clone(), 1, || self.v)?;
                let x_c2 = region.assign_advice(|| "x_c2",
                    config.advice[2].clone(), 1, || t2)?;

                // third row
                config.s_mul_c.enable(&mut region, 2)?;
                let x_a3 = region.assign_advice(|| "x_a3",
                    config.advice[0].clone(), 2, || t2)?;
                region.assign_fixed(|| "constant 3",
                    config.constant.clone(), 2, || Value::known(Field::from(3)))?;
                let x_c3 = region.assign_advice(|| "x_c3",
                    config.advice[2].clone(), 2, || t3)?;

                Ok((
                    (x_a1.cell(), x_b1.cell(), x_c1.cell()),
                    (x_a2.cell(), x_b2.cell(), x_c2.cell()),
                    (x_a3.cell(), x_c3.cell())
                ))
            }
        )?;

        let t4 = t1 + t3;
        let t5 = t4 + self.v;
        let t6 = t5 + Value::known(Field::from(5));

        // define addition region
        let (
            (x_a4, x_b4, x_c4),
            (x_a5, x_b5, x_c5),
            (x_a6, x_c6)
        ) = layouter.assign_region(
            || "addition region",
            |mut region| {
                // first row
                config.s_add.enable(&mut region, 0)?;
                let x_a4 = region.assign_advice(|| "x_a4",
                    config.advice[0].clone(), 0, || t1)?;
                let x_b4 = region.assign_advice(|| "x_b4",
                    config.advice[1].clone(), 0, || t3)?;
                let x_c4 = region.assign_advice(|| "x_c4",
                    config.advice[2].clone(), 0, || t4)?;

                // second row
                config.s_add.enable(&mut region, 1)?;
                let x_a5 = region.assign_advice(|| "x_a5",
                    config.advice[0].clone(), 1, || t4)?;
                let x_b5 = region.assign_advice(|| "x_b5",
                    config.advice[1].clone(), 1, || self.v)?;
                let x_c5 = region.assign_advice(|| "x_c5",
                    config.advice[2].clone(), 1, || t5)?;

                // third row
                config.s_add_c.enable(&mut region, 2)?;
                let x_a6 = region.assign_advice(|| "x_a6",
                    config.advice[0].clone(), 2, || t5)?;
                region.assign_fixed(|| "constant 5",
                    config.constant.clone(), 2, || Value::known(Field::from(5)))?;
                let x_c6 = region.assign_advice(|| "x_c6",
                    config.advice[2].clone(), 2, || t6)?;
                Ok((
                    (x_a4.cell(), x_b4.cell(), x_c4.cell()),
                    (x_a5.cell(), x_b5.cell(), x_c5.cell()),
                    (x_a6.cell(), x_c6.cell())
                ))
            }
        )?;

        // t6 is result, assign instance
        layouter.constrain_instance(x_c6, config.instance, 0)?;

        // enforce copy constraints
        layouter.assign_region(|| "equality",
            |mut region| {
                region.constrain_equal(x_a1, x_a2)?; // namely, x_a1 = x_a2
                region.constrain_equal(x_a2, x_b1)?; // namely, x_a2 = x_b1

                region.constrain_equal(x_b2, x_b5)?; // namely, x_b2 = x_b5

                region.constrain_equal(x_a4, x_c1)?; // namely, x_a4 = x_c1

                region.constrain_equal(x_a3, x_c2)?; // namely, x_a3 = x_c2

                region.constrain_equal(x_b4, x_c3)?; // namely, x_b4 = x_c3

                region.constrain_equal(x_a5, x_c4)?; // namely, x_a5 = x_c4

                region.constrain_equal(x_a6, x_c5)?; // namely, x_a6 = x_c5
                Ok(())
            }
        )?;
        Ok(())
    }
}

PLONKish Arithemetization​

A Simple Arithmetic Circuit​

Transforming to PLONKish Arithmetization​

Specifying columns​

Transforming to Constraints and Meaning of Columns​

Specifying Table Values and Gate Constraints​

A Simple Halo 2 Program​