fix(acir_gen): only compute a fallback offset for a predicate-gated read - #13477
Draft
AztecBot wants to merge 3 commits into
Draft
fix(acir_gen): only compute a fallback offset for a predicate-gated read#13477AztecBot wants to merge 3 commits into
AztecBot wants to merge 3 commits into
Conversation
`compute_offset` was called for every `array_get` before it was known whether the index would be gated, so a read at a safe index paid for an offset that `get_flattened_index` then discarded — and, when the result type described no field of the element, aborted compilation over an offset it would not have used. The gating decision now picks the offset, so an ungated read never asks for one. The remaining no-match case is reported through `InternalError` rather than `unreachable!`: the SSA type system does not enforce that an `array_get`'s result type is one of the element's fields (`ssa::validation` only checks it when a reference is involved, and deliberately tolerates a numeric mismatch a pass left in code it proved unreachable), so this is reachable enough to deserve a compiler error with a call stack instead of a panic. Also carries the fallback offset out of the gating match in `get_flattened_index`, so an index that was not multiplied by the predicate has no offset in scope to be biased by, and pins two untested properties of the scheme: a safe-index read is never masked, and a repeated field type falls back to its first occurrence.
`regression_NNNN` under `test_programs/` names a noir issue. Both `regression_1601` and `regression_1615` took their number from noir-claude, and both collide with real, unrelated noir issues (#1601 "Remove `examples_failing/pow_const`", #1615 "Refactor Logging to use Brillig"). Name them for what they pin instead, and record the actual issue URLs in the programs' header comments. `regression_11744` keeps its name but gains a note that the number is a PR, not an issue.
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
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.
Follow-up to #13466, addressing review findings from https://gist.github.com/AztecBot/35b0524e4ac8e6274f358243bf8383da. Rebased onto
masterafter #13466 merged.Every existing ACIR snapshot is unchanged, so the generated circuits are byte-identical to what #13466 produces.
1. The ICE surface
#13466 justifies
compute_offset'sunreachable!with "a result type matching no field cannot come out of SSA generation … reachable only through hand-written SSA".ssa/validation/mod.rssays otherwise, in a comment written for exactly this hazard:…and the result-type check it guards only runs
if array_type.contains_reference(). The cited test builds the shape (v5 = array_get v1, index v4 -> u1on a[u8; 2], from an index replaced with a default after a proven overflow); that pass then deletes the instruction, so I have not demonstrated one reaching ACIR gen. But the invariant as stated is not the one the compiler enforces, and #13466 removed the fallback that made a mismatch harmless.Two changes:
handle_array_operationcomputedcompute_offsetfor every read and passed it down, whereconvert_array_operation_inputsdiscarded it for a safe index. So a mismatched read at a constant, in-bounds index — the shape a defaulted index produces — aborted compilation over an offset that would never have been used. It now cannot: an ungated read never asks for one. Pinned bytype_mismatched_safe_array_get_needs_no_fallback_offset.InternalErrorinstead of panicking. Same outcome for a genuinely impossible state, but a compiler error with a call stack rather than a raw panic and backtrace, and consistent with howhandle_array_operationalready reports "should be impossible" states.type_mismatched_array_get_is_an_icebecomes an error assertion instead of#[should_panic].This is a robustness change, not a proof: if anyone demonstrates the shape reaching ACIR gen for real, an error is still the wrong answer there and the fallback would need to mask instead. Also worth deciding whether the SSA-validator rule #13466 deferred is still wanted — I did not add one, since tightening it would reject SSA the validator intends to accept.
2. Tying the bias to the gating decision
The bias's precondition — "the flat index is
raw * predicate" — was violated once inside #13466 itself (its last commit, #13471, plus the twopredicated_vector_constant_index*programs, exists because the bias was landing on an index the constant-index shortcut had already resolved). It was held up only by where the code sits.get_flattened_indexnow carries the offset out of the gating match:An index that took the ungated arm has no offset in scope below and so cannot be biased. Also records why the bias is measured from slot
0on both flat-index paths (element_type_sizes[0]is the start of element 0's first field, and a constant element size scales0to0).3. Test names
regression_NNNNundertest_programs/means a noir issue.regression_1601andregression_1615took their numbers from noir-claude and collide with real, unrelated noir issues — #1601 is "Removeexamples_failing/pow_const", #1615 is "Refactor Logging to use Brillig". Renamed topredicated_composite_get_wide_slotandpredicated_safe_get_stale_predicate, with the real issue URLs in the programs' headers.regression_11744keeps its name and gains a note that the number is a PR, not an issue.4. Coverage and comments
predicated_safe_get_on_heterogeneous_element_is_not_masked: a constant-index read on(u8, Field)under a dynamic predicate reaches its consumer unmultiplied. This is the noir-claude#1615 defect at the ACIR level —predicated_safe_get_stale_predicatecovers it end to end, but nothing pinned the circuit shape.predicated_get_of_repeated_field_type_biases_to_the_first_match:(u8, u8, Field)read at the secondu8falls back to slot0, pinning that first-match is intentional rather than incidental.compute_offsetas returningSome(0); the one on thearray_settest was doubly stale, since a store no longer calls it at all.vector_ops.rs'sIndexGating::Gated { fallback_offset: 0 }toIndexGating::without_fallback. At that call site there is nois_safe_indexto pass, andwithout_fallback(false)reads worse than the explicit variant. Same reasoning for thearray_setarm added here.Not addressed here
One review finding is about #13466's description rather than its code, and is left for @asterite: the body says the scheme costs "a free linear term instead of a mask per leaf", but the size report showed only regressions (nested_array_dynamic +16 opcodes, nested_array_in_vector +6, regression_struct_array_conditional +2, nothing shrinking). The deleted
apply_index_side_effectshad a free fast path — no mask at all when slot 0's type was no wider than the leaf's — and the bias costs a fresh witness for the index wheneveroffset != 0. That is a fine trade for a much simpler invariant; it just is not a cost win.Tests
cargo test -p noirc_evaluator --lib— 1947 pass, 0 fail. No existing ACIR snapshot changed, which is the evidence that the refactor is a no-op on generated circuits.cargo test -p nargo_cli --test execute -- array vector slice conditional regression— 5188 pass, 0 fail (includes all renamed programs across the inliner × Brillig matrix).cargo fmt --all --checkandcargo clippy -p noirc_evaluator --all-targetsclean.Created by claudebox · group:
slackbot· requested by Tom (@TomAFrench) · Slack thread