FEAT-092 (scry#126): one operator, one name - #168
Closed
avrabe wants to merge 2 commits into
Closed
Conversation
This was referenced Aug 27, 2026
📐 rivet artifact deltaPR: #168 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
avrabe
force-pushed
the
feat-092-op-names
branch
from
August 27, 2026 05:34
eca0e77 to
58890f7
Compare
avrabe
force-pushed
the
feat-092-op-names
branch
from
August 27, 2026 05:47
58890f7 to
fa6e7d7
Compare
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
ci.yml recorded the rule: require a job only once its name exists on every PR, i.e. after it merges to main. Correct, and incomplete -- a PR opened BEFORE the job existed still does not have it, so it can never report and is blocked forever. Observed rather than theorised. When #167 added two jobs and both were required, PRs #168 and #169 each showed 11 checks with 0 of the 2 new ones. Both would have deadlocked on a check that could never run. Both were rebased and now register 13. The complete procedure is now in ci.yml: 1. merge the PR that adds the job 2. add the context to the ruleset AND to required-checks.txt, ruleset FIRST (CI gates on the file, so a file ahead of the ruleset means CI is gating on a fiction -- the live-mode cross-check says exactly that) 3. REBASE EVERY OPEN PR drift-gate=0 gate-coverage=0 claim-check=0 rivet=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
`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>
avrabe
force-pushed
the
feat-092-op-names
branch
from
August 27, 2026 06:50
fa6e7d7 to
b3a8dbe
Compare
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
* Sync required-checks.txt to the ruleset: 10 -> 12 (scry#130) #167 landed FEAT-091 and FEAT-093, so `Commit traceability (rivet)` and `Required checks track CI jobs (scry#130)` now exist on main and run on every PR. The drift gate immediately moved them from PENDING to FAIL -- which is the transition it was built to make: a requirable job that is not required is scry#130 recurring one job at a time. Both were added to ruleset 16891064 (10 -> 12 contexts), and this syncs the checked-in file so the two agree. Order matters: the RULESET was updated first and the file second, because CI gates on the file -- a file listing checks the ruleset does not require would mean CI gating on a fiction, which the live-mode cross-check reports in exactly those words. Briefly red on main is the honest state during that window. Verified: file mode PASS, live mode PASS with `file agrees: True`. rivet=0 claim-check=0 drift-self-test=0. Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com> * "Require it after merge" was necessary but not sufficient ci.yml recorded the rule: require a job only once its name exists on every PR, i.e. after it merges to main. Correct, and incomplete -- a PR opened BEFORE the job existed still does not have it, so it can never report and is blocked forever. Observed rather than theorised. When #167 added two jobs and both were required, PRs #168 and #169 each showed 11 checks with 0 of the 2 new ones. Both would have deadlocked on a check that could never run. Both were rebased and now register 13. The complete procedure is now in ci.yml: 1. merge the PR that adds the job 2. add the context to the ruleset AND to required-checks.txt, ruleset FIRST (CI gates on the file, so a file ahead of the ruleset means CI is gating on a fiction -- the live-mode cross-check says exactly that) 3. REBASE EVERY OPEN PR drift-gate=0 gate-coverage=0 claim-check=0 rivet=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>
Contributor
Author
|
Superseded by #172 — same branch, rebased onto main. Auto-closed by GitHub when I deleted |
avrabe
added a commit
that referenced
this pull request
Aug 27, 2026
…175) Operating the gate exposed a hole in the procedure it enforces. Landing a job while its required-checks.txt entry arrives in a SEPARATE PR leaves main AND every open PR red until that follow-up merges. #167 did exactly that: the moment it merged, main failed its own drift gate and #168/#169 went red on a file they could not fix. The fix is structural, not another comment. The gate now FAILS a PR that adds a requirable job which is not in required-checks.txt, so the job and its entry ship together and the window does not exist. VERIFIED ON THE REAL REPO, both directions: job added, no file entry -> exit 1, naming it and quoting the instruction same job WITH its entry -> exit 0 (pending the ruleset update only) restored -> exit 0 Plus two new self-test cases covering exactly those, 7 in total. The procedure in ci.yml is now three steps with no red window: 1. in the SAME PR: add the job AND its required-checks.txt entry 2. after merge: add the context to the ruleset (instant, via the API) 3. rebase every open PR Steps 2 and 3 were each learned by getting them wrong. A required context whose job does not exist deadlocks everything; a job whose context does not exist deadlocks nothing. The asymmetry is why the ordering matters. drift-self-test=0 drift-file=0 gate-coverage=0 trailer-self-test=0 claim-check=0 rivet=0 fmt=0. 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.
The defect
TrapCheck::opis documented as "the operator name (e.g.i32.div_s)" — wasm textformat. Measured on scry's own
scry_mcdc.wasm, 2,800 of 10,520 advisories carrieda Rust enum identifier instead:
I64Store,I32Load8U,I32Store8,MemoryCopy,F64Load…Counts are identical on the stripped and unstripped module, so this isn't an
artifact of how the module was built.
Mechanism
op_report_namefalls back toformat!("{op:?}")for any operatorop_namehas no armfor — and among memory operators
op_namecovered exactly two:I32LoadandI32Store. Every other load/store rendered as its Rust variant name.Why this is #126's operator ranking, not cosmetics
The same operator carried two names at once.
i64.storeop_report_name)I64StoreA consumer ranking operators by frequency sees one operator as two rows and
under-counts the top entry by ~4.5× —
i64.storeis really 1,295 sites. Same fori64.load(261 + 669).Naming only — measured, not argued
After the change, on the real module:
out-of-boundsEvery code count is identical across all 10,520 advisories. The test also pins the
verdicts, so a later edit can't move what scry proves while claiming to rename.
Oracles
Red first, and the red was the contract rather than an empty fixture — the
non-vacuity assertion (
>= 3trap checks) passed before the failure:Mutation-checked: deleting the
i32.load8_uarm — asserted to match exactly onesite before applying — turns the test red naming exactly
I32Load8U; restoring is green.Not covered, stated rather than implied
71 advisories still render a Rust identifier. All 71 are
unsupported-opon i64/i32arithmetic and comparison operators (
I64GtS,I64Add,I32Rotl, …) that scrygenuinely does not model — and each carries a single name, so the ranking-splitting
defect doesn't apply to them. Naming that family is a separate mechanical slice that
would also serve #126's fallback ranking.
And this fixes the name, not the coverage. The reason
i64.storeappeared 1,008times via the degraded path is that those functions were already scrubbed by an
unsupported operator upstream. The corrected ranking now shows honestly how much of the
out-of-bounds population comes from degraded functions.
tests=0 clippy=0 fmt=0 rivet=0 claim-check=0 gate-coverage=0gh pr checksby hand.🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc