Witness Complexity Remediation

Overview

Related Detector: Witness Complexity

Complex unconstrained assignments (<--) with multiple operations (division, comparison, modular arithmetic) are difficult to constrain correctly. The more operations in a single witness computation, the wider the gap between what the prover computes and what the constraints verify. The fix is to decompose complex computations into individual steps, each with its own constraint.

Recommended Fix

Before (Vulnerable)

template UnsafeCompute() {
    signal input a, b, c, d, e;
    signal output result;

    // Five operations in one unconstrained assignment
    result <-- ((a * b) / c + d) % e;
    // Writing a single constraint for this is error-prone
}

After (Fixed — Step-by-Step Decomposition)

template SafeCompute() {
    signal input a, b, c, d, e;
    signal output result;

    // Step 1: Multiply
    signal ab;
    ab <== a * b;

    // Step 2: Divide (with remainder constraint)
    signal quotient;
    signal remainder;
    quotient <-- ab / c;
    remainder <-- ab % c;
    ab === quotient * c + remainder;

    // Range check remainder
    component ltRem = LessThan(252);
    ltRem.in[0] <== remainder;
    ltRem.in[1] <== c;
    ltRem.out === 1;

    // Step 3: Add
    signal sum;
    sum <== quotient + d;

    // Step 4: Modulo (with remainder constraint)
    signal modQuot;
    signal modRem;
    modQuot <-- sum / e;
    modRem <-- sum % e;
    sum === modQuot * e + modRem;

    component ltMod = LessThan(252);
    ltMod.in[0] <== modRem;
    ltMod.in[1] <== e;
    ltMod.out === 1;

    result <== modRem;
}

Alternative Mitigations

1. Use Library Components for Standard Operations

Replace hand-written arithmetic with audited library components:

// Instead of manual division with remainder checking,
// use a well-tested DivMod component if available.
component div = IntegerDivision(nBits);
div.dividend <== a;
div.divisor <== b;
signal quotient;
quotient <== div.quotient;

2. Verify Output Against Known Relationship

When full decomposition is impractical, compute the result in witness generation and verify it against a higher-level property:

signal result;
result <-- complexFunction(a, b, c);
// Verify: result satisfies the expected relationship
result * c + remainder === a * b;
// Must also range-check remainder

3. Split Into Sub-Templates

Encapsulate each operation in a dedicated template:

template SafeDivMod() {
    signal input dividend;
    signal input divisor;
    signal output quotient;
    signal output remainder;

    quotient <-- dividend / divisor;
    remainder <-- dividend % divisor;
    dividend === quotient * divisor + remainder;

    component lt = LessThan(252);
    lt.in[0] <== remainder;
    lt.in[1] <== divisor;
    lt.out === 1;
}

Common Mistakes

Constraining only the final result: Writing one constraint for a five-operation computation almost certainly leaves intermediate values unconstrained. The prover can find alternative paths to the same final result.

Forgetting range checks on division remainders: The constraint a === q * b + r has multiple solutions in finite fields. Without r < b, the prover can choose any (q, r) pair that satisfies the equation.

Assuming multiplication is safe without decomposition: While a * b can be expressed as a single R1CS constraint, chaining it with other operations (e.g., a * b / c) requires intermediate signals to maintain constraint coverage.

References

• Circom Documentation: Signals and Constraints
• circomlib GitHub repository — reference implementations of constrained arithmetic
• Pailoor, S. et al. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IEEE S&P 2023.