Boolean Circuits in Libsnark
At Statebox we use category theory to model computation, where the objects of a category represent the possible states of a system and morphisms between states represent a computation taking some state to another. One natural way to express these kinds of morphisms is to use boolean circuits.
A boolean circuit is a function that transforms a bitstring of m bits into a bitstring of n bits. It is called a circuit because it can be imagined as a diagram of wires and gates, where a 1 is a wire carrying a charge and a 0 is a wire with no charge. The gates can be logical operators like OR or NAND.
Boolean circuit satisfiability is NP-complete, so any problem in NP can be expressed as a boolean circuit. Due to the PCP Theorem, any decision problem in NP has probabilistically checkable proofs that can be verified in a reasonable amount of time.
Connecting everything together, we ought to be able to construct a non-interactive zero-knowledge proof that a morphism exists between two states of a system.
Libsnark is a library for creating zkSNARKs, and it has an efficient method for constructing SNARKs from two-input boolean circuits. (Two-input boolean circuits consist of gates where each gate has exactly two inputs.) Let’s look at how we can use libsnark to create a zkSNARK for a tiny example circuit.
An Example Circuit
Suppose we want a boolean circuit that can test whether a three-bit number is divisible by three. The input to our circuit is a bitstring of length three while the output is a single bit. Out of eight total three-bit numbers there are only two that are divisible by three: 011 and 110. Our circuit must be able to test any three-bit number and return 1 only on 011 or 110.
Designing the Circuit
Both correct bitstrings have a middle bit of 1 and each has exactly two set bits. These statements completely characterize the two bitstrings we are trying to select.
If the middle bit must be 1, then there is only one set bit left for the outer bits. So one of the outer bits must be 1 and the other must be 0. We can use an XOR gate to test that the outer bits are opposites. Then all we need to do is test that the middle bit is 1. Here is a diagram of a two-input boolean circuit with two gates and five wires that accomplishes the task.
How a Boolean Circuit becomes a SNARK
Most SNARKs are based on a Quadratic Arithmetic Program which is constructed from an arithmetic circuit. The arithmetic circuit is first written as a rank-1 constraint system (R1CS), then a special polynomial is constructed from the R1CS that has roots corresponding to each gate of the arithmetic circuit. Then it is possible to check that each gate of the arithmetic circuit is satisfied by checking that the polynomial has the expected roots.
While it is possible to convert boolean circuits into arithmetic circuits and use a quadratic arithmetic program, it is not very efficient to do so. Instead, we can use what is called a Square Span Program.
Square Span Programs
A Square Span Program is another system for building a SNARK that is designed to be efficient for boolean circuits. Each boolean gate is written as a linear combination of the input and output bits. For example, if a and b are bits, then 2a + 2b + 4c - 5 will be either 1 or -1 if NAND(a,b) = c. Each type of boolean gate gets one of these linear combinations that equal -1 or 1 if the gate is satisfied. Then all that needs to be checked is that(2a + 2b + 4c — 5)² = 1. This is called a Unitary Square Constraint System (USCS). It is similar to a R1CS but is much more simple for boolean circuits and produces smaller SNARKs. Libsnark can express a boolean circuit as a USCS.
Writing Our Circuit in Libsnark
Writing our boolean circuit in libsnark is quite simple. For each gate, we specify its left and right input wires, its output wire, its gate type, and whether or not the gate is an output of the entire circuit.
Gate Types
A two-input boolean gate can be represented as a truth table for its inputs and output. Here is the truth table for NAND:
| a | b | c |
|---|---|---|
| 0 | 0 | 1 |
| 0 | 1 | 1 |
| 1 | 0 | 1 |
| 1 | 1 | 0 |The last column specifies exactly how NAND functions for each input. Since the last column is 1110, NAND is given an op code of 14. There are sixteen possible two-input boolean gates and libsnark recognizes each one.
Circuit Output Gates
The proof generated for a boolean circuit is a proof that each gate behaves according to its type and that the outwire of any circuit output gate is 0. This is the opposite of the usual intuition for circuits and will cause the circuit we designed earlier to fail verification in libsnark. We can easily fix this by changing the output gate of our circuit to its negation, so that AND becomes NAND.
Our corrected circuit:
Specifying our Circuit in Libsnark
Our circuit is specified in libsnark like this:
int main()
{
// Choose the field
typedef libff::Fr<default_tbcs_ppzksnark_pp> FieldT; // Initialize public parameters
default_tbcs_ppzksnark_pp::init_public_params(); // Initialize the circuit
tbcs_circuit div_by_3; // Set the circuit size
div_by_3.primary_input_size = 0; // number of PUBLIC inputs
div_by_3.auxiliary_input_size = 3; // number of PRIVATE inputs tbcs_gate g1;
tbcs_gate g2; g1.left_wire = 1;
g1.right_wire = 3;
g1.type = tbcs_gate_type(6); // XOR
g1.output = 4;
g1.is_circuit_output = false; g2.left_wire = 4;
g2.right_wire = 2;
g2.type = tbcs_gate_type(14); // NAND
g2.output = 5;
g2.is_circuit_output = true; div_by_3.add_gate(g1);
div_by_3.add_gate(g2);
Valid Circuits
For a circuit to be considered valid by libsnark, the output wire of each gate must be exactly one more than the number of previous wires already specified. Also, the left and right input wires must each be less than the output wire.
Libsnark provides a constant wire (wire 0), so the first input wire is wire 1.
Specifying an Assignment
An assignment to our circuit is a vector of bits, with one bit for each wire (including the internal wires). Here is a correct assignment showing 110 (six) is divisible by three:
vector<bool> assgn_six = {1,1,0,1,0};Note that the last wire needs to be 0 because we marked the last gate as a circuit output.
Create the Proving and Verifying Keys (Trusted Setup)
const tbcs_ppzksnark_keypair<default_tbcs_ppzksnark_pp> keypair =
tbcs_ppzksnark_generator<default_tbcs_ppzksnark_pp>(div_by_3);Make an Assignment to the Circuit
// public input is empty tbcs_primary_input pi = {};// private input
tbcs_auxiliary_input ai = assgn_six;
Generate a Proof
tbcs_ppzksnark_proof<default_tbcs_ppzksnark_pp> proof = tbcs_ppzksnark_prover<default_tbcs_ppzksnark_pp>(keypair.pk, pi, ai);Verify the Proof
bool verified = tbcs_ppzksnark_verifier_strong_IC<default_tbcs_ppzksnark_pp>
(keypair.vk, pi, proof);Thank you to Christian Lundkvist and Howard Wu for their helpful libsnark tutorials on which this code is based.
