v3.3 plan + FEAT-070/FEAT-064: agent-verifiable groundwork - #115
Merged
Conversation
Release plan from the Wasm Research Day read-out (6 Aug 2026): the AI-consumer axis is the decisive one. Planned in rivet on the `release:` axis; readiness is the `rivet release status v3.3.0` query, not an opinion. Thesis (measured, not assumed): scry's self-analysis reports 0 proven faults against 6,191 unproven obligations. No agent can act on 6,191 items — so for an AI consumer PRECISION IS THE PRODUCT, and agent-usability work and precision work are the same work. This release scopes both. DEPTH — the blocker REQ-018 left open. v3.1 shipped a verification oracle as PROSE. Two things stop it being a loop: - FEAT-064 stable obligation identity. scry keys findings on (func_index, pc); one inserted instruction renumbers every later pc, so DISCHARGED and MOVED are indistinguishable. Content-addressed ID over function identity + structural CFG path + operator kind + intra-block ordinal (DD-020). - FEAT-065 `scry verify --against`: scry adjudicates its own oracle — discharged / still-open / regressed / moved / removed-with-code, with a machine-usable exit code. `removed-with-code` is kept strictly distinct from `discharged`, or an agent learns to delete rather than fix. - DD-020 records the scheme, why each component was chosen for what it is invariant under, the honest degradation when no name section exists, and the three rejected alternatives (DWARF, persisted map, fuzzy matching). BREADTH — six independently shippable surfaces: FEAT-066 scry-mcp (analyze/query/verify as MCP tools — agents can't run cargo) FEAT-067 query filters over AnalysisResult (FEAT-056 lite) FEAT-068 guidance.json v2 (versioned schema + obligation IDs + module hash) FEAT-069 safe-accesses.json (the synth#901 bounds-elision channel) FEAT-070 br_if-on-value guard refinement (precision; credited to WasmBounds) FEAT-071 machine-readable capability manifest (the Scope block as data) SCOPE MOVE, logged not silent: FEAT-057 (polyhedra) held v3.3.0 and is displaced to v3.4.0 — agent-consumability outranks a precision ceiling we cannot yet wire into the fixpoint, and its slice-2 was already reframed as a multi-slice arc. Nothing in v3.3.0 depends on it. rivet validate PASS. Held local (not pushed): GitHub Actions/Pages degraded. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…gation identity
Feature loop for the first two v3.3.0 items. Oracle-gated, clean-room reviewed,
and the review's findings reconciled into BOTH the code and the artifacts.
FEAT-070 — guard refinement for `br_if` on a bare value (clean-room: CLEAN).
`try_guard_brif` now also accepts a leading `local.tee` and a 2-op bare
`<get|tee> L; br_if D` (truthiness), whose FALL-THROUGH pins L to {0} — the
count-to-zero loop shape LLVM emits and the reason its exit value is knowable.
Three soundness details: the tee form's net stack effect is -1 (not 0), the tee
ASSIGNS the local so the peephole applies it, and every bail-out precedes any
mutation so a None return leaves ctx untouched.
Clean-room MINOR fixed: the blanket octagon `forget` was a precision regression
on this feature's own motivating idiom — replaced with `octagon_transfer`, whose
own fallback is forget, so it is at least as sound and strictly more precise.
FEAT-064 — stable obligation identity (clean-room: property REFUTED as
specified; implemented, reconciled, NOT complete).
Content-addressed id over function identity + structural CFG path + operator
kind + intra-region same-kind ordinal + advisory code, stamped onto every
Advisory. Fixes applied from the review:
- one operator can raise SEVERAL obligations (i32.div_s raises div-by-zero AND
signed-overflow at one pc) — the site alone did not discriminate, so the
advisory code is now a component;
- module-scoped advisories (unbounded-stack, a (func 0, pc 0) SENTINEL) got
func 0's site identity, colliding with genuine advisories there and yielding
nothing when index 0 is an import — they now get a module-scoped identity.
Honest reconciliation (the review was right and the artifacts changed):
- FEAT-064 AC#2 was FALSE as written. Pc-shift immunity holds only for
insertions containing no same-kind operator in the same region and opening no
new sibling region. The AC is qualified; the original passed only because my
fixture was selected around the failing case — twice over, since writing
local 0 also flipped the advisory's class.
- DD-020 gains a limitations section: ordinal ALIASING (deleting the first of
two same-kind ops transfers its id to the survivor) is the same failure mode
DD-020 rejected fuzzy matching for, reintroduced in bounded form.
- FEAT-065 therefore gains a CONSERVATISM rule: the adjudicator must treat
`discharged` as the analyzer treats PROVEN-SAFE — degrade to `uncertain` when
a region's same-kind multiset changed. Over-claiming a discharge is an unsound
analysis one layer up, and the error an agent would exploit fastest.
- Also recorded: if/else share an ordinal counter; unnamed identical bodies
collide; try_table desyncs the region path.
Verified locally: 102 core tests (+6), sibling crates green, clippy clean across
CI's five packages, cargo fmt clean, rivet validate PASS.
NOT verified (blocked, not skipped): witness MC/DC and the ObligationId.v Rocq
proof both need a Wasm/Bazel build, and Bazel fetches from GitHub which is
degraded; scry-host-tests feat013_live_analyze_gate fails locally for the same
reason (no bazel-bin/scry.wasm) and is covered by CI.
FEAT-064/070 stay `proposed` — neither is done until those gates run.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #115 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
…parately New advisory published during the GitHub outage: wasmtime "Stores can mix up type indices between engines". Not introduced by this branch — no dependency was added. Reachability verified rather than assumed: wasmtime is a dependency of scry-host-tests ONLY (publish = false); `cargo metadata` confirms no published scry-sai-* crate carries it as a normal dependency, and the shipped scry.wasm embeds no engine. The harness runs our own fixtures against our own composed component — not a multi-tenant sandbox host — so the crafted cross-engine usage the advisory requires has no attack surface here. Explicitly time-boxed: there is no patched 45.x line (fixes are in 46.0.2 / 47.0.3), so the durable fix is a wasmtime major bump, filed separately rather than smuggled into a feature PR. The entry says to DELETE it when that lands. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This was referenced Aug 7, 2026
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.
Two commits: the v3.3.0 "agent-verifiable" release plan (rivet), and the first two features implemented through the feature loop. Authored during the GitHub outage, so this PR run is the first CI has seen of it — the Bazel/MC-DC gates below were blocked locally, not skipped.
The plan (commit 1)
Read-out from Wasm Research Day: the AI-consumer axis is decisive. Thesis, from a measurement rather than a vibe — scry reports 0 proven faults against 6,191 unproven obligations, so for an AI consumer precision is the product, and agent-usability work and precision work are the same work.
scry verify --against) + DD-020FEAT-070 — guard refinement on bare
br_if(clean-room: CLEAN)try_guard_brifnow accepts a leadinglocal.teeand the 2-op truthiness form; the fall-through pins the local to{0}— the count-to-zero shape LLVM emits. Soundness details handled: the tee form's net stack effect is −1, the tee assigns the local, and every bail-out precedes any mutation.Clean-room MINOR fixed: the blanket octagon
forgetwas a precision regression on this feature's own motivating idiom → replaced withoctagon_transfer(whose fallback is forget, so at least as sound, strictly more precise).Technique credited to WasmBounds (Sudo & Winstein, Stanford), whose
BrIfrule handles this shape.FEAT-064 — stable obligation identity (property refuted as specified, reconciled)
Content-addressed ID over function identity + structural CFG path + operator kind + intra-region ordinal + advisory code. The clean-room refuted the AC and I've changed the artifacts rather than the claim:
local 0, flipping the advisory's class). AC now qualified.try_tabledesyncs the region path.dischargedas the analyzer treatsPROVEN-SAFE— degrade touncertainwhen a region's same-kind multiset changed. Over-claiming a discharge is an unsound analysis one layer up.i32.div_sraises two obligations at one pc), and module-scoped advisories no longer borrow func 0's identity.Status
Local: 102 core tests (+6), sibling crates green, clippy clean across CI's five packages, fmt clean,
rivet validatePASS.Both features remain
proposed— not done until MC/DC and theObligationId.vproof land.rivet release status v3.3.0correctly reports not cuttable (9 artifacts).🤖 Generated with Claude Code