Lambda VM: what a constraint is

What does a zkVM actually prove? Not that it ran your program. That a record of the run follows a fixed list of rules. The record is written by the executor, step by step, as the program runs. The rules are the constraints, and this post is about them: what one is, why a polynomial equation can stand for a statement like "this is a bit" or "this is the sum of those two", and what the full list looks like in Lambda VM, in the spec and in the code.

To make that concrete we will walk through one chip, EQ, first in the spec and then in the code. There is nothing special about EQ. It is just small enough to show in full, and every other chip in the VM is built the same way, so whatever you learn to read in it you can read in the rest. At the end we take one line out of it to see what breaks.

The only thing a proof can check

By the time the prover gets involved, the executor has already run the program and logged every step, and that log has been laid out as tables, one per kind of operation, with a row for every operation of that kind and a column for every value involved in it. A row of the CPU table holds the program counter, the instruction, the register values it read and the value it wrote. A row of the multiplication table holds two operands and a product. Everything that happened is in some row of some table.

From this point on, the proof system can check exactly two kinds of statements about those tables. The first is an equation: a polynomial in the values of a row that has to evaluate to zero on every row of the table. The second is a lookup: a claim that a tuple of values taken from one table appears, as a row, in another table. That is the entire vocabulary, and it has no "if" and no "less than" in it. The STARK machinery exists to verify that polynomials vanish on a domain, and lookups are themselves reduced to equations under the hood.

From a claim to an equation

The reason an equation can express a rule is that you get to choose the polynomial, so you choose one whose zeros are the values you want to allow. The simplest example is the bit. The polynomial x·(1 − x) is zero when x = 0 and when x = 1, and for no other value of the field (a prime field has no zero divisors, so a product is zero only when a factor is). Demanding that x·(1 − x) = 0 on every row is therefore the same as demanding that the column x contains only bits. The claim "x is a bit" has become an equation.

A sum works the same way. The polynomial a + b − c is zero only when c equals a + b, so that equation pins down c as the sum of the other two columns. And once you have bits, you can build logic out of arithmetic: if a and b are bits, then a + b − 2ab is 1 when exactly one of them is 1 and 0 otherwise, which is a xor. The formula only means xor when a and b are already constrained to be bits, so those constraints have to be there as well. Constraints that depend on other constraints are the norm in a chip.

The field arithmetic is modulo a large prime, not modulo 2⁶⁴, so a 64-bit CPU addition is not a single equation. In Lambda VM a 64-bit value is held as two 32-bit limbs, and the addition c = a + b (mod 2⁶⁴) becomes a statement about limbs and carries: the low limbs satisfy a_lo + b_lo − c_lo = 2³²·carry₀, the high limbs satisfy a_hi + b_hi + carry₀ − c_hi = 2³²·carry₁, and each carry is a bit. Both carries can be written as expressions in the limbs (divide the left-hand side by 2³², which in a field is a multiplication by a constant), so the whole thing reduces to two bit constraints on those expressions, and that is how our ADD template is written. The limbs themselves have to be in range for any of this to mean what it says, which brings us to lookups.

The degree of the polynomial also shapes how constraints get written. The prover's cost grows with the highest degree in the system, so a degree-two constraint is cheaper than a degree-five one, and the spec keeps everything at degree three or below. That is less limiting than it sounds, because degree can always be traded for columns. A product of four values becomes a product of two if you add an auxiliary column that holds the product of the first pair, pinned down by its own degree-two equation, and the same trick works for any expression. It is also why a template that applies only under some condition requires that condition to be linear: the condition multiplies the constraint, and the product has to stay within the bound.

Why there are lookups

Equations have a blind spot. There is no cheap polynomial that says "this value is below 2¹⁶", because in a prime field an element is just an element and "smaller than" is not something the arithmetic knows about. You could write the product (x − 0)(x − 1)…(x − 65535), which is zero exactly on the valid values, but that is a polynomial of degree 65536, and we just said degree is what we pay for.

So ranges are checked the other way, with a lookup: a fixed table lists every valid value, and the chip claims that its value appears in it. In Lambda VM, lookups are also what links one table to another. How a lookup becomes something a proof can check, and how one argument ties every table together, is a post of its own. For this one it is enough to know that a lookup is a statement the proof can verify, and that a chip is allowed to rely on it.

An example: EQ in the spec

EQ is the chip behind BEQ and BNE. It takes two 64-bit values a and b and a bit called invert, and returns one bit, res = (a == b) xor invert. The CPU sends it the operands and the flag, gets the bit back, and uses it to decide whether to jump. It is our example for one reason only: it is the smallest chip that uses every tool above (equations, templates, range checks, a lookup for the result and the bus line to the CPU), so the whole of it fits on one page of the spec. What follows is how to read that page, and the same reading works for any other chip.

Every chip in the spec starts with its variables. EQ has seven: the inputs a, b and invert, the output res, two auxiliary values that exist only to make the constraints expressible, diff and eq, and a multiplicity μ that counts how many times the CPU asked for this particular row (two identical comparisons share a row). Each variable has a type, and the type says how it is laid out in columns: a and b are double words held as two 32-bit limbs, diff is a double word held as four 16-bit halves, and invert, res and eq are bits. That makes seven variables laid out over twelve columns.

Then come the assumptions: facts the chip relies on but does not check, because the chip that sent the inputs already did. EQ assumes that the limbs of a and b are valid 32-bit words. That is the CPU's job, and checking it again here would be a waste. Assumptions are written down explicitly because, when you audit a chip, you need to know which of its inputs are trusted and who is responsible for them.

Then the constraints, in the order the spec lists them:

1. Each of the four halves of diff is a valid half-word (four range lookups).
2. invert is a bit (the IS_BIT template, invert·(1 − invert) = 0).
3. diff = a − b modulo 2⁶⁴ (the SUB template, which is ADD with the roles rearranged: b + diff = a, two carries, both bits).
4. eq = 1 if and only if diff[0] + diff[1] + diff[2] + diff[3] = 0 (a lookup that answers "is this zero?" with a bit).
5. res = eq xor invert, written as res − (eq + invert − 2·eq·invert) = 0.
6. The row (a, b, operation and flag, res) is what the CPU asked for (the ALU bus interaction, with multiplicity μ).

The interesting one is how a == b gets decided, because there is no cheap equation for "these two are equal" either. What the chip does is compute the difference and ask whether it is zero, and "is zero" is itself delegated to a lookup on the sum of the four halves. The step that makes this valid is the range check in line 1: four values each below 2¹⁶ add up to something below 2¹⁸, far smaller than the field modulus, so their sum is zero in the field only when all four are zero, which is the same as diff being zero, which is the same as a and b being equal. Take the range check away and that chain of "the same as" breaks, and we will do that in a moment.

ADD, SUB and IS_BIT are not special constraint types. They are named bundles of ordinary equations that many chips need, defined once in the spec with their own correctness argument, and referenced by name everywhere else. The spec page for EQ renders each line of the list with a tag (EQ-C1, EQ-C2, …), the expression, and the polynomial it expands to when it is an equation. That tag is how a constraint gets named in a review or an issue.

The same example in the code

The chip lives in one Rust file, and the file has the same three parts as the spec page. First a block of column indices that mirrors the variable list, in the same order: a takes columns 0 and 1, b takes 2 and 3, invert is 4, res is 5, the four halves of diff are 6 to 9, eq is 10 and μ is 11. Then a function that declares the lookups, one call per interaction: the four half-word range checks on diff, the ZERO lookup on the sum of the halves, and the ALU interaction that receives the CPU's request. And then the equations, as a constraint set with one emit per constraint. Here is that last part, essentially as it is in the repository:

impl ConstraintSet<GoldilocksField, GoldilocksExtension> for EqConstraints {
    fn eval<B: ConstraintBuilder<GoldilocksField, GoldilocksExtension>>(&self, b: &mut B) {
        // diff = a - b, encoded as b + diff = a.
        emit_add_pair(
            b, 0, &[],
            &AddOperand::dword(cols::B_0),
            &AddOperand::from_dword_hl(cols::DIFF_0),
            &AddOperand::dword(cols::A_0),
        );
        // IS_BIT(invert)
        emit_is_bit(b, 2, cols::INVERT, None);
        // res = eq XOR invert = eq + invert - 2*eq*invert
        let res = b.main(0, cols::RES);
        let eq = b.main(0, cols::EQ);
        let invert = b.main(0, cols::INVERT);
        let two = b.const_base(2);
        b.emit_base(3, res - (eq.clone() + invert.clone() - two * eq * invert));
    }
}

The templates are functions with the spec's names. The SUB line of the spec is the call to the ADD template with the operands rearranged (b + diff = a), and because ADD produces two carries it takes two slots, 0 and 1. IS_BIT is the next call, slot 2. The xor is written out by hand in slot 3, and if you put it next to the spec's entry for the same constraint, they are the same thing written twice:

[[constraints.all]]
kind = "arith"
constraint = "$#`res` = #`eq` xor #`invert`$"
poly = ["-", ["+", "res", ["*", 2, "eq", "invert"]], "eq", "invert"]

The same polynomial, res + 2·eq·invert − eq − invert, once as a tree of operators the spec renders into math, once as Rust operators over symbolic column references. Reading the two files side by side is the whole method: each line of the spec's list has to show up either in the lookup function or in the constraint set, with the same columns in the same roles, and nothing in the code should be doing something the spec does not list.

One thing in the file is deliberately not part of this comparison. The same file also contains the code that fills the rows of the EQ table during execution, computing diff, eq and res from the actual operands. That code is the prover's business and the verifier never sees it; if it has a bug, an honest prover produces a trace that fails the constraints, which is annoying but safe. The constraints are the part that has to be right, because they are the only thing standing between a dishonest prover and a valid-looking proof.

What happens if one line is missing

Take line 1 out, the range check on the halves of diff, and leave everything else as it is. Nothing visibly breaks: honest traces still satisfy every other constraint, and every test that runs a real program still passes. What changed is what a dishonest prover can get away with.

Say it wants to claim that a and b are equal when they are not. It fills the four halves of diff with 1, p − 1, 0 and 0, where p is the field modulus. Nothing says those have to be below 2¹⁶ any more, and now:

• The zero lookup (line 4) sees 1 + (p − 1) + 0 + 0 = p = 0 and answers eq = 1.
• The subtraction (line 3) still has to hold. The low limb of diff is 1 + 2¹⁶·(p − 1) = 1 − 2¹⁶ in the field, so the prover picks a with b's low limb plus 1 minus 2¹⁶ and the same high limb. Both carries come out to 0, which is a bit.
• Lines 2 and 5 are untouched, res = 1, and line 6 hands that bit to the CPU, which takes the branch.

That is a valid proof of a program that branched on a = b with a = b − 65535. Every remaining constraint is satisfied. What broke is the chain from the spec section: the sum of the halves is still zero, but "the sum is zero" no longer implies "the halves are zero", because 1 and p − 1 are allowed to cancel. The range check was the line that made those halves behave like integers.

This is the most common kind of soundness bug there is: a 2024 survey of 141 real vulnerabilities in SNARK implementations found that almost every circuit bug was a missing constraint, with range checks singled out. A test that builds this exact trace and checks that the prover rejects it is cheap to write, and documents what the line is for better than any comment.

Why we write it down this way

A zkVM is, in the end, its list of constraints. The executor, the trace generation, the prover and all the engineering around them exist to produce and check that list efficiently, but what the proof actually certifies is "every row of every table satisfies these equations and these lookups", nothing more. When the list is right the proof means what it says, and when a line is missing no amount of engineering elsewhere brings the guarantee back.

That is why in Lambda VM the list comes first: each chip is one file with its variables, assumptions and constraints, the spec is rendered from it, and the code mirrors it chip by chip.