From 98e258003e81053ae97aa7e4332ba0ed015e3961 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 6 Aug 2026 21:29:41 +0200 Subject: [PATCH 1/3] =?UTF-8?q?plan:=20v3.3.0=20"agent-verifiable"=20?= =?UTF-8?q?=E2=80=94=20close=20the=20fix-verify=20loop=20(REQ-020)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- artifacts/design.yaml | 65 ++++++++ artifacts/roadmap-3.0.yaml | 310 ++++++++++++++++++++++++++++++++++++- 2 files changed, 370 insertions(+), 5 deletions(-) diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 8429715..debe0c6 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -572,3 +572,68 @@ artifacts: target: REQ-016 - type: traces-to target: FEAT-057 + + - id: DD-020 + type: design-decision + title: "v3.3 — Obligation identity: structural content-address, not (func, pc)" + status: proposed + tags: [ai-agent, identity, fix-verify-loop, schema, v3.3] + description: > + How FEAT-064 names a finding so the name survives an edit. scry's internal + key is `(func_index, pc)`, which is correct for the analyzer and useless as + an external identity: any inserted instruction renumbers every later pc, so + a consumer comparing two runs cannot tell DISCHARGED from MOVED. Since the + whole REQ-020 fix-verify loop rests on that distinction, identity is a + design decision in its own right rather than a field format. + fields: + decision: > + An obligation ID is a content address over four components, in this + order: (1) FUNCTION IDENTITY — the name-section name if present, else the + export name, else a hash of the function body's structural shape (opcode + sequence with immediates elided); (2) STRUCTURAL PATH — the chain of + enclosing block/loop/if indices from the function root, NOT raw pcs; + (3) OPERATOR KIND — e.g. `i32.load`, `i32.div_s`; (4) ORDINAL — the + operator's index among same-kind operators within its own basic block. + The ID is the hash of that tuple. `(func_index, pc)` remains in the + output as a positional convenience, explicitly documented as unstable. + The adjudicator (FEAT-065) reports five outcomes and must keep + `removed-with-code` strictly distinct from `discharged`. + rationale: > + Each component is chosen for what it is invariant under. Function + identity by name survives the function moving in the index space (adding + a function elsewhere renumbers indices). The structural path survives + instruction insertion elsewhere in the same function, which raw pcs do + not. The intra-block ordinal keeps two same-kind operators in one block + distinguishable without reintroducing a global counter. Hashing the tuple + keeps the ID opaque and fixed-width, so consumers cannot start parsing it + and depending on the layout. + The body-shape hash is the fallback, and it is deliberately the WEAKEST + of the three: a module stripped of names gets IDs that change whenever + the function is edited at all. That is honest degradation — with no name + section there is no stable notion of "the same function" — and it is why + the fallback is last rather than the default. + On the correctness claim: only `id(a) == id(b) ⇒ same structural site` is + provable and will be mechanized (ObligationId.v). The converse is FALSE + by construction — a rewritten function should produce new IDs, because + the old site genuinely no longer exists. Claiming stability under + arbitrary edits would be the overclaim here, and it is the one an agent + would be most damaged by trusting. + alternatives: > + (a) Source-line identity via DWARF — rejected as the primary: scry + analyses Wasm binaries that frequently carry no DWARF, and it would + make identity depend on the producer toolchain. + (b) A persisted ID map written by scry and carried between runs — + rejected: it makes identity stateful, needs a store the consumer must + not lose, and fails exactly when an agent runs scry on a fresh + checkout. + (c) Fuzzy matching between runs (nearest-pc / diff heuristics) — + rejected: a heuristic that guesses "this is probably the same + obligation" would report `discharged` on a coincidence, which is the + single failure this design exists to prevent. + links: + - type: satisfies + target: REQ-020 + - type: traces-to + target: FEAT-064 + - type: traces-to + target: FEAT-065 diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index a77370f..36684cc 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -18,9 +18,14 @@ artifacts: # v3.2 "Content-sensitive memory" — linear-memory segmentation: # track values inside memory ranges instead of one havoc'd ⊤ # blob (scry's biggest current precision cliff). FEAT-058. - # v3.3 "Precision ceiling" — convex polyhedra, ELINA- + # v3.3 "Agent-verifiable" — close the fix-verify loop so an + # AI agent is GATED on a sound checker: stable obligation identity + # + `scry verify` adjudication (depth), plus the MCP/query/schema + # surfaces and the precision work that make 6,191 unproven + # obligations actionable at all (breadth). REQ-020, FEAT-064..071. + # v3.4 "Precision ceiling" — convex polyhedra, ELINA- # decomposed, for exact linear inequalities above the octagon. - # FEAT-057. Sequenced AFTER v3.2 (segmentation first). + # FEAT-057. Displaced from v3.3 on 2026-08-06 (see its section). # Release axis = the top-level `release:` field (rivet >= 0.21). Track with # `rivet release status ` / `rivet list --release `. # ══════════════════════════════════════════════════════════════════════ @@ -198,6 +203,58 @@ artifacts: - type: references-paper target: AC-015 + # ── v3.3 requirement (from the Wasm Research Day read-out) ──────────── + + - id: REQ-020 + type: requirement + title: "An AI agent can be GATED on scry: stable obligation identity + a machine-checkable oracle" + status: proposed + release: v3.3.0 + description: > + REQ-018 shipped ranked, honesty-classed advisories each carrying a + VERIFICATION ORACLE — but as PROSE ("re-run scry: this trap_check becomes + ProvenSafe"). A human can follow that; an agent loop cannot be gated on it. + Two things block the loop, and this requirement closes both. + + (1) IDENTITY. scry keys every finding on `(func_index, pc)`. The moment an + agent edits the module and recompiles, every pc shifts, so "did my fix + discharge obligation X?" is unanswerable — DISCHARGED and MOVED are + indistinguishable. Without identity that survives the edit there is no + loop, only a diff of two unrelated reports. scry shall therefore emit a + STABLE, content-addressed obligation identity that is invariant under + edits elsewhere in the module and elsewhere in the same function. + + (2) ADJUDICATION. scry shall be able to compare a new run against a prior + one and classify each obligation: discharged / still-open / regressed / + moved / removed-with-code. That converts the v3.1 prose oracle into a + machine verdict, so an agent's edit is gated by a SOUND CHECKER rather + than by tests — the actual value of REQ-018, finally executable. + + MOTIVATION (measured, not assumed): scry's own self-analysis reports 0 + proven faults against 6,191 unproven obligations and 1,962 precision gaps. + No agent can act on 6,191 items, so for an AI consumer PRECISION IS THE + PRODUCT — an unproven obligation is a bill for the analyzer's imprecision + handed to the user. Agent-usability work and precision work are the same + work; this release scopes both. + + HONESTY: a rewritten function SHOULD lose its obligation IDs. That is + correct behaviour (the site genuinely no longer exists), not a defect, and + the adjudicator must report it as `removed-with-code`, never as + `discharged`. + tags: [ai-agent, fix-verify-loop, identity, oracle, precision, v3.3] + fields: + priority: must + category: functional + links: + - type: traces-to + target: REQ-018 + - type: traces-to + target: REQ-017 + - type: traces-to + target: G-005 + - type: evaluates-tech + target: TE-011 + # ══════════════════════════════════════════════════════════════════════ # RELEASE v2.6.0 — "Make the analysis observable" # Cash in computed-but-hidden facts; cheap precision; agent/qual readiness. @@ -661,15 +718,22 @@ artifacts: target: REQ-017 # ══════════════════════════════════════════════════════════════════════ - # RELEASE v3.3.0 — "Precision ceiling" (the second big domain bet) + # RELEASE v3.4.0 — "Precision ceiling" (the second big domain bet) # Convex polyhedra above the octagon. Sequenced AFTER v3.2 segmentation. + # + # SCOPE MOVE (2026-08-06, logged not silent): this held the v3.3.0 slot. + # Displaced to v3.4.0 by the Wasm Research Day read-out — agent-consumability + # (REQ-020) outranks a precision ceiling we cannot yet wire into the fixpoint, + # and slice-2 was already reframed as a multi-slice fixpoint arc rather than + # the cheap straight-line pass originally planned (vacuous over wrapping ints). + # Nothing in v3.3.0 depends on it; the shipped scry-sai-poly crate is unaffected. # ══════════════════════════════════════════════════════════════════════ - id: FEAT-057 type: feature - title: "v3.3 — Convex polyhedra domain (ELINA-decomposed)" + title: "v3.4 — Convex polyhedra domain (ELINA-decomposed)" status: proposed - release: v3.3.0 + release: v3.4.0 description: > Convex polyhedra (Cousot-Halbwachs 1978, AC-012; DD-019) for exact linear inequalities Σ a_i·x_i ≤ c above the octagon, made tractable by ELINA-style @@ -868,3 +932,239 @@ artifacts: target: REQ-017 - type: evaluates-tech target: TE-011 + + # ══════════════════════════════════════════════════════════════════════ + # RELEASE v3.3.0 — "Agent-verifiable" (REQ-020) + # Read-out from Wasm Research Day (6 Aug 2026): the AI-consumer axis is the + # decisive one. Two halves, deliberately paired: + # DEPTH — close the fix-verify loop (identity + adjudication), so an + # agent's edit is gated by a sound checker instead of by tests. + # BREADTH — make the analysis reachable and askable by an agent at all + # (MCP surface, queries, versioned schema, manifest), plus the + # precision work that makes 6,191 obligations actionable. + # Thesis: for an AI consumer, precision IS the product — an unproven + # obligation is a bill for the analyzer's imprecision handed to the user. + # ══════════════════════════════════════════════════════════════════════ + + # ── DEPTH: the spine ────────────────────────────────────────────────── + + - id: FEAT-064 + type: feature + title: "v3.3 — Stable obligation identity (survives the edit)" + status: proposed + release: v3.3.0 + description: > + Replace raw `(func_index, pc)` as the EXTERNAL key for every finding with a + content-addressed obligation ID (DD-020). Composed of: function identity + (name-section name → export name → a hash of the body's shape, in that + order of preference), a structural path through the CFG (block/loop nesting + indices, not raw pcs), the operator kind, and the operator's index within + its own basic block. Result: the ID is invariant under edits elsewhere in + the module AND elsewhere in the same function, so a fix in one place does + not renumber every obligation in the binary. + `(func_index, pc)` stays in the output as a positional convenience; the ID + becomes the thing consumers key on. + Soundness/mechanization scope: the provable property is directional — + `id(a) == id(b)` implies a and b denote the same structural site. The + converse does NOT hold (a rewritten function legitimately produces new + IDs) and must not be claimed. + tags: [ai-agent, identity, fix-verify-loop, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a module and an edit that changes code in an unrelated function, When scry re-analyzes, Then every obligation ID outside the edited function is unchanged." + - "Given an edit that inserts instructions EARLIER in the same function, When scry re-analyzes, Then obligation IDs for later sites in that function are unchanged (pc-shift immunity)." + - "Given proofs/rocq/ObligationId.v, When built, Then `id equality implies same structural site` is proven admit-free; the converse is explicitly NOT claimed." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-018 + + - id: FEAT-065 + type: feature + title: "v3.3 — `scry verify --against`: scry adjudicates its own oracle" + status: proposed + release: v3.3.0 + description: > + Turn the v3.1 prose verification oracle into a machine verdict. `scry verify + --against ` compares a fresh analysis with a prior one and + classifies every obligation by its stable ID (FEAT-064): + discharged — was open, now PROVEN-SAFE (the fix worked) + still-open — unchanged + regressed — was PROVEN-SAFE, now an obligation (the fix broke it) + moved — same ID, different position (informational, NOT progress) + removed-with-code — the site no longer exists (NOT a discharge) + Exit code is machine-usable so an agent loop can gate on it. This is the + capability REQ-018 promised: an agent's edit judged by a SOUND + over-approximation, so a satisfied oracle is a proof the trap cannot fire — + not "the tests still pass". + HONESTY (the load-bearing distinction): `removed-with-code` must never be + reported as `discharged`. Deleting the code that contained an unproven + obligation is not proving anything, and an agent optimising against a + conflated verdict would learn to delete rather than to fix. + tags: [ai-agent, oracle, fix-verify-loop, gate, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a POTENTIAL-TRAP obligation and an edit that adds a correct guard, When `scry verify --against` runs, Then that obligation is reported `discharged` and the exit code signals success." + - "Given an edit that DELETES the function containing an open obligation, When verify runs, Then it is reported `removed-with-code`, never `discharged`." + - "Given an edit that invalidates a previously PROVEN-SAFE site, When verify runs, Then it is reported `regressed` and the exit code signals failure." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-018 + - type: traces-to + target: FEAT-064 + + # ── BREADTH: six surfaces, each independently shippable ─────────────── + + - id: FEAT-066 + type: feature + title: "v3.3 — scry-mcp: analyze / query / verify as MCP tools" + status: proposed + release: v3.3.0 + description: > + An MCP server exposing scry to agents directly. Agents cannot run `cargo`; + today consuming scry means shelling out or scraping a 5.7 MB JSON. Tools: + `analyze` (module → summary + counts), `query` (FEAT-067 filters), + `verify` (FEAT-065 adjudication). Returns structured results, never HTML. + Single biggest adoption lever for the AI-consumer axis (TE-011: + structured-primary — agents under-read rendered output). + tags: [ai-agent, mcp, interop, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given an MCP client, When it calls `analyze` on a Wasm module, Then it receives a structured summary (counts by advisory class, trap verdicts, gaps) without parsing HTML or reading a multi-MB dump." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-017 + - type: evaluates-tech + target: TE-011 + + - id: FEAT-067 + type: feature + title: "v3.3 — Query filters over AnalysisResult (FEAT-056 lite)" + status: proposed + release: v3.3.0 + description: > + A filter/selection surface so a consumer asks instead of scrapes — + e.g. "every site where kind=Top and op in (call_indirect, memory.grow)", + "every UnprovenObligation in function $f". The bounded, shippable slice of + the FEAT-056 queryable-CPG idea: filtering + projection over the existing + result, no new graph substrate and no query language to design. + tags: [ai-agent, query, observability, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given an AnalysisResult, When a consumer filters by advisory class / gap kind / operator / function, Then it receives only the matching records with their stable obligation IDs." + links: + - type: traces-to + target: REQ-017 + - type: traces-to + target: REQ-020 + + - id: FEAT-068 + type: feature + title: "v3.3 — guidance.json v2: versioned schema carrying obligation IDs" + status: proposed + release: v3.3.0 + description: > + The v3.2.2 guidance feed shipped un-versioned. v2 adds an explicit + `schema` field, the FEAT-064 stable obligation IDs, per-class counts, and + the module hash that binds the feed to one exact module. Documented as a + stable contract so an agent can code against it across scry releases. + tags: [ai-agent, schema, contract, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given guidance.json v2, When a consumer reads it, Then every advisory carries a stable obligation ID and the document declares its schema version and module hash." + links: + - type: traces-to + target: REQ-018 + - type: traces-to + target: REQ-013 + + - id: FEAT-069 + type: feature + title: "v3.3 — safe-accesses.json: proven-safe sites for bounds-check elision" + status: proposed + release: v3.3.0 + description: > + Export the PROVEN-SAFE OutOfBounds verdicts scry already computes as a flat, + engine-agnostic list keyed on the wasmparser operator index — the channel + synth's `ProvenSafeBoundsChecker` consumes (pulseengine/synth#901) to elide + software bounds checks on no-MMU targets, where every access is checked and + synth measures that at ~25-40% overhead. + Consumer contract: `module_sha256` binds the verdicts to one module and the + consumer FAILS CLOSED on mismatch; verdicts are proven against the memory's + guaranteed MINIMUM size, so growth cannot invalidate them; absence from the + list means "not proven", never "unsafe". + Interop note: the same shape as the output contract in WasmBounds (Sudo & + Winstein, Stanford), which is a cleaner interface than our full feed. + tags: [bounds-elision, synth, interop, embedded, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a module with provably in-bounds i32 accesses, When scry exports safe-accesses.json, Then each entry carries (func, pc, op, width) plus the module hash, and a consumer that fails the hash check elides nothing." + links: + - type: traces-to + target: REQ-014 + - type: traces-to + target: REQ-004 + + - id: FEAT-070 + type: feature + title: "v3.3 — Guard refinement for `br_if` on a bare value (precision)" + status: proposed + release: v3.3.0 + description: > + Our guard refinement recognises `local.get X; i32.const c; ; br_if`, + `local.get X; i32.eqz; br_if`, and the two-local compare. It does NOT handle + `local.tee $x; br_if` — a branch on the raw value's truthiness (implicit + `≠ 0`), which is what LLVM emits for count-to-zero loops and is therefore + common in real bounds-check code. Fall-through gets the local `= {0}`, the + taken edge gets `≠ 0`; the dual of the `i32.eqz` shape already supported. + Credit: this shape is handled by WasmBounds' BrIf rule (Sudo & Winstein); + their (value, expression) operand-stack pairing generalises better than our + syntactic peephole, and a light provenance tag (`Local(i) | Const | Mem | + Other`) on the abstract stack is the follow-on worth taking from it. + Directly reduces the 6,191 unproven obligations that make the output + unusable to an agent — precision as agent UX (REQ-020). + tags: [precision, guard-refinement, ai-agent, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given a count-to-zero loop guarded by `local.tee $i; br_if`, When scry analyzes it, Then $i is bounded on both edges instead of ⊤, and the loop's memory accesses become eligible for PROVEN-SAFE." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-014 + + - id: FEAT-071 + type: feature + title: "v3.3 — Machine-readable capability manifest (the Scope block as data)" + status: proposed + release: v3.3.0 + description: > + The v3.2.2 dashboard states scry's scope in prose: what is mechanized vs + γ-sweep-validated, and what scry does NOT prove. An agent deciding whether + to trust a verdict needs that as DATA, not paragraphs. Emit a manifest + enumerating each domain/transfer with its evidence kind + (`mechanized | gamma-swept | asserted`) and the named open gaps. + Same single source as the claim ledger (claims.yaml), so the manifest, the + dashboard prose, and CI cannot drift apart. + tags: [ai-agent, honesty, qualification, schema, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given the manifest, When an agent reads it, Then every domain carries an evidence kind and the not-proven list is enumerated rather than prose — and claim-check gates it against the same source as the README claims." + links: + - type: traces-to + target: REQ-017 + - type: traces-to + target: G-005 From f42fdd4ec4c617f0c7f2be385fae47859ddcd3dd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 6 Aug 2026 22:00:35 +0200 Subject: [PATCH 2/3] v3.3 FEAT-070 + FEAT-064: guard refinement on bare br_if; stable obligation identity MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 ` 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 --- artifacts/design.yaml | 27 ++ artifacts/roadmap-3.0.yaml | 15 +- crates/scry-analyze-core/src/lib.rs | 489 ++++++++++++++++++++++++++-- crates/scry-viz/src/lib.rs | 1 + 4 files changed, 497 insertions(+), 35 deletions(-) diff --git a/artifacts/design.yaml b/artifacts/design.yaml index debe0c6..0e64ad6 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -618,6 +618,33 @@ artifacts: the old site genuinely no longer exists. Claiming stability under arbitrary edits would be the overclaim here, and it is the one an agent would be most damaged by trusting. + limitations: > + Recorded after adversarial clean-room review of the v3.3 implementation + — these are properties the scheme does NOT have, and the FEAT-065 + adjudicator is required to be conservative in exactly these cases. + (1) ORDINAL ALIASING (the significant one). The intra-region same-kind + ordinal is positional, so deleting the first of two same-kind + operators makes the survivor inherit the deleted one's id. An + adjudicator diffing those two runs would report the deleted + obligation as still-open and the survivor as new — both wrong. This + is the very failure mode alternative (c) was rejected for; the + ordinal reintroduces a bounded form of it by construction. It is + accepted because the alternatives are worse, and MITIGATED at the + consumer: FEAT-065 degrades to `uncertain` rather than claiming + `discharged` when a region's same-kind multiset changed. + (2) The pc-shift invariance holds only for insertions that contain no + same-kind operator in the same region and open no new sibling region + (a new sibling renumbers `opened[depth]` and every path beneath it). + FEAT-064's AC is qualified accordingly. + (3) `if`/`else` share one region and one ordinal counter, so an edit in + one branch renumbers same-kind operators in the other. + (4) Two UNNAMED functions with byte-identical bodies share a + `body_shape_hash` and therefore collide across functions. Only the + name-section/export identities are function-unique. + (5) `try_table` (and legacy `try`) open an `End`-terminated region but are + not treated as path markers, so their `End` pops a region they never + opened and the paths below are wrong for exception-handling modules. + Tracked; no panic and no intra-function collision. alternatives: > (a) Source-line identity via DWARF — rejected as the primary: scry analyses Wasm binaries that frequently carry no DWARF, and it would diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 36684cc..33adc9b 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -973,7 +973,9 @@ artifacts: phase: phase-3 acceptance-criteria: - "Given a module and an edit that changes code in an unrelated function, When scry re-analyzes, Then every obligation ID outside the edited function is unchanged." - - "Given an edit that inserts instructions EARLIER in the same function, When scry re-analyzes, Then obligation IDs for later sites in that function are unchanged (pc-shift immunity)." + - "Given an edit that inserts instructions EARLIER in the same function AND the inserted code contains no operator of the same kind in the same region and opens no new block/loop/if at the same-or-shallower depth, When scry re-analyzes, Then obligation IDs for later sites in that function are unchanged (pc-shift immunity). QUALIFIED after clean-room review: the unrestricted form of this AC is FALSE — see DD-020's limitation section. The original wording was met only by a fixture selected around the failing case." + - "Given one operator that raises SEVERAL obligations (an `i32.div_s` raises both div-by-zero and signed-overflow at one pc), When scry stamps identities, Then the obligations receive DISTINCT ids — the site alone is not a discriminator." + - "Given a module-scoped advisory (unbounded-stack, which uses a `(func 0, pc 0)` sentinel rather than a real site), When scry stamps identities, Then it receives a module-scoped identity that neither collides with a genuine advisory at func 0 pc 0 nor drifts when func 0's first instruction changes." - "Given proofs/rocq/ObligationId.v, When built, Then `id equality implies same structural site` is proven admit-free; the converse is explicitly NOT claimed." links: - type: traces-to @@ -999,6 +1001,17 @@ artifacts: capability REQ-018 promised: an agent's edit judged by a SOUND over-approximation, so a satisfied oracle is a proof the trap cannot fire — not "the tests still pass". + CONSERVATISM (added after the FEAT-064 clean-room): obligation identity is + not injective across arbitrary edits — a same-kind operator deleted earlier + in a region transfers its id to the next one (DD-020 limitation). The + adjudicator must therefore treat `discharged` exactly as the analyzer + treats PROVEN-SAFE: claim it only when it is certain. When a function's + same-kind operator multiset changed in a way that could alias, the verdict + degrades to `uncertain`, never to `discharged`. A sound checker that + over-claims a discharge is the same error as an unsound analysis, one layer + up — and it is the error an agent optimising against the verdict would + exploit fastest. + HONESTY (the load-bearing distinction): `removed-with-code` must never be reported as `discharged`. Deleting the code that contained an unproven obligation is not proving anything, and an agent optimising against a diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index ec8dc18..177d0cb 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -666,6 +666,15 @@ pub struct Advisory { /// state. `None` for other classes. A ready seed for a repro / regression /// test; see [`Counterexample`] for the reachability caveat. pub counterexample: Option, + /// FEAT-064 (REQ-020, DD-020): a STABLE, content-addressed identity for this + /// site — invariant under instruction insertion elsewhere in the module and + /// elsewhere in the same function, unlike `(func_index, pc)` which renumbers + /// on any edit. It is what a fix-verify loop keys on: without it a consumer + /// comparing two runs cannot distinguish DISCHARGED from MOVED. + /// + /// Empty when no identity could be derived. Opaque by construction — the + /// layout is not a contract; do not parse it. + pub obligation_id: String, } /// FEAT-055 (REQ-018): a candidate counterexample for an `UnprovenObligation` @@ -2385,13 +2394,16 @@ pub fn analyze( compute_handle_findings(&defined_funcs, &import_func_meta, import_func_count); // FEAT-059: synthesise the sound findings into ranked remediation guidance // (pure synthesis over the results above; borrows before they are moved). - let advisories = compute_advisories( + let mut advisories = compute_advisories( &gaps, &trap_checks, &handle_findings, &stack_usage, memory_min_bytes, ); + // FEAT-064: give every advisory an identity that survives the next edit, so + // a consumer comparing two runs can tell DISCHARGED from MOVED. + stamp_obligation_ids(&mut advisories, &defined_funcs, &function_meta); Ok(AnalysisResult { invariants, @@ -2988,6 +3000,156 @@ fn trap_counterexample(kind: TrapKind, op: &str, memory_size_bytes: u64) -> Coun /// finding it derives from (a POTENTIAL-TRAP becomes an `UnprovenObligation`, /// never a `DefiniteFault`). Ranked DefiniteFault > UnprovenObligation > /// PrecisionGap > LeverageableFact. +/// FEAT-064 (REQ-020, DD-020): the STRUCTURAL KEY of every operator in a body — +/// the part of an obligation identity that survives an edit. +/// +/// For each pc returns `(path, ordinal)`: +/// * `path` — the chain of enclosing `block`/`loop`/`if` SIBLING ordinals from +/// the function root, e.g. `"b0.l1"` = the 2nd region (a loop) inside the +/// 1st region (a block). Raw pcs never appear, which is exactly why +/// inserting instructions earlier in the function does not disturb it. +/// * `ordinal` — the operator's index among SAME-KIND operators within its own +/// enclosing region, so two `i32.load`s in one block stay distinguishable +/// without reintroducing a global counter. +/// +/// Pure function of the operator list: it perturbs no analysis state and is +/// independently testable. +fn structural_keys(ops: &[Operator<'_>]) -> Vec<(String, u32)> { + let mut out: Vec<(String, u32)> = Vec::with_capacity(ops.len()); + // Enclosing regions as (kind marker, sibling ordinal at that depth). + let mut path: Vec<(char, u32)> = Vec::new(); + // How many regions have been opened so far at each depth. + let mut opened: Vec = alloc::vec![0]; + // Per-region same-kind operator counters. + let mut kinds: Vec> = + alloc::vec![alloc::collections::BTreeMap::new()]; + + for op in ops { + let path_str = path + .iter() + .map(|(c, n)| format!("{c}{n}")) + .collect::>() + .join("."); + let kind = op_report_name(op); + let slot = kinds + .last_mut() + .expect("kind stack non-empty") + .entry(kind) + .or_insert(0); + let ordinal = *slot; + *slot += 1; + out.push((path_str, ordinal)); + + let marker = match op { + Operator::Block { .. } => Some('b'), + Operator::Loop { .. } => Some('l'), + Operator::If { .. } => Some('i'), + _ => None, + }; + if let Some(m) = marker { + let depth = path.len(); + let n = opened[depth]; + opened[depth] += 1; + path.push((m, n)); + opened.push(0); + kinds.push(alloc::collections::BTreeMap::new()); + } else if matches!(op, Operator::End) { + // The body's final `End` closes no region — guard the pops. + if !path.is_empty() { + path.pop(); + opened.pop(); + kinds.pop(); + } + } + } + out +} + +/// FEAT-064: hash of a body's structural SHAPE (opcode sequence, immediates +/// elided). The last-resort function identity, used only when a module carries +/// neither a name section nor an export for the function — see DD-020 for why +/// it is deliberately the weakest of the three. +fn body_shape_hash(ops: &[Operator<'_>]) -> String { + let mut h = Sha256::new(); + for op in ops { + h.update(op_report_name(op).as_bytes()); + h.update(b";"); + } + let d = h.finalize(); + let mut out = String::with_capacity(16); + for b in d.iter().take(8) { + out.push_str(&format!("{b:02x}")); + } + out +} + +/// FEAT-064: the content address itself. Opaque, fixed-width; consumers must not +/// parse it (DD-020). +fn obligation_id_of(func_ident: &str, path: &str, kind: &str, ordinal: u32, code: &str) -> String { + let mut h = Sha256::new(); + h.update(func_ident.as_bytes()); + h.update(b"|"); + h.update(path.as_bytes()); + h.update(b"|"); + h.update(kind.as_bytes()); + h.update(b"|"); + h.update(ordinal.to_le_bytes()); + // Clean-room: one operator can raise SEVERAL obligations (an `i32.div_s` + // raises both div-by-zero and signed-overflow), so the site alone does not + // discriminate. The advisory's code is the fifth component. + h.update(b"|"); + h.update(code.as_bytes()); + let d = h.finalize(); + let mut out = String::with_capacity(16); + for b in d.iter().take(8) { + out.push_str(&format!("{b:02x}")); + } + out +} + +/// FEAT-064: does this advisory describe the MODULE rather than a code site? +/// Such advisories carry `(func 0, pc 0)` as a SENTINEL, so giving them a site +/// identity would collide with a genuine advisory there, drift whenever func 0's +/// first instruction changes, and yield nothing when index 0 is an import +/// (clean-room finding). +fn is_module_scoped(code: &str) -> bool { + code == "unbounded-stack" +} + +/// FEAT-064: stamp every advisory with its stable obligation identity. +/// Function identity is the name-section / export name when the module carries +/// one, else the body-shape hash (DD-020's precedence). +fn stamp_obligation_ids( + advisories: &mut [Advisory], + defined_funcs: &[DefinedFunc<'_>], + function_meta: &[FunctionMeta], +) { + for a in advisories.iter_mut().filter(|a| is_module_scoped(&a.code)) { + a.obligation_id = obligation_id_of("", "", "", 0, &a.code); + } + for f in defined_funcs { + let ident = function_meta + .iter() + .find(|m| m.func_index == f.abs_index) + .and_then(|m| m.name.clone()) + .unwrap_or_else(|| body_shape_hash(&f.ops)); + let keys = structural_keys(&f.ops); + for a in advisories + .iter_mut() + .filter(|a| a.func_index == f.abs_index && !is_module_scoped(&a.code)) + { + if let Some((path, ordinal)) = keys.get(a.pc as usize) { + let kind = f + .ops + .get(a.pc as usize) + .map(op_report_name) + .unwrap_or_else(|| a.code.clone()); + a.obligation_id = obligation_id_of(&ident, path, &kind, *ordinal, &a.code); + } + } + } +} + fn compute_advisories( gaps: &[Gap], trap_checks: &[TrapCheck], @@ -3025,6 +3187,7 @@ fn compute_advisories( suggested_action: action.into(), verification: "re-run scry: this handle_findings entry disappears".into(), counterexample: None, + obligation_id: String::new(), }); } @@ -3064,6 +3227,7 @@ fn compute_advisories( t.op, code ), counterexample: Some(trap_counterexample(t.kind, &t.op, memory_size_bytes)), + obligation_id: String::new(), }); } TrapVerdict::ProvenSafe => { @@ -3090,6 +3254,7 @@ fn compute_advisories( t.op ), counterexample: None, + obligation_id: String::new(), }); } } @@ -3130,6 +3295,7 @@ fn compute_advisories( g.func_index, g.pc ), counterexample: None, + obligation_id: String::new(), }); } @@ -3148,6 +3314,7 @@ fn compute_advisories( .into(), verification: "re-run scry: stack_usage.max_stack_bytes becomes Bytes(n)".into(), counterexample: None, + obligation_id: String::new(), }); } @@ -3883,49 +4050,98 @@ impl Interp<'_, '_> { &mut labels[idx] } - /// FEAT-016 slice-2b-i guard refinement. If the ops at `pc` are the - /// canonical comparison-guarded branch `local.get L; i32.const C; ; br_if D` (4 ops) or `local.get L; i32.eqz; br_if D` (3 ops), - /// refine `L`'s interval by the guard on both edges — record the - /// taken-edge locals (guard true) into label `D`, set `ctx.locals` to the - /// not-taken-edge locals (guard false) — and return the pc just past the - /// idiom. Returns `None` (caller handles `pc` normally) for anything else. - /// The idiom's net operand-stack effect is zero (push L, push C, cmp pops - /// 2 / pushes 1, br_if pops 1), so the stack is left untouched. + /// FEAT-016 slice-2b-i guard refinement, extended by FEAT-070 (REQ-020). + /// If the ops at `pc` are a guarded branch on a single local, refine `L`'s + /// interval by the guard on both edges — record the taken-edge locals + /// (guard true) into label `D`, set `ctx.locals` to the not-taken-edge + /// locals (guard false) — and return the pc just past the idiom. Returns + /// `None` (caller handles `pc` normally) for anything else. + /// + /// Recognised shapes, where the leading op is `local.get L` **or** + /// `local.tee L` (FEAT-070 — LLVM emits the tee form constantly, for + /// increment-and-test and count-to-zero loops): + /// + /// ```text + /// L; i32.const C; ; br_if D (4 ops) + /// L; i32.eqz; br_if D (3 ops) taken ⇔ L == 0 + /// L; br_if D (2 ops) taken ⇔ L ≠ 0 + /// ``` + /// + /// The 2-op form is the bare-truthiness branch: `br_if` takes the edge when + /// the popped value is non-zero, so the FALL-THROUGH pins `L` to exactly 0. + /// That is the dual of the `i32.eqz` shape and the reason a count-to-zero + /// loop's exit value is knowable at all. + /// + /// Operand stack: with a leading `local.get` the idiom's net effect is zero + /// (push L, push C, cmp pops 2 / pushes 1, br_if pops 1). With a leading + /// `local.tee` it is **−1** — the tee'd value arrives on the stack and is + /// ultimately consumed by the `br_if` — so the tee form pops once. A + /// shape-blind skip would leak or underflow the modelled stack. + /// + /// Soundness note for the tee form: `local.tee L` **assigns** `L`, and this + /// peephole bypasses the normal `LocalTee` transfer (including + /// [`Self::octagon_transfer`]). The assignment is therefore applied here and + /// `L`'s octagon relations are FORGOTTEN — retaining a relation for a local + /// that was just overwritten would be unsound. All bail-out checks run + /// before any mutation, so a `None` return leaves `ctx` untouched and the + /// caller can re-process the ops normally. fn try_guard_brif(&self, pc: usize, ctx: &mut FuncCtx, labels: &mut [Label]) -> Option { if ctx.degraded { return None; } let ops = self.ops; - // Recognise `local.get L; i32.const C; ; br_if D`. - let (local, c, op, depth, next) = match ops.get(pc)? { - Operator::LocalGet { local_index } => { - let l = *local_index; - match (ops.get(pc + 1)?, ops.get(pc + 2)?, ops.get(pc + 3)) { - // 4-op: local.get L; const C; cmp; br_if D - ( - Operator::I32Const { value }, - cmp, - Some(Operator::BrIf { relative_depth }), - ) => { - let gop = guard_op(cmp)?; - (l, *value as i64, gop, *relative_depth, pc + 4) - } - // 3-op: local.get L; i32.eqz; br_if D (L == 0) - (Operator::I32Eqz, Operator::BrIf { relative_depth }, _) => { - (l, 0, GuardOp::Eq, *relative_depth, pc + 3) - } - _ => return None, - } + // Leading op: a read (`local.get`) or a read-modify (`local.tee`). + let (local, is_tee) = match ops.get(pc)? { + Operator::LocalGet { local_index } => (*local_index, false), + Operator::LocalTee { local_index } => (*local_index, true), + _ => return None, + }; + // Guard shape, longest match first. + let (c, op, depth, next) = match (ops.get(pc + 1)?, ops.get(pc + 2), ops.get(pc + 3)) { + (Operator::I32Const { value }, Some(cmp), Some(Operator::BrIf { relative_depth })) => { + (*value as i64, guard_op(cmp)?, *relative_depth, pc + 4) + } + (Operator::I32Eqz, Some(Operator::BrIf { relative_depth }), _) => { + (0, GuardOp::Eq, *relative_depth, pc + 3) } + // FEAT-070: bare truthiness — taken ⇔ L ≠ 0, fall-through ⇔ L == 0. + (Operator::BrIf { relative_depth }, _, _) => (0, GuardOp::Ne, *relative_depth, pc + 2), _ => return None, }; - // The local must be a tightenable i32 interval; otherwise no refine. - let iv = match ctx.locals.get(local as usize) { - Some(AbstractValue::I32Interval(iv)) => *iv, - _ => return None, + // ── all bail-out checks BEFORE any mutation ────────────────────── + if local as usize >= ctx.locals.len() { + return None; + } + // The interval to refine: for the tee form it is the value being + // assigned (the stack top), not the local's stale pre-assignment value. + let iv = if is_tee { + match ctx.operand_stack.last() { + Some(AbstractValue::I32Interval(iv)) => *iv, + _ => return None, + } + } else { + match ctx.locals.get(local as usize) { + Some(AbstractValue::I32Interval(iv)) => *iv, + _ => return None, + } }; + + // ── mutation from here on ──────────────────────────────────────── + if is_tee { + // Consume the tee'd value and apply the assignment this peephole + // is skipping; forget the local's relations (see the doc comment). + let _ = ctx.operand_stack.pop(); + ctx.locals[local as usize] = AbstractValue::I32Interval(iv); + // Apply the octagon side of the assignment this peephole skips. + // `octagon_transfer` models the recognised producer shapes (const / + // copy / add-const) and FORGETS `local` otherwise — at least as + // sound as a blanket forget, and strictly more precise on the + // increment/decrement-and-test idiom FEAT-070 exists to handle + // (clean-room finding: the blanket forget was a precision + // regression on this feature's own motivating shape). + self.octagon_transfer(pc, ctx); + } let taken_iv = refine_interval(iv, op, c, true); let not_taken_iv = refine_interval(iv, op, c, false); @@ -8710,6 +8926,211 @@ mod tests { ); } + /// First non-empty obligation id recorded for `func`. + fn adv_id(r: &AnalysisResult, func: u32) -> String { + r.advisories + .iter() + .find(|a| a.func_index == func && !a.obligation_id.is_empty()) + .unwrap_or_else(|| { + panic!( + "an advisory with an id for func {func}; got {:?}", + r.advisories + ) + }) + .obligation_id + .clone() + } + + /// FEAT-064 AC#1 (REQ-020) — an edit in an UNRELATED function must not + /// disturb this function's obligation identity. + #[test] + fn feat064_id_survives_edit_in_unrelated_function() { + let base = analyze_default( + "(module \ + (func (export \"a\") (param i32) (result i32) i32.const 10 local.get 0 i32.div_s) \ + (func (export \"b\") (param i32) (result i32) i32.const 20 local.get 0 i32.div_s))", + ); + // Function "a" grows two instructions; "b" is untouched. + let edited = analyze_default( + "(module \ + (func (export \"a\") (param i32) (result i32) \ + i32.const 7 local.set 0 i32.const 10 local.get 0 i32.div_s) \ + (func (export \"b\") (param i32) (result i32) i32.const 20 local.get 0 i32.div_s))", + ); + assert_eq!( + adv_id(&base, 1), + adv_id(&edited, 1), + "an edit in another function must not change func 1's obligation id" + ); + } + + /// FEAT-064 AC#2 — pc-shift immunity: inserting instructions EARLIER in the + /// SAME function must not change the identity of a later site. This is the + /// property `(func_index, pc)` cannot provide, and the one the fix-verify + /// loop depends on. + #[test] + fn feat064_id_survives_pc_shift_in_same_function() { + let base = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) (local i32) \ + i32.const 20 local.get 0 i32.div_s))", + ); + // The inserted code writes a DIFFERENT local, so the observed div keeps + // the same class and code — an insertion that changed the divisor would + // legitimately change the identity and prove nothing about pc-shift. + let shifted = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) (local i32) \ + i32.const 99 local.set 1 i32.const 20 local.get 0 i32.div_s))", + ); + // The div moved from pc 2 to pc 4 … + let base_pc = base + .advisories + .iter() + .find(|a| a.func_index == 0) + .map(|a| a.pc); + let shifted_pc = shifted + .advisories + .iter() + .find(|a| a.func_index == 0) + .map(|a| a.pc); + assert_ne!(base_pc, shifted_pc, "fixture must actually shift the pc"); + // … but its identity did not. + assert_eq!( + adv_id(&base, 0), + adv_id(&shifted, 0), + "a pc shift within the same function must not change the obligation id" + ); + } + + /// FEAT-064 (clean-room finding) — ONE operator can raise SEVERAL + /// obligations: an `i32.div_s` with an unknown divisor raises both + /// div-by-zero and signed-overflow at the same pc. The site alone therefore + /// does not discriminate, and two obligations sharing an id would make the + /// FEAT-065 adjudicator conflate them. + #[test] + fn feat064_two_obligations_at_one_pc_get_distinct_ids() { + let r = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) \ + local.get 0 local.get 0 i32.div_s))", + ); + let at_pc: Vec<(&str, &str)> = r + .advisories + .iter() + .filter(|a| !a.obligation_id.is_empty()) + .map(|a| (a.code.as_str(), a.obligation_id.as_str())) + .collect(); + assert!( + at_pc.len() >= 2, + "fixture must raise several obligations; got {at_pc:?}" + ); + let mut ids: Vec<&str> = at_pc.iter().map(|(_, i)| *i).collect(); + ids.sort_unstable(); + let before = ids.len(); + ids.dedup(); + assert_eq!( + ids.len(), + before, + "distinct obligations must not share an id; got {at_pc:?}" + ); + } + + /// FEAT-064 anti-vacuity — the id must actually DISCRIMINATE. Two distinct + /// div sites in one function must not collapse to the same identity, or the + /// "survives the edit" tests above would pass on a constant. + #[test] + fn feat064_distinct_sites_get_distinct_ids() { + let r = analyze_default( + "(module (func (export \"b\") (param i32) (result i32) \ + i32.const 10 local.get 0 i32.div_s \ + i32.const 20 local.get 0 i32.div_s i32.add))", + ); + let ids: Vec<&String> = r + .advisories + .iter() + .filter(|a| a.func_index == 0 && !a.obligation_id.is_empty()) + .map(|a| &a.obligation_id) + .collect(); + assert!( + ids.len() >= 2, + "fixture must yield two advisories; got {ids:?}" + ); + assert_ne!(ids[0], ids[1], "distinct sites must get distinct ids"); + } + + /// FEAT-070 (REQ-020) — guard refinement for `br_if` on a BARE value. + /// `local.tee $i; br_if` is the count-to-zero loop LLVM emits: it branches + /// while the value is non-zero, so the FALL-THROUGH edge pins the local to + /// exactly 0. Before FEAT-070 scry matched only comparison-guarded idioms + /// (`local.get L; const C; cmp; br_if` / `local.get L; i32.eqz; br_if`), + /// so this shape left the counter unrefined. + /// + /// The assertion is deliberately position-specific: `(local i32)` is + /// zero-initialised, so an "any point has [0,0]" predicate passes VACUOUSLY + /// on the entry point and tests nothing (caught by running this oracle red + /// before implementing). + #[test] + fn feat070_brif_on_bare_tee_pins_fallthrough_to_zero() { + let r = analyze_default( + "(module (func (export \"run\") (result i32) (local i32) \ + i32.const 5 local.set 0 \ + block loop \ + local.get 0 i32.const 1 i32.sub local.tee 0 \ + br_if 0 \ + end end \ + local.get 0))", + ); + // The LAST emitted point is after the loop; the only way out of the + // loop is br_if falling through, i.e. the counter is exactly 0 there. + let last = r + .invariants + .points + .iter() + .max_by_key(|p| p.pc) + .expect("at least one program point"); + let l0 = last + .locals + .iter() + .find(|l| l.local_index == 0) + .expect("local 0 present"); + assert!( + matches!(&l0.value, AbstractValue::I32Interval(iv) if iv.lo == 0 && iv.hi == 0), + "post-loop local 0 must be pinned to [0,0] by the br_if fall-through; \ + got {:?} at pc={}", + l0.value, + last.pc + ); + } + + /// FEAT-070 — the peephole must keep the modelled operand stack balanced. + /// `local.tee` consumes an incoming stack value that `local.get` does not, + /// so a shape-blind skip of the idiom leaks (or underflows) the stack. + #[test] + fn feat070_tee_guard_keeps_operand_stack_balanced() { + let r = analyze_default( + "(module (func (export \"run\") (result i32) (local i32) \ + i32.const 3 local.set 0 \ + block loop \ + local.get 0 i32.const 1 i32.sub local.tee 0 \ + br_if 0 \ + end end \ + i32.const 7))", + ); + let last = r + .invariants + .points + .iter() + .max_by_key(|p| p.pc) + .expect("at least one program point"); + // Exactly the `i32.const 7` is live at the end. A leaked tee value + // would leave 2; an underflow would have degraded the function. + assert_eq!( + last.operand_stack.len(), + 1, + "operand stack must carry exactly the final const; got {:?} at pc={}", + last.operand_stack, + last.pc + ); + } + /// FEAT-062 — the tracked memory content is SURFACED on the program points /// (so scry-viz can render it). A `i32.store 42 @16` records the cell /// [16,17) → [42,42]; it must appear in `point.memory`. diff --git a/crates/scry-viz/src/lib.rs b/crates/scry-viz/src/lib.rs index 422a3ac..142f2a3 100644 --- a/crates/scry-viz/src/lib.rs +++ b/crates/scry-viz/src/lib.rs @@ -2130,6 +2130,7 @@ mod tests { suggested_action: "guard it".into(), verification: "re-run scry".into(), counterexample: None, + obligation_id: format!("test-{i:04x}"), }; for i in 0..(ADVISORY_PER_CLASS_CAP as u32 + 25) { r.advisories.push(mk(i)); From f33f57a9426ce16648030b07f653204b56c3829e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 7 Aug 2026 06:43:09 +0200 Subject: [PATCH 3/3] =?UTF-8?q?deny:=20ignore=20RUSTSEC-2026-0222=20(wasmt?= =?UTF-8?q?ime,=20dev-only)=20=E2=80=94=20bump=20tracked=20separately?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- deny.toml | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/deny.toml b/deny.toml index 37fc803..ed5a626 100644 --- a/deny.toml +++ b/deny.toml @@ -41,6 +41,21 @@ ignore = [ # harness does not format crossbeam pointers. No impact on shipped crates or # the analyzer component. Re-evaluate when wasmtime/rayon are bumped. "RUSTSEC-2026-0204", + # RUSTSEC-2026-0222 — wasmtime: "Stores can mix up type indices between + # engines" (a type-confusion / sandbox-integrity bug in the embedding API). + # Reachability, verified rather than assumed: wasmtime is a dependency of + # `scry-host-tests` ONLY, which is `publish = false`; `cargo metadata` + # confirms NO published `scry-sai-*` crate has wasmtime as a normal + # dependency, and it is not in the shipped `scry.wasm` (which embeds no + # engine). The harness is a test process running OUR OWN fixtures and OUR + # OWN composed component — it is not a multi-tenant sandbox host, so the + # crafted cross-engine usage this advisory requires has no attack surface + # here. NOTE: this is deliberately NOT a permanent exemption — there is no + # patched 45.x line (fixes landed in 46.0.2 / 47.0.3), so the durable fix is + # a wasmtime major bump, tracked as its own change rather than smuggled into + # a feature PR. Re-evaluate when that bump lands; this entry should then be + # DELETED, not carried forward. + "RUSTSEC-2026-0222", ] [licenses]