# Missing constraint on remainder in shr opcode implementation

zkSync Era zkEVM shr circuit omitted remainder<divisor constraint, letting a malicious validator prove arbitrary shift results and corrupt on-chain contract execution.

- Payout: Contest reward
- Severity: high
- Program: zkSync
- Credited: chainlight
- Disclosed: 2024-02-29
- Write-up quality: 9/10
- Original: https://github.com/code-423n4/2023-10-zksync-findings/issues/697
- Library page: https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-04
- Tags: domain:web3 impact:funds-loss impact:integrity kind:contest platform:code4rena sev:high tech:evm technique:chained technique:source-review vuln:business-logic

**Target:** zkEVM main_vm circuit shr opcode (MulDivRelation)
**Root cause:** The shr implementation converts right shift to division via MulDivRelation but never constrains the remainder to be less than the divisor, so the quotient (shift result) is under-constrained.
**Steps:**
1. Read `main_vm/opcodes/shifts.rs` `apply_shifts`: `allocate_div_result_unchecked` returns `rshift_q`/`rshift_r`; only `MulDivRelation` with `rem=_rshift_r` is enforced, no `rem < divisor` check.
2. Compare with `div` opcode which enforces remainder<divisor via subtraction relation.
3. Patch witness generation to return quotient=0, remainder=a when dividend==1337, bypassing the honest div_mod.
4. Run `run_hack` test: `add! 1337, r0, r1; add! 1, r0, r2; shr r1, r2, r3` yields r3=0 instead of 668, and witness still proves.
5. Repeat against bellman/franklin-crypto deployed circuits via `add_div_relation_shift` hack to confirm same flaw.
**How found:** Code review of the shift opcode circuit; noticed the div path enforces remainder<divisor but the shr path reuses unchecked division and only wires the remainder into MulDivRelation without a range check, then built a witness-generation patch to confirm provability of a wrong result.
**Exploitation:** A malicious validator/prover crafts a witness where shr returns an attacker-chosen value (e.g. 0) and generates a valid proof, since the circuit accepts it. Submitting such blocks lets them manipulate any contract logic depending on shr (DEX price math, elliptic-curve precompiles) to steal funds or corrupt state.
**Escalation:** Affects every contract using shr, including deployed bellman-based circuits, so impact spans arbitrary DeFi logic and precompiles.
**Insight:** In zkVM/zkEVM circuits, any opcode lowered to division must independently constrain the remainder range; unchecked division helpers are safe only when the caller adds the remainder<divisor relation, so audit each call site of `allocate_div_result_unchecked` rather than trusting the helper.