zkc — a ZK compiler that refuses to build under-constrained circuits

There is a class of bug in zero-knowledge circuits that testing cannot find. Not because you tested too little, but because the bug lies in a direction nobody looks.

A ZK circuit is a system of constraints. The prover supplies an assignment to every variable — the witness — and the proof says: "I know a witness that satisfies every constraint." When you test the circuit, you feed it inputs, let the honest solver compute the witness, and check the result. The result is correct. All tests green.

The question you did not ask is: is there a second witness? One that satisfies every constraint on the same inputs — and claims a different output. If there is, the circuit is under-constrained, and the prover gets to choose which of the two results it proves. Both proofs verify. That is not a bug any test will show you; it is a bug only the attacker notices.

I spent about eighteen months building a compiler whose only real thesis is that this belongs in the type system. A circuit whose outputs are not uniquely determined by its inputs is a compile error.

The project is zkc — frontend in Haskell, backend in Rust, and the proving path rebuilt from the ground up: own field, own FFT, own commitment, own FRI, own STARK.

This post is less about what I built than about what building it turned up. The most interesting thing about the project is three findings, and two of them contradict something I believed myself.

#Part 1: The idea

#The bug, concretely

The standard example is is_zero: out should be 1 when x == 0, and 0 otherwise. The usual trick uses the inverse:

gadget is_zero(x: field) -> (out: field) {
    advice inv = inv_or_zero(x);
 
    assert x * inv == 1 - out;
    assert x * out == 0;
}

The constraint system cannot compute inv — division is not something a constraint expresses. The prover guesses it, and the assertions are supposed to pin it down. In zkc that is advice, and advice is legal only inside a gadget definition. That is deliberate: it is the point where the author says "I know this is subtle, and I claim the assertions below pin the result down anyway."

Drop the second assertion from Listing 1 and here is what happens. The prover sets inv = 0 and claims x = 5, out = 1. The remaining assertion reads 5 * 0 == 1 - 1, or 0 == 0. Satisfied. The proof verifies. The claim "5 is zero" has been proved.

That forgery — the phase-0 forgery, in the project's vocabulary — has been the regression test since the first month. Every layer added since (SMT, the second arithmetization, the STARK, the recursion work) is tested to reject it.

#Determinacy as a typing question

"Is the output unique?" is a question about self-composition:

Do two assignments exist that satisfy every constraint, agree on all inputs, and differ on an output?

So you put two copies of the circuit side by side, glue the inputs together, and ask for a point where they come apart. If there is none, the output is a function of the inputs — determined. If there is one, it is precisely the forgery.

zkc settles this for most circuits with a decidable core over polynomial ideals, including case splits on whether an atom is zero. What the core cannot settle is escalated to an SMT solver — which can refute as well as prove. That is what makes the diagnostic useful.

Here is what a proof looks like:

$ zkc build examples/iszero.zkc -o build/iszero.ir.json --explain
compiled 'IsZero' over bn254: 2 inputs, 6 nodes, 2 assertions
  determinacy: 1 output(s) proved determined (out), 2 case(s)
    case x == 0
    case x != 0

The compiler found that case split itself: when x == 0 the first assertion forces out = 1; when x != 0, x is invertible and the second forces out = 0. Gadgets are proved once, and every instantiation inherits the result.

And here is the opposite. Ask for a square root:

gadget root(x: field) -> (out: field) {
    assert out * out == x;
}

$ zkc build root.zkc -o /dev/null --smt-solver z3 --smt-dialect int
error: 'root' is under-constrained — the solver constructed a forgery
  --> root.zkc:1
     |
   1 | gadget root(x: field) -> (out: field) {
     |
     = two witnesses satisfy every constraint and agree on all inputs:
     =     x = 4
     = but disagree on:
     =     out = 2   vs   out = -2
     = the prover picks whichever it prefers, and proves it
help: add a constraint that rules out one of these two witnesses

That output is where I became convinced the idea works. The diagnostic does not say "this looks risky." It puts the forgery on the table, with values. You cannot argue with a counterexample.

The third possibility matters as much as the other two. When the analysis cannot decide, it says so, and says it unmistakably:

error: could not decide whether 'root' is determined
     = this is not a claim that the circuit is wrong: the analysis ran out of
     = room before it could decide either way

The analysis is sound, not complete. Stalling never quietly becomes approval. That sounds like table stakes, but it is exactly where tools of this kind usually fail: a checker that waves things through when unsure is worse than no checker, because it manufactures confidence it cannot back.

#Two invariants holding it together

Two things I kept from the start, and both are demonstrated rather than asserted:

The Core IR is arithmetization-agnostic. It is a typed constraint graph, not an R1CS in disguise. The proof is that the same IR is lowered two independent ways — to R1CS and to Plonkish — with identical results. And because I measured both, I also know neither dominates: they tie on multiplication-shaped circuits, and R1CS wins decisively on a wide linear sum. That is what justifies a neutral IR — if there were a winner, the intermediate format would be dead weight.

Everything is generic over the field. The proof: the same lowerings run over a hand-written Goldilocks field with identical constraint counts to BN254. When phase 5 came, I could slide a new field and an entire prover underneath the compiler without changing a line of it.

#Part 2: Three things the project found out

A compiler is only as interesting as what it turns up. Here are the three findings I did not have going in — each with the test that is still in the suite.

#1. Determinate and forgeable anyway

This is the finding that stung, because it constrains the project's own thesis.

While building a FRI verifier in the language itself, I needed the query index: the position in the codeword that gets opened. Fiat–Shamir gives you a challenge, and the index is that challenge modulo the domain size. In a circuit you write that the natural way:

gadget derive_index(challenge: field, b0: field, b1: field, high: field)
    -> (idx: field)
{
    assert b0 * (1 - b0) == 0;
    assert b1 * (1 - b1) == 0;
    let index = b0 + 2 * b1;
    assert challenge == index + 4 * high;
    assert idx == index;
}

Read it closely: index is two bits, and challenge == index + 4*high says that index is the remainder of challenge on division by 4. It looks entirely right.

The compiler proves it determinate. And that is correct — idx really is a function of the inputs.

And every index in {0,1,2,3} satisfies the circuit. high is unconstrained, so the prover sets high = (challenge - index)/4 and reaches any position it likes. The test says it without ceremony:

for index in 0u64..4 {
    let high = challenge.sub(g(index)).mul(inv4); // always solvable — the hole
    /* ... */
    if ir.is_satisfied::<F>(&wires) {
        satisfying.push(index);
    }
}
 
assert_eq!(
    satisfying,
    vec![0, 1, 2, 3],
    "every index satisfies the naive binding — it is determinate but unsound"
);

Stated cleanly, the lesson is: determinacy rules out under-constrained outputs. It does not certify that an output is a canonical reduction. Because that is a range property — "index lies in [0,4) and high is the quotient" — and a system of equations does not see range properties.

What is worth noticing is what the fix was not. I did not strengthen the analysis. The failure was not in the prover but in what the language could express: there was no way to introduce a bit decomposition, hence no way to write the range property down at all. The fix was a new primitive (bits), after which the perfectly ordinary analysis proves the perfectly ordinary thing.

And with the primitive in hand, the right construction is not the one I had planned. Instead of constraining high after the fact, you stop relating the index to the challenge and read it off:

gadget canonical_low2(v: field) -> (i0: field, i1: field) {
    advice (b0, b1, /* ... */, b63) = bits(v);
    // The desugaring emits the reconstruction
    //     v == b0 + 2*b1 + 4*b2 + ... + 2^63*b63
    // which leaves the prover no freedom at all: the bits ARE the
    // representative.
 
    /* ... canonicity, see below ... */
 
    assert i0 == b0;
    assert i1 == b1;
}

The range bound on the upper bits now comes for free — they are a bit decomposition. And determinacy falls out with no case split and no SMT: the closeBits rule marks the bits as determined once their source is. That is a marking, not a search, which is why it scales, and why a 64-bit decomposition is practical at all.

#2. Goldilocks wraps below 2⁶⁴, and rare is not sound

The second finding came from thinking the first one through, and it is why the gadget is a hundred lines rather than three.

Goldilocks is $p = 2^{64} - 2^{32} + 1$. That is less than 2⁶⁴. So a 64-bit string is not a unique representative: whenever the canonical value c is below 2⁶⁴ − p = 2³² − 1, the string for c + p also fits in 64 bits — and satisfies the same reconstruction.

Its low bits are different ones. Since p ≡ 1 (mod 2^k) for every k ≤ 32, the forged index is off by exactly one. So the prover can shift the query position by a step — for roughly one challenge in 2³².

One in four billion. That is the kind of probability that tempts you to move on. But rare is not sound: a prover that can grind is precisely the prover this thing exists to stop.

The non-canonical strings are exactly those in [p, 2⁶⁴), and because of the shape of p that interval has a clean description: the top 32 bits are all set AND the low 32 bits are not all zero. One constraint suffices:

    // ones30 == 1 exactly when every one of the top 32 bits is set.
    let ones0 = b32 * b33;
    let ones1 = ones0 * b34;
    /* ... */
    let ones30 = ones29 * b63;
 
    // Canonicity: a string with all top bits set may only be p − 1's, whose
    // low half is zero.
    assert ones30 * lo == 0;

It refuses every non-canonical string and no canonical one — including p − 1 = 2⁶⁴ − 2³², whose top bits are all set and whose low half is zero. The all-ones test is a product of 31 multiplications: no advice, no case split, everything stays inside the decidable core.

The test does more than show the circuit rejects the forgery. It shows that this one constraint is what rejects it. On the sharpest case — c = 2³² − 2, whose alternative is the all-ones string 2⁶⁴ − 1 — every bit is a bit, the reconstruction holds, the claimed index matches the supplied bits, and exactly one obligation refuses:

let unmet = attempt(&ir, c, wrapped, wrapped % DOMAIN);
assert_eq!(unmet.len(), 1);
match &unmet[0] {
    Unmet::Assertion { label, .. } => assert_eq!(label, "(ones30 * lo) == 0"),
    other => panic!("expected the canonicity assertion, got {other:?}"),
}

Remove that assertion and the circuit accepts two indices. That is the difference between a load-bearing constraint and a decorative one — and it is checkable.

Worth noting: the proof here is by exhaustion, not by sampling. The prover's entire freedom is the choice of bit string, and at most two are congruent to any challenge (c and c + p; c + 2p never fits in 64 bits). The test walks all of them against every candidate index.

#3. A spot check is not a proof

The third finding is about the STARK itself, and it is the one I had wrong in my head the longest.

A STARK commits the trace columns and the grand-product column Z, forms the composite constraint, divides by the vanishing polynomial, and uses FRI to prove the quotient is low-degree. The verifier then opens at the query positions and checks the identity composite = Q · Z_H there.

That is a spot check. Nothing in the protocol asks the trace and Z to be polynomials at all, and nothing looks at them at any position a query does not land on. The query positions follow publicly from the commitment — so a prover can simply retry until they miss whatever it wants hidden.

The standard answer is DEEP, and it moves where the check happens. An out-of-domain point ζ is drawn after every commitment. The prover sends each column's value there, and the identity is checked once, at ζ — one equation, off the domain, at a point the prover could not have known while committing.

On its own that binds nothing: six invented values satisfying one equation is cheap. What binds it is the batch. For each committed column,

is a polynomial iff P is one and takes the claimed value at ζ. A non-polynomial column has no low-degree quotient; a lied-about evaluation leaves a pole. These quotients are combined with random challenges, and FRI tests the combination. One low-degree test now carries the trace, Z and the quotient alike.

One detail that reads like housekeeping and is not: each quotient enters the batch scaled by λ + λ'·x^e rather than a plain λ. Without that degree correction the batch is bounded by the largest degree in it — and a trace column of a third that degree would pass a test it should fail.

The test for this is, in hindsight, the best one in the project, because it builds the prover you want to refuse — and that prover is no clumsy liar:

/// A prover that commits a column which is NOT the low-degree extension of the
/// trace: the committed value at `position` is shifted by `delta`, while the
/// quotient is built from the honest one.
pub fn prove_with_corrupted_column<F, H>(
    air: &Air<F>, trace: &Trace<F>, config: &FriConfig,
    position: usize, delta: F,
) -> StarkProof<F>

Everything about that proof stays self-consistent. The quotient really is low-degree, because it comes from the uncorrupted polynomial. The identity holds at every position but one. Every Merkle opening checks out, because the corrupted value is the committed value.

The test then searches for a position no query opens — which a prover can grind for — confirms that none does, and watches the proof fail anyway. The assertion is on the reason:

let reason = outcome.unwrap_err();
assert_eq!(reason, "final FRI codeword is not constant (input was not low-degree)");

The verifier gets past the check at ζ — which passes, since the quotient is honest — and dies in the low-degree test. What refuses the proof is not an inspection of the corrupted value but the fact that it now sits inside FRI. A second test walks every position in the domain. A spot check has positions it does not look at, by construction; this one has none.

And the cost? Seven field elements. 56 bytes. One commitment plus six out-of-domain values. The per-query openings do not grow at all, because the trace and Z were already being opened there. I spell that out because "we hardened it and the proof doubled" is what people expect. The last open soundness boundary closed for a constant, not a factor.

#What I took away

The interesting work was thinking things through, not building them. The index finding was an afternoon of implementation and three days of working out what it actually meant. The wraparound would never have surfaced if I had not had to write down why the bit decomposition is unique — and noticed, while writing, that it isn't.

Mark boundaries instead of burying them. Phase 5 shipped with an explicitly documented gap: FRI proved the quotient low-degree, not the columns. It said so in the status document, with an argument for why it did not affect the other results. A year later that document was the instruction sheet for closing it. A marked boundary is work waiting for you; a buried one is a bug with a delay fuse.

A testing failure I am leaving in, because it teaches something. While cleaning up, I replaced hand-pasted IR literals in the backend tests with real compiler output — and six tests fell over. The reason: those tests did string surgery on valid IR ("schema_version": 2 → 99) and asserted the loader rejected it. The patterns were written against the pretty-printed literal; the emitter writes compact JSON ("schema_version":2). Against real output, not one of those replacements matched. The tests would have loaded valid, unmodified IR and asserted that it was rejected. A replace that matches nothing is silently a no-op — that class of test can stay green for years while checking nothing. Every such site now goes through a mutate() that asserts the pattern is present.

#What the project is not

• Verification here means equisatisfiability of the lowering, not a proof-assistant development. The rigour is executable specifications, SMT, differential and mutation testing — not Coq or Lean. What is verified is that this lowering implements this IR semantics. Whether FRI is cryptographically sound is the literature's business.
• The determinacy analysis is sound, not complete. It proves, or it tells you it could not.
• Not audited, not production. This is a from-scratch implementation built to be understood and argued with.

The code is on GitHub. If you only read one file: docs/in-circuit-index.md — the determinate-but-unsound finding and how it was closed. It is the best single account of what the project is actually for.