Field Underflow Subtraction

Overview

Remediation Guide: How to Fix Field Underflow in Subtraction

The field underflow subtraction detector flags unconstrained assignments (<--) whose expression subtracts one signal from another, where the result signal carries no range constraint. Circuit arithmetic is modular: there are no negative numbers in a prime field. If a < b, the value a - b does not fail or clamp to zero — it wraps to p - (b - a), a number close to the field modulus (roughly 2^254 for BN254).

Developers reading balance - amount as integer arithmetic expect underflow to be impossible or to error out. In a circuit, it silently succeeds and produces a huge field element that passes any check not specifically designed to catch it.

Why This Is an Issue

Wrap-around subtraction is the field-arithmetic version of an unchecked integer underflow, and its consequences are similar: balance and allowance logic breaks first. A circuit computing remaining <-- balance - withdrawal without range constraints lets a prover withdraw more than the balance; remaining wraps to an astronomically large value, and unless a later constraint independently range-checks it, the witness verifies. Comparators are not a backstop by default — circomlib’s LessThan(n) is only sound for operands under n bits, and a wrapped value near the modulus is far outside that range, so comparisons on it can be gamed too.

The detector focuses on the <-- case because that is where no constraint exists at all; the wrapped value flows onward with nothing in the R1CS system recording how it was produced.

How to Resolve

Range-constrain the subtraction result so that wrap-around values cannot satisfy the circuit, and enforce the ordering assumption explicitly.

// Before: underflow wraps silently
signal remaining;
remaining <-- balance - withdrawal;

// After: enforce ordering, then bind the result
component ok = LessEqThan(64);
ok.in[0] <== withdrawal;
ok.in[1] <== balance;
ok.out === 1;                     // withdrawal <= balance, proven

remaining <== balance - withdrawal;

component bits = Num2Bits(64);    // remaining fits in 64 bits
bits.in <== remaining;

With the ordering constraint in place, balance - withdrawal cannot wrap, and the Num2Bits decomposition rejects any witness where it somehow did.

Examples

Vulnerable Code

template Withdraw() {
    signal input balance;
    signal input amount;
    signal output remaining;

    // If amount > balance, remaining wraps to ~2^254
    remaining <-- balance - amount;
}

Fixed Code

template Withdraw() {
    signal input balance;
    signal input amount;
    signal output remaining;

    component le = LessEqThan(64);
    le.in[0] <== amount;
    le.in[1] <== balance;
    le.out === 1;

    remaining <== balance - amount;

    component range = Num2Bits(64);
    range.in <== remaining;
}

Sample Sigvex Output

HIGH  field-underflow-subtraction
  Assignment `remaining <-- balance - amount` contains subtraction between
  signals. In finite field arithmetic, if the minuend is smaller than the
  subtrahend, the result wraps around the field modulus to a very large
  value. Without a range constraint on `remaining`, this could be exploited.

  Template: Withdraw
  Signal:   remaining
  Confidence: 0.65

Detection Methodology

The detector inspects each template’s unconstrained assignments for subtraction between signals (constant-only subtractions are ignored, since their outcome is fixed). It then collects the template’s range-constrained signals — those passed through bit decompositions or recognized range-check components — and reports the assignment only when the result signal is not in that set. Findings carry 0.65 confidence, reflecting that an ordering guarantee may exist in a form the analysis does not recognize. The circuit’s field is inferred from pragmas (BN254 by default), which determines the wrap-around magnitude reported.

Limitations

Ordering constraints enforced in a parent template, or through custom comparator components the detector does not recognize, are invisible — these cases produce false positives.
Only direct subtraction inside <-- expressions is inspected; a subtraction computed in a constrained assignment and later weakened by other logic is out of scope for this check.
The range-check recognition is pattern-based; unconventional range proofs may not be credited.

Field Overflow — multiplicative chains and exponentiation exceeding the field modulus
Range Check — signals used as small integers without range constraints
Unsafe Comparison — comparators applied to operands that may exceed their bit width