Missing Range Check

Overview

The missing range check detector finds signals that are handed to a component whose correctness depends on the input fitting in a fixed number of bits, but where no constraint in the enclosing template bounds the signal to that range. Circom operates over a 254-bit prime field, and nothing in the language prevents a signal from taking any value in that field. Components such as LessThan(n), Num2Bits(n), BitDecompose(n), and Sign assume their inputs fit in n bits and produce nonsense — or, worse, arithmetically valid but semantically wrong answers — when that assumption is violated.

The detector works on the call graph of component instantiations. Each known range-sensitive template is annotated with the bit width of each input. For every instantiation, the detector looks at the signal passed to that input and checks whether the signal has been constrained by a Num2Bits, LessThan, or equivalent bounding component earlier in the same template.

Severity is Medium by default. It rises to High when the range-sensitive component is used to gate a transfer amount, a Merkle-tree index, or another security-critical value.

Why This Is an Issue

LessThan(n) works by subtracting its inputs and decomposing the result into n + 1 bits; if the real difference does not fit, the top bit of the decomposition wraps around and the comparator silently returns the wrong boolean. A circuit that believes it has enforced amount < maxAmount may therefore accept values that are much larger than maxAmount but whose two’s-complement-style difference happens to have a zero top bit.

The same class of bug affects Merkle-path indices, RLC accumulators, and bit-packed identifiers. In each case the symptom is identical: honest provers always stay within the intended range, tests pass, and the malicious case only appears when someone deliberately constructs an out-of-range witness.

How to Resolve

Run the signal through an explicit range-bounding component before handing it to the range-sensitive consumer.

// Vulnerable: amount is any field element, LessThan(64) is unsound
template Transfer() {
    signal input amount;
    signal input maxAmount;
    component lt = LessThan(64);
    lt.in[0] <== amount;
    lt.in[1] <== maxAmount;
    lt.out === 1;
}

// Fixed: Num2Bits bounds amount before the comparison
template Transfer() {
    signal input amount;
    signal input maxAmount;

    component bound = Num2Bits(64);
    bound.in <== amount;            // forces amount ∈ [0, 2^64)

    component lt = LessThan(64);
    lt.in[0] <== amount;
    lt.in[1] <== maxAmount;
    lt.out === 1;
}

Examples

Sample Sigvex Output

{
  "detector": "missing-range-check",
  "severity": "medium",
  "confidence": 0.75,
  "title": "`LessThan(16)` input `index` has no range bound",
  "template": "ArrayAccess",
  "signal": "index",
  "line": 12,
  "component": "LessThan",
  "expected_bits": 16,
  "description": "Signal `index` is passed to `LessThan(16).in[0]` but no `Num2Bits(n<=16)` or equivalent constraint applies to it earlier in `ArrayAccess`. Values ≥ 2^16 wrap the comparator and may be incorrectly reported as less than the bound.",
  "recommendation": "Add `component b = Num2Bits(16); b.in <== index;` before the `LessThan` instantiation."
}

Detection Methodology

The detector loads a table of range-sensitive templates and, for each, the bit width of each input port. During circuit traversal it records two things per template body: the set of signals bound by a range component (and the bit width of that binding), and the set of consumer instantiations that need bounded inputs.

After the traversal it joins the two sets. A finding is emitted whenever a consumer input is wired to a signal that either has no recorded bound or whose bound exceeds the consumer’s expected width. Bounds that come from arithmetic derivations (for example, a signal computed as the product of two already-bounded signals) are recognised when the derivation uses only linear combinations with constant coefficients.

Limitations

• Custom range-check templates that do not follow the Num2Bits-style interface are not recognised; their outputs are treated as unbounded.
• Bounds propagated across template boundaries are only tracked one level deep; a signal bounded inside a grandchild component may be reported at the grandparent.
• The detector conservatively reports comparisons between two signals when only one is bounded, even though some use cases are safe.

Related Detectors

• Field Overflow — arithmetic that may exceed the field prime
• Signal as Array Index — indices reaching array accesses without bounds
• Unsafe Comparison — comparators used outside their intended range

References

• Circom Documentation: Signals
• iden3/circomlib: bitify.circom
• iden3/circomlib: comparators.circom
• Bailey, B., Miller, A. “An Empirical Study of ZK Circuit Bugs.” IACR ePrint 2023/190.