Witness Complexity

Overview

The witness complexity detector flags unconstrained (<--) assignments whose right-hand side combines multiple nondeterministic operators into a single expression. The assumption behind a <-- assignment is that the author will follow it with enough === constraints to re-derive the value from verifier-visible inputs. In practice, the more operators the expression contains — divisions, modulos, comparisons, bit extractions, conditional branches — the harder it is to write a constraint set that fully pins the result.

Complexity is measured along two axes. The first is the count of nondeterministic operators; a single division is ordinary, a division followed by a modulo followed by a comparison is a warning. The second is the nesting depth: expressions that feed one nondeterministic operator into another typically require a cascade of constraints in the reverse order, and authors frequently constrain only the outermost step.

The detector does not try to prove that constraints are missing. It reports assignments that look risky enough to deserve manual review, and ranks them by the estimated number of constraints a complete rebinding would require.

Why This Is an Issue

Every nondeterministic step in a witness expression adds one more obligation on the author. A simple division needs q * b === a and a range check on the remainder. A modulo adds a second range check. A comparison adds a bit-decomposition constraint. When all three appear in the same line, the required constraint block is half a dozen lines long and is almost always the first thing that gets trimmed during refactoring.

The resulting circuits tend to have a characteristic shape: the <-- line survives every rewrite, but the constraints beneath it drift out of sync with the witness computation. Reviewers focus on the visible expression and miss the missing constraints, because the expression “looks complicated, so presumably the author thought about it.” That presumption is exactly what the detector challenges.

How to Resolve

Decompose the complex expression into a sequence of one-operator steps, and attach the appropriate constraint to each step.

// Vulnerable: five operators, one line, unclear constraint obligations
template Complex() {
    signal input a;
    signal input b;
    signal input c;
    signal input d;
    signal input e;
    signal output r;
    r <-- ((a * b) / c + d) % e;
}

// Fixed: each nondeterministic step has its own constraint
template Complex() {
    signal input a;
    signal input b;
    signal input c;
    signal input d;
    signal input e;
    signal output r;

    signal ab;
    ab <== a * b;                     // deterministic, constrained directly

    signal q;
    signal rem1;
    q <-- ab \ c;                     // integer division hint
    rem1 <-- ab % c;
    ab === q * c + rem1;
    // + range checks: rem1 < c, c != 0 (see related detectors)

    signal sum;
    sum <== q + d;

    signal q2;
    q2 <-- sum \ e;
    r  <-- sum % e;
    sum === q2 * e + r;
    // + range checks: r < e, e != 0
}

Examples

Sample Sigvex Output

{
  "detector": "witness-complexity",
  "severity": "high",
  "confidence": 0.70,
  "title": "High-complexity unconstrained assignment",
  "template": "Complex",
  "signal": "r",
  "line": 12,
  "operators": ["*", "/", "+", "%"],
  "depth": 4,
  "description": "Unconstrained assignment combines four nondeterministic or arithmetic operators at depth 4. A full rebinding would require at least five accompanying constraints; only zero were found on this signal.",
  "recommendation": "Split the expression into single-operator steps and constrain each step explicitly."
}

Detection Methodology

The right-hand side of every <-- assignment is parsed into an operator tree. The detector counts nondeterministic operators (/, %, <, >, ==, !=, ternary) and the maximum depth of the tree, then computes a complexity score. Assignments above a tunable threshold are kept for the next stage.

For each candidate the detector walks the template body and counts constraints that reference the assigned signal. It compares that count against the minimum number of constraints required to rebind an expression of the given shape, derived from a small table of per-operator obligations. A candidate is reported when the count of actual constraints is lower than the minimum, weighted by confidence in how the constraints map to operators.

Limitations

• Complexity is a heuristic; circuits that legitimately need elaborate witness code (for example, elliptic-curve point addition with a single final ===) may be flagged.
• The operator-to-constraint table covers common patterns only; bespoke constraint shapes may be undercounted and produce false positives.
• Function calls in the witness expression are not expanded, so operators hidden behind a helper function are not counted.

Related Detectors

• Nondeterministic Witness — individual nondeterministic operators in <--
• Division by Zero — divisors that lack a non-zero binding
• Under-Constrained Signal — signals missing any constraint

References

• Circom Documentation: Signals
• iden3/circomlib
• Pailoor, S., Wang, Y., Wang, X., Dillig, I. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IACR ePrint 2023/512.