Signal as Array Index

Overview

The signal-as-array-index detector finds expressions of the form arr[idx], where arr is a signal array and idx is a signal, inside the right-hand side of a witness assignment. In Circom, signal-indexed array reads are legal during witness generation but cannot be compiled into a static R1CS: the constraint system is fixed before the witness is known, so there is no way to encode “the element selected depends on a signal” without expanding the read into a multiplexer circuit.

When authors write result <-- arr[idx] directly, the compiler records the witness-time lookup but emits no constraint that ties result to a particular entry of arr. The prover, who knows which entry they want to be “selected”, can write any value into result — the witness is still consistent with the <-- semantics, and nothing in the circuit disagrees. The correct pattern is to instantiate a multiplexer component (such as Mux1, MultiMux, or QuinSelector) that reads all array entries through constrained assignments and exposes a single output governed by idx.

Why This Is an Issue

The security property an author expects from arr[idx] is “the output equals the element at position idx”. The circuit enforces neither half of that statement: it does not check that idx is in range, and it does not check that the chosen element actually came from arr. The prover is free to return any field element as result, and the proof verifies.

This is a common root cause of stolen-funds bugs in circuits that represent per-account state as arrays. The circuit appears to look up a balance by account index, but in fact lets the prover name any balance they please.

How to Resolve

Replace the direct index with a multiplexer that reads every element and selects among them with constrained arithmetic. Combine this with a range check on the index if it is not already bounded.

// Vulnerable: prover-chosen element, prover-chosen index
template Lookup(N) {
    signal input arr[N];
    signal input idx;
    signal output result;
    result <-- arr[idx];
}

// Fixed: constrained multiplexer with a bounded index
template Lookup(N) {
    signal input arr[N];
    signal input idx;
    signal output result;

    // 1. Bound idx to [0, N).
    component bound = Num2Bits(8);  // assuming N < 256
    bound.in <== idx;

    // 2. Build a one-hot selector: sel[i] = 1 iff i == idx.
    signal sel[N];
    var acc = 0;
    for (var i = 0; i < N; i++) {
        sel[i] <-- (i == idx) ? 1 : 0;
        sel[i] * (sel[i] - 1) === 0;      // sel[i] boolean
        sel[i] * (idx - i) === 0;         // sel[i] == 1 ⇒ idx == i
        acc += sel[i];
    }
    acc === 1;                            // exactly one selector set

    // 3. result = Σ sel[i] * arr[i]
    var sum = 0;
    for (var i = 0; i < N; i++) {
        sum += sel[i] * arr[i];
    }
    result <== sum;
}

Examples

Sample Sigvex Output

{
  "detector": "signal-array-index",
  "severity": "high",
  "confidence": 0.88,
  "title": "Unconstrained signal `idx` used as array index",
  "template": "Lookup",
  "signal": "idx",
  "line": 7,
  "description": "Expression `arr[idx]` is evaluated during witness generation but no multiplexer or selector constraints bind the result to the entry at position `idx`. The prover can return any value as `result`.",
  "recommendation": "Replace the direct lookup with a one-hot selector or a `Mux` / `QuinSelector` component, and range-check `idx`."
}

Detection Methodology

The detector visits every expression inside <-- and <== assignments and looks for array subscripts whose index is a signal or a signal-derived expression. When found, it records the array, the index, and the assignment target.

For each flagged access it then searches the enclosing template for structural evidence of a multiplexer: a loop that reads each entry of arr through <==, a set of boolean-constrained selector signals, and a linear combination that reduces to a single element. If such a pattern exists and covers the flagged index, the finding is suppressed. Otherwise it is reported, with confidence weighted by whether the index has any range constraint at all.

Limitations

• Multiplexers built from unusual constraint shapes (for example, product trees instead of one-hot sums) may not be recognised and can produce false positives.
• Two-dimensional array reads are analysed element by element; nested signal-indexed reads share the same finding rather than being reported per-dimension.
• Array writes indexed by a signal are out of scope for this detector; they are covered by the unconstrained-output detector.

Related Detectors

• Under-Constrained Signal — signals with no binding constraint
• Missing Range Check — indices and other values lacking a bit-width bound
• Nondeterministic Witness — other forms of prover-chosen values

References

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