Nondeterministic Witness

Overview

The nondeterministic witness detector finds <-- assignments whose right-hand side uses an operator the verifier cannot audit — division, modulo, integer comparison, bit extraction, or a conditional — and whose result is not pinned by a later constraint. The purpose of <-- in Circom is to let the author compute a value for the witness and then, in the same template, write one or more === constraints that re-derive the value from verifier-visible inputs. When the re-derivation is missing, the result behaves exactly like an unconstrained signal and the prover chooses it freely.

Unlike the generic under-constrained detector, this check focuses on the operators that make constraint obligations non-obvious. A plain q <-- a * b is deterministic: if the author wrote it at all, they almost certainly meant q === a * b. A q <-- a / b, by contrast, is valid in infinitely many ways — any q that combines with a carefully chosen remainder to satisfy a == q*b + r works — and the author must explicitly choose which semantics they want (Euclidean quotient, field inverse, fractional representative, etc.). The detector looks for such operators and reports them when no matching constraint follows.

Why This Is an Issue

The verifier only sees the R1CS. It never executes <-- assignments and does not know what the author intended. When the right-hand side of <-- involves a multi-valued operation, the only thing that makes the computation “correct” is the constraint block that follows it. If that block is missing, partially written, or written against a different variable, the circuit silently accepts whatever value the prover picked during witness generation.

This is the most common cause of under-constrained bugs in Circom audits. It is easy to write, easy to miss in review, and the failure mode is invisible until somebody constructs a hostile witness.

How to Resolve

Follow each nondeterministic <-- with a constraint block that rebinds the result using constrained inputs. For integer division the canonical block is a quotient-plus-remainder equality combined with a range check on the remainder.

// Vulnerable: quotient is unbound
template IntDiv() {
    signal input a;
    signal input b;
    signal output q;
    q <-- a \ b;
}

// Fixed: quotient and remainder are both constrained
template IntDiv(nBits) {
    signal input a;
    signal input b;
    signal output q;
    signal r;

    q <-- a \ b;
    r <-- a % b;

    a === q * b + r;              // binds q given b and r

    component lt = LessThan(nBits);
    lt.in[0] <== r;
    lt.in[1] <== b;
    lt.out === 1;                 // r < b

    // + b != 0 (see division-by-zero detector)
}

Examples

Sample Sigvex Output

{
  "detector": "nondeterministic-witness",
  "severity": "high",
  "confidence": 0.85,
  "title": "Nondeterministic `/` in `<--` assignment has no rebinding constraint",
  "template": "IntDiv",
  "signal": "q",
  "line": 8,
  "operator": "/",
  "description": "Assignment `q <-- a / b` uses a multi-valued operator. No constraint in `IntDiv` of the form `a === q * b + r` or `q * b === a` binds `q` back to verifier-visible inputs.",
  "recommendation": "Add a quotient-remainder constraint and a range check on the remainder, or wire the division through a dedicated helper template."
}

Detection Methodology

For each <-- assignment the detector classifies the RHS operators into deterministic (+, -, *, constants, already-constrained signals) and nondeterministic (/, \, %, <, >, <=, >=, ==, !=, ternary, bit extraction). If any nondeterministic operator is present, the assigned signal is added to a candidate list along with the operator kind.

A second pass walks the template’s constraint list and tries to match each candidate to a rebinding pattern. The pattern catalogue is keyed by operator: integer division expects a === q * b + r plus a remainder range check, modulo reuses the same pattern, comparisons expect the LessThan-style boolean-plus-bit-decomposition shape, and ternaries expect the linear-combination selector shape. Candidates without a matching pattern are reported, with confidence proportional to how clearly the catalogue entry was matched (none, partial, structural).

Limitations

• Rebindings written in a helper function that is called after the <-- are recognised only when the helper is inlined by the front-end.
• Chained nondeterministic operators (for example q <-- (a / b) % c) are reported as a single finding even when two distinct constraint blocks would be needed; the report lists both operators.
• Constraints placed in a sibling template and transported through wiring are not attributed to the original <--, which can cause false positives in heavily decomposed circuits.

Related Detectors

• Nondeterministic Control — ternary and conditional hints in witness code
• Division by Zero — divisors without non-zero bindings
• Under-Constrained Signal — signals with no binding at all

References

• Circom Documentation: Signals and Constraints
• iden3/circomlib
• Pailoor, S., Wang, Y., Wang, X., Dillig, I. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IACR ePrint 2023/512.
• Bailey, B., Miller, A. “An Empirical Study of ZK Circuit Bugs.” IACR ePrint 2023/190.