feat(ssa): remove range checks and unsigned lt comparisons implied by a dominating bound

[jeswr]

Description

This change was developed with support from generative AI; I am reviewing it as the PR author before requesting maintainer review.

Summary

Adds a remove_redundant_range_checks SSA pass (issue #9463): it tracks, per value, the smallest exclusive upper bound proven by a dominating fact — a range_check (value < 2^N), a constrain (lt value, c) == u1 1 (value < c), or an unsigned mod by a non-zero constant (result < c, recorded only under a constant-true side-effects condition since ACIR-gen predicates the division) — and removes range_checks and unsigned lt-against-constant comparisons that a dominating fact already implies. Only range_check-derived facts may elide another range_check, so the narrowing-cast validation rule keeps a visible justification in the SSA. Runs right after remove_truncate_after_range_check, reusing its dominance/map-clearing discipline.

Measured (bb 5.0.0-nightly.20260522, bb gates -s ultra_honk; ACIR opcodes via nargo info --force):

Program	ACIR opcodes	UltraHonk circuit_size
vector_dynamic_index (existing test)	733 → 616 (−16.0%)	5047 → 4772 (−5.4%)
redundant_range_check_elision (new fixture)	41 → 33 (−19.5%)	2889 → 2879

Across the full execution_success suite + benchmarks (555 programs): 3 improve in ACIR (vector_dynamic_index −117, lambda_from_array −8, bit_shifts_runtime −5), 3 improve in Brillig opcodes (uhashmap −18, brillig_nested_arrays −9, array_sort −3), none regress. Caveat: an external 39-program corpus of real ZK circuits (fixed-point/IEEE-754/XPath kernels) is unchanged — the win concentrates in code with repeated dynamic-index bounds checks on the same value, where the first check dominates and implies the rest.

Fact sources, guard conditions and measurement notes

Fact sources (each with an SSA-level test)

• range_check value to N bits proves value < 2^N; constrain (lt value, c) == u1 1 proves value < c. Both are enforced unconditionally at ACIR generation (flattening bakes the predicate into their operands), so their bounds hold regardless of the side-effects condition.
• result = mod value, c (unsigned, constant c != 0) proves result < c, but ACIR generation predicates the euclidean division — under a false predicate the remainder is unconstrained — so this bound is only recorded while the side-effects condition is the constant true (tested non-firing under a non-constant predicate).

Guard conditions

• Dominance: same reverse-post-order traversal + bound-map clearing discipline as remove_truncate_after_range_check; a fact only elides an instruction it dominates (tested non-firing across non-dominated blocks).
• Direction: a bound only implies weaker (larger-or-equal) bounds; strictly tighter checks are kept and tighten the map (tested for both lt and range_check).
• range_check elision is restricted to range_check-derived facts: the narrowing-cast validation rule justifies casts by the range checks that remain in the SSA, so a removed check's justification must stay visible as a range_check on the same value; an lt-constraint-derived bound must not elide a range_check (tested non-firing).
• No type-derived facts: a range_check can itself be the instruction that establishes a value's type invariant, so bounds are never derived from types; a fact is learned only when its enforcing instruction is visited, so it can never elide that instruction itself. (Checks implied by a value's statically-known bit width are already removed on insertion via get_value_max_num_bits.)
• Failure ordering unchanged: the dominating fact is enforced earlier on every path and already fails any witness the elided weaker check would have failed.
• Signedness: signed lt orders by signed value, not the representation the bound map tracks, so it is neither learned from nor elided (tested non-firing).

Measurement notes

• vector_dynamic_index repeatedly indexes the same vector with the same witness indices, so each access's bounds comparison after the first is implied by a dominating one; the backend win is real (−275 UltraHonk gates) because the removed comparisons carried gate cost beyond the shared range-table floor.
• Corpus: all 508 execution_success programs + the 9 test_programs/benchmarks programs (sha512_100_bytes 13173 → 13173, semaphore_depth_10 5699 → 5699, bench_eddsa_poseidon 4147 → 4147, bench_poseidon2_hash_100 202 → 202), plus an external corpus of 31 real ZK circuit binaries and 8 library-kernel probes (IEEE-754 double arithmetic, XPath string/numeric kernels, 34–22313 opcodes): all unchanged apart from the 6 programs listed above.
• The fixture's circuit_size barely moves because its removed checks ride on already-present range tables; its win is ACIR opcodes and witness work.

Validation

• New SSA-level tests in the pass cover: duplicate lt constraint removal (keeping the enforcing one), implied lt across a dominated block, tighter-bound non-firing, non-dominating-constraint non-firing, signed non-firing, range_check-implied-by-range_check removal, lt-constraint-must-not-elide-range_check, mod-derived lt removal, mod under a non-constant predicate non-firing, constraint-derived facts under a non-constant predicate.
• cargo nextest run -p noirc_evaluator: 1841 passed (the pre-existing ssa::interpreter::tests::infinite_recursion SIGABRT reproduces identically on unpatched master on this machine, so it is environmental).
• New execution_success/redundant_range_check_elision fixture: all 16 generated harness variants pass (ACIR + --force-brillig × inliner settings, minimal, interpreter, comptime, expand); it keeps a semantically-active reversed-direction control assert.
• cargo fmt / cargo clippy clean; no existing SSA snapshots changed.

Documentation

• No documentation needed (internal SSA optimization).

cc @jeswr for author review.

[github-actions]

Thank you for your contribution to the Noir language.

Please do not force push to this branch after the Noir team have started review of this PR. Doing so will only delay us merging your PR as we will need to start the review process from scratch.

Thanks for your understanding.