diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index febc7c0..3310493 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -347,3 +347,38 @@ jobs: path: ${{ github.workspace }}/scry-self-analysis.html if-no-files-found: error retention-days: 14 + # FEAT-073 self-adjudication harness — OBSERVATION MODE. + # + # FEAT-025 (above) dogfoods scry on its own module at ONE commit. This + # extends the same instrument across TIME: build scry_mcdc.wasm at the + # last few commits and compare consecutive pairs BY STABLE OBLIGATION + # IDENTITY (FEAT-064/072). + # + # It DOES NOT GATE, and that is deliberate, not an oversight (DD-022). + # The adjudicator this would drive was refuted in review (scry#122): an + # adjudicator that can wrongly report a fix is worse than none, because + # the cheapest way for an agent to satisfy it is to delete the code. So + # the harness reports and never judges — `continue-on-error` is belt to + # the script's braces, which exits 0 unconditionally by construction. + # + # This already paid for itself: its first run surfaced scry#123 (43-45% + # of function identities churn per build via the Rust symbol + # disambiguator), a defect no fixture suite could have found because it + # lives in the toolchain's output rather than in scry's logic. + # + # It graduates to a gate only when REQ-021 closes. + - name: Self-adjudication harness (FEAT-073, observation only — never gates) + continue-on-error: true + run: | + git fetch --deepen=5 origin "$GITHUB_SHA" 2>/dev/null || true + bash scripts/self-history.sh 3 "${{ github.workspace }}/self-history" + - name: Upload self-history observation + uses: actions/upload-artifact@v4 + with: + name: scry-self-history + # if-no-files-found: warn — an observation that produced nothing is a + # fact to report, not a build failure. `error` here would turn the + # non-gating harness into a gate through the back door. + if-no-files-found: warn + path: ${{ github.workspace }}/self-history + retention-days: 14 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 09ff130..ed18deb 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -411,6 +411,35 @@ jobs: -o "$GITHUB_WORKSPACE/dist/self-analysis.html" \ --title "scry ${VERSION} — self-analysis (scry_mcdc.wasm)" + # FEAT-072: a release-over-release delta, keyed on stable obligation + # identity. Answers "what actually moved since the last release?" — the + # question the single-snapshot dashboard has never been able to answer, + # because (func_index, pc) shifts on every edit. + # + # It reports what CHANGED and asserts no verdict (scry#122 / DD-022); the + # page carries that constraint in its own copy and a unit test greps for + # it. `continue-on-error` because a missing or unbuildable previous tag + # is a fact about the history, not a reason to block a release — the + # landing page links this view only when it exists. + - name: Render release delta vs the previous tag (FEAT-072) + continue-on-error: true + run: | + set -uo pipefail + PREV="$(git tag --list 'v*' --sort=-v:refname | grep -v "^${VERSION}$" | head -1)" + if [[ -z "$PREV" ]]; then + echo "no previous tag — skipping the delta view (first release)"; exit 0 + fi + echo "delta: $PREV -> $VERSION" + WT="$(mktemp -d)/prev" + git worktree add --detach -q "$WT" "$PREV" || exit 0 + ( cd "$WT/crates/scry-mcdc" && cargo build --release --target wasm32-wasip1 -q ) || exit 0 + cargo run --release -p scry-sai-viz -- delta \ + "$WT/crates/scry-mcdc/target/wasm32-wasip1/release/scry_mcdc.wasm" \ + crates/scry-mcdc/target/wasm32-wasip1/release/scry_mcdc.wasm \ + -o "$GITHUB_WORKSPACE/dist/delta.html" \ + --title "${PREV} → ${VERSION} (by stable obligation identity)" + git worktree remove --force "$WT" 2>/dev/null || true + - name: Build landing page (scry-viz index) run: | set -euo pipefail diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 0e64ad6..bac29c5 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -664,3 +664,256 @@ 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 ORDINAL-STABLE FRACTION and suppress the discharge + count entirely while scry#122 is open, enforced by a test that greps the + rendered page — which must also assert the LIMITATION is disclosed, not + merely that the over-claim is absent. + CORRECTED TWICE IN DRAFTING, and the second correction matters more than + the first. + (a) It first said "K adjudicable", which over-claims: nothing here + certifies that a site can be adjudicated. + (b) It was then changed to "K provably ALIAS-FREE", justified by + `ObligationId.v: survivor_inherits_deleted_identity` needing a same-kind + sibling that a singleton ordinal domain does not have. THAT IS ALSO + WRONG, and it is wrong in the same way DD-021 was. It reasons from the + one theorem that happens to be proven rather than from what aliasing is; + a proof of ONE sufficient condition does not enumerate them. + The counterexample, found before publication and now pinned as + `feat072_region_shift_is_not_certified_as_identity_held`: `group_key` + hashes the region PATH, and a path is a sibling index at its depth. + Delete a whole region and its later siblings renumber, so a surviving + region moves into the deleted region's path and its sole operator + inherits the entire key — while BOTH domains remain singletons, so the + ordinal check sees nothing. An obligation removed by deleting its region + is then indistinguishable from one that changed state. + The claim is therefore named for its SCOPE: `OrdinalStable` excludes + sibling-ORDINAL donation and nothing else. It is a filter that says which + rows to look at first, never a warrant that a change belongs to a site. + RECORDED AS A PATTERN, because this is now the third instance: every + attempt to certify identity from the KEYS ALONE has failed, at three + different levels — the ordinal (DD-021), the region path (here), and the + function ident (scry#123). The keys are a good address and a bad proof. + Corroboration has to come from CONTENT. + 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..8dcfb08 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. @@ -972,7 +1037,9 @@ artifacts: 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 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. FALSIFIED IN PRACTICE on Rust-produced modules (measured 2026-08-20 by FEAT-073, scry#123) — holds only for functions whose name-section name is itself stable. It is met by the unit fixture and NOT met by real toolchain output; see the AC below, which states what was measured." + - "MEASURED, not assumed (FEAT-073 over scry's own history, commits 582cfb06→524b3e0b). Given two builds of the same Rust source differing by an unrelated edit, When identities are compared, Then 334 of 744 functions carrying advisories (45%) lose EVERY obligation identity and 410 keep every one — an all-or-nothing split with ZERO partial cases. Cause: Rust legacy mangling ends in `17h<16 hex>E`, a symbol disambiguator derived from crate metadata and instantiation rather than from the function body, so an unrelated edit renames the function. `func_ident` is the first component of every key, so the churn takes the whole function's obligations with it." + - "OPEN, deliberately not claimed: whether a genuine FIX presents as a changed obligation at a surviving site. Across 7 consecutive commit pairs of scry's own history, ZERO shared sites changed their obligation set. That is a fact about the SAMPLE — scry's commits alter analyzer logic, which recompiles into different monomorphizations — and must not be restated as a structural claim without a fixture that isolates it." - "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." @@ -986,9 +1053,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 +1091,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 +1118,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 +1259,117 @@ 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 + ORDINAL-STABLE fraction: sites whose ordinal domain is a singleton in both + runs, so no same-kind SIBLING could have donated an ordinal + (`survivor_inherits_deleted_identity` needs one). + NAMED FOR ITS SCOPE after a pre-publication counterexample: this excludes + sibling-ordinal donation and NOTHING ELSE. A whole-region deletion + renumbers later sibling regions, so a survivor can occupy the deleted + region's path and inherit its key with both domains still singletons. The + page must disclose that, and the grep test asserts the disclosure is + present as well as asserting the over-claim is absent. 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 modules from different commits, When `scry-viz delta` renders them, Then every row is keyed on stable identity (not pc) and the summary reports the ORDINAL-STABLE / NOT-EXCLUDED split. Renamed twice during implementation, and the history is the point: 'adjudicable' over-claimed, then 'alias-free' over-claimed in exactly DD-021's way — reasoning from the one proven theorem rather than from what aliasing is." + - "Given a module where a whole region carrying an unproven obligation is DELETED and a later sibling region moves into its path, When `scry-viz delta` renders it, Then the page DISCLOSES that ordinal-stability does not cover a region-path shift. The survivor is still counted ordinal-stable — the check cannot see it — so the acceptance is on the disclosure, and the limitation is pinned by feat072_region_shift_is_not_certified_as_identity_held so a later fix must update the disclosure in the same commit." + - "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." + - "FIRST RUN, 2026-08-20 (8 commits, 7 pairs). The harness paid for itself before scry#122 was touched: it surfaced a defect that is on NEITHER the issue's nine items nor DD-020's limitations — 43-45% of function identities churn per build via the Rust symbol disambiguator (scry#123). Recorded as the harness's own acceptance evidence: a fixture-only test suite could not have found this, because the defect lives in the toolchain's output rather than in scry's logic." + - "The same run REFUTED a hypothesis of the author's before it was published — that ordinal shifts inside surviving functions would masquerade as gone+new. The discriminating probe found ZERO partial-overlap functions, so ordinal shift contributed nothing to the observed churn. Recorded because the harness's value is symmetric: it must be able to kill our explanations, not only confirm them." + 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 + - type: traces-to + target: DD-022 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..d81a7ee 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,22 @@ 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 +1432,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 +1469,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 +1483,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 +1492,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 +1590,12 @@ const STYLE: &str = "