Prover-Controlled Loop Bound

Overview

Remediation Guide: How to Fix Prover-Controlled Loop Bounds

The prover-controlled loop bound detector identifies for and while loops in Circom circuits where the loop condition references a signal that is not constrained by any === or <== expression. In ZK circuits, the prover controls witness computation. If a loop’s iteration count depends on an unconstrained signal, the prover can choose how many iterations run, producing incorrect results that the verifier cannot detect.

This is distinct from standard under-constrained signal detection because the impact is amplified: rather than a single signal being forgeable, the prover controls the structure of the computation — which operations execute and which are skipped.

Why This Is an Issue

Circom compiles loops into a fixed number of constraint rows determined at compile time. However, the witness generator evaluates the loop condition at proving time using the prover-supplied signal values. If the bound signal is unconstrained, the prover can manipulate which iterations execute during witness generation without violating any constraint.

Consider a summation circuit: for (var i = 0; i < n; i++) { acc += values[i]; }. If n is unconstrained, the prover can set n = 0 to skip the entire loop, or n = 1 to sum only the first element, regardless of how many elements should be summed. The resulting acc value feeds into constraints, but those constraints only verify that acc equals what was computed — not that the computation was correct.

How to Resolve

Use constants or template parameters for loop bounds. If the bound must come from a signal, constrain that signal.

// Before: Vulnerable -- signal-dependent loop bound
template SumN() {
    signal input n;
    signal input values[100];
    signal output sum;
    var acc = 0;
    for (var i = 0; i < n; i++) {  // n is unconstrained!
        acc += values[i];
    }
    sum <== acc;
}

// After: Fixed (Option 1) -- use a template parameter
template SumN(N) {
    signal input values[N];
    signal output sum;
    var acc = 0;
    for (var i = 0; i < N; i++) {  // N is a compile-time constant
        acc += values[i];
    }
    sum <== acc;
}

// After: Fixed (Option 2) -- constrain the signal
template SumN() {
    signal input n;
    signal input values[100];
    signal output sum;
    n === 50;  // constrained to a known value
    var acc = 0;
    for (var i = 0; i < n; i++) {
        acc += values[i];
    }
    sum <== acc;
}

Examples

Vulnerable Code

template SelectiveHash() {
    signal input count;
    signal input data[32];
    signal output hash;

    var acc = 0;
    for (var i = 0; i < count; i++) {
        acc += data[i];
    }
    hash <== acc;
    // The prover controls `count`, so they can hash
    // any subset of the data array
}

template DynamicLoop() {
    signal input limit;
    signal output result;
    var acc = 0;
    while (acc < limit) {
        acc += 1;
    }
    result <== acc;
    // The prover controls when the while loop terminates
}

Fixed Code

template SelectiveHash(N) {
    signal input data[N];  // N is a template parameter (compile-time)
    signal output hash;

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

Sample Sigvex Output

CRITICAL  prover-controlled-loop-bound
  Loop bound depends on unconstrained signal: count

  A loop in template `SelectiveHash` at line 7 has a bound that references signal
  `count`, which is not constrained by any `===` or `<==` expression. Since the
  prover controls witness computation, a malicious prover can choose how many
  iterations the loop executes, potentially producing incorrect results that the
  verifier cannot detect. This enables proof forgery.

  Template: SelectiveHash
  Signal:   count
  Line:     7
  Confidence: 0.92

  Recommendation: Ensure the loop bound signal is constrained:
    1. Add a constraint: `n === expected_value;`
    2. Use a constant or template parameter for the loop bound instead of a signal.
    3. If the signal must be dynamic, constrain the loop result:
       `result === expected_computation(n);`

Detection Methodology

The detector combines source text scanning with parsed constraint analysis:

1. Source scanning: scans raw Circom source lines within each template’s brace-delimited scope for for and while loop patterns. For for loops, the condition (second clause between semicolons) is extracted. For while loops, the parenthesized condition is extracted. Parenthesis balancing handles nested expressions.

2. Signal resolution: signal names from the condition expression are extracted using word-boundary tokenization. Each extracted name is checked against the template’s declared signals (inputs, outputs, intermediates). Names that are not declared signals (e.g., var counters like i, constants like 10) are ignored.

3. Constraint check: for each signal found in a loop condition, the detector checks whether that signal appears in any === or <== expression in the template. If it does not, the signal is unconstrained and the loop bound is prover-controlled.

Template boundaries are determined by tracking brace depth from the template declaration line.

Limitations

• Source-text scanning: the detector scans the raw source for loop patterns rather than analyzing an AST. Multi-line loop headers may not be recognized.
• Does not detect indirect signal dependency. If limit <-- n * 2 and the loop uses limit, the detector checks limit against constraints but does not trace back to n.
• Cannot detect prover influence through control flow. If the loop bound is a constant but a conditional branch (controlled by an unconstrained signal) determines which loop executes, this is not caught.
• Circom-only: Noir loops are checked at the language level and typically use bounded iteration, so this detector focuses on Circom.

Related Detectors

• under-constrained-signal — general under-constrained signal detection
• unconstrained-public-input — public inputs without constraints
• unconstrained-output — output signals without constraints

References

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