FEAT-092 (scry#126): one operator, one name - #172
Merged
Conversation
`TrapCheck::op` is documented as "the operator name (e.g. `i32.div_s`)" -- wasm
text format. Measured on scry's own scry_mcdc.wasm, 2,800 of 10,520 advisories
carried a RUST ENUM IDENTIFIER instead: I64Store, I32Load8U, I32Store8,
MemoryCopy, F64Load. Identical counts on the stripped and unstripped module, so
not an artifact of the build.
MECHANISM: op_report_name falls back to format!("{op:?}") for any operator
op_name has no arm for, and among memory operators op_name covered exactly two
-- I32Load and I32Store. Every other load/store rendered as its Rust variant.
WHY THIS IS #126's OPERATOR RANKING AND NOT COSMETICS: the same operator carried
TWO names at once. The non-degraded path labels the access from a literal
(`i64.store`, 287 sites); the degraded path calls op_report_name (`I64Store`,
1,008 sites). Both are out-of-bounds advisories. A consumer ranking operators by
frequency sees ONE operator as TWO rows and under-counts the top entry ~4.5x --
i64.store is really 1,295 sites.
NAMING ONLY, and measured rather than argued: after the change EVERY
advisory-code count on the real module is identical -- out-of-bounds 8,162 ->
8,162, proven-safe OOB 55 -> 55, every code equal across all 10,520 -- while
leaked identifiers drop 2,800 -> 71. The test pins the verdicts too, so a later
edit cannot move what scry proves while claiming to rename.
Red-first: failed with leaked: ["I32Load8U", "I32Store8"], AFTER the
non-vacuity assertion (>= 3 trap checks) passed -- the red was the contract, not
an empty fixture. Mutation-checked: deleting the i32.load8_u arm (asserted to
match exactly one site before applying) turns it red naming exactly I32Load8U.
NOT COVERED, stated rather than implied: 71 advisories still render a Rust
identifier. All 71 are `unsupported-op` on i64/i32 arithmetic and comparison
operators scry genuinely does not model, and each carries a SINGLE name -- the
ranking-splitting defect does not apply to them. Naming that family is a
separate mechanical slice.
tests=0 clippy=0 fmt=0 rivet=0 claim-check=0 gate-coverage=0.
Refs: FEAT-092
Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
FEAT-069 (safe-accesses.json, a v3.3.0 blocker) proposes exporting scry's PROVEN-SAFE out-of-bounds verdicts so synth can elide software bounds checks. Measured before anyone builds it, on scry's own scry_mcdc.wasm and identical stripped vs unstripped: scry proves 55 memory accesses safe against 8,162 it cannot -- a 0.67% proven rate. The export would carry 55 sites out of 8,217. synth measures bounds checks at ~25-40% overhead, so eliding 0.67% of them recovers on the order of 0.2% of runtime. That does not kill the feature; it relocates the work. The blocker is not the export FORMAT, it is PRECISION -- the same module shows 1,639 unmodeled-control-flow and 623 unsupported-op advisories, an if/else havocs its region by design, and FEAT-089 measured that a disequality guard cannot refine an interval at all. Shipping the channel before the payload exists would hand synth a correct and nearly empty file. Recorded on the artifact rather than only on the tracker, so a future tick does not build it expecting a full payload. (Also repairs three terms this edit itself blanked: the first attempt used an unquoted heredoc, so the shell ran the backticked operator names as command substitutions. `rivet validate` passed over the gaps -- structural validation cannot see missing prose, which is worth remembering before trusting it as a review.) rivet=0 claim-check=0 fmt=0. Refs: FEAT-069 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #172 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 27, 2026
Both shipped and CI-verified; leaving them proposed understates the release the same way promoting them early would overstate it. FEAT-091 (#167, 13/13 green) -- commit traceability. Its gate's --self-test PASSES and the real check PASSES on main against HEAD~1..HEAD, and the job runs in CI as a REQUIRED check. FEAT-092 (#172, 13/13 green) -- one operator, one name. Its oracle re-run on main just now; the naming-only claim was measured, not argued (every advisory-code count identical on a real module, leaks 2,800 -> 71). NOT promoted, and the reason matters: FEAT-093 -- merged in #167 and green, but #175 is OPEN and adds ACs to it. Promoting now would produce an `accepted` artifact that immediately gains unmet criteria. It goes accepted after #175 lands, not before. FEAT-089 -- filed, not built; its AC#1 demands a test still red by design. FEAT-057 / FEAT-065 / REQ-021 -- unbuilt. FEAT-064 -- AC1 still falsified, so REQ-020 stays blocked. rivet=0 claim-check=0 drift-gate=0 fmt=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
Both shipped and CI-verified; leaving them proposed understates the release the same way promoting them early would overstate it. FEAT-091 (#167, 13/13 green) -- commit traceability. Its gate's --self-test PASSES and the real check PASSES on main against HEAD~1..HEAD, and the job runs in CI as a REQUIRED check. FEAT-092 (#172, 13/13 green) -- one operator, one name. Its oracle re-run on main just now; the naming-only claim was measured, not argued (every advisory-code count identical on a real module, leaks 2,800 -> 71). NOT promoted, and the reason matters: FEAT-093 -- merged in #167 and green, but #175 is OPEN and adds ACs to it. Promoting now would produce an `accepted` artifact that immediately gains unmet criteria. It goes accepted after #175 lands, not before. FEAT-089 -- filed, not built; its AC#1 demands a test still red by design. FEAT-057 / FEAT-065 / REQ-021 -- unbuilt. FEAT-064 -- AC1 still falsified, so REQ-020 stays blocked. rivet=0 claim-check=0 drift-gate=0 fmt=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
…→4 (#176) * Promote FEAT-091 / FEAT-092 to accepted — v3.4.0 not-ready 7 -> 5 Both shipped and CI-verified; leaving them proposed understates the release the same way promoting them early would overstate it. FEAT-091 (#167, 13/13 green) -- commit traceability. Its gate's --self-test PASSES and the real check PASSES on main against HEAD~1..HEAD, and the job runs in CI as a REQUIRED check. FEAT-092 (#172, 13/13 green) -- one operator, one name. Its oracle re-run on main just now; the naming-only claim was measured, not argued (every advisory-code count identical on a real module, leaks 2,800 -> 71). NOT promoted, and the reason matters: FEAT-093 -- merged in #167 and green, but #175 is OPEN and adds ACs to it. Promoting now would produce an `accepted` artifact that immediately gains unmet criteria. It goes accepted after #175 lands, not before. FEAT-089 -- filed, not built; its AC#1 demands a test still red by design. FEAT-057 / FEAT-065 / REQ-021 -- unbuilt. FEAT-064 -- AC1 still falsified, so REQ-020 stays blocked. rivet=0 claim-check=0 drift-gate=0 fmt=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Also promote FEAT-071 — v3.3.0 not-ready 6 -> 5 #174 landed FEAT-071 with 13/13 green, so it belongs in this pass rather than a follow-up. Its oracle re-run on main just now: the scope manifest reaches the feed as data, and the anti-drift property (every not-proven item present in BOTH the page and the feed) holds. That property was mutation-checked when it landed -- emitting empty strings in the feed while the page kept them kills the test. Folded in here rather than opened separately because #176 had not started CI, so it costs nothing; had it been mid-run the trade would have gone the other way. rivet=0 claim-check=0 drift-gate=0 fmt=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * Also promote FEAT-093 — its refinement landed, so its criteria are complete FEAT-093 was deliberately held back from the earlier promotion because #175 was OPEN and adding acceptance criteria to it; promoting then would have produced an `accepted` artifact that immediately acquired unmet criteria. #175 has now merged, so the criteria are complete AND met. Evidence re-run on main: the gate's 7-case --self-test passes, file mode passes, and live mode passes with `file agrees: True` -- the ruleset, the checked-in file and the CI jobs are all in agreement. Folded in here rather than opened separately because #176 still had not started CI. Same trade as FEAT-071 a moment ago, and the same reason. rivet=0 claim-check=0 drift-gate=0 fmt=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com> --------- 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.
Reopens the work from #168, which GitHub auto-closed when I deleted its base branch
during the #170 merge (my error —
--delete-branchon a branch that was the base ofthree stacked PRs). Branch is unchanged apart from a clean rebase onto main; #168
carries the full review discussion.
The defect
TrapCheck::opis documented as "the operator name (e.g.i32.div_s)" — wasm textformat. Measured on
scry_mcdc.wasm, 2,800 of 10,520 advisories carried a Rust enumidentifier instead (
I64Store,I32Load8U,MemoryCopy, …). Identical counts strippedand unstripped, so not a build artifact.
op_report_namefalls back toformat!("{op:?}")for any operatorop_namelacks anarm for — and among memory ops it covered exactly two.
Why it's #126's operator ranking, not cosmetics
The same operator carried two names: the non-degraded path emits
i64.store(287sites), the degraded path
I64Store(1,008). Bothout-of-bounds. A frequency rankingsees one operator as two rows and under-counts the top entry ~4.5× —
i64.storeisreally 1,295 sites.
Naming only — measured, not argued
out-of-boundsEvery advisory-code count identical across all 10,520. The test pins the verdicts too,
so a later edit can't move what scry proves while claiming to rename.
Red first:
leaked: ["I32Load8U", "I32Store8"], after the non-vacuity assertion(
>= 3trap checks) passed. Mutation-checked: deleting thei32.load8_uarm —asserted to match one site — turns it red naming exactly
I32Load8U.Not covered: 71 advisories still render a Rust identifier, all
unsupported-oponi64/i32 arithmetic scry doesn't model, each with a single name — the splitting defect
doesn't apply. Separate slice.
Also records the FEAT-069 pre-build measurement (0.67% proven rate) on its artifact.
🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc