When line coverage lies

This note is written to be read twice. The first two sections assume no prior exposure to constraint systems and build the mechanism from the ground up. The rest is written for people who build and audit these circuits, and it goes to the exact code, the algebra of the exploit and a validation designed so it cannot flatter itself.

What a constraint system actually checks

A zero knowledge proof of a computation rests on one idea. Instead of re-running the work, a verifier checks that a filled-in table, called the trace, obeys a fixed set of algebraic rules. Each row is one step of the computation and each column is one register or intermediate value. Formally the trace is $T\in {\mathbb{F}}^{n\times w}$, a matrix of $n$ rows and $w$ columns over a finite field.

Each rule is a polynomial that must evaluate to zero. A rule that acts on a single row asks that some polynomial $C$ vanish on every row:

A rule that ties one step to the next acts on a pair of adjacent rows, $C({\mathbf{t}}_i,{\mathbf{t}}_{i+1})=0$. The prover sends a trace and the verifier checks that every rule vanishes. If they all do, the verifier is convinced the computation was carried out correctly.

Soundness is the property that makes this trustworthy. The rules have to pin the trace down, so that for a given public input there is no valid trace other than the honest one. When the rules are too weak, a different trace satisfies all of them and the system is under-constrained.

A prover who wants to cheat fills in that other trace, every rule still vanishes and the result is a valid proof of a false statement. Under-constraint is not a theoretical worry. It is the dominant soundness bug class in production zero knowledge systems, and it has moved real money.

What matters here is conditionality. Most rules apply only sometimes. A boundary rule applies only on the first row, a transition rule applies between consecutive rows but not across the wraparound at the end, an instruction rule applies only on rows where a particular opcode flag is set. The framework does not write an if. It multiplies the rule by a selector polynomial $s$ that is one where the rule should apply and zero elsewhere, then asks the product to vanish:

Everything follows from that one equation. Where $s=1$ the row must satisfy $C$. Where $s=0$ the product is zero no matter what $C$ is, so on those rows the constraint enforces nothing. It is inert.

The blind spot

A circuit is code, and teams test it like code. The usual reflex is line coverage: run the tests, confirm that every line of the constraint definition executed, treat green as safe.

Line coverage answers a different question than soundness needs. It asks whether the assertion statement ran, and it did. The evaluator walks every row of the trace and calls the constraint on each one, so the line is covered on all of them, even the rows where the selector is zero and the constraint enforces nothing. The statement executed while the constraint went untested.

On top is what a coverage tool reports, one hundred percent: the assertion ran on all eight rows. The strip below is what actually happened, the constraint enforced on three of them. A line tool cannot separate a correctly wired guard from a broken one, because both run the same line the same number of times. The green checkmark measures execution and reports it as safety.

This is not a rare corner. Conditional constraints are the default shape in these systems, which is close to all of them.

The bug this hides

One family of bugs lives in the gap, and it is simple to state: a correct constraint attached to the wrong selector. It runs, it shows green and it fails to constrain the rows that matter.

Take an accumulator. Exponentiation by repeated squaring builds a running value where each step squares the previous one and multiplies in a bit-dependent factor:

where the value on the last row, $a_{n-1}$, is the claimed result $r$. The recurrence has to hold on every row after the first, since row zero has no predecessor. Guarded correctly, with a selector that is one everywhere except the first row, it is enforced on rows $1$ through $n-1$ and reaches the last row, so the result is tied to the computation.

Guarded with the wrong selector, one that is zero on the last row instead of the first, it is enforced on rows $0$ through $n-2$ and never touches the output row. An honest trace looks fine, because an honest trace satisfies the recurrence everywhere anyway. The result is now free.

A prover sets $a_{n-1}$ to any chosen value, every enforced row still holds, the boundary rule that ties the output column to the public claim is satisfied by construction and the verifier accepts a proof of a false exponent. This is a real finding from a published audit of a production zero knowledge virtual machine, and the whole defect is one wrong selector.

A metric that measures enforcement, not execution

The rest of this note is for people who work on these systems.

The fix is not a better line coverage tool but a different measurement. For each constraint site, over a valid trace, record where the guard was actually active rather than whether the statement ran. Call the record its activation profile:

struct ConstraintCov {
    active_rows: usize,             // guard nonzero
    inactive_rows: usize,          // guard zero
    min_active_row: Option<usize>, // first row reached
    max_active_row: Option<usize>, // last row reached
    // ... plus active_zero / active_nonzero
}

One design point was not obvious in advance. A boolean, "was this constraint ever active", does not catch the real bugs. In the accumulator above the broken guard is active on seven of eight rows and the correct one is also active on seven of eight rows, so both report "ever active". The signal is not how many rows but which rows: the correct guard reaches the last row and the broken one does not. The activation profile carries that distinction and the boolean discards it.

The instrumentation is small, which is the point. In a Plonky3 style builder the guard multiply lives in exactly one place, the filtered builder that folds a condition into an assertion:

// FilteredAirBuilder::assert_zero
fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    self.inner.assert_zero(self.condition() * x.into());
}

Every guarded constraint in the whole system passes through that one multiplication. So one hook there, fed by the concrete-trace evaluator, sees them all:

fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
    // Report the guard before it is folded into the term. After the
    // multiply, the guard and the constrained expression are indistinguishable.
    self.inner.aircov_note_guard(&self.condition);
    self.inner.assert_zero(self.condition() * x.into());
}

That recorder is gated behind a feature flag and stays inert unless a session is open, so ordinary builds pay nothing. The metric is read off a valid trace: run the constraints through the evaluator, and instead of pass or fail the output is the set of rows on which each guard was live.

The exploit, on the activation profile

The accumulator bug is now visible before anyone runs the exploit. Toggle the guard below and watch the last row, the one that carries the result.

Under the correct guard the recurrence reaches the output row, so a wrong result cannot pass. The broken guard leaves the output row unconstrained, which is exactly the freedom the forgery uses. Two profiles, one different selector, same code and same executed lines. The shipped bug looked like this:

// Enforce the accumulation recurrence.
builder
    .when(local.is_real)
    .when_not(local.is_last)   // shipped guard; the fix is is_first
    .assert_eq(local.accum, local.prev_accum_squared_times_multiplier);

Line coverage of that assertion is one hundred percent under any honest test, because the assertion runs on every row. The activation profile is the only cheap signal that separates it from the correct version on a valid trace, without anyone having to think of the forgery first.

Validation, built so it cannot flatter itself

There is an obvious objection. The row-position fields were added while looking at a row-guard bug, so validating the metric on that same bug proves nothing, because a metric will always catch the case it was shaped around.

To separate prediction from fitting, the metric was frozen in writing and the predictions were registered in advance. The criterion was fixed before any held-out bug was built: AIRCov distinguishes a bug when the frozen per-site profile, computed on a valid trace, differs between the correct and the broken circuit for at least one shared site. Four bug classes were then reconstructed as minimal hand-authored circuits, each a faithful rebuild of a documented pattern rather than a bug caught in the wild, and each confirmed genuinely exploitable, meaning a forged trace the broken circuit accepts and the correct one rejects.

All four predictions held. Look at the wrong-selector row, which carries the weight. It is a different mechanism from the row-guard bug the metric was shaped on, so a catch there is evidence that the profile generalizes to a bug it was not designed around, rather than evidence that it memorized one case. The three misses were predicted in advance and mark the honest boundary of the method.

One caveat sits inside the criterion. It asks whether the profile differs between the correct and the broken circuit, which presumes a known-correct reference to diff against. A real audit has no such reference. That absence is the whole problem. In deployment the metric emits a single profile and a reviewer judges it on its own, where a recurrence that never reaches the output row reads as wrong with no sibling to compare it against. The four of four is measured under that more favorable oracle. The deployment signal is the weaker read of the same fingerprint, which is why the closing framing calls it a reviewer's fingerprint and not a verdict.

Freeze the metric, write the predictions down first, then reconstruct the bugs. Results that only hold once they are fit afterward are a measurement of hindsight.

What it cannot catch

This boundary is sharp, and stating it plainly is the point of a metric worth trusting.

AIRCov catches guard and selector bugs whose activation profile differs on a valid trace. Three things stay out of reach:

• Missing constraints. With no site, there is nothing to measure. A metric over the constraints that exist cannot see the one that does not.
• Narrow-expression bugs. A rule that checks one limb of a word where it should check all of them has the same site, the same guard and the same activation profile as the correct version. There is no difference to detect, because the difference sits inside the expression rather than in when it fires.
• Guard bugs invisible on valid traces. A spurious extra condition that honest data happens to satisfy leaves no mark in coverage measured on valid traces. This is a limit of any valid-trace coverage, AIRCov included, not a gap a sharper metric closes.

So this is one instrument for one class, with a characterized edge. It surfaces a fingerprint, a recurrence that never reaches the output row, a constraint that fires on the rows its sibling skips, which a reviewer or a downstream rule then interprets. It does not hand down a verdict.

On the real stack, and where this sits

None of the above depends on a toy. The instrumentation runs on the production stack. Current SP1 evaluates its chips through a re-export of the published p3-air crate, so the same one-line hook, vendored into that crate and patched in, flows through the real constraint builder. Coverage was collected on a chip that ships in SP1, run through its own evaluator. The exploit was run on a chip built with SP1's real traits and constraint builder that carries the same wrong-selector class, though not one of the pre-existing production chips such as the arithmetic units. On that live path the defect is at once exploitable, with a forged trace accepted at zero failing rows, invisible to line coverage, measured at one hundred percent on the constraint that carries it and visible in the activation profile. Injecting documented patterns into the production chips themselves is the remaining work.

A word on prior work. A metamorphic fuzzer for zero knowledge virtual machines already finds soundness and completeness bugs, already uses lightweight instruction-coverage feedback and names constraint-tailored coverage as future work. It is both the baseline and independent evidence that the direction is worth walking. The jobs differ. That line of work generates tests and finds bugs, while AIRCov measures whether a test suite already in hand is adequate, for one bug class, with the boundary drawn. No claim is made to being first at mutation testing in this space. What is claimed is narrower: a row-position activation-profile adequacy metric, with pre-registered held-out evidence that it separates a real bug class line coverage cannot see.

The instrumented forks and every test above are public, from the feasibility case through the forged-proof exploit and the reconstructed audit finding to the frozen pre-registered validation, so the numbers here can be rerun rather than taken on faith.

Reproduce it

Two forks carry the instrumentation and the tests.

• Plonky3 fork: the recorder, the one-line guard hook, and the four tests, feasibility, the forged-proof exploit, the reconstructed audit finding and the frozen pre-registered validation. Details in its AIRCOV.md.
• SP1 fork: the same hook on the production stack, wired through a vendored copy of p3-air and SP1's own constraint builder, with the coverage run on a real chip. Details in its AIRCOV.md.