feat(ssa): elide overflow check dominated by a later checked add (#7161) - #13315
Draft
jeswr wants to merge 1 commit into
Draft
feat(ssa): elide overflow check dominated by a later checked add (#7161)#13315jeswr wants to merge 1 commit into
jeswr wants to merge 1 commit into
Conversation
Contributor
|
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. |
Author
@jeswr — draft ready for your review before it goes up. This is a fresh re-derivation of the #7161 dominated-overflow-check elision, gated ACIR-only per the Brillig caveat in the issue body. Measured tables + full soundness argument are in the PR description. It stays a draft until you flip it. |
…r-lang#7161) In ACIR functions, `checked_to_unchecked` now elides the overflow check of an intermediate checked `add` when its single-use result is consumed by a later checked `add` in the same block under the same side-effects predicate (a monotone add chain). Over the field, arithmetic does not wrap: a checked op's overflow is enforced solely by the range check on its result. If `v = a + b` overflows (`a + b >= 2^bit_size`) then any `w = v + z` with `z >= 0` also overflows, so `w`'s range check rejects exactly the inputs `v`'s check would have. The accepted-witness set and observable outputs are unchanged, and one range decomposition is saved per elided intermediate check. The reasoning is ACIR-specific and the pass is gated to ACIR functions (mirroring `check_u128_mul_overflow` and the other passes that reason about the ACIR-vs-Brillig overflow split). In Brillig, integer arithmetic wraps at `bit_size` and a checked op traps at its own location, so eliding an intermediate check would change the observable failure point; Brillig functions keep every check and execute identically. Soundness guards for eliding an intermediate add `v`: - `v` is used exactly once across the function (no leak of the un-range-checked value into any other instruction, terminator or return); - that use is an operand of a checked `add` in the same block and under the same predicate epoch (an `EnableSideEffectsIf` between them prevents elision); - `v` is unsigned and the dominating consumer is an `add` (monotone; `mul`/`sub` are excluded). Measured (bb gates -s ultra_honk, before -> after): focused fixture 2777 -> 2772; no package regresses. ACIR opcodes drop on several real circuits (e.g. -11 / -10 / -10 on chained-arithmetic kernels) though the backend's redundant-range optimizer absorbs some of those at the gate level. Compile time on sha512_100_bytes is within noise. This change was developed with support from generative AI. I am currently reviewing it before requesting maintainer review. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
jeswr
force-pushed
the
feat/elide-overflow-check-dominated
branch
from
July 10, 2026 05:22
ef30ba8 to
d4bec64
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Addresses #7161. In ACIR functions,
checked_to_uncheckedelides the overflow check of an intermediate checkedaddwhose single-use result feeds a later checkedaddin the same block (a monotone add chain): over the field, if the intermediate overflows so does the dominating add, so the later range check rejects exactly the same inputs. Gated to ACIR because Brillig wraps and traps per-op, so eliding would move the failure point (the Brillig caveat noted in the issue) — mirrorscheck_u128_mul_overflow.Measured (
bb gates -s ultra_honk, before → after; basebeta.22 0df14918):Caveat: on some circuits the eliminated checks are already absorbed by the ACVM
redundant_rangeoptimizer + backend, so the ACIR drop doesn't always reach the gate count; no circuit regresses, andsha512_100_bytescompile time is within noise.Soundness argument + guards
An intermediate add
vis elided only when:vis used exactly once (no leak of the un-range-checked field value), that use is an operand of a checkedaddin the same block under the same side-effects predicate (anEnableSideEffectsIfbetween the two prevents elision),vis unsigned, and the dominating consumer is anadd(mul's other operand may be0;subisn't monotone). New unit tests cover the positive chains and each negative case;cargo test -p noirc_evaluatoris green; the existingopt/hint.rsfixture (a 5-add chain) exercises it and its snapshot is updated.