Division by Zero Remediation

Overview

Related Detector: Division by Zero Risk

Division by zero in ZK circuits produces undefined witness values. The fix is to constrain the divisor to be non-zero before any division operation.

Recommended Fix

Before (Vulnerable)

signal input a;
signal input b;
signal quotient;
quotient <-- a / b;      // Undefined if b == 0
quotient * b === a;       // Constraint holds trivially when b == 0 and a == 0

After (Fixed)

signal input a;
signal input b;
signal quotient;
signal b_inv;

// Force b != 0 by requiring its inverse exists
b_inv <-- 1 / b;
b_inv * b === 1;          // Only satisfiable when b != 0

quotient <-- a / b;
quotient * b === a;       // Now safe because b is guaranteed non-zero

Alternative Mitigations

Use the IsZero component from circomlib to explicitly check:

component isZero = IsZero();
isZero.in <== b;
isZero.out === 0;  // Asserts b is NOT zero

Common Mistakes

• Checking only in witness code: assert(b != 0) in JavaScript witness helpers is not a constraint — the prover can bypass it.
• Assuming compiler catches it: Circom does not detect division by zero at compile time.
• Missing constraint on 0/0 case: When both a and b might be zero, quotient * b === a is satisfied by any quotient, producing an unconstrained result.

References

• circomlib: IsZero
• Circom Documentation: Operators