Three Ways a Soundness Detector Lies

Abstract

The interesting bugs in a zero-knowledge circuit analyser are supposed to be about constraints: a signal that is assigned but never constrained, an output that no constraint relates to its inputs, a witness the prover can choose freely. This article is about a month in which every defect we fixed in the ZK track was somewhere else. A parameter list was split on the wrong comma. A signal graph merged a component’s output port with an unrelated local signal because they shared a name. A verifier classifier’s confidence score turned out to depend on which Solidity code-generation pipeline compiled the verifier. And a confidence threshold, compared after a narrowing from 64-bit to 32-bit floats, rejected findings that sat exactly on it. None of these touched constraint reasoning, and each one produced a wrong soundness verdict. We think that is the normal case, and worth documenting: the constraint logic is where attention goes, and the plumbing around it is where the verdicts actually get lost.

Lie one: the parameter that was not in the source

The Cairo and Noir front-ends both parse function signatures, and both split the parameter list on a flat comma. That is fine until a parameter’s own type contains a comma. pairs: Array<(u8, u8)> splits into pairs: Array<(u8 and u8)>, and the first fragment is truncated at the comma. Truncation is the quiet failure: a type is wrong, a count is right.

The loud failure came from path-qualified nested types. m: LegacyMap<felt252, core::integer::u256> split into m: LegacyMap<felt252 and core::integer::u256>, and the second fragment, reaching the name/type split on its first colon, became a parameter named core of type :integer::u256>. A parameter that does not exist in the source. Every downstream consumer that counts parameters, arity checks, unused-input detection, the mapping from public inputs to constraints, now had one extra, and no way to know it was invented.

The distinction between the two failures matters for how seriously to take them. Truncating a type is a precision problem. Inventing a parameter is a fabrication, and the analyser’s first rule is that it never fabricates: a wrong answer must be visibly wrong, not plausibly right. So the fix is held to that standard. The shared splitter tracks bracket depth across (, [ and < with one counter, and the counter saturates at zero on decrement, so an unbalanced line degrades toward more fragments than parameters rather than toward one fragment swallowing the list. More fragments fail an arity check; fewer fragments pass it wrongly.

Circom was deliberately not given the same treatment. Its signatures do not carry generics, and no fixture demonstrated the failure there. Widening a fix on reasoning alone is the habit this change exists to correct.

Lie two: the port and the local with the same name

The under-constrained-signal detector for Circom builds a graph: signals are nodes, constraints and assignments are edges, and a signal that is written but has no constraint path to an output is flagged. The graph is built from the names that appear in each constraint.

The name extractor, given y <== p.out, returned the tokens p and out. Both were inserted as bare signal nodes. Two things went wrong, in opposite directions, from that one decision.

A template with its own local signal named out would have that signal marked as constrained the moment any unrelated p.out appeared in a constraint. That is a missed under-constrained signal, the exact bug class the detector exists to find, suppressed by a naming coincidence.

And a signal mid that reached y only through the component p would be reported as disconnected, because the edge went to a phantom node called out, not to the component’s port. That false positive is what hid the false negative: the detector was noisy in a way that made its silence look like a strength.

The fix separates the two kinds of node. A local signal is a node. A component’s port, p.out, is a node keyed by both component and port. A bare component reference p is not a node at all, and that last decision is the one that took the longest to get right: admitting the component as a node would restore the same over-connection one level up, joining every port of p the moment any one of them was wired.

Reachability is then asked per output port, not per component. The fixture that makes this load-bearing has a template Inner with two independent halves, each with its own input and output. A collapsed relation would answer “yes, a reaches an output of Inner” and clear it, when in fact a reaches only the output that b does not, and the caller wired the other one. Per-port reachability distinguishes those. An unresolved template, one whose definition the parser did not find, answers “reaches” rather than “does not”, on the rule that not-read is not the same as shown-absent.

Lie three: a score that depended on the compiler

On-chain verifiers are classified from bytecode as Groth16 or PLONK, and the classifier’s main signal is the count of static addmod and mulmod sites, since PLONK’s verification does far more field arithmetic than Groth16’s pairing check. The threshold was set at 50 from a handful of fixtures.

An issue predicted that the legacy Solidity code generator, which shares Yul helpers across call sites, would deflate the static count and push PLONK verifiers under the threshold. That is a testable claim, and it deserved real artefacts rather than a re-examination of the existing fixtures. So the fixture set became fourteen genuine snarkjs verifiers: real circuits, a real powers-of-tau ceremony, both proving systems, three solc versions, both the legacy and the via-IR pipelines, with the generating commands checked in.

The mechanism was confirmed. Legacy codegen emits 79 addmod/mulmod sites for a PLONK verifier where via-IR emits 109 to 110, a 28 percent deflation. The consequence was refuted. Every PLONK build stays above 50 (the smallest was 79, and the eight-input variant reads 124 legacy and 140 via-IR) and every Groth16 build sits at two or below. The threshold holds, and the issue was closed with the numbers rather than with an argument.

What the wider fixture set found instead was in the confidence score. Having classified a verifier as PLONK by clearing 50, the scorer then applied a bonus if the same count cleared 100, a second volume test on the quantity the classifier had already spent. Identical circuit source therefore scored 0.70 under legacy codegen and 0.90 under via-IR. Worse, whether the score depended on the build depended on the circuit: the eight-input variant clears 100 both ways and scored 0.90 regardless, so the defect was invisible on the fixture that happened to be checked.

The bonus is now unconditional, and the scoring function no longer takes the counts at all. Their absence from the signature is what says the score cannot move with the build. The test that pins this was split into two properties, because they are different claims: what the detector concludes must not depend on the build, while what it counted legitimately may, since a static call site is not an invocation. The second property is asserted with its counterexample, the via-IR build of one fixture recording eight elliptic-curve additions where the legacy build records twelve.

Lie four: the threshold that rounded

The last one is small and general. A finding’s confidence is stored as a 32-bit float on the wire and compared against thresholds written as 64-bit literals. The migration that changed the storage width was described as “a widening and narrowing change only”, and for arithmetic it is. For a comparison against a threshold it is not:

A finding sitting exactly on a 0.7 or 0.9 floor was dropped. One on a 0.8 floor survived. Which side of the boundary a finding landed on was decided by the bit pattern of the literal, which is not a property anyone designing the threshold had in mind.

The fix narrows the threshold to the same width before comparing, so both sides take the same rounding. The first test written for it passed before the fix was applied, because the test narrowed the threshold itself and so applied the fix before the code under test ran. That is a good reminder that a test which cannot fail has not tested anything, and it was rewritten to compare against the literal the production code sees.

And one the users saw

The other bugs in this article were caught internally. This one shipped. The ZK backend serialised finding severities in PascalCase, Critical, and the portal’s report generator keyed its severity weights in lowercase. The lookup returned undefined, the weighted risk sum became NaN, every threshold comparison against NaN is false, and the overall-risk function fell through all three of its branches to its default. A circuit whose only finding was a Critical under-constrained signal exported an audit report whose overall risk read low. That is the product’s central claim, inverted, in the artefact a user hands to someone else.

The fix normalises the case once, at the boundary where findings enter the portal, rather than at the ten lookups downstream. It normalises the key, not the lookup: a default of zero at the lookup would have kept the same failure in a quieter form. And the reason the test suite was green is the same reason as the fixture problem in Ratchets That Can Fail: the report generator’s tests built their fixtures in lowercase, a shape the backend does not emit.

The common thread

Each of these is a place where the analyser’s verdict passed through code that was not about constraints, and each of them changed the verdict. The parser decided how many public inputs a circuit has. The graph model decided whether a signal was constrained. The scorer decided how much to trust a classification. The comparison decided whether a finding was shown at all. The serialiser decided what the report said.

The constraint reasoning in the middle was correct throughout. If there is a recommendation here, it is to give the plumbing the same standard of evidence as the reasoning: real artefacts rather than hand-built fixtures, a falsification step that confirms the test can fail, and a rule that a wrong answer must be visibly wrong. Every one of these bugs was plausible-looking output, and plausible is the failure mode a soundness tool cannot afford.

References

• Circom documentation: signals, components and constraints
• snarkjs — zkSNARK implementation in JavaScript and WASM
• Groth, “On the Size of Pairing-based Non-interactive Arguments” (Groth16)
• Gabizon, Williamson, Ciobotaru, “PLONK” (2019)
• Solidity: the via-IR code generation pipeline
• IEEE 754 floating-point arithmetic — Wikipedia