# Under-constrained ZK circuit witness Witness values used in checks but never range-, uniqueness-, or linkage-constrained _Area: Smart contract access control and control flow. Seen in 13 disclosed reports; one confirmed bounty: $200,000; latest 2026-06-22. Updated 2026-10-22._ ## How it works A ZK circuit proves statements by constraining witness values with algebraic relations. Soundness depends on every witness that influences a boolean flag, comparison, or public output being fully pinned down. When a constraint is missing — a range check, a remainder bound, an equality tying a witness to a derived value, or a uniqueness/multiplicity bound — the prover is free to choose a non-canonical witness that satisfies the remaining constraints while proving a false statement. The assumption that breaks: that satisfying the written constraints implies the intended relation. It does not, if any intermediate is left free. ## Where it shows up - `AllocatedNum::alloc` (or equivalent) with no following `enforce` tying it to public/derived signals [E3](https://bugbountylibrary.com/r/blog%3Aimmunefi-com-blog-bug-fix-reviews-zksync-insufficient-proof-verification-bugfix-review.md). - `public_witness_ct` used to expose a value that gates on-chain accounting, without an equality constraint [E4](https://bugbountylibrary.com/r/dhl%3A20260622-aztecescapehatch-exp2.md). - Subtraction/borrow results used in comparisons but not range-constrained to limb width [E1](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-01.md). - Division lowered from another opcode without a `remainder < divisor` relation [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-04.md). - Limb decompositions tied by equality but with no per-limb bit-width check [E7](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.5.md). - Counters/timestamps where only the delta is bounded, not the absolute value [E6](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.2.md). - Lookup/bus arguments with no bound on send multiplicity [E5](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.1.md). - Selector flags (e.g. "first difference") not constrained to imply the condition they mark [E8](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.6.md). ## How to review For each witness column, ask: is there a constraint that uniquely determines it, or does it merely relate it to something else? The invariant: every value feeding a comparison, borrow flag, selector, or public output must be range-constrained to its canonical domain, and every allocated witness must be tied by an equality to a public or derived signal. Check that witness-generation logic is mirrored by hard constraints — a set flag must imply the fact it asserts [E8](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.6.md). For division helpers, confirm the caller adds the remainder bound [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-04.md). For buses, confirm multiplicity is bounded below the field characteristic [E5](https://bugbountylibrary.com/r/cantina%3Aopenvm_january2025%3A3.1.1.md). ## Variants seen - Missing range check on subtraction result flips borrow flag [E1](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-01.md). - Missing remainder