# Range check fails to bind limbs to value, enabling invalid witnesses

KoalaBearRangeCheck in Succinct's gnark FFI enforces limb bitlengths but never binds hinted limbs to the source value, letting a malicious prover supply inconsistent witnesses.

- Payout: Contest reward
- Severity: high
- Program: Succinct
- Credited: Matte
- Disclosed: 2026-02-18
- Write-up quality: 7/10
- Original: https://code4rena.com/reports/2025-09-succinct#h-01
- Library page: https://bugbountylibrary.com/r/c4%3A2025-09-succinct%3AH-01
- Tags: domain:web3 impact:integrity kind:contest platform:code4rena sev:high tech:go tech:solidity technique:incomplete-fix technique:source-review vuln:misconfiguration

**Target:** gnark-ffi Go circuit range-check helper (koalabear.go)
**Root cause:** KoalaBearRangeCheck splits value into hinted low/high limbs and only constrains per-limb bitlengths plus a boundary guard, omitting the assertion value == highLimb*2^24 + lowLimb; gnark hints are advice, not constraints, so the limbs are unbound to value.
**Steps:**
1. Read `KoalaBearRangeCheck()` in `crates/recursion/gnark-ffi/go/sp1/koalabear/koalabear.go` L79-L97; note `SplitLimbsHint` produces lowLimb/highLimb but no recomposition assert.
2. Compare with `reduceWithMaxBits()` in same file, which does assert `remainder == highLimb*2^24 + lowLimb`.
3. Construct a minimal circuit calling only `KoalaBearRangeCheck(x)`; supply arbitrary limbs within bit bounds (avoid highLimb==127) and observe acceptance for any x.
4. Confirm downstream gadgets in `sp1.go` treat value as valid without re-reducing/asserting canonical form.
**How found:** Code review of the range-check helper; noticed the hint computes limbs but no constraint ties them back to value, and contrasted against the correct recomposition pattern already used in reduceWithMaxBits() in the same file.
**Exploitation:** Malicious prover picks witness values that benefit later constraints (e.g. zeroing a product or aligning a digest preimage), chooses highLimb/lowLimb within bit bounds avoiding the highLimb==127 boundary case, and passes the range check regardless of value; downstream gadgets then accept out-of-range/inconsistent inputs, breaking soundness of the proof system.
**Insight:** In gnark (and any hint-based circuit), a hint function's internal checks (like the modulus bound in SplitLimbsHint) are not constraints; always verify a recomposition/equality assertion exists between hinted outputs and the source variable, and grep sibling helpers for the correct pattern to spot the missing one.