Under-Constrained ZK-Rollup Circuits: How Missing Constraints Break State Proofs

Abstract: a valid proof is not the same as a valid state transition

ZK-Rollup security does not end at Groth16, PLONK, Halo2, or any other proof system satisfying its cryptographic soundness definition. The more practical failure mode is semantic: the circuit constraints do not fully encode the execution rule that the Rollup claims to prove. The verifier only checks that a set of field elements satisfies a system of polynomial equations. If those equations do not force the balance, address, nonce, storage key, range check, Merkle path, or public-input binding to be unique, a malicious prover may produce a valid proof for an invalid state transition. This article studies under-constrained ZK circuits from an engineering perspective: R1CS and PLONKish semantics, Circom and Halo2 assignment pitfalls, SMT-based uniqueness checks, static analysis, trace-constraint consistency, and the risk that circuit bugs create for cross-chain settlement and AllSwap-style route execution.

Scope: defensive circuit assurance, not exploit construction

This is a defensive analysis of circuit security. It does not provide exploit templates, target-selection procedures, reusable forged witnesses, or instructions for attacking deployed protocols. The system roles are a Rollup sequencer, a prover, an off-chain executor, the ZK circuit, the on-chain verifier contract, users, cross-chain routers, and audit tools. The adversary is allowed to choose witness values, search boundary states, manipulate unconstrained intermediate variables, and submit proofs that satisfy the circuit while violating the intended execution semantics. The adversary is not assumed to break hash functions, compromise trusted setup material, or solve elliptic-curve discrete logarithms.

The critical boundary is that a computation program and a constraint system are different objects. A program can compute `z = f(x)`. A proof system sees only a set of equations over a finite field. Unless those equations force `z` to be uniquely determined by `x`, the prover may be able to choose a different `z` that satisfies the circuit but violates the business rule. Circom's distinction between witness-only assignment and constrained assignment is the smallest useful example. One form only computes witness values; the other also emits constraints. Halo2 and other PLONKish systems have the same conceptual boundary: assigning an advice cell does not mean the cell is checked by a gate, lookup, equality constraint, or enabled selector.

In a Rollup, this risk has larger blast radius than in a standalone privacy application. A missing bit constraint in a small identity proof may corrupt one statement. A missing state-transition constraint in a Rollup can corrupt the state root for an entire batch. The L1 verifier sees a proof and public inputs; it does not replay the off-chain execution trace. Once an invalid proof is accepted, bridge release, withdrawal finality, cross-chain liquidity settlement, and refund attribution may all inherit the wrong state.

Formal model: uniqueness matters more than constraint count

Let the off-chain execution function be:

```text T(s_old, txs) = (s_new, receipts, aux) ```

`s_old` is the old state root, `txs` is the ordered transaction sequence, `s_new` is the new state root, `receipts` are execution receipts, and `aux` includes read-write tables, Merkle paths, range-check decompositions, hash preimages, lookup rows, and intermediate trace values. The circuit actually defines a relation:

```text C(public, witness) = 0 public = (s_old, s_new, batch_hash, data_commitment) witness = (txs, traces, reads, writes, paths, intermediate) ```

The desired safety property is not merely that there exists a witness satisfying `C`. It is semantic equivalence:

```text C(public, witness) = 0 iff witness encodes a valid execution of T ```

Under-constraint is a failure of the reverse direction. There exists `witness_bad` such that `C(public, witness_bad) = 0`, but the witness does not encode a valid execution of `T`. More operationally, a security-critical output or intermediate variable is not uniquely determined by the public input and prior witness values. The PLDI work on automated detection of under-constrained circuits frames this as uniqueness reasoning over polynomial equations in finite fields. The USENIX Security 2024 work on practical ZK circuit analysis emphasizes a related point: real bugs often come from divergence between program traces and generated constraints, not from a single visibly wrong equation.

For circuit engineers, the useful question is not "does this circuit have many constraints?" It is "is every security-critical value consumed by the right constraint under the right domain?" A circuit may contain millions of constraints and still miss the one boolean selector that controls asset ownership. A much smaller circuit can be safe if outputs are uniquely determined, range boundaries are explicit, lookup tables are constrained, and public inputs bind the intended domain. Circuit safety is semantic coverage, not size.

Engineering sources of under-constraint

The first source is confusion between witness computation and constraint generation. Circom witness-only assignments are necessary for operations that cannot directly be expressed as a quadratic constraint, such as bit extraction, division, or preprocessing for a hash gadget. But after such assignment, the circuit must add constraints. If a value is decomposed into bits, the circuit must prove each bit is boolean and must prove that the weighted sum reconstructs the original value. Otherwise, the prover can provide plausible-looking bits while bypassing the actual range check.

The second source is disabled selectors, missing lookups, or unused custom gates. In Halo2 and PLONKish circuits, semantics are built from advice columns, fixed columns, instance columns, selectors, custom gates, equality constraints, and lookup arguments. Assigning a cell only stores witness data. If the selector is not enabled on that row, or the lookup does not include the cell, the assigned value is memory, not a proven fact. Automated Halo2 analysis work has treated unconstrained cells, unused gates, and selector mismatches as serious bug signals for exactly this reason.

The third source is range and aliasing mismatch. Field elements are interpreted modulo a prime field. Application logic often expects uint64, uint160, uint256, address domains, or bounded limb decompositions. If the circuit does not prove that `x` lies inside the required business range, two different integers can collapse to the same field element. For balances, nonces, amounts, and storage slots, this creates one-proof-many-meanings behavior: the executor reasons in integer semantics while the circuit reasons in field semantics.

The fourth source is incomplete state-path binding. A ZK-Rollup state circuit must do more than recompute a Merkle or sparse-Merkle root. It must bind leaf encoding, path direction, tree height, empty-leaf semantics, old value, new value, account key, storage key, and path index. If the circuit only proves that some leaf is in some tree, but not that the target account's target slot was updated according to the transition rule, the proof has the wrong meaning.

The fifth source is incomplete public-input binding. A proof that does not bind chain ID, batch number, data commitment, verifier address, circuit version, or message queue root may be replayed under the wrong context. For cross-chain settlement, `s_new` being mathematically correct is not sufficient. The state root must belong to the correct Rollup, the correct batch, the correct data-availability commitment, and the correct withdrawal or bridge-message domain.

Rollup state circuits: where local correctness becomes global error

In ZK-Rollups, the most dangerous under-constraints often appear at component boundaries rather than inside a small arithmetic gadget. The transaction circuit believes it updated balances. The state-tree circuit believes it recomputed a leaf. The aggregation circuit believes it published the new state root. If those components do not bind the same account key, storage key, nonce, write index, and batch context, each component may be locally valid while the batch is globally invalid. An audit should treat "component passed" as an intermediate fact, not a final safety conclusion.

The read-write table is the first boundary to inspect. Every storage read, storage write, balance deduction, fee charge, log write, and withdrawal-message write should enter a unified table ordered by transaction index, call depth, account, slot, and access type. If the circuit checks that each row is well-formed but does not check continuity for the same key, it can admit a ghost state: one part of the trace reads an old value, another writes a new value, and a later operation silently continues from another old value. For a cross-chain withdrawal message, this can corrupt whether a message has already been consumed.

Commitment domains are the second boundary. A zkEVM often splits execution traces, state-tree paths, log commitments, and data-availability commitments into separate subcircuits to control proving cost. If subcircuits exchange only a field element without binding domain tag, batch context, input sequence, and schema version, a valid commitment from one subsystem can be moved into the semantic position of another. The safer design is to treat every commitment as typed data: domain, schema, batch, and sequence are part of what is proven.

Failure transactions are the third boundary. A Rollup executor must handle revert, out-of-gas, invalid signature, wrong nonce, and missing account states. The circuit must prove that failed transactions do not create unauthorized writes, while still proving the correct fee behavior and receipt behavior. If a circuit mostly encodes the success path and treats failure as "no output," edge cases can create disagreement between the ledger and receipts. Cross-chain routers depend on receipts to decide release or refund. Receipt-state disagreement becomes user-visible settlement ambiguity.

Formal verification: treat the circuit as a finite-field program

Formal verification should not promise a vague "no bugs" result. It should prove concrete, machine-checkable properties. The first layer is constraint coverage: every output, public-input-derived intermediate value, state-root component, balance update, nonce update, and withdrawal-message component should occur in a non-trivial constraint. Circomspect-style static analysis can detect under-constrained signals, unused variables, suspicious assertions, hard-coded curve constants, and other patterns that are cheap to catch early. This should be a CI gate, not an after-audit suggestion.

The second layer is uniqueness checking. Given a public input and part of the witness, an SMT solver or algebraic solver tries to find two distinct witnesses that both satisfy the constraints while differing on a critical value:

```text C(public, w1) = 0 C(public, w2) = 0 critical(w1) != critical(w2) ```

If the formula is satisfiable, the circuit has at least one semantic degree of freedom for that critical value. Z3 is useful for bit-vectors, arrays, integer ranges, and control-flow conditions. Picus-style tools reason closer to the finite-field polynomial equations emitted by ZK compilers, which reduces dependence on the source-language frontend.

The third layer is trace-constraint consistency. zkFuzz frames ZK circuit bugs as discrepancies between values permitted by the computation trace and values permitted by the constraint system. That is closer to how Rollup bugs happen in practice. A batch trace is not just a final state root. It contains reads, writes, call depth, gas behavior, logs, withdrawal messages, and failure rollback. If mutating the computation still leaves the constraints satisfiable under carefully chosen inputs, the circuit did not lock down the intended semantics.

The fourth layer is differential constraint auditing. The same transition should have at least three representations: high-level specification, executor trace, and constraint system. Any optimization must explain how semantic equivalence is preserved. Replacing a Keccak-heavy path with a SNARK-friendly Poseidon auxiliary commitment is not automatically safe. The audit must show that L1 public inputs, data-availability bytes, hash domains, and circuit commitments cannot be substituted across contexts.

Audit state machine: from source review to settlement gates

A production circuit pipeline can be modeled as:

```text spec, zkDSL, compiler IR, constraints, proving key, verifier, on-chain binding ```

Each layer needs traceable evidence. The specification states invariants: total supply conservation, non-negative balances, monotonic nonce, single-use withdrawal messages, deterministic failure handling, and state-root continuity. The zkDSL layer checks that witness computation and constraints are paired. The compiler IR layer checks that simplification did not delete safety-relevant constraints. The constraint layer runs uniqueness and coverage checks. The proving-key and verifier layers bind circuit version, public-input order, and verifier contract address. The on-chain binding layer ensures a proof can only be used for the intended batch and Rollup.

Version management is often underestimated. A circuit upgrade is not a normal backend deployment. If public-input ordering, lookup-table layout, range-check width, hash domain, state-leaf encoding, or verifier key changes, historical proofs may no longer have the same semantics. Production systems should bind `circuitId`, `constraintHash`, `verifierKeyHash`, and `publicInputSchemaVersion` into verifiable on-chain context. Otherwise, "the proof verified" is not enough information to know which statement was verified.

Settlement systems also need failure-before-finality behavior. If a circuit anomaly is detected, the correct action is not to rely on human judgment after proof generation. The state root should be blocked before it propagates to bridge release or withdrawal finality. A high-risk batch can enter quarantine: large withdrawals pause, bridge releases stop, users can still inspect status, and refund paths remain accountable. That state machine is more reliable than attempting to recover assets after a bad root has become the dependency for downstream systems.

Failure modes and detection signals

The first failure mode is unconstrained output. The prover can change amount, recipient, nonce, or part of a state leaf while satisfying the rest of the circuit. Signals include intermediate values appearing in too few constraints, outputs lacking reverse constraints, and selectors covering fewer rows than intended. Defenses are output uniqueness tests, critical-signal allowlists, and constraint coverage reports.

The second failure mode is missing range checks. A field element is treated as an application integer, causing overflow, aliasing, or signedness mismatch. Signals include bit decompositions that assign bits without reconstruction, lookup tables that do not cover every limb, and cross-field conversions without upper-bound proofs. Defenses are reusable range-check gadgets, limb-width audits, and field-modulus-specific tests.

The third failure mode is incomplete state-path binding. The circuit proves that a Merkle path is valid, but not that the path belongs to the intended account or storage slot. Signals include account key, path index, leaf preimage, and root recomputation being spread across components without a common public binding. Defenses bind account key, storage key, old value, new value, path direction, and root into one state-transition assertion.

The fourth failure mode is optimizer-induced semantic drift. Constant folding, constraint simplification, and unused-signal removal are normal compiler behavior. But if high-level code relies on assertions or witness-only computations, optimization can leave a semantic gap. Defenses include constraint hashes, differential builds across optimization settings, and inclusion of compiler artifacts in the audit package.

The fifth failure mode is verifier and public-input mismatch. The on-chain contract verifies a proof but decodes public inputs in the wrong order or fails to bind the data commitment. Signals include verifier upgrades without schema updates, multiple circuits sharing one entrypoint, and proofs that appear reusable across deployment contexts. Defenses are domain separation, schema hashes, chain IDs, verifier addresses, and batch-commitment binding.

AllSwap relevance: route safety depends on proof semantics

AllSwap does not write ZK-Rollup circuits, but cross-chain exchange depends on Rollup finality, bridge messages, withdrawal proofs, and refund paths. If a route depends on a Rollup whose proof semantics are unstable, "batch proven" may not mean "assets can be safely released." A route engine should not score paths only by fee, latency, and liquidity. It should also track circuit audit posture, verifier-key version, recent circuit upgrades, data-availability binding, and exceptional-batch handling.

A practical route-risk model can split proof quality into five components:

```text proofRisk = constraintCoverageRisk + formalVerificationRisk + verifierBindingRisk + upgradeRisk + incidentResponseRisk ```

`constraintCoverageRisk` comes from audit and static-analysis evidence. `formalVerificationRisk` comes from uniqueness, SMT, and fuzzing results. `verifierBindingRisk` comes from public-input schema and on-chain domain separation. `upgradeRisk` comes from recent changes to circuits, proving keys, lookup tables, or verifier contracts. `incidentResponseRisk` comes from whether abnormal batches support pause, limit reduction, refund, or quarantine. A cheaper route that depends on a recently upgraded, weakly audited circuit may be worse than a slower route with stable proof semantics.

User-facing status should not expose every circuit term. It should separate stages that are often collapsed: `batchSubmitted`, `proofGenerated`, `proofVerified`, `withdrawalFinalized`, and `refundAvailable`. Before proof verification, target-chain release should not be presented as deterministic. If a circuit or verifier anomaly appears, the priority should be refund attribution and explainable asset state, not optimistic completion language.

When proof-quality signals degrade, a router can apply tiered handling instead of fully disabling a path. Small transfers may keep running with lower limits and longer confirmation windows. Large transfers may move to a slower but better-audited settlement path. In-flight orders should preserve refund and status-query functionality. The point is not to certify a Rollup's circuit. The point is to avoid passing proof-semantics risk directly to users without route-level controls.

Open problems

First, the industry lacks a common machine-readable format for circuit semantics. Audit reports can describe risk, but routers and settlement systems cannot easily compare constraint coverage, public-input binding, and circuit-upgrade posture across Rollups.

Second, formal tools still face scale limits. SMT solving, symbolic execution, algebraic reasoning, and fuzzing can expose deep bugs, but zkEVM-scale circuits require modular proofs of safety properties. Proving a gadget safe is not enough if the batch-level composition remains unchecked.

Third, the compiler trust boundary remains unresolved. zkDSL source code, compiler IR, constraint simplification, proving keys, and verifier contracts need reproducible builds and artifact hashes. Many systems still treat these as internal deployment artifacts rather than public security evidence.

Fourth, cross-chain systems lack real-time proof-quality signals. A router can observe latency and failure rate, but it may not know that a circuit was just upgraded, that a verifier key changed, or that a batch entered an exceptional proving path.

Fifth, user comprehension remains hard. A good interface should not force users to read circuit audit details, but it must explain waiting reason, refund state, settlement risk, and abnormal pause status with enough precision to be useful.

References

[1] Circom Documentation, Constraint Generation, https://docs.circom.io/circom-language/constraint-generation/

[2] Circom Documentation, Signals, https://docs.circom.io/circom-language/signals/

[3] Circom Documentation, Constraint Simplification, https://docs.circom.io/circom-language/circom-insight/simplification/

[4] Zcash Halo2 Book, PLONKish Arithmetization, https://zcash.github.io/halo2/concepts/arithmetization.html

[5] Zcash Halo2 Book, Tips and Tricks, https://zcash.github.io/halo2/user/tips-and-tricks.html

[6] Ariel Gabizon, Zachary J. Williamson, Oana Ciobotaru, PLONK, IACR ePrint 2019/953, https://eprint.iacr.org/2019/953

[7] Shankara Pailoor et al., Automated Detection of Underconstrained Circuits in Zero-Knowledge Proofs, IACR ePrint 2023/512, https://eprint.iacr.org/2023/512

[8] Hongbo Wen et al., Practical Security Analysis of Zero-Knowledge Proof Circuits, USENIX Security 2024, https://www.usenix.org/conference/usenixsecurity24/presentation/wen

[9] Trail of Bits, Circomspect Static Analyzer, https://github.com/trailofbits/circomspect

[10] Trail of Bits, Circomspect Analysis Passes, https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md

[11] Leonardo de Moura and Nikolaj Bjørner, Z3: An Efficient SMT Solver, Microsoft Research, https://www.microsoft.com/en-us/research/publication/z3-an-efficient-smt-solver/

[12] Hideaki Takahashi et al., zkFuzz: Foundation and Framework for Effective Fuzzing of Zero-Knowledge Circuits, arXiv 2025, https://arxiv.org/abs/2504.11961