Field Underflow Subtraction Remediation

Overview

Related Detector: Field Underflow Subtraction

In a prime field there is no negative result: a - b with a < b wraps to p - (b - a), a value near the field modulus. A subtraction that models balances, quantities, or deadlines must therefore prove two things the field does not give for free: that the minuend is at least the subtrahend, and that the result fits the intended bit width. Both are one comparator and one bit decomposition away.

Recommended Fix

Before (Vulnerable)

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

    // amount > balance wraps remaining to ~2^254 and still verifies
    remaining <-- balance - amount;
}

After (Fixed)

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

    // 1. Operands must fit the comparator's bit width
    component balBits = Num2Bits(64);
    balBits.in <== balance;
    component amtBits = Num2Bits(64);
    amtBits.in <== amount;

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

    // 3. Bind the result — cannot wrap given (2)
    remaining <== balance - amount;
}

Step 1 makes the comparison sound (LessEqThan(n) assumes n-bit operands), step 2 rules out the wrap-around case, and step 3 uses <== so the subtraction itself is part of the constraint system. Given 64-bit operands and amount <= balance, the difference is provably a 64-bit value.

Alternative Mitigations

Range-check the result instead of the operands. Where the ordering is guaranteed elsewhere, Num2Bits(64) on the result alone rejects wrapped witnesses, since p - x for small x never fits in 64 bits. This is weaker documentation of intent but fewer constraints.
Signed representation. If negative differences are legitimate (profit/loss, deltas), encode sign explicitly — e.g., compute diff = a + OFFSET - b with a fixed offset and range-check against 2 * OFFSET — rather than letting the field’s wrap-around stand in for a sign bit.
Constrain at the boundary. For values arriving from public inputs or hashes, apply the range check once at circuit entry; downstream subtractions between checked values then only need the ordering constraint.

Common Mistakes

Mistake: Comparing Unranged Field Elements

component le = LessEqThan(64);
le.in[0] <== amount;      // WRONG if amount was never range-checked:
le.in[1] <== balance;     // a wrapped 254-bit value breaks the comparator
le.out === 1;

The comparator’s soundness contract is “operands < 2^64”. Enforce it with Num2Bits before trusting the comparison.

Mistake: Guarding in Witness Code Only

remaining <-- (amount <= balance) ? balance - amount : 0;  // prover-controlled

A conditional inside <-- is not a constraint — the prover can ignore it. The guard must be a constrained comparator with === 1.