Constructing ZK SNARK Circuits
Beyond Domain Specific Languages
The rise of domain-specific languages (DSL) and zkSNARK based virtual machines brings an unprecedented developer experience to an otherwise near-inaccessible branch of cryptography. However, the level of abstraction in these languages is very high and does not provide much insight into how the underlying technology works.
This article does not step through the fundamentals of zkSNARK’s or why they are possible, there are some great resources for this that will be linked at the bottom of the article. Instead, this assumes at least a fundamental understanding of the zkSNARK and walks through how to build a zk-circuit using the halo2 rust crate by the Zcash team.
Terminology
The terminology around zk-technology can seem esoteric, so before diving into circuit construction, we should define a few key terms first.
Field Element: a number within a finite field. Field element operations are performed modulo
p - 1wherepis roughly a ~252 bit integer.Public Input: an input known to the verifier and prover.
Private Input: an input known only to the prover.
Relation: specifies which combination of public and private inputs are valid.
Arithmetization: an arithmetic expression of a relation, usually in the form of polynomial constraints.
Circuit: the implementation of a relation.
Advice Value: an intermediate value used by the circuit.
Witness: collective of advice values and private inputs.
SNARK: a Succinct Non-Interactive Argument of Knowledge allows a prover to create a proof that they knew a witness value that was composed into a valid relation; the succinct property of the proof is that it is of length poly-logarithmic in the circuit size.
PLONK: Permutations over Lagrange-bases for Oecumenical Non-Interactive Arguments of Knowledge, a type of SNARK algorithm.
Halo2: a variant of PLONK using bulletproofs.
Also notice that terminology around zk-circuits is similar to hardware. Chips contain gates and regions, chips can be composed into higher order chips, which can be composed into gadgets, which can be composed into circuits.
Designing the Circuit
The circuit will be a simple calculator that supports addition, subtraction, and multiplication. Division is fairly complicated to manually implement, so it is beyond the scope of this article. The final product will take user input, parses it into an operator and two operand (i.e. a + b), computes the output, generates a proof of valid computation, and verifies the proof.
PLONKish Zk-Circuit
Each PLONKish zk-circuit requires a configuration including the following information.
A matrix of cells where cells are elements of a finite field.
Matrix columns:
Fixed columns are fixed by the circuit.
Advice columns correspond to witness values.
Instance columns for public inputs and anything else.
A subset of columns to participate in equality constraints.
A maximum constraint degree.
Chip Composition
The circuit architecture will consist of three operator chips: addition, subtraction, and multiplication, a top-level arithmetic chip that contains the three operator chips, and a calculator circuit that conditionally chooses which circuits and gates to use.
Operator Chip
The operator chip’s configuration layout is as follows.
We need three columns and two rows. The top row contains the two private inputs to the circuit (a and b) and a selector. The second row contains the output of the operation.
The selector determines whether or not to constrain the operation. If the selector is a zero value, we do not constrain any of the cells. However, if the selector is a non-zero value, we constrain the following.
c = operation(a, b)Arithmetic Chip
The arithmetic chip’s configuration layout is as follows.
Our top level chip will contain three operator chips for addition, subtraction, and multiplication. We will also need to define functions that load private values into the circuit and expose public values to the circuit.
Circuit Design
The circuit that contains the arithmetic chip will be the zk-calculator. This will take two operands, an operator, and decide which functions on the arithmetic chip to execute and constrain.
Constraints must evaluate to zero to be valid. The way we express this with pseudo-code is as follows.
Note that if a given selector is zero, the corresponding expression it is multiplied by is not constrained. If a selector is non-zero, though, the corresponding expression must evaluate to zero for the constraint to hold.
Building The Circuit
This section will walk through building the circuit in Rust. A basic understanding of the Rust programming language is assumed for the scope of this section.
Full example source code linked here.
Directory Structure, Dependencies, and Boilerplate
First, we create a rust crate using the cargo package manager.
cargo new zk-calculatorThe directory structure will be as follows.
We only need one dependency for this project, halo2_proofs.
Implementing the Addition Chip
This implementation will be more or less the same for the subtraction and multiplication operator chips. The differences will be documented as necessary.
Tip: Implement the subtraction and multiplication chips manually, rather than copy-pasting the addition chip and renaming. This will solidify what each function, type, and variable is doing.
Imports
The following contains all of the imports needed in this chip. Note that the local import of the Number type will be defined in the arithmetic_chip module. Each operator chip will reuse this type.
Trait Definition
We define one trait, AddInstructions, which defines a local Num type and an addition function. We include a Layouter argument for assigning regions. The FieldExt type is a commonly used trait for operating with field elements. We also assert that implementing AddInstructions requires implementing Chip.
On the other operator chips will use their own respective instruction traits.
Struct Definition
We define two structs, the AddConfig which holds the configuration state of the chip, and the AddChip itself. The configuration requires two advice columns and an addition selector. The chip itself requires the configuration and an unused value that will contain PhantomData, as this chip architecture in particular does not need the value.
On the other operator chips, the only difference is in the selector’s name.
Struct Implementations
The following are implementations of the AddChip struct and the traits Chip and AddInstructions as defined above.
Base AddChip Implementation
We implement a construct function to return an instance of the AddChip and a configure function to create and return the chip’s configuration.
In the configure function, we enable equality constraints on the advice columns and create the addition gate. The rotations (cur and next) define which rows in the column to query. To query the output value c we need to query column a on the next rotation. Revisit the operator chip’s design if this is unclear.
On the other operator chips the difference will be the selector name, gate name, the return value of the closure in create_gate, and the configuration returned. The following contains the different closure return values.
Chip Trait’s AddChip Implementation
We implement two types, Config and Loaded, as well as two functions to return each, config and loaded. The Loaded data is any data that needs to be loaded at the start of Circuit::synthesize, however we need no data to be loaded so we simply return ().
There are no functional differences between this and the other operator chips’ Chip implementations.
AddInstructions Trait’s AddChip Implementation
We implement the Num type and the add function. The Num is defined as the generic Number type we imported. The add function gets the configuration, enables the addition selector, copies the two advice columns for a and b, then assigns the sum of them to the region in column a row 1 (rows are index zero).
Note that the copy_advice function first copies the value then constrains the copied value to equal the original; this is why equality constraints must be enabled in the configuration.
On the other operator chips, the difference is the operator used to compute c.
Implementing the Arithmetic Chip
The arithmetic chip is the top-level chip composed of all three operator chips.
Imports
The following contains all of the imports needed in this chip.
Trait Definition
We define an ArithmeticInstructions trait where implementors must also implement the AddInstructions, SubInstructions, and MulInstructions traits. We also include functions to load private values into the circuit and expose values as public inputs to the circuit.
Struct Definitions
We define three structs, the Number imported into the operator chips, the ArithmeticConfig and the ArithmeticChip. Notice the configuration contains the two advice columns used in the operator chips, an instance column for public inputs, and the configurations of each operator chip.
Struct Implementations
The following are implementations of the ArithmeticChip struct and the traits Chip, ArithmeticInstructions, AddInstructions, SubInstructions, and MulInstructions as defined above.
Base ArithmeticChip Implementation
We implement a construct function to return an instance of the ArithmeticChip and a configure function to create and return the chip’s configuration.
In the configure function we configure each of the operator chips, enable equality constraints on the instance column, and return the configuration.
Chip Trait’s ArithmeticChip Implementation
Like the operator chips, we implement two types, Config and Loaded, as well as two functions to return each, config and loaded. The Loaded data is any data that needs to be loaded at the start of Circuit::synthesize, however we need no data to be loaded so we simply return ().
ArithmeticInstructions Trait’s ArithmeticChip Implementation
We implement the Num type and the functions load_private and expose_public. The Num is defined as the generic Number type we defined above.
The load_private function gets the chip configuration, then assigns an advice value to a region at column a row 0.
The expose_public function gets the chip configuration, then constrains a given number to be equal to a cell in the instance column at a given row.
AddInstructions Trait’s ArithmeticChip Implementation
The following implementation of the AddInstructions trait will be functionally comparable to that of SubInstructions and MulInstructions, so these will be omitted in this article for the sake of brevity, though implementing the other two traits is intuitive.
We implement the Num type to be the Number struct as defined above and the add function.
The add function gets the addition chip configuration, constructs the addition chip, then executes the addition instruction.
Declare Chip Modules
We declare each of the above modules as public in the chips directory.
Implementing the CalculatorCircuit
The calculator circuit contains the arithmetic chip and determines which of the arithmetic chip’s instructions to use based on a given operator.
Imports
The following contains all of the imports needed for the CalculatorCircuit. Note that the local import of Operator will be defined in the zk_calculator module.
Struct Definition
We define the calculator circuit to have two operands and one operator as follows. The Value type is comparable to the Option type, but with some guards to ensure propagation of unknown witness values.
Trait Implementation
We implement only the Circuit trait for the CalculatorCircuit. This includes type definitions for Config and FloorPlanner, and functions without_witnesses, configure, and synthesize. We reuse ArithmeticConfig for the circuit configuration and we use the SimpleFloorPlanner for simplicity.
The without_witnesses function just returns default values for the operators and whatever operator is contains.
The configure function uses the ArithmeticChip configure function using two advice columns and an instance column.
The synthesize function constructs the arithmetic chip, loads the operands as private values, computes the output with the appropriate function based on the operator, and exposes the output as a public value.
Tests
Next we implement tests for each chip in the circuit because we’re not bad developers that don’t write tests. Right? Right.
We declare a tests submodule in the calculator_circuit module. For the sake of brevity, the test_sub and test_mul functions are omitted.
Building the Zk-Calculator
The full zk-calculator takes user input from the terminal, parses it in to operands and an operator, proves and verifies the respective circuit, and prints the output.
Errors
We define ParserError and CircuitError to bubble up any errors into the ZkCalculator::run function.
Zk-Calculator
We define Operator and Operand types, a trait to parse string slices into Operators and Operands, an Operation, and the ZkCalculator.
Imports
The following contains all of the imports needed for the ZkCalculator.
Trait Definition
We define FromToken which contains a from_token function that parses a string slice into the respective type.
Operator and Operand Implementations
We define an Operator enum containing the valid instructions and an Operand type aliased to u64. We also implement the FromToken trait for each.
Struct Definitions
We define Operation and ZkCalculator.
Struct Implementation
We implement the runtime of the program in the ZkCircuit struct.
The run function takes user input, parses it into an operation, runs the circuit, proves and verifies, then prints the output if nothing fails.
Running the Program
Finally, we declare modules, import the ZkCalculator, and run it in the program’s entry point.
We test the program and run it by running the following.
cargo test && cargo runConclusion
If you made it this far, great! I hope this was helpful in both explaining how zk-circuits work and illustrating just how much code is abstracted away by domain specific languages.
The following is a list of helpful resources that have helped me immensely so far.
Elliptic Curve Basics by Nick Sullivan
Elliptic Curve Pairings by Vitalik Buterin
zkSnarks in a nutshell by Christian Reitwiessner
Why zkSnarks work by Vitalik Buterin
Quadratic Arithmetic Programs by Vitalik Buterin
Halo2 Book by Zcash
DarkFi Documentation by DarkFi
DarkFi zkVM built using Halo2 by DarkFi
PLONK by Ariel Gabizon, Zachary J. Williamson, and Oana Ciobotaru
That’s all for this one. If you enjoyed this, consider subscribing below, and until next time, good hacking! 🤘