v3.2.5 (#125, #126): don't trap the host, and name every fallback - #127
Merged
Conversation
`analyze` PANICKED with "index out of bounds: the len is 0 but the index is 0"
on valid, tiny modules from the official WebAssembly test suite. Reported by
avrabe against the released scry-3.2.4-wasm32-wasip2.wasm: 2 of 281 analysed
modules in a 468-module real-world corpus crashed deterministically.
A panic is worse than an error here, and that is the point. The WIT signature is
`analyze -> result<analysis-result, analyze-error>`, and `analyze-error` exists
precisely so an unanalysable module gets a structured refusal. A panic traps the
guest, so the host gets NEITHER arm — a consumer cannot tell "scry declined"
from "scry died".
ROOT CAUSE. `Interp::target()` resolved a branch's label with
`labels.len().saturating_sub(1 + relative_depth)` and then INDEXED. The label
stack is pushed only on ENTERING a block/loop/if, so the function body's own
implicit label is never on it — and `br 0` at function top level indexes an
empty slice. `saturating_sub` guards `relative_depth >= n` but not `n == 0`.
SECOND DEFECT IN THE SAME LINE, found while fixing the first. The clamp was also
wrong when it did not panic: `(block br 1)` exits the function, but clamping sent
it to index 0, recording the function-exit state into the OUTERMOST region's
label — a state that never arrives there. Over-approximate, hence sound, but
attributed to a label it cannot reach. `checked_sub` fixes both: reaching past
every enclosing region means the function label, which is a RETURN with no
in-function successor to carry state to.
Returning `None` records nothing, and that is deliberately NOT a gap. A return is
fully modelled; emitting one would inflate the gap report with an ordinary
construct and make REQ-017's "no silent top" surface less readable.
VERIFIED ON THE REPORTER'S OWN SOURCES, before and after. The two named modules
are generated from test/core/func.wast and test/core/unwind.wast; both contain
the triggering shape verbatim (`func.wast:150 (func (export "break-empty") (br 0))`,
`unwind.wast:7 (func (export "func-unwind-by-br") ... (br 0))`). Measured against
a worktree at the pre-fix commit:
unwind before: PANIC → after: OK, 49 functions, 100 program points
func before: PANIC → after: Internal("func 90 pc 7: i32 binop with
single operand") — a STRUCTURED error
The regression oracle was written RED FIRST and reproduced the reporter's exact
message at the same site from a one-line module. It covers every branch form that
resolves a label, because a fix guarding only `br` would leave `br_if` live.
RESIDUAL, filed separately rather than folded in: the fix UNMASKED a pre-existing
operand-stack defect in func.wast that the crash was hiding. Two hypotheses for
it were tested and REFUTED (a polymorphic stack after `br`, and after
`unreachable` — both analyse cleanly in isolation), so its cause is recorded as
uncharacterised rather than guessed at.
104 core tests + 34 viz pass; clippy -D warnings clean; rivet validate PASS.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
In avrabe's real-world corpus run the LARGEST bucket of fallback diagnostics was
not an operator at all: 579 said only `<unsupported>` — more than any named
operator, including `i32.and` at 433. A consumer was told THAT analysis degraded
but not WHAT caused it, so the diagnostic was non-actionable in exactly the case
it exists for, and the operator ranking that makes the precision work
prioritisable had to be reconstructed from outside rather than read off scry's
own output.
The fix already existed. `op_report_name()` falls back to the operator's Debug
variant name precisely so an unsupported op is still identified, and it was
already wired into the GAP records. The fallback DIAGNOSTIC used the lower-level
`op_name()`, which returns the literal `<unsupported>` for anything outside its
short hardcoded list. The two surfaces therefore disagreed about the same event
at the same pc: the gap named the operator, the diagnostic did not.
This is a REQ-017 defect rather than a cosmetic one. "No silent top" is not met
by a record that announces a degradation without identifying its cause. An
unnameable fallback is marginally better than silence for a human and WORSE than
silence for an agent, which cannot ask a follow-up question.
Two vacuous versions of the oracle were written and caught before this landed,
which is the reason the test is worth trusting now:
1. The first used AnalysisConfig::default(), where emit_diagnostics is FALSE.
It asserted over an empty diagnostic set and would have passed against no
fix at all.
2. The second asserted on `F64Add`, but `f64.const` is itself unmodelled and
takes the fallback first — and only ONE fallback fires per function, since
the scrub degrades the locals once. It failed against a WORKING fix.
The fixture now makes the operator under test the only unmodelled one, and the
test also asserts the diagnostic and the gap name the same operator.
MUTATION-CHECKED: reverting the one-word change reproduces the reporter's exact
string, so the oracle tests the fix rather than the fixture.
Does NOT model any of the operators. avrabe's ranking — nop/drop/unreachable
(215), the bitwise/shift family (597), select (203) — is the actual precision
work and is not in this release. What changes is that the ranking becomes
readable from scry's own output instead of reconstructed by a third party.
104 core tests pass; clippy -D warnings clean; rivet validate PASS.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
avrabe
changed the title
This was referenced Aug 21, 2026
📐 rivet artifact deltaPR: #127 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
avrabe
added a commit
that referenced
this pull request
Aug 21, 2026
…4/075 (#129) * rivet: promote FEAT-074/075 to accepted — v3.2.5 is cuttable Both features' acceptance criteria are met and verified on main, not merely implemented: FEAT-074 (#125) — measured before/after on the reporter's own sources. Both spec modules PANICKED at the pre-fix commit; after the fix unwind.wast analyses cleanly (49 functions, 100 program points) and func.wast returns a structured error instead of trapping the guest. FEAT-075 (#126) — mutation-checked: reverting the one-word change reproduces the reporter's exact string, so the oracle tests the fix and not the fixture. Both regression oracles were written RED FIRST and both reproduced the reported symptom before the fix existed. All 11 CI checks green on #127. `accepted` rather than `implemented`, per the release-gate semantics tested in rivet 0.22: `accepted` is cuttable, `implemented` means NOT yet verified. rivet release status v3.2.5: Cuttable. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc * FEAT-075: fix the SECOND <unsupported> site, and measure FEAT-074's AC#3 Two gaps closed after review, both of the "asserted rather than measured" kind. 1. A SECOND defective op_name site. After fixing the interpreter's fallback I grepped every `op_name` call site instead of assuming the reported one was the only one. The taint pass has its own "operator not modelled" diagnostic whose TRIGGER is an unmodelled operator — so it printed `<unsupported>` for precisely the population it exists to describe: "taint: operator <unsupported> not modelled — taint state conservatively raised to High (sound, FEAT-009)" Same one-word fix, own red-first test. A third site (the write-set-havoc Info at a region opener) is SAFE and was left alone: `op_name` does cover `block`/`loop`/`if`, so it never reaches the placeholder. FEAT-075's AC is widened from "its unsoundness-fallback diagnostic" to ANY diagnostic naming an operator, since the original wording would have let this site through. 2. FEAT-074's AC#3 said a precision or soundness regression "must be excluded rather than assumed" — and then I promoted on a green unit suite, which is exactly the assumption the AC forbids. `checked_sub` changed behaviour for every branch whose depth reaches past its enclosing regions, and small fixtures are where that would NOT show. Measured properly: the same 8.2 MB compiler-emitted module through the pre-fix and post-fix analyzer. Identical — 8530 advisories, 6490 trap checks, 28 proven-safe, 6462 potential-trap, same class breakdown. Note this needed a different experiment than the self-history harness, which varies the MODULE; the question here was whether the ANALYZER change moved results, so the module had to be held fixed and the binary varied. 105 core tests pass; clippy -D warnings clean; rivet validate PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
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.
Fixes #125. Fixes the diagnostic half of #126.
Two issue-driven fixes from @avrabe's corpus run, cut as a patch release ahead of v3.3.0 — #125 is a crash in the released 3.2.4, so a consumer is blocked today and v3.3.0's scope is nowhere near closed.
FEAT-074 — a branch to the function label must not panic (#125)
Why a panic is worse than an error. The WIT signature is
analyze -> result<analysis-result, analyze-error>, andanalyze-errorexists precisely so an unanalysable module gets a structured refusal. A panic traps the guest, so the host receives neither arm — a consumer cannot tell "scry declined" from "scry died".Root cause.
The label stack is pushed only on entering a block/loop/if, so the function body's own implicit label is never on it.
br 0at function top level indexes an empty slice.saturating_subguardsrelative_depth >= nbut notn == 0. Your guess — "an operand-stack or block-frame lookup on an empty stack" — was right in shape; it's the label stack.A second defect in the same line. The clamp was also wrong when it didn't panic:
(block br 1)exits the function, but clamping sent it to index 0, recording the function-exit state into the outermost region's label — a state that never arrives there. Sound, but attributed to a label it cannot reach.checked_subfixes both.Verified on your sources, before and after.
pulseengine/w2c2wasn't reachable, so I went to what those files are generated from. Both contain the triggering shape verbatim (func.wast:150,unwind.wast:7). Against a worktree at the pre-fix commit:unwind.wastfunc.wastInternal("func 90 pc 7: i32 binop with single operand")— structuredThat residual is filed as #128 — the crash was hiding it. I tested two hypotheses for it and refuted both, so its cause is recorded as uncharacterised rather than guessed at.
FEAT-075 — every unsoundness fallback names its operator (#126)
Your largest bucket wasn't an operator: 579 fallbacks said only
<unsupported>, more thani32.andat 433.The fix already existed.
op_report_name()falls back to the Debug variant name precisely so an unsupported op is still identified — and it was already wired into the gap records. The diagnostic used the lower-levelop_name(). So the two surfaces disagreed about the same event at the same pc.I'm treating this as a REQ-017 defect, not a cosmetic one: "no silent ⊤" isn't met by a record that announces a degradation without identifying its cause. An unnameable fallback is marginally better than silence for a human and worse than silence for an agent, which can't ask a follow-up.
This names the operators; it doesn't model any. Your ranking — nop/drop/unreachable (215), the bitwise/shift family (597), select (203) — is the real precision work and isn't in this release. What changes is that the ranking becomes readable from scry's own output instead of reconstructed from outside.
Test discipline
Both oracles were written red first. Worth stating plainly: the #126 test was vacuous twice before it was right.
AnalysisConfig::default(), whereemit_diagnosticsis false — it asserted over an empty diagnostic set and would have passed against no fix at all.F64Add, butf64.constis itself unmodelled and takes the fallback first, and only one fallback fires per function. It failed against a working fix.Both fixes are mutation-checked: reverting each reproduces the reporter's exact symptom.
104 core tests + 34 viz · clippy
-D warningsclean ·rivet validatePASS.