Presenting zekrom: A library of arithmetization-oriented constructions for zk-SNARK circuits. Part 2: Halo2

zekrom is an open-source library of arithmetization-oriented constructions for zkSNARK circuits. It was created as part of the MSc thesis work of Laurent Thoeny on the Kudelski Security Research team. The goal of zekrom is twofold: to analyze the performance of novel constructions for circuits using modern libraries such as arkworks-rs and Halo2 and to provide ready-to-use constructions for privacy-preserving applications. In this post we describe zekrom for Halo2, which provides the Griffin, Neptune and Rescue Prime, and Reinforced Concrete hashing constructions. Further, it includes the authenticated-encryption Ciminion primitive and the respective AE constructions of Neptune and Griffin using the recently proposed SAFE API.

Introduction

zk-SNARKs are a powerful binding block for creating privacy-preserving applications because they allow us to convince someone that a particular statement is true without revealing any information about it. Consequently, the main applications that can benefit from zk-SNARKS are those where there is a party, not generally trusted, that need to demonstrate some type of accountability about an action it has taken or to remain compliant to an enforced policy. Recent proposals involving zk-SNARKs prove the existence of vulnerabilities, properties of machine learning models and the adherence to an encryption policy by network equipment.

In this article, we present zekrom for the Halo2 proving system. At the time of writing this article it provides the following hashing constructions: Griffin, Neptune, Rescue Prime and Reinforced Concrete. Moreover, it also provides the respective authenticated-encryption constructions of Neptune and Griffin using the recently proposed SAFE API. Note that the SAFE API was introduced in the first part of this series of articles.

Typical applications based on zk-SNARKS require hashing and/or encryption primitives specifically designed for circuits. When designing a zk-app we can decide to write the circuit ourselves, using a low-level library such as gnark or arkworks. Further, we could use a DSL such as circom and Leo. On the other hand, we can rely on a library of gadgets such as zekrom and circomlib. We have created zekrom to fulfill this need. Further, our library also serves to study the complexity of implementing this new type of constructions, so called arithmetization-oriented primitives as well as their performance in an state-of-the-art library such as Halo2.

Halo2

In the past, we have implemented arithmetization-oriented schemes in ecosystems that provided the Groth16, PlonK and Marlin proving systems. In this blog post, we present zekrom for Halo2.

Halo2 provides many advantages against the aforementioned proving systems:

TurboPlonK custom gates

In TurboPlonK, the authors proposed a modification of the PlonK original constraint to support custom gates. In PlonK, gates consist of the multiplication and addition operation. Circuit constraints are encoded in the so-called vanilla PlonK constraint, defined as:

$q_L \cdot x_a + q_R \cdot x_b + q_0 \cdot x_c + q_M \cdot (x_a \cdot x_b) = 0$

In this case, the $q$ -type polynomials are related to the selectors (that is, they allow us to toggle and activate a certain operation in the constraint) whereas the $x$ -polynomials are related to the witnesses. Creating an addition gate means setting $q_L, q_R$ to 1, $q_0$ to -1 and $q_M$ to 0. This would allow us to check if the inputs $x_a, x_b$ are equal to $x_c$ : $x_a + x_b = x_c$ . On the other hand, a multiplication gate is implemented by setting $q_L, q_R$ to 0, $q_0$ to -1 and $q_M$ to 1.

Instead, TurboPlonK provides custom gates as lineal combinations of the original PlonK gate, which are verified together.

2. Support for look-up arguments

One of the limitations for using constructions such as SHA-256 in a zk-SNARK circuit was the utilization of bitwise operations, which are expensive to implement using the available field operations. However, we can rely on look-up tables for implementing this type of operations. First, we load values in a table related to the execution trace of our circuit. Then, we prove that a pair of values appear in the table as witnesses, according to the other columns in the table. This also serves to prove that a set of constants utilized in the circuit are correc. Similarly, we can implement the XOR operation in our circuit. Moreover, we can prove that we are using the correct round constants of a hashing construction for instance. Moreover, constructions such as Reinforced Concrete rely on the support of look-up tables for optimizing the performance scheme and defining constraints.

3. Proof recursion

Recursion in the field of zk-SNARKs means verfying a zk-SNARK proof inside another zk-SNARK: we prove that we know a zk-SNARK whose proof verification process result is correct. zk-SNARKs are succinct (proof material is short and in general, fast to be verified) and we can exploit this property via recursion: a recursive zk-SNARK contains more knowledge and its verification time is not expensive.

In order to support recursion, Halo2 uses two curves (collectively called the Pasta curves): Pallas and Vesta. Halo2 relies on proof systems instantiated in both curves but in different scalar fields, creating a 2-cycle. They instantiate the Halo2 proof system over the curve $E_p$ , defined over the field $F_p$ . This allows to prove statements using circuits in $F_q$ arithmetic, also called the scalar field. However, since, the verifier-related arithmetic is generally performed over $F_p$ , the Halo2 team built another curve with scalar field in $F_p$ and uses a circuit with $F_p$ arithmetic that verifies proofs of the first curve. To complete the cycle, the second curve has a base field over $F_q$ for generating proofs that can be verified in the circuit over $F_q$ of the first curve.

4. Trusted Setup

Zero-knowledge proof protocols generally require a trusted setup procedure, where the standard parameters of the protocol are generated. Generally, this involves some type of multi-party computation protocol where randomness is generated (also called toxic waste). If the randomness is not deleted accordingly and is captured by an attacker, it could create fake proofs that will be accepted as valid ones.

Halo2, through the use of the Inner Product Argument (IPA) polynomial commitment scheme (PCS) removes the need of a trusted setup. A polynomial commitment scheme is used to prove that a value of the polynomial in a particular point satisfies $f(x) = y$ via a proof and without revealing the complete polynomial, that is, we can open certain evaluation of the polynomials without revealing the whole polynomial. This is crucial in zk-SNARKs to prove the validity of a statement, translated into a circuit (given a set of public and private inputs) and encoded into a set of polynomials.

Despite the case that IPA produces larger proofs (particularly of logarithmic complexity vs. 1 group element in the KGZ PCS used by PlonK) this shortcoming is balanced in Halo2 by the ability of the proving system for aggregating many proof openings.

Defining circuits in Halo2

In the past, we have seen how to define circuits in DSLs such as Circom and in embedded DSLs such as gnark. Typically, we start with a description of the circuit in terms of public and private inputs and the type of operations (gates) we perform.

This process is different in Halo2. We need to work with the concept of execution trace, that is, all the steps that the circuit goes through, from the inputs to the generation of the output. The execution trace is represented as a matrix of $m$ columns and $n$ rows. Every element in a cell belongs to a finite field element. We can see columns of this table as the type of inputs we work with in our circuit. Halo2 defines different types of columns:

Instance columns: they are shared inputs by te prover and verifier, also called public inputs.
Advice columns: they contain private inputs (witnesses), chosen by the prover.
Fixed columns: the include values like constants and they can define the logic of the circuit.

For instance, we can define the columns related to the Griffin-based authenticated-encryption scheme as:

pub struct GriffinAECircuitVestaConfig {
    pub message_input: Column<Advice>,
    pub key_input: Column<Advice>,
    pub nonce: Column<Advice>,
    pub output: Column<Advice>,
    pub config: GriffinConfig<Fq>,
}

For every operation involved in our circuit, we create custom gates where different selectors are involved and with certain constraints in place. We have access to the different cells in the table via the Rotation type. For instance, we can create a a custom gate for the M layer of Griffin as:

   meta.create_gate("M layer of Griffin", |meta| {
            let s = meta.query_selector(m);
            let x = state.map(|v| meta.query_advice(v, Rotation::prev()));
            let y = state.map(|v| meta.query_advice(v, Rotation::cur()));
            let c = round_constants.map(|c| meta.query_fixed(c, Rotation::prev()));
            let sum = x[0].clone() + x[1].clone() + x[2].clone();
            vec![
                s.clone() * (y[0].clone() - (x[0].clone() + sum.clone() + c[0].clone())),
                s.clone() * (y[1].clone() - (x[1].clone() + sum.clone() + c[1].clone())),
                s * (y[2].clone() - (x[2].clone() + sum + c[2].clone())),
            ]
        });

Reinforced Concrete

Reinforced Concrete (RC) is a hash function for circuits and native architectures that exploits the advantages of look-ups provided by novel proving systems such as Halo2. It the relies on three components or layers: Bars (a non-linear layer that can be represented using look-up tables) and the Concrete and Bricks components for creating diffusion.

The RC permutation works with a state of 3 element ( $F_p^3$ ) for a prime $p$ .

The RC permutation applies the following operations to the state: Concrete $\circ$ Bricks $\circ$ Concrete $\circ$ Bricks $\circ$ Concrete $\circ$ Bricks $\circ$ Concrete $\circ$ Bars $\circ$ Concrete $\circ$ Bricks $\circ$ Concrete $\circ$ Bricks $\circ$ Concrete $\circ$ Bricks $\circ$ Concrete.

The different components of the RC permutation are:

Bricks: Bricks is defined as we saw in Griffin: Bricks $(x_1, x_2, x_3) = (x_1^d, x_2 \cdot (x_1^2 + \alpha_1 \cdot x_1 + \beta_1), x_3 \cdot (x_2^2 + \alpha_2 \cdot x_2 ) \cdot \beta_2))$ where $\alpha_1, \alpha_2, \beta_1, \beta_1 \in F_p$ and $\alpha_i^2 - 4\cdot \beta_i$ is not a quadratic residue $\mod p$ . In this case, $d = 5$ , where $gcd(p-1, d)=1$ as we have seen already in the past.
Concrete: It consists on the multiplication of the state by an MDS matrix of 3×3 dimensions, being the circular matrix $circ(2,1,1)$ , following the addition of a (pseudo-random) vector round constant $c \in F_p^3$ .
Bars: Defined as Bars $(x_1, x_2, x_3) =$ Bar( $x_1$ ), Bar( $x_2$ ), Bar( $x_3$ ). In the Bar function, each field element is decomposed and a substitution box is applied and the result is composed again. In this respect, RC provides tables and a set of look-up constraints so it its possible to prove that given $x, y \in F_p, y =$ Bar( $x$ ) if and only if the set of constraints is fulfilled.