v3.2.5: second <unsupported> site, AC#3 measured, and promote FEAT-074/075 - #129
Merged
Conversation
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
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
avrabe
changed the title
📐 rivet artifact deltaPR: #129 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
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.
Completes v3.2.5. Two gaps closed after review, both of the asserted rather than measured kind — then the promotion.
1. A second defective
op_namesite (#126)After fixing the interpreter's fallback I grepped every
op_namecall site instead of assuming the reported one was the only one. The taint pass has its own "operator not modelled" diagnostic, and its trigger is an unmodelled operator — so it printed the placeholder for precisely the population it exists to describe:Same one-word fix, own red-first test. A third site (the write-set-havoc
Infoat a region opener) is safe and was left alone —op_namedoes coverblock/loop/if.FEAT-075's AC is widened from "its unsoundness-fallback diagnostic" to any diagnostic naming an operator, because the original wording would have let this site through.
2. FEAT-074's AC#3 was asserted, not measured
The AC said a precision or soundness regression "must be excluded rather than assumed" — and I had promoted on a green unit suite, which is exactly the assumption it forbids.
checked_subchanged behaviour for every branch whose depth reaches past its enclosing regions, and small fixtures are where that would not show.Measured properly — same 8.2 MB compiler-emitted module, both analyzers:
Identical. Worth noting this needed a different experiment than the
self-historyharness: that varies the module, and the question here was whether the analyzer change moved results — so the module had to be held fixed and the binary varied.3. Promotion
FEAT-074 and FEAT-075 →
accepted(acceptedis cuttable;implementedmeans not yet verified).Cutting the tag and publishing is a separate, deliberate step — this PR only makes the release assessable.
105 core tests · clippy
-D warningsclean ·rivet validatePASS.