Nondeterministic Division in Noir Circuits

Overview

Division does not behave in a finite field the way it does over the integers. There is no rounding and no “remainder” — a / b is a multiplied by the modular inverse of b. When a Noir author writes a division and treats the result as a normal quotient, two things can go wrong at once: the result is a witness value the prover supplies, and nothing in the circuit forces that witness to equal the intended quotient. The verifier sees a number, not a proof that the number is correct.

This detector looks at division operations inside Noir functions and asks whether the surrounding code actually pins the result down. Inside an unconstrained function the quotient is computed off-circuit entirely, so it is reported with higher confidence. Inside a constrained function the detector checks whether any assertion references the divisor; if no assertion mentions it, the divisor could be zero and the quotient is left free.

Why This Is an Issue

A division that is not backed by a constraint lets a malicious prover choose the quotient. Suppose a circuit computes share = total / participants and uses share later in a balance check. If no assertion ties share back to total and participants, the prover can claim any share they like and still produce a valid proof. Funds, voting weights, or eligibility thresholds derived from that value become forgeable.

The zero-divisor case is the sharper edge. Field division by zero is not a runtime error the way it is in most languages — it produces a value the prover controls. A circuit that never asserts divisor != 0 has no defence against a prover who picks a divisor of zero precisely to unlock an otherwise-unreachable result.

How to Resolve

Constrain the division. The result of any division that feeds a checked value must be re-derived inside the constraint system, and the divisor must be proven non-zero.

// Before: the quotient is an unconstrained witness
fn compute_share(total: Field, participants: Field) -> Field {
    let share = total / participants; // prover-controlled, divisor may be zero
    share
}

// After: the relationship is rebound and the divisor is checked
fn compute_share(total: Field, participants: Field) -> Field {
    assert(participants != 0);
    let share = total / participants;
    assert(share * participants == total); // re-derives the quotient in-circuit
    share
}

For integer division where a remainder is expected, assert the full Euclidean relation: assert(quotient * divisor + remainder == dividend) together with assert(remainder < divisor).

Detection Methodology

The Noir front-end is parsed into a typed representation that records each function’s operations, assertions, and visibility. For every function the detector collects the operations whose expressions contain a division operator, taking care to skip // comment sequences. Division found inside an unconstrained function is reported directly, because the quotient is computed outside the constraint system by construction. For a constrained function the detector extracts the divisor sub-expression and scans the function’s assertions for any reference to that identifier. When no assertion mentions the divisor, the operation is reported: the quotient is unconstrained and the divisor is potentially zero.

Limitations

Divisor matching is identifier-based. A divisor that is validated indirectly — for example, an assertion on a different variable that is provably equal to the divisor — may still be flagged.
The detector recognises divisor checks expressed as assertions; a divisor constrained through a separate helper function call may not be tracked.
Constant divisors that are clearly non-zero in source are still reported when no quotient-relating assertion is present, since the quotient itself remains unconstrained.

Noir Circuit Detectors — the broader family of Noir soundness checks
Division by Zero — the divisor-is-zero hazard in Circom circuits
Unconstrained Divisor — an unvalidated divisor in the Circom setting
Range Check — bounding witness values that feed arithmetic

References

Sample Sigvex Output

{
  "detector": "nondeterministic-division",
  "severity": "high",
  "confidence": 0.80,
  "title": "Division in unconstrained function `compute_share` produces nondeterministic witness",
  "template": "compute_share",
  "signal": "share",
  "line": 3,
  "description": "Operation `share = total / participants` in unconstrained function `compute_share` uses division. The quotient is a witness value computed outside the circuit, so the prover can supply any result without constraint verification.",
  "recommendation": "Add an assertion to verify the quotient: `assert(quotient * divisor == dividend);` and ensure the divisor is non-zero: `assert(divisor != 0);`"
}