From b10413fa8c0d78c2333ad158073ce43df2aed4b8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 20 Aug 2026 06:41:40 +0200 Subject: [PATCH 1/5] plan: split REQ-020, unblock v3.3.0, and add the dogfood + visualization features MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit v3.3.0 was uncuttable for a TRACEABILITY reason, not a code reason. REQ-020 is written as a conjunction — "stable obligation identity + a machine-checkable oracle" — and the oracle half (FEAT-065) was refuted in review before it shipped (six wrong-verdict paths, scry#122; DD-021's rationale retracted in place). A conjunctive requirement cannot be half-discharged, so the identity half was being held hostage to a design defect it does not share. Split rather than reword. Rewording REQ-020 to hide its second half would be the artifact-level version of the four vacuous oracles written this month. REQ-020 (v3.3.0) identity an agent can CITE — verifiable on its own REQ-021 (v3.4.0) the GATE, with an adversarial acceptance bar drawn directly from scry#122: self-comparison yields only still-open; deletion never yields discharged; a cardinality-preserving delete+insert yields uncertain; a newly introduced fault always yields a verdict. Each case must be shown RED against the pre-rework adjudicator before it is fixed. FEAT-065 follows REQ-021 to v3.4.0. FEAT-066's `verify` MCP tool follows it — exposing a refuted adjudicator over MCP would put a wrong verdict directly into an agent's tool loop, so the v3.3.0 server omits the tool rather than documenting a caveat. Two new v3.3.0 features, neither depending on the adjudicator: FEAT-072 Obligation anchors + the delta view. FEAT-064 currently ships a key that nothing displays and no consumer can cite; the dashboard still hands out (func_index, pc) references it knows will break. Anchors ship unconditionally. The delta view renders the ADJUDICABLE FRACTION and suppresses the discharge count while scry#122 is open, enforced by a test that greps the page. FEAT-073 Self-adjudication harness — scry adjudicates scry across its own history, in observation mode. Purpose is evidence: scry#122 lists nine work items and nothing says which fire on real code. The harness exits 0 unconditionally and stamps scry#122 into every artifact, so observation mode is a property of the code rather than a convention a later edit can drop. DD-022 records all three decisions with the alternatives rejected, and states the separation the plan depends on: scale does not substitute for adversarial reading. The six findings came from reading, not volume, and a 6,191-obligation run producing plausible numbers has exactly the shape of a vacuous oracle. FEAT-073 measures WHICH failures occur; REQ-021's bar establishes THAT each is fixed. Neither is evidence for the other. DD-021 lands here in its already-retracted form: a refuted design decision belongs in the design record whether or not its code ever merges. rivet validate: PASS. v3.3.0 is now free of the adjudicator; v3.4.0 carries REQ-021 + FEAT-065 + FEAT-057. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- artifacts/design.yaml | 226 +++++++++++++++++++++++++++++++++++++ artifacts/roadmap-3.0.yaml | 210 +++++++++++++++++++++++++++++++--- 2 files changed, 420 insertions(+), 16 deletions(-) diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 0e64ad6..5ebedbe 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -664,3 +664,229 @@ artifacts: target: FEAT-064 - type: traces-to target: FEAT-065 + + - id: DD-021 + type: design-decision + title: "v3.3 — Adjudicating a NON-INJECTIVE identity: three keys, and `discharged` as a certainty claim" + status: proposed + tags: [ai-agent, fix-verify-loop, oracle, conservatism, v3.3] + description: > + How FEAT-065 compares two runs given that FEAT-064's identity is provably + NOT injective across arbitrary edits. Two findings forced this to be a + decision rather than an implementation detail. + (1) `proofs/rocq/ObligationId.v` PROVES the aliasing hazard + (`survivor_inherits_deleted_identity`): delete the first of two same-kind + operators in a region and the survivor's ordinal — hence its identity — + becomes exactly the deleted site's. A naive diff-by-identity can therefore + report a FALSE `discharged`: site A is an open obligation, site B at the + same kind is PROVEN-SAFE, A is deleted, B inherits A's identity, and A's + identity now resolves to a proven-safe advisory although A was never fixed. + (2) The advisory CODE is a required component of the identity (clean-room: + one `i32.div_s` raises both div-by-zero and signed-overflow at one pc, so + the site alone does not discriminate). But fixing an obligation CHANGES its + code — `div-by-zero` becomes `proven-safe` — so the full identity is + unstable across exactly the transition the adjudicator exists to detect. + Matching on it alone would render every genuine discharge as + "one identity vanished, an unrelated one appeared". + fields: + decision: > + Emit THREE keys per advisory, each with one job: + * `obligation_id` = hash(func_ident, path, kind, ordinal, CODE) — + globally unique per obligation. What a consumer stores and cites. + * `site_key` = hash(func_ident, path, kind, ordinal) — identifies + the SITE, stable across a code/class change. This is what FEAT-065 + MATCHES ON, so a div-by-zero becoming proven-safe is recognised as + the same site changing state rather than two unrelated events. + * `group_key` = hash(func_ident, path, kind) — the ORDINAL DOMAIN. + Its membership is what aliasing perturbs, so it is the conservatism + signal. + Adjudication outcomes: `discharged`, `still-open`, `regressed`, `moved`, + `removed-with-code`, `uncertain`. + `discharged` is a CERTAINTY CLAIM and requires all of: the site_key was an + open obligation before; it is proven-safe (or raises no obligation) after; + AND its `group_key`'s site_key SET is unchanged between the two runs. + If that set changed, the verdict is `uncertain` — never `discharged`. + `removed-with-code` (the site no longer exists) is a distinct outcome and + must never be reported as `discharged`. + rationale: > + The adjudicator inherits the analyzer's discipline one layer up: scry + claims PROVEN-SAFE only when the abstract state rules the trap out, and + FEAT-065 claims `discharged` only when identity cannot have aliased. + Over-claiming a discharge is the same class of error as an unsound + analysis, and it is the error an agent optimising against the verdict + would exploit fastest — an agent rewarded for `discharged` learns to + DELETE code, which is why `removed-with-code` is kept strictly separate. + RETRACTED 2026-08-11 by adversarial review — this decision originally + justified the group-set check by asserting that "aliasing by deletion or + insertion NECESSARILY changes the ordinal domain's membership". THAT IS + FALSE, and it was the sentence the whole conservatism rule rested on. A + deletion PAIRED WITH a same-kind insertion in the same region leaves the + group's site_key set byte-identical, so the check passes and a FALSE + `discharged` is produced — the delete-instead-of-fix reward hack this + rule exists to prevent. The group-set check is therefore a NECESSARY but + NOT SUFFICIENT condition, and on its own it does not make `discharged` + a certainty claim. Sound matching needs CONTENT corroboration (hashing + the operator's local context so a replaced operator cannot inherit a + predecessor's identity) rather than a positional ordinal plus a + population check. See the limitations field; the implementation is held + in draft until this is resolved. + limitations: > + FOUND BY ADVERSARIAL REVIEW 2026-08-11 (all reproduced; the + implementation is in draft, nothing shipped): + (1) CARDINALITY-PRESERVING DELETION defeats the group-set check — delete + the open operator and append a same-kind safe one, and the site set + is unchanged, yielding a false `discharged`. This falsifies the + rationale's central claim (see above). + (2) `body_shape_hash` is the WHOLE function identity in the no-name / + no-export case, so two structurally identical functions share + site/group keys — deleting a whole function carrying an obligation + reports `discharged`. Conversely ANY opcode edit in such a function + moves every key in it, so for stripped modules `discharged` is + unreachable for the canonical fix shape (insert a guard / replace a + `local.get` with a constant). Mitigation direction: never claim + `discharged` when the function identity came from the shape-hash + fallback — degrade to `uncertain`. + (3) OBLIGATION LAUNDERING: wrapping the site in a typed `block`/`if` + routes it through `havoc_region`, which emits no trap check, no gap + and no advisory when the write set is empty and the region contains + no call — so a LIVE obligation disappears and reads as + `removed-with-code`. Root cause is a pre-existing FEAT-040/046 + reporting hole, tracked separately; the adjudicator must treat + "absent from a function that degraded or gained a havoc region" as + `uncertain`. + (4) `regressed` is FABRICATED on a byte-identical module: `site_key` + excludes the code, so an open div-by-zero and a proven + signed-overflow at one `i32.div_s` share a site key, putting it in + the proven set. Self-comparison returns contradictory `still-open` + and `regressed` verdicts under one id with an invented before-code. + The proven-safe advisory does not record WHICH trap kind it proves, + which is the underlying data gap. + (5) NEW obligations produce NO verdict at all (only sites that + previously carried a proven fact are checked), so a fault introduced + where nothing was flagged before passes the gate clean. This is the + blindest direction for an autonomous agent. + (6) `obligation_id` is not unique, against this decision's own claim: two + ProvenSafe trap kinds at one pc both use code `proven-safe`, and the + shape-hash collision duplicates ids across functions. + PRE-EXISTING RESIDUAL, disclosed from the start: a pure REORDERING of two + same-kind operators within one region preserves the group's site_key set + while swapping which site each key denotes (each op takes the other's + ordinal). The group-set check cannot see it, so that edit shape can still + mis-attribute a verdict. It is an unusual edit, its consequence is a + wrong verdict rather than an unsound analysis, and closing it would need + content corroboration beyond the key (e.g. hashing the operator's local + context) — deferred, and named here so a consumer is not surprised. + Consequence for consumers: a `discharged` verdict is evidence, not proof, + under a same-kind reordering; `uncertain` is the honest default whenever + the domain moved. + links: + - type: satisfies + target: REQ-021 + - type: traces-to + target: FEAT-065 + - type: traces-to + target: DD-020 + + - id: DD-022 + type: design-decision + title: "Dogfood the adjudicator in OBSERVATION MODE, and publish the uncertain fraction rather than the discharge count" + status: proposed + description: > + Two coupled decisions taken on 2026-08-20, after adversarial review found + six wrong-verdict paths in the FEAT-065 adjudicator (scry#122) and DD-021's + central rationale was retracted in place. + + DECISION 1 — MEASURE BEFORE REWORKING. Run the REFUTED adjudicator over + scry's own commit history (FEAT-073) before implementing any of scry#122's + nine work items, and let the observed distribution order them. + Alternative rejected: fix all nine, then dogfood. Rejected because nine + fixes guessed at in the dark is how the first implementation was built, and + because scry's own history is a better adversary than any fixture we would + write — it contains real deletions, real same-kind insertions and real + renames at 6,191-obligation scale. Four vacuous oracles were written in + this project during August 2026; every one passed a fixture chosen by the + same person who wrote the code. Real history is not chosen. + + DECISION 2 — OBSERVATION MODE IS STRUCTURAL, NOT PROCEDURAL. The harness + exits 0 unconditionally and stamps scry#122 into every artifact it writes. + Alternative rejected: run it as a gate with a generous threshold. Rejected + because an adjudicator that can wrongly report `discharged` is worse than + none — an agent optimising against the verdict finds the cheapest exploit + (delete the code) before it finds a fix — and a threshold makes that + exploit merely quieter. A comment saying "do not gate on this" is a + convention; a function that cannot return non-zero is a property. + + DECISION 3 — THE PUBLISHED HEADLINE IS THE ADJUDICABLE FRACTION. While + scry#122 is open, the delta view (FEAT-072) renders "of M obligations, K + adjudicable, N uncertain" and NO discharge count, enforced by a test that + greps the rendered page. + Alternative rejected: publish discharges with a caveat paragraph. Rejected + because the dashboard is public, the standing bar is that every public + claim survives Conrad Watt, and a caveat does not travel — the number gets + quoted, the paragraph does not. The uncertain fraction is the one figure + the refutation did not undermine, and it is also the more useful one: it + states how far the matcher can be trusted. When REQ-021 closes, the + discharge count is UN-SUPPRESSED rather than re-implemented, so the + constraint carries no rework cost. + + SEPARATION OF CONCERNS (recorded because it was nearly conflated): scale + does not substitute for adversarial reading. The six findings came from + reading, not from volume, and a 6,191-obligation run producing plausible + numbers has exactly the shape of the vacuous oracles. FEAT-073 measures + WHICH failures occur; REQ-021's adversarial acceptance bar establishes + THAT each is fixed. Both are required; neither is evidence for the other. + tags: [ai-agent, dogfood, honesty, observability, v3.3] + fields: + decision: > + (1) Run the REFUTED adjudicator over scry's own commit history and let + the observed verdict distribution ORDER scry#122's nine work items, + before implementing any of them. + (2) Enforce observation mode STRUCTURALLY — the harness cannot return + non-zero — rather than by a comment asking readers not to gate on it. + (3) Publish the ADJUDICABLE FRACTION ("of M obligations, K adjudicable, + N uncertain") and suppress the discharge count entirely while scry#122 + is open, enforced by a test that greps the rendered page. + rationale: > + ALTERNATIVE REJECTED for (1) — fix all nine items, then dogfood. + Nine fixes guessed at in the dark is exactly how the first + implementation was built. scry's own history is a better adversary than + any fixture we would write: it holds real deletions, real same-kind + insertions and real renames at 6,191-obligation scale. Four vacuous + oracles were written in this project during August 2026 and every one + passed a fixture chosen by whoever wrote the code. Real history is not + chosen. + ALTERNATIVE REJECTED for (2) — run it as a gate with a generous + threshold. An adjudicator that can wrongly report `discharged` is worse + than no adjudicator: an agent optimising against the verdict finds the + cheapest exploit (delete the code) before it finds a fix, and a + threshold only makes that exploit quieter. A comment is a convention; a + function that cannot fail is a property. + ALTERNATIVE REJECTED for (3) — publish discharges with a caveat + paragraph. The dashboard is public and the standing bar is that every + claim survives Conrad Watt. A caveat does not travel: the number gets + quoted, the paragraph does not. The uncertain fraction is both the one + figure the refutation did not undermine and the more useful one, since + it states how far the matcher can be trusted. When REQ-021 closes the + discharge count is UN-SUPPRESSED rather than re-implemented, so the + constraint carries no rework cost. + limitations: > + Scale does not substitute for adversarial reading, and this decision + must not be read as claiming it does. The six findings came from + reading, not from volume, and a 6,191-obligation run producing + plausible numbers has precisely the shape of the four vacuous oracles. + FEAT-073 measures WHICH failures occur; REQ-021's adversarial + acceptance bar establishes THAT each is fixed. Both are required and + neither is evidence for the other. + The harness also samples only scry's own coding style — a Rust/LLVM + Wasm producer. Edit shapes common in hand-written or other-toolchain + Wasm may be absent from the sample, so an UNOBSERVED failure path is + not a refuted one, only an unmeasured one. + links: + - type: satisfies + target: REQ-020 + - type: traces-to + target: FEAT-072 + - type: traces-to + target: FEAT-073 + - type: traces-to + target: DD-021 diff --git a/artifacts/roadmap-3.0.yaml b/artifacts/roadmap-3.0.yaml index 4dc3fa1..3a1659d 100644 --- a/artifacts/roadmap-3.0.yaml +++ b/artifacts/roadmap-3.0.yaml @@ -22,7 +22,8 @@ artifacts: # 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. + # obligations actionable at all (breadth). REQ-020, FEAT-064, + # 066..073. The GATE half split to v3.4.0 as REQ-021/FEAT-065. # v3.4 "Precision ceiling" — convex polyhedra, ELINA- # decomposed, for exact linear inequalities above the octagon. # FEAT-057. Displaced from v3.3 on 2026-08-06 (see its section). @@ -207,14 +208,20 @@ artifacts: - id: REQ-020 type: requirement - title: "An AI agent can be GATED on scry: stable obligation identity + a machine-checkable oracle" + title: "An AI agent can CITE a scry obligation: stable identity that survives the edit" 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. + Two things block the loop. This requirement closes the FIRST; REQ-021 + closes the second. They were ONE requirement until 2026-08-20, when + adversarial review falsified the adjudicator's matching rule before it + shipped (scry#122) — at which point holding a verifiable identity half + hostage to a refuted adjudication half became the wrong trade. Splitting + is the honest move: a conjunctive requirement cannot be half-discharged, + and rewording it to hide the second half would be a vacuous gate. (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 @@ -224,11 +231,12 @@ artifacts: 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. + (2) ADJUDICATION — SPLIT OUT to REQ-021 (v3.4.0) on 2026-08-20. Comparing + a new run against a prior one and classifying each obligation is the other + half of the loop, and it remains the point of the arc; but its matching + rule was refuted in review (DD-021's rationale retracted in place; six + wrong-verdict paths in scry#122) and it must not ship on a positional + ordinal. Identity is verifiable on its own and ships in v3.3.0. MOTIVATION (measured, not assumed): scry's own self-analysis reports 0 proven faults against 6,191 unproven obligations and 1,962 precision gaps. @@ -239,8 +247,9 @@ artifacts: 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`. + the adjudicator (REQ-021) must report it as `removed-with-code`, never as + `discharged`. This statement is the shared honesty constraint across both + halves and is why the split does not weaken either. tags: [ai-agent, fix-verify-loop, identity, oracle, precision, v3.3] fields: priority: must @@ -255,6 +264,56 @@ artifacts: - type: evaluates-tech target: TE-011 + - id: REQ-021 + type: requirement + title: "An AI agent can be GATED on scry: a machine-checkable verdict on its own edit" + status: proposed + release: v3.4.0 + description: > + The ADJUDICATION half of the original REQ-020, split out on 2026-08-20 + after adversarial review refuted the first implementation's matching rule. + + scry shall compare a fresh analysis against a prior one and classify every + obligation by its stable identity (REQ-020 / FEAT-064): discharged / + still-open / regressed / moved / removed-with-code / uncertain. That turns + the v3.1 PROSE oracle ("re-run scry; this trap_check becomes ProvenSafe") + into a machine verdict, so an agent's edit is judged by a SOUND + over-approximation rather than by whether the tests still pass. + + WHY IT IS ITS OWN REQUIREMENT, AND WHY IT IS NOT IN v3.3.0. The first + implementation (FEAT-065, PR #120, never merged) matched obligations on a + positional intra-region ordinal plus a population check, justified by the + claim that aliasing "necessarily" changes the ordinal domain's membership. + That claim is FALSE: a deletion paired with a same-kind insertion leaves + the group byte-identical, producing a false `discharged`. Five further + wrong-verdict paths were found in the same pass (scry#122). + + THE BAR THIS REQUIREMENT MUST CLEAR. An adjudicator that can wrongly + report `discharged` is strictly WORSE than no adjudicator, because an + agent optimising against the verdict finds the cheapest exploit — deleting + the code — before it finds a fix. Verification of this requirement is + therefore adversarial by construction: a self-comparison yields only + `still-open`; a deletion never yields `discharged`; a cardinality- + preserving delete+insert yields `uncertain`; a newly introduced fault + always yields a verdict. Matching must be CONTENT-CORROBORATED, not + positional — DD-020 named this as a deferred option; the review made it + mandatory. + + EVIDENCE BEFORE REWORK: FEAT-073 runs the refuted adjudicator over scry's + OWN commit history in observation mode, so which of the nine scry#122 work + items actually fire on real code is a measurement rather than a guess. + tags: [ai-agent, oracle, fix-verify-loop, gate, adversarial, v3.4] + fields: + priority: must + category: functional + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-018 + - type: traces-to + target: G-005 + # ══════════════════════════════════════════════════════════════════════ # RELEASE v2.6.0 — "Make the analysis observable" # Cash in computed-but-hidden facts; cheap precision; agent/qual readiness. @@ -934,11 +993,17 @@ artifacts: target: TE-011 # ══════════════════════════════════════════════════════════════════════ - # RELEASE v3.3.0 — "Agent-verifiable" (REQ-020) + # RELEASE v3.3.0 — "Agent-citable" (REQ-020) + # RE-SCOPED 2026-08-20. Was "Agent-verifiable" and carried BOTH halves of the + # fix-verify loop. The adjudication half was refuted in review before it + # shipped (scry#122) and moved to v3.4.0 with the new REQ-021. What remains + # here is verifiable on its own: an obligation an agent can CITE, surfaces it + # can reach, and the precision that makes the citations worth having. # 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. + # DEPTH — identity that survives the edit, MADE VISIBLE (anchors, delta + # view) and EXERCISED ON OURSELVES (self-adjudication harness, + # observation mode). The gate itself follows in v3.4.0. # 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. @@ -986,9 +1051,9 @@ artifacts: - id: FEAT-065 type: feature - title: "v3.3 — `scry verify --against`: scry adjudicates its own oracle" + title: "v3.4 — `scry verify --against`: scry adjudicates its own oracle" status: proposed - release: v3.3.0 + release: v3.4.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 @@ -1024,9 +1089,14 @@ artifacts: - "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." + - "ADVERSARIAL BAR (added 2026-08-20 after review refuted the first implementation; each case must be shown RED against the pre-rework adjudicator before it is fixed). Given a module compared with ITSELF, When verify runs, Then EVERY verdict is `still-open` — no `regressed`, no `moved`, no `discharged`. The original test for this passed vacuously." + - "Given a cardinality-preserving edit — one same-kind operator deleted and another inserted in the same region, leaving the group multiset byte-identical — When verify runs, Then the affected obligations are `uncertain`, never `discharged`. This is the case that falsified DD-021's rationale." + - "Given a function whose identity was derived from `body_shape_hash` (no name-section name, no export name), When verify runs, Then no obligation in it is ever reported `discharged` — the fallback identity cannot corroborate a discharge." + - "Given an edit that INTRODUCES a new obligation at a site that had no prior advisory, When verify runs, Then a verdict is emitted for it. Pre-rework this produced ZERO verdicts, so an agent that fixed A while breaking B passed clean." + - "Given the harness of FEAT-073 over scry's own history, When the reworked adjudicator replaces the refuted one, Then the verdict distribution is re-measured and any newly-silent verdict class is explained rather than assumed to be an improvement." links: - type: traces-to - target: REQ-020 + target: REQ-021 - type: traces-to target: REQ-018 - type: traces-to @@ -1046,11 +1116,16 @@ artifacts: `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). + SCOPE SPLIT (2026-08-20): the v3.3.0 slice is `analyze` + `query` only. + The `verify` tool follows FEAT-065 into v3.4.0 with REQ-021 — exposing a + refuted adjudicator over MCP would put a wrong verdict directly into an + agent's tool loop, which is the single worst place for it to land. 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." + - "Given the v3.3.0 server, When a client enumerates its tools, Then `verify` is ABSENT rather than present-and-unreliable — the deferral is enforced by the tool list, not by documentation." links: - type: traces-to target: REQ-020 @@ -1182,3 +1257,106 @@ artifacts: target: REQ-017 - type: traces-to target: G-005 + + # ── DOGFOOD + VISUALIZATION: the two surfaces that make identity real ── + # Added 2026-08-20. Identity (FEAT-064) is landed and correct within its + # qualified scope, but it is INVISIBLE: nothing publishes it, nothing cites + # it, and nothing exercises it at scale. These two features fix that without + # depending on the refuted adjudicator. + + - id: FEAT-072 + type: feature + title: "v3.3 — Obligation anchors + the delta view (identity, made visible)" + status: proposed + release: v3.3.0 + description: > + The dashboard renders ONE snapshot. The entire value of a stable obligation + identity is across TIME, so today FEAT-064 ships a key that nothing + displays, nothing links to, and no consumer can cite. Two pieces: + + (a) ANCHORS. Every obligation in the rendered page carries + `id="ob-"` plus a copyable deep link, so a verdict, a + GitHub issue, a commit message, or an agent's citation resolves to a URL + that SURVIVES the next release. Today a consumer can only cite + `(func_index, pc)`, which is exactly the key that shifts on every edit — + the dashboard has been handing out references it knows will break. This + piece is independent of adjudication and ships in v3.3.0 unconditionally. + + (b) DELTA VIEW. `scry-viz diff ` + renders a page keyed on obligation ID rather than pc: what is new, what is + gone, what is unchanged, what cannot be matched. The 6,191-obligation dump + is untriageable; a delta is naturally small, which is the point. + + HONESTY CONSTRAINT (non-negotiable while scry#122 is open): the delta view + MUST NOT publish a `discharged` count. Its headline is the ADJUDICABLE + FRACTION — "of M obligations, K adjudicable, N uncertain" — because the + uncertain fraction is the number that states how far the matcher can be + trusted, and it is the one number the refutation did not undermine. The + dashboard is public and every public claim must survive Conrad Watt; a + discharge count from a matcher with six known wrong-verdict paths does not. + When REQ-021 lands, the discharge count is UNSUPPRESSED — it is not + re-implemented, only un-hidden, so the constraint costs nothing later. + tags: [ai-agent, visualization, identity, honesty, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given the published self-analysis page, When a consumer deep-links to one obligation, Then the URL fragment is that obligation's stable ID — not its pc — and the same fragment still resolves after an UNRELATED function is edited and the page re-rendered." + - "Given two guidance feeds from different commits, When `scry-viz diff` renders them, Then every row is keyed on obligation ID and the summary reports the adjudicable/uncertain split." + - "Given `scry-viz diff` while scry#122 is open, When it renders any pair, Then NO discharge count appears anywhere in the output — enforced by a test that greps the rendered page, not by reviewer discipline." + - "Given a feed compared with ITSELF, When `scry-viz diff` renders it, Then it reports zero changes and every obligation unchanged — the page's own vacuity check, so a plausible-looking delta cannot come from an empty comparison." + - "Given a pair known to differ, When `scry-viz diff` renders it, Then the change set is NON-EMPTY — the dual check, so 'no changes' can never be the silent result of a broken match." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-017 + - type: traces-to + target: FEAT-064 + - type: traces-to + target: FEAT-063 + + - id: FEAT-073 + type: feature + title: "v3.3 — Self-adjudication harness: scry adjudicates scry, in observation mode" + status: proposed + release: v3.3.0 + description: > + Roll the fix-verify loop out ON OURSELVES. FEAT-025 already dogfoods scry + on its own compiled module (`scry_mcdc.wasm`) at a single commit; this + extends the same instrument across TIME — run the adjudicator over N + consecutive commits of scry's own history and publish the verdict + distribution. + + PURPOSE IS EVIDENCE, NOT GATING. scry#122 lists nine work items and there + is no data on which of them fire on real code. scry's own history contains + real deletions, real same-kind insertions, and real function renames at + 6,191-obligation scale — a far stronger sample than a hand-built fixture, + and the four vacuous oracles written in this project during August 2026 + are the standing argument for preferring measured behaviour to designed + behaviour. The measurement ORDERS the rework instead of guessing at it. + + OBSERVATION MODE IS ENFORCED BY CONSTRUCTION (DD-022): the harness exits 0 + unconditionally, gates nothing, and every artifact it writes carries a + header naming scry#122 so that no reader — human or agent — mistakes a + `discharged` count for truth. It graduates to a gate only when REQ-021 has + closed and the distribution is understood. A gate on an unvalidated + adjudicator is precisely the failure mode the adjudicator exists to + prevent, one layer up. + tags: [ai-agent, dogfood, ci, evidence, honesty, v3.3] + fields: + phase: phase-3 + acceptance-criteria: + - "Given N consecutive commits of scry, When the harness runs, Then it emits a per-pair verdict distribution, and every artifact it writes names scry#122 as the reason no verdict in it is authoritative." + - "Given a pair of commits KNOWN to differ, When the harness runs, Then its verdict set is NON-EMPTY — the harness's own vacuity check, so a clean run can never be an empty run silently reported as agreement." + - "Given a commit compared with ITSELF, When the harness runs, Then it reports only `still-open` — the same self-comparison invariant REQ-021 is held to, measured on the real module rather than a fixture." + - "Given the harness in CI, When any pair yields `regressed` or `discharged`, Then the job still exits 0 — observation mode is a property of the code, not a convention a future edit can quietly drop." + - "Given the measured distribution, When scry#122 is prioritized, Then each of its nine work items is annotated with whether the path was OBSERVED on real history or remains theoretical — the ordering is evidence-led." + links: + - type: traces-to + target: REQ-020 + - type: traces-to + target: REQ-021 + - type: traces-to + target: FEAT-025 + - type: traces-to + target: FEAT-064 From 8e7a7afa60cb990594548c6edf4ef5d03d361183 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 20 Aug 2026 07:00:11 +0200 Subject: [PATCH 2/5] FEAT-068/072/073: make obligation identity visible, citable, and measured MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Three surfaces that make FEAT-064's identity real, none of which depends on the adjudicator refuted in scry#122. FEAT-068 — guidance.json v2. The feed shipped un-versioned and carried no identity at all, so an agent could not tell an OLD PRODUCER from a module with no such finding, and identity that existed only in Rust structs could not cross a process boundary. Adds `guidance_schema: 2` plus `obligation_id`, `site_key` and `group_key` on every advisory. `site_key` / `group_key` are lifted onto main from the withdrawn FEAT-065 branch. Their DERIVATION was never what the review refuted — the refuted part was the inference "group set unchanged, therefore safe to claim a discharge". The keys are shipped here as data, with the docs saying plainly that nothing in this release may conclude a discharge from them. FEAT-072 — anchors + the delta view. * Every advisory row is now `id="ob-"` with a permalink. Until now the only handle a consumer could quote was `fn{index}:{pc}` — precisely the key that shifts on the next edit. The dashboard was handing out references it knew would break. * `scry-viz delta ` compares two analyses BY IDENTITY. It takes modules rather than feeds so the comparison cannot drift from the producer's key derivation. The delta view makes exactly one soundness claim, and it is a new one: ALIAS-FREE. `ObligationId.v` proves aliasing needs a deleted same-kind sibling to inherit an ordinal from (survivor_inherits_deleted_identity), so an ordinal domain holding one member in BOTH runs has nothing to inherit from. That is checkable, and it is the honest headline — not "K adjudicable" but "K provably alias-free, the rest not excluded". Note this is strictly stronger than DD-021's refuted rule: a singleton domain rules aliasing out; an unchanged domain does not. No discharge count is published, enforced by a test that greps the rendered page rather than by reviewer discipline (DD-022). FEAT-073 — scripts/self-history.sh, the self-adjudication harness. Builds scry_mcdc.wasm at the last N commits and compares consecutive pairs. Exits 0 unconditionally; every artifact names scry#122. Observation mode is a property of the code, not a convention a later edit can drop. Carries a self-comparison control so a clean run can never silently be an empty one. Test discipline: the four new oracles were mutation-checked, not just run. Forcing `alias` to AliasFree kills only the alias test; deleting the anchor kills only the two anchor tests. Both vacuity directions are covered — a self-comparison must show no change AND a known-different pair must show one, so "no changes" can never be the silent result of a broken match. 134 tests pass; clippy -D warnings clean across the CI package set. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --- crates/scry-analyze-core/src/lib.rs | 76 ++++ crates/scry-mcdc/Cargo.lock | 42 +- crates/scry-viz/src/lib.rs | 669 +++++++++++++++++++++++++++- crates/scry-viz/src/main.rs | 99 ++++ scripts/self-history.sh | 153 +++++++ 5 files changed, 1026 insertions(+), 13 deletions(-) create mode 100755 scripts/self-history.sh diff --git a/crates/scry-analyze-core/src/lib.rs b/crates/scry-analyze-core/src/lib.rs index 177d0cb..c35a0ba 100644 --- a/crates/scry-analyze-core/src/lib.rs +++ b/crates/scry-analyze-core/src/lib.rs @@ -675,6 +675,29 @@ pub struct Advisory { /// 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-072 (DD-021): identity of the SITE, excluding the advisory code — + /// so it is STABLE when an obligation changes state. A `div-by-zero` + /// becoming `proven-safe` changes `obligation_id` but NOT this, which is + /// what lets a delta view report "this site changed state" instead of + /// "one identity vanished and an unrelated one appeared". + /// + /// Derived here as DATA. It is deliberately NOT paired with an adjudicator + /// in this release: matching on this key alone was refuted in review + /// (scry#122), because a positional ordinal can be inherited by a + /// surviving sibling. Consumers may group and diff by it; nothing in this + /// release may conclude "discharged" from it. + pub site_key: String, + /// FEAT-072 (DD-021): the ORDINAL DOMAIN this site's ordinal is counted + /// within (function + region path + operator kind), WITHOUT the ordinal. + /// + /// This is the aliasing signal made observable: `ObligationId.v` proves a + /// surviving site can inherit a deleted sibling's ordinal + /// (survivor_inherits_deleted_identity), and that can only happen inside + /// one group. Comparing a group's membership across two runs therefore + /// bounds where identity may have shifted. Necessary but NOT sufficient to + /// rule aliasing out — the pairing of a deletion with a same-kind insertion + /// leaves the group unchanged, which is precisely what falsified DD-021. + pub group_key: String, } /// FEAT-055 (REQ-018): a candidate counterexample for an `UnprovenObligation` @@ -3107,6 +3130,45 @@ fn obligation_id_of(func_ident: &str, path: &str, kind: &str, ordinal: u32, code out } +/// FEAT-072 (DD-021): the SITE key — everything the obligation id has EXCEPT +/// the advisory code, so it survives an obligation changing state. +fn site_key_of(func_ident: &str, path: &str, kind: &str, ordinal: u32) -> String { + let mut h = Sha256::new(); + h.update(b"site|"); + 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()); + 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-072 (DD-021): the ORDINAL DOMAIN key — function + region path + kind, +/// WITHOUT the ordinal. Aliasing can only occur WITHIN one such domain, so a +/// change in a group's membership bounds where identity may have shifted. +fn group_key_of(func_ident: &str, path: &str, kind: &str) -> String { + let mut h = Sha256::new(); + h.update(b"group|"); + h.update(func_ident.as_bytes()); + h.update(b"|"); + h.update(path.as_bytes()); + h.update(b"|"); + h.update(kind.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 @@ -3126,6 +3188,8 @@ fn stamp_obligation_ids( ) { for a in advisories.iter_mut().filter(|a| is_module_scoped(&a.code)) { a.obligation_id = obligation_id_of("", "", "", 0, &a.code); + a.site_key = site_key_of("", "", "", 0); + a.group_key = group_key_of("", "", ""); } for f in defined_funcs { let ident = function_meta @@ -3145,6 +3209,8 @@ fn stamp_obligation_ids( .map(op_report_name) .unwrap_or_else(|| a.code.clone()); a.obligation_id = obligation_id_of(&ident, path, &kind, *ordinal, &a.code); + a.site_key = site_key_of(&ident, path, &kind, *ordinal); + a.group_key = group_key_of(&ident, path, &kind); } } } @@ -3188,6 +3254,8 @@ fn compute_advisories( verification: "re-run scry: this handle_findings entry disappears".into(), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } @@ -3228,6 +3296,8 @@ fn compute_advisories( ), counterexample: Some(trap_counterexample(t.kind, &t.op, memory_size_bytes)), obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } TrapVerdict::ProvenSafe => { @@ -3255,6 +3325,8 @@ fn compute_advisories( ), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } } @@ -3296,6 +3368,8 @@ fn compute_advisories( ), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } @@ -3315,6 +3389,8 @@ fn compute_advisories( verification: "re-run scry: stack_usage.max_stack_bytes becomes Bytes(n)".into(), counterexample: None, obligation_id: String::new(), + site_key: String::new(), + group_key: String::new(), }); } diff --git a/crates/scry-mcdc/Cargo.lock b/crates/scry-mcdc/Cargo.lock index cb83757..f1df585 100644 --- a/crates/scry-mcdc/Cargo.lock +++ b/crates/scry-mcdc/Cargo.lock @@ -75,33 +75,61 @@ dependencies = [ "scry-sai-core", ] +[[package]] +name = "scry-sai-bits" +version = "3.2.4" + [[package]] name = "scry-sai-core" -version = "1.13.0" +version = "3.2.4" dependencies = [ + "scry-sai-bits", + "scry-sai-float", + "scry-sai-handle", "scry-sai-interval", "scry-sai-octagon", + "scry-sai-pentagon", "scry-sai-provenance", + "scry-sai-segment", "scry-sai-taint", "sha2", "wasmparser", ] +[[package]] +name = "scry-sai-float" +version = "3.2.4" + +[[package]] +name = "scry-sai-handle" +version = "3.2.4" + [[package]] name = "scry-sai-interval" -version = "1.13.0" +version = "3.2.4" [[package]] name = "scry-sai-octagon" -version = "1.13.0" +version = "3.2.4" + +[[package]] +name = "scry-sai-pentagon" +version = "3.2.4" [[package]] name = "scry-sai-provenance" -version = "1.13.0" +version = "3.2.4" + +[[package]] +name = "scry-sai-segment" +version = "3.2.4" +dependencies = [ + "scry-sai-interval", +] [[package]] name = "scry-sai-taint" -version = "1.13.0" +version = "3.2.4" [[package]] name = "sha2" @@ -128,9 +156,9 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "wasmparser" -version = "0.247.0" +version = "0.252.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e6fb4c2bee46c5ea4d40f8cdb5c131725cd976718ec56f1c8e82fbde5fa2a80" +checksum = "d3eb099dcadcde5be9eef55e3a337128efd4e44b4c93122487e4d2e4e1c6627c" dependencies = [ "bitflags", ] diff --git a/crates/scry-viz/src/lib.rs b/crates/scry-viz/src/lib.rs index 142f2a3..a79152d 100644 --- a/crates/scry-viz/src/lib.rs +++ b/crates/scry-viz/src/lib.rs @@ -877,6 +877,12 @@ fn advisory_class_name(c: AdvisoryClass) -> &'static str { /// Render one advisory as a `
  • ` — the shared body of the (capped) HTML /// Guidance list. +/// +/// FEAT-072: the row carries `id="ob-"` and a `¶` permalink, so +/// an obligation is CITABLE by URL. Until now the only handle a consumer could +/// quote was `fn{index}:{pc}` — which is precisely the key that shifts on the +/// next edit, so the dashboard was handing out references it knew would break. +/// The `(func_index, pc)` pair stays visible as a positional convenience. fn render_advisory_row(s: &mut String, a: &scry_analyze_core::Advisory) { let (cls, label) = match a.class { AdvisoryClass::DefiniteFault => ("err", "FIX"), @@ -884,9 +890,21 @@ fn render_advisory_row(s: &mut String, a: &scry_analyze_core::Advisory) { AdvisoryClass::PrecisionGap => ("info", "PRECISION"), AdvisoryClass::LeverageableFact => ("info", "LEVERAGE"), }; + // An empty id means no identity could be derived (FEAT-064). Emit no anchor + // rather than a dead `#ob-` fragment that would resolve to the wrong row. + if a.obligation_id.is_empty() { + let _ = write!(s, "
  • "); + } else { + let _ = write!( + s, + "
  • ", + esc(&a.obligation_id), + ); + } let _ = write!( s, - "
  • {label} \ + "{label} \ fn{}:{} {} — {}
    Action: {}
    Verify: {}", a.func_index, a.pc, @@ -1413,14 +1431,32 @@ fn esc(raw: &str) -> String { // ── structured guidance feed ──────────────────────────────────────────────── +/// FEAT-068: the guidance-feed schema version. Bumped when a field is added or +/// its meaning changes, so a consumer can tell "this producer is old" from +/// "this module has no such finding" — the distinction the un-versioned v1 feed +/// could not express. +/// +/// v2 (this release) adds `guidance_schema` itself plus `obligation_id`, +/// `site_key` and `group_key` on every advisory. +pub const GUIDANCE_SCHEMA_VERSION: u32 = 2; + /// Serialize the actionable findings as a machine-consumable JSON document — the /// feed an AI-agent consumer reads instead of scraping the (now capped) HTML. /// -/// Shape (stable): a top-level object -/// `{ "module_sha256": "…", "schema": "…", "advisories": [ … ], "trap_checks": [ … ] }`. +/// Shape: a top-level object +/// `{ "guidance_schema": 2, "module_sha256": "…", "schema": "…", +/// "advisories": [ … ], "trap_checks": [ … ] }`. +/// +/// FEAT-068: `guidance_schema` is an explicit integer version. v1 (the v3.2.2 +/// feed) had none, so a consumer could not tell a field's ABSENCE from an old +/// producer. v2 adds the version and the three FEAT-064/DD-021 identity keys. +/// Absence of `guidance_schema` means v1; a consumer requiring identity must +/// check for it rather than assume. +/// /// Each advisory is /// `{ "func_index", "pc", "class", "code", "detail", "suggested_action", -/// "verification", "counterexample"? }`, mirroring the [`Advisory`] fields +/// "verification", "obligation_id", "site_key", "group_key", +/// "counterexample"? }`, mirroring the [`Advisory`] fields /// (`class` uses the machine-stable name, e.g. `"unproven-obligation"`). Each /// trap check is `{ "func_index", "pc", "op", "kind", "verdict" }`. /// @@ -1432,7 +1468,8 @@ pub fn render_guidance_json(result: &AnalysisResult) -> String { s.push('{'); let _ = write!( s, - "\"module_sha256\":\"{}\",\"schema\":\"{}\",", + "\"guidance_schema\":{},\"module_sha256\":\"{}\",\"schema\":\"{}\",", + GUIDANCE_SCHEMA_VERSION, json_esc(&result.invariants.module_sha256), json_esc(&result.invariants.schema), ); @@ -1445,7 +1482,8 @@ pub fn render_guidance_json(result: &AnalysisResult) -> String { let _ = write!( s, "{{\"func_index\":{},\"pc\":{},\"class\":\"{}\",\"code\":\"{}\",\ - \"detail\":\"{}\",\"suggested_action\":\"{}\",\"verification\":\"{}\"", + \"detail\":\"{}\",\"suggested_action\":\"{}\",\"verification\":\"{}\",\ + \"obligation_id\":\"{}\",\"site_key\":\"{}\",\"group_key\":\"{}\"", a.func_index, a.pc, advisory_class_name(a.class), @@ -1453,6 +1491,9 @@ pub fn render_guidance_json(result: &AnalysisResult) -> String { json_esc(&a.detail), json_esc(&a.suggested_action), json_esc(&a.verification), + json_esc(&a.obligation_id), + json_esc(&a.site_key), + json_esc(&a.group_key), ); if let Some(cx) = &a.counterexample { let _ = write!( @@ -1548,6 +1589,12 @@ const STYLE: &str = "