# Under-constrained circuit accounting values

Witness values assigned without copy constraints or full range checks, letting provers choose accounting inputs

_Area: DeFi accounting and math bugs. Seen in 2 disclosed reports; latest 2026-07-06. Updated 2026-10-29._

## How it works
A circuit is supposed to prove that a value equals something fixed or derived. When the gadget only *assigns* the value as a witness (advice) without a copy constraint tying it to the intended source, or only range-checks some of the decomposed limbs, the prover is free to pick that value. The proof still verifies, but it now attests to a false statement about balances, notes, or arithmetic results. The broken assumption is "the witness equals the committed/derived value"; nothing in the constraint system enforces it.

## Where it shows up
- `assign_advice()` used where the intent is "equals a known/fixed value" but no `copy_advice()`/equality gate follows [E1](https://bugbountylibrary.com/r/ghsa%3AGHSA-ww9q-8r59-xv46.md)
- Equality gates (e.g. `q_mul_2`) that only force equality *within* a loop, not to the external base [E1](https://bugbountylibrary.com/r/ghsa%3AGHSA-ww9q-8r59-xv46.md)
- Composite values split into limbs where only a subset is range-checked [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-05.md)
- `from_variable_unchecked` / unchecked casts applied to a limb that was never constrained [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-05.md)
- Algebraic relations enforced unconditionally while outputs are conditionally zeroed for a special case [E3](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06.md)

## How to review
For each witness assignment, ask: what constraint forces this cell to equal its intended source? Trace every value that feeds an accounting result (balance, note, quotient, remainder) back to a copy constraint or a range check. The invariant: every prover-chosen cell is either copy-constrained to a committed/derived value or fully range-checked across all limbs. For conditional logic, confirm the enforcing relation is gated by the same condition that zeroes the outputs [E3](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06.md).

## Variants seen
- Missing copy constraint on a base point in variable-base scalar multiplication, breaking Orchard Action soundness [E1](https://bugbountylibrary.com/r/ghsa%3AGHSA-ww9q-8r59-xv46.md)
- Partial range-check on decomposed and/or/xor, leaving one limb free to overflow [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-05.md)
- Unconditional mul/div relation conflicting with spec-mandated zeroing when divisor is zero [E3](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06.md)

## Impact and severity
Critical: forged proofs enable undetectable double-spends and note theft [E1](https://bugbountylibrary.com/r/ghsa%3AGHSA-ww9q-8r59-xv46.md); forged arithmetic outputs corrupt in-circuit accounting [E2](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-05.md); unprovable transactions can DoS the priority queue [E3](https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06.md). Severity rises when the under-constrained value directly gates value transfer or block production.

## Evidence
- E1: https://bugbountylibrary.com/r/ghsa%3AGHSA-ww9q-8r59-xv46.md
- E2: https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-05.md
- E3: https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06.md