# Mul/div relation should not be enforced when divisor is zero

zkSync EraVM mul/div circuit enforces src0=q*src1+rem even when divisor is zero, making div-by-zero transactions unprovable and DoSing the priority queue.

- Payout: Contest reward
- Severity: high
- Program: zkSync
- Credited: xuwinnie
- Disclosed: 2024-02-29
- Write-up quality: 7/10
- Original: https://github.com/code-423n4/2023-10-zksync-findings/issues/598
- Library page: https://bugbountylibrary.com/r/c4%3A2023-10-zksync%3AH-06
- Tags: domain:web3 impact:dos kind:contest platform:code4rena sev:high tech:evm technique:source-review vuln:dos

**Target:** EraVM zk circuit (mul_div.rs opcode constraint)
**Root cause:** The mul/div relation src0 = q*src1 + rem is enforced whenever div applies, but the spec sets q=rem=0 when divisor is zero, so the relation cannot hold for nonzero dividend.
**Steps:**
1. Read `mul_div.rs` L286-L292: quotient/remainder forced to zero when divisor_is_zero.
2. Read L358: `apply_any = should_apply_mul || should_apply_div` gates the MulDivRelation push.
3. Observe relation `src0 = q*src1 + rem` is enforced for div even with src1=0.
4. Submit div with nonzero dividend and zero divisor: q=rem=0, relation fails, proof cannot be generated.
5. Unprovable tx blocks the priority queue, DoSing the sequencer.
**How found:** Code review of the mul/div circuit constraints against the EraVM spec, noticing the conditional zeroing of q/rem conflicts with the unconditional relation enforcement gated by should_apply_div.
**Exploitation:** Attacker submits a transaction containing a div opcode with nonzero dividend and zero divisor; the circuit cannot produce a valid proof, stalling the priority queue.
**Insight:** When a circuit conditionally zeroes outputs for a special case (divisor=0), check whether the algebraic relation enforcing those outputs is also conditionally disabled; mismatched gating between special-case handling and relation enforcement yields unprovable witnesses.