Prover-Controlled Loop Bound Remediation

Overview

Related Detector: Prover-Controlled Loop Bound

When a loop’s iteration bound depends on an unconstrained signal, the prover controls how many iterations execute during witness generation. This can produce incorrect results that the verifier cannot detect. The fix is to use compile-time constants for loop bounds or constrain the signal that determines the bound.

Recommended Fix

Before (Vulnerable)

template UnsafeSum() {
    signal input n;          // unconstrained -- prover controls iteration count
    signal input values[100];
    signal output sum;

    var acc = 0;
    for (var i = 0; i < n; i++) {
        acc += values[i];
    }
    sum <== acc;
}

After (Fixed — Template Parameter)

The best fix is to make the loop bound a template parameter, which is resolved at compile time:

template SafeSum(N) {
    signal input values[N];
    signal output sum;

    var acc = 0;
    for (var i = 0; i < N; i++) {
        acc += values[i];
    }
    sum <== acc;
}

// Instantiation -- N is fixed at circuit compilation
component s = SafeSum(50);

Template parameters are constants in the compiled circuit. The prover cannot influence them.

After (Fixed — Constrained Signal)

If the bound must come from a signal (rare, but sometimes needed), constrain it:

template ConstrainedBound() {
    signal input n;
    signal input values[100];
    signal output sum;

    // Constrain n to a known value
    n === 50;

    var acc = 0;
    for (var i = 0; i < n; i++) {
        acc += values[i];
    }
    sum <== acc;
}

Or constrain it indirectly by including it in a verifiable computation:

template ConstrainedBoundIndirect() {
    signal input n;
    signal input values[100];
    signal output sum;

    var acc = 0;
    for (var i = 0; i < n; i++) {
        acc += values[i];
    }
    sum <== acc;

    // Constrain: n participates in a verifiable relationship
    sum <== n * (n - 1) / 2;  // only valid if values[i] == i
}

Alternative Mitigations

1. Fixed Upper Bound with Masking

Process all elements up to a fixed maximum, using a mask signal to select active elements:

template MaskedSum(MAX_N) {
    signal input values[MAX_N];
    signal input active[MAX_N];  // 1 if element is active, 0 otherwise
    signal output sum;

    var acc = 0;
    for (var i = 0; i < MAX_N; i++) {
        // active[i] is constrained to be 0 or 1
        active[i] * (1 - active[i]) === 0;
        acc += values[i] * active[i];
    }
    sum <== acc;
}

This iterates a fixed number of times (MAX_N is a template parameter) but processes only active elements. The prover cannot skip iterations.

2. Constrain the Loop Result

If you cannot constrain the bound directly, constrain the result of the loop computation:

template ResultConstrained() {
    signal input n;
    signal input expected_sum;
    signal input values[100];
    signal output sum;

    var acc = 0;
    for (var i = 0; i < n; i++) {
        acc += values[i];
    }
    sum <== acc;
    sum === expected_sum;  // verifier checks the result
}

This does not prevent the prover from choosing n, but the result must match expected_sum, limiting what the prover can achieve. This is weaker than constraining n directly but may be sufficient depending on the use case.

Common Mistakes

Using var as the bound thinking it’s safe: a var initialized from an unconstrained signal is just as dangerous. The issue is whether the value is constrained, not whether it is a signal or var:

// STILL VULNERABLE: limit comes from unconstrained signal
signal input n;
var limit = n;
for (var i = 0; i < limit; i++) { ... }  // prover controls limit

Constraining the bound after the loop: the constraint must exist in the R1CS, but Circom evaluates constraints after witness generation. A constraint n === 10 placed after the loop still constrains n because R1CS constraints are not ordered. However, placing it before the loop is clearer:

// Works (constraints are unordered in R1CS) but confusing
for (var i = 0; i < n; i++) { ... }
n === 10;

// Clearer
n === 10;
for (var i = 0; i < n; i++) { ... }

Assuming “while” loops are safe: Circom supports while loops, and the same vulnerability applies. If the while condition depends on an unconstrained signal, the prover controls loop termination.

References

• Circom Documentation: Control Flow
• Circom Documentation: Constraint Generation
• circomlib GitHub repository
• Pailoor, S. et al. “Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs.” IEEE S&P 2023.