Turning a computation into a circuit you can prove

Why a proof needs equations, not code

In the previous guide you met the three promises of a zero-knowledge proof — completeness, soundness, and zero-knowledge — and saw how the Fiat-Shamir trick turns an interactive proof into a single non-interactive one. But there is a gap between that beautiful theory and a real program. A proof system cannot 'run your Python.' Underneath, all of its machinery — polynomials, commitments, random challenges — speaks exactly one language: arithmetic over a finite field, the operations `+` and `×` on numbers taken modulo a large prime.

So the very first job of every ZK system is translation: take the statement 'I executed this computation correctly' and rewrite it as 'this set of algebraic equations is all satisfied.' That translation is called arithmetization, and it is the unglamorous, load-bearing step that everything else stands on. If the equations don't faithfully capture the computation, no amount of cryptography downstream can save you.

This guide walks the first three stops of the pipeline that nearly every proof takes: program → arithmetic circuit → Rank-1 Constraint System (R1CS) → (polynomial form). We will stop just before the cryptographic magic — the polynomial commitments and trusted setup that turn the equations into a tiny proof — because that is the whole of the next guide. By the end you will be able to look at a few lines of code and see the equations hiding inside them.

Arithmetic circuits: just plus and times over a field

An arithmetic circuit is a directed graph of gates where every gate is either an addition or a multiplication, and the wires carry numbers. That is it — no `if`, no loops, no strings, no comparisons. A ZK circuit is exactly this kind of object: you wire up `+` and `×` gates so that the output wire equals the value you want to prove something about. Any computation a computer can do can, in principle, be unrolled into such a graph.

The numbers are not ordinary integers — they are elements of a finite field: every value lives in `0, 1, …, p−1` for some large prime `p`, and all arithmetic is done modulo `p`. For SNARK-friendly curves, `p` is around 254 bits. Working in a field is what makes the later polynomial math work: subtraction and even division are well-defined (every non-zero element has a multiplicative inverse), values never overflow, and there are no floating-point rounding surprises. The price is that the field knows nothing about `<`, integer division, or bit operations — we will have to rebuild those by hand later.

Here is the key simplification that makes the whole scheme tractable: in this world, additions are nearly free, but each multiplication is what really 'costs.' As you will see, additions and multiplications-by-a-constant melt into the linear bookkeeping of the next step, while every multiplication of two unknown wires earns its own equation. So when an engineer says a circuit has 'four million constraints,' they roughly mean it has four million non-trivial multiplications.

Flattening a program into single gates

Take a concrete claim: *'I know a secret `x` such that `x³ + x + 5 = 35`.'* (The answer is `x = 3`, but the verifier should never learn that.) You cannot hand a multi-operation expression like `x*x*x + x + 5` to a circuit directly — a gate does exactly one operation. So you flatten it: rewrite the computation so that every line performs a single `+` or `×` and introduces exactly one new intermediate wire. This is the same idea as a compiler's three-address / SSA form.

# Statement: "I know x such that x^3 + x + 5 == 35"
#
# Original expression (too complex for a single gate):
#     out = x*x*x + x + 5
#
# Flattened — every line is ONE multiply or ONE add,
# and each introduces exactly one new wire:

    sym1 = x   * x        # gate 1 (multiply)   -> x^2
    y    = sym1 * x       # gate 2 (multiply)   -> x^3
    sym2 = y   + x        # gate 3 (add)
    out  = sym2 + 5       # gate 4 (add a constant)

# Public  (the verifier sees this):  out = 35
# Private (the prover's secret):     x   = 3
# Intermediate wires the prover must also fill in: sym1, y, sym2

Now the computation is a flat list of four gates over five working wires (`x`, `sym1`, `y`, `sym2`, `out`). Notice that the secret `x` is just one wire; the others are derived values the prover computes on the way to the answer. The complete set of values the prover assigns to all of these wires — public, private, and intermediate — is what we will call the witness, and it is the heart of the next two sections.

R1CS: one equation per multiplication

A Rank-1 Constraint System (R1CS) expresses the whole flattened program as a list of constraints, each of the rigid shape (A · s) × (B · s) = (C · s). Here `s` is the witness vector — every working wire stacked into one list, with a leading constant `1` so we can express additions and constants. Each constraint comes with three rows `A`, `B`, `C` that pick out a linear combination of the witness. It is called *rank-1* because each of the two factors on the left is a single linear combination — the only nonlinearity allowed is that one multiplication in the middle.

Let us order the witness as `s = [ 1, x, out, sym1, y, sym2 ]`. Each of our four gates becomes exactly one constraint. Watch how the two additions (gates 3 and 4) fold into the linear `A` row and need no multiplication of their own — that is the 'additions are free' claim made concrete.

Witness order:  s = [  1,   x,  out, sym1,   y, sym2 ]
For x = 3:      s = [  1,   3,   35,    9,  27,   30 ]

Gate 1:   x * x = sym1
  A1 = [0, 1, 0, 0, 0, 0]    A1·s = 3
  B1 = [0, 1, 0, 0, 0, 0]    B1·s = 3
  C1 = [0, 0, 0, 1, 0, 0]    C1·s = 9     check:  3 * 3 = 9    OK

Gate 2:   sym1 * x = y
  A2 = [0, 0, 0, 1, 0, 0]    A2·s = 9
  B2 = [0, 1, 0, 0, 0, 0]    B2·s = 3
  C2 = [0, 0, 0, 0, 1, 0]    C2·s = 27    check:  9 * 3 = 27   OK

Gate 3:   (x + y) * 1 = sym2        <-- an ADD: both addends go in A, B = 1
  A3 = [0, 1, 0, 0, 1, 0]    A3·s = 30
  B3 = [1, 0, 0, 0, 0, 0]    B3·s = 1
  C3 = [0, 0, 0, 0, 0, 1]    C3·s = 30    check:  30 * 1 = 30  OK

Gate 4:   (5 + sym2) * 1 = out        <-- constant 5 rides on the leading 1
  A4 = [5, 0, 0, 0, 0, 1]    A4·s = 35
  B4 = [1, 0, 0, 0, 0, 0]    B4·s = 1
  C4 = [0, 0, 1, 0, 0, 0]    C4·s = 35    check:  35 * 1 = 35  OK

Checking the whole proof statement is now mechanical: a witness is valid if and only if every constraint holds. There is no execution, no interpreter — just a few dot products and multiplications.

def r1cs_satisfied(A, B, C, s):
    for i in range(num_constraints):
        left  = dot(A[i], s)
        right = dot(B[i], s)
        out   = dot(C[i], s)
        if (left * right) % p != out % p:
            return False        # gate i is violated -> witness is invalid
    return True                 # every gate holds  -> s is a valid witness

The witness: public, private, and everything in between

The witness `s` is the full assignment of values to every wire, and it is naturally partitioned into three parts: the constant `1`; the public inputs and outputs (here `out = 35`) that the verifier is allowed to see; and the private part — the secret input `x` plus every intermediate wire (`sym1`, `y`, `sym2`). The prover knows all of `s`. The verifier knows only the public slice and the proof. This split is the whole point: zero-knowledge, layered on top in the next guide, lets the prover convince the verifier that some valid `s` exists matching the public values, without revealing the private part. The R1CS is the skeleton; zero-knowledge is the curtain drawn over it.

Now the tiny example the scope promised. Suppose the public number is `n = 15` and you want to prove *'I know two factors of n'* without revealing them. Flattened, that is a single multiplication, so the R1CS has exactly one constraint: `a × b = n`. In the circuit DSL Circom — which compiles directly to R1CS — it looks like this:

pragma circom 2.1.0;

// Prove: "I know two factors of the public number n."
template Factoring() {
    signal input  a;     // private witness
    signal input  b;     // private witness
    signal output n;     // public output

    // '<==' both ASSIGNS n = a*b AND emits the R1CS
    // constraint  a * b = n  (one rank-1 multiplication).
    n <== a * b;
}

component main = Factoring();

// Public value the verifier checks:  n = 15
// Private witness the prover supplies: a = 3, b = 5
// The proof reveals that SOME a, b multiply to 15 -- not which ones.

From R1CS to a single polynomial check

Checking `m` separate constraints one by one is fine for us, but clumsy for a proof system — we want the verifier to confirm the whole execution in roughly constant work, no matter how big the circuit is. The bridge is to bundle all the constraints into polynomials. Pick `m` distinct evaluation points `r₁, …, r_m` in the field, one per constraint. For each witness slot `j`, the column of the `A` matrix across all constraints defines a polynomial `Aⱼ(x)` by interpolation, so that `Aⱼ(rᵢ)` equals the entry `A[i][j]`. Do the same for `B` and `C`. This packaging is the Quadratic Arithmetic Program (QAP).

Now combine with the witness: define `A(x) = Σⱼ sⱼ · Aⱼ(x)`, and likewise `B(x)` and `C(x)`. Here is the payoff. At each point `rᵢ`, evaluating these gives back exactly `(Aᵢ·s)`, `(Bᵢ·s)`, `(Cᵢ·s)` — so 'all `m` constraints hold' is the same as saying the polynomial `P(x) = A(x)·B(x) − C(x)` is zero at every `rᵢ`. A polynomial that vanishes at `r₁, …, r_m` is exactly one that is divisible by the target polynomial `Z(x) = (x − r₁)(x − r₂)…(x − r_m)`.

So the entire execution collapses to one clean algebraic statement: *there exists a quotient polynomial `H(x)` such that `A(x)·B(x) − C(x) = H(x)·Z(x)`.* The prover knows the witness, builds `A, B, C, H`, and must convince the verifier this single divisibility holds. That is the door into zk-SNARKs: the prover commits to these polynomials and proves the identity at one random point (chosen via Fiat-Shamir), because two different polynomials of bounded degree can agree at only a tiny fraction of points — so one lucky-looking equality at a random spot is overwhelming evidence the identity is true everywhere. The commitment scheme and the trusted setup that make this succinct and hiding are precisely the next guide.

Where circuits go wrong: cost, non-native ops, and missing constraints

Arithmetization is powerful but unforgiving, and three honest limits shape the whole field. The first is cost: every constraint is real work for the prover in time and memory, and the count explodes for real programs. Proving correct execution of the EVM inside a zkEVM runs to millions of constraints per block, which is why proving is the heavy, specialized, often GPU-bound part of the stack. Reducing constraint count is the central engineering sport of ZK.

The second is non-native operations. Field arithmetic has no `<`, no integer division, no bitwise AND. To compare two numbers you must first bit-decompose them: introduce a wire per bit, constrain each bit to be boolean, constrain that the bits recompose to the value, and then compare bit by bit — a single 256-bit comparison can cost hundreds of constraints. Division `c = a / b` is done not by dividing but by having the prover witness the answer `c` and adding the constraint `c × b = a`. The circuit checks a guess rather than computing it; the prover does the hard work off-circuit and only proves consistency.

The third — and most dangerous — is the under-constrained circuit. Because the prover supplies the witness, any value you fail to pin down is a value an attacker is free to choose. The canonical example is a boolean: you intend a wire `b` to be a 0/1 selector, but if you forget to constrain it, a malicious prover can set `b = 7` and satisfy downstream 'if' logic that assumed `b ∈ {0,1}`.

// b is meant to be a 0/1 selector used elsewhere as: out = b*high + (1-b)*low
signal input b;

// BUG (under-constrained): nothing forces b into {0, 1}.
// A malicious prover can set b = 7 and forge 'out' to an
// arbitrary value -- the proof STILL VERIFIES. No error, no crash.

// FIX: one quadratic constraint pins b to a single bit.
b * (b - 1) === 0;   // (b)(b-1) = 0  holds ONLY when b == 0 or b == 1

What makes this bug class so insidious is that it is silent: a missing constraint never throws an error and never reverts. The forged proof simply verifies, and the false statement is accepted as true — a direct break of soundness, the property that should make lying impossible. Under-constrained circuits are consistently the dominant finding in ZK audits. This is why ZK code gets specialized review, why DSLs and tooling (Circom compiling to R1CS, Halo2, Noir, Cairo) and automated under-constraint detectors exist, and why writing circuits is its own discipline rather than ordinary programming.