Non-dominating RangeCheck removes sibling-branch truncate in Brillig

Summary

The remove_truncate_after_range_check SSA optimization pass can silently delete a truncate instruction in a Brillig (unconstrained) function when a RangeCheck exists in a non-dominating sibling branch. This is a proof-soundness vulnerability: inputs that should be rejected by caller-side ACIR constraints become provable.

Details

remove_truncate_after_range_check (compiler/noirc_evaluator/src/ssa/opt/remove_truncate_after_range_check.rs:28) maintains a function-wide HashMap<ValueId, u32> that records every RangeCheck it encounters while walking blocks in reverse post-order. When a later Truncate on the same ValueId has a compatible bit size, it is removed unconditionally — with no check that the RangeCheck dominates the Truncate.

For ACIR functions this is harmless because flatten_cfg (compiler/noirc_evaluator/src/ssa/opt/flatten_cfg.rs:184) eliminates all branching before this pass runs. But flatten_cfg explicitly skips Brillig functions, so if/else diamonds survive into remove_truncate_after_range_check.

The RPO walk order is determined by BTreeSet-ordered CFG successors (compiler/noirc_evaluator/src/ssa/ir/cfg.rs:19). When the block containing the RangeCheck has a higher block ID than its sibling, RPO visits it first. The RangeCheck is recorded, and the sibling's Truncate on the same value is then incorrectly removed.

The pass was introduced in #7832 to optimize the straight-line pattern assert_max_bit_size followed by as uN. Its tests only cover single-block and linear-CFG cases. The Brillig multi-block case was not considered.

PoC

Nargo.toml

[package]
name = "truncate_bug"
type = "bin"
authors = ["test"]

[dependencies]

src/main.nr

unconstrained fn helper(cond: bool, x: Field) -> Field {
    if cond {
        (x as u8) as Field
    } else {
        x.assert_max_bit_size::<8>();
        0
    }
}

fn main(cond: bool, x: pub Field) {
    let y = unsafe { helper(cond, x) };
    assert(y == x);
}

Prover.toml

cond = true
x = "300"

test_bug.sh

#!/usr/bin/env bash
set -euo pipefail

cd "$(dirname "$0")"

NARGO="${NARGO:-nargo}"

echo "Compiling..."
"$NARGO" compile

echo "Executing (should fail with assertion error)..."
if "$NARGO" execute; then
    echo "BUG: execution succeeded, truncate was incorrectly removed"
    exit 1
else
    echo "PASS: execution failed as expected"
    exit 0
fi

Expected behavior: nargo execute fails. (300 as u8) truncates to 44, so assert(44 == 300) should reject.

Actual behavior: nargo execute succeeds. The optimizer removes the truncate in the then branch because it sees the sibling else branch's RangeCheck first in RPO. The compiled helper returns 300 untruncated on the then path, so assert(300 == 300) passes.

Compiling with --show-ssa confirms the truncate disappears at the "Removing Truncate after RangeCheck" step:

// Before (step 61):
b1():
    v4 = truncate v1 to 8 bits, max_bit_size: 254
    jmp b3(v4)

// After (step 62):
b1():
    jmp b3(v1)    // truncate removed, raw v1 passed through

Impact

This is a proof-soundness vulnerability. The optimizer silently rewrites a Brillig function so that a value bypasses truncation. When the caller constrains the Brillig result in ACIR (the documented safe usage pattern per unconstrained.md), the constraint checks a corrupted value and accepts inputs that should be rejected.

An adversary who crafts inputs triggering the then branch can produce a valid proof for a statement that does not hold at the source-code level — the truncation that the developer wrote is silently erased by the compiler.

Affected versions: All versions since #7832 (merged March 2025).

Mitigating factors:

• The pattern requires assert_max_bit_size and a numeric cast on the same Field value in sibling branches of a single unconstrained function. This is not a common idiom.
• A search of all public Noir repositories on GitHub and the full aztec-packages codebase found no instances of this pattern in production code.
• Only specific block ID orderings trigger the bug (the RangeCheck block must be visited first in RPO).

Recommended fix: Make the pass dominance-aware. Only remove a Truncate when the supporting RangeCheck's block dominates the Truncate's block. Alternatively, skip Brillig functions entirely in this pass.