FEAT-065: scry adjudicates its own oracle (verify_against), conservative by construction - #120
Draft
avrabe wants to merge 2 commits into
Draft
FEAT-065: scry adjudicates its own oracle (verify_against), conservative by construction#120avrabe wants to merge 2 commits into
avrabe wants to merge 2 commits into
Conversation
…tive by construction
Closes the fix-verify loop REQ-018 promised: the v3.1 verification oracle was
PROSE; this makes it a machine verdict, so an agent's edit is gated by a sound
checker rather than by tests.
`verify_against(before, after) -> Vec<VerifyVerdict>` with outcomes
discharged / still-open / regressed / moved / removed-with-code / uncertain.
DD-021 (new) records two findings that forced the design:
1. `obligation_id` includes the advisory CODE (clean-room: one i32.div_s raises
two obligations at one pc, so the site alone does not discriminate) — but
FIXING an obligation changes its code (div-by-zero → proven-safe) and hence
its id, which is exactly the transition to detect. Matching on the id would
render every genuine discharge as two unrelated events. So THREE keys, each
with one job: obligation_id (cite), site_key (match — excludes code),
group_key (the ordinal domain — the conservatism signal).
2. `ObligationId.v` PROVES identity can alias (survivor_inherits_deleted_identity),
which admits a FALSE discharge: an open site is deleted, a proven-safe
same-kind sibling inherits its identity, and the deleted obligation looks
fixed. So `discharged` is a CERTAINTY claim — withheld unless the ordinal
domain's site set is unchanged; otherwise `uncertain`.
Verified the conservatism actually FIRES on that scenario rather than passing by
another route (a probe printed the real verdict before it was removed):
Uncertain before=div-by-zero after=Some("proven-safe")
"looks proven safe, but this site's ordinal domain changed membership so
identity may have aliased — discharge withheld"
Without the rule this case reports `discharged` for an obligation never fixed.
`removed-with-code` is kept strictly distinct from `discharged` — deleting the
code that carried an obligation proves nothing, and an agent rewarded for
conflating them learns to delete rather than fix.
HONEST RESIDUAL (DD-021 limitations): a pure REORDERING of two same-kind
operators in one region preserves the group's site set while swapping which site
each key denotes, so that edit shape can still mis-attribute a verdict. Disclosed;
closing it needs content corroboration beyond the key.
Tests: 4 FEAT-065 oracles (real fix → Discharged; deletion → RemovedWithCode and
never Discharged; aliasing → Uncertain; lost fact → Regressed). core 106, viz 25,
segment 10, poly 9, interval 8, octagon 26. clippy -D warnings clean across CI's
package set, fmt clean, rivet validate PASS.
Scope: the PURE adjudicator. CLI/MCP surfacing is FEAT-066/067. FEAT-065 stays
`proposed` pending clean-room + CI.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
marked this pull request as draft
August 11, 2026 19:59
Contributor
Author
Converting to draft — clean-room found 6 criticals, and one of them falsifies DD-021's core rationaleAdversarial review of this adjudicator found six wrong-verdict paths, four of which the design did not anticipate. Not mergeable. Recording them here; the rework is tracked separately. The rationale sentence is falseDD-021 asserts: "aliasing by deletion or insertion NECESSARILY changes the ordinal domain's membership." That is the sentence the entire conservatism rule rests on, and it is wrong. Pair a deletion with a same-kind insertion in the same region and the group's ;; before — div#0 OPEN (param divisor), div#1 proven safe
i32.const 10 local.get 0 i32.div_s i32.const 20 i32.const 5 i32.div_s i32.add
;; after — the OPEN one deleted, a new SAFE one appended
i32.const 20 i32.const 5 i32.div_s i32.const 30 i32.const 6 i32.div_s i32.addGroup set identical ⇒ The other criticals
Confirmed closedThe advisory-less-operator vector I suspected is not a hole (ordinals are per-kind and per-region, and nested regions get their own counters), and ⊤-degradation does not suppress trap checks. The module sentinel cannot collide with a real site ( AssessmentAn adjudicator that can wrongly say "fixed" is worse than none, because an agent optimises straight into it. Findings 1–3 are that failure; finding 5 means it cannot see new faults; finding 4 makes the |
Adversarial review of the FEAT-065 adjudicator (PR #120, now draft) falsified this decision's central justification. DD-021 asserted that "aliasing by deletion or insertion NECESSARILY changes the ordinal domain's membership" — the sentence the whole conservatism rule rested on. It is FALSE: a deletion paired with a same-kind insertion 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 the rule exists to prevent. Retracted in place (not quietly reworded) and the six reproduced findings recorded in `limitations`, including two the design did not anticipate at all: new obligations produce no verdict whatsoever, and `regressed` is fabricated on a byte-identical module (contradictory verdicts under one id). Correcting the claim, not the ledger. The implementation stays in draft until matching uses CONTENT corroboration rather than a positional ordinal plus a population check. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #120 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
avrabe
added a commit
that referenced
this pull request
Aug 20, 2026
…and disclose Caught in review before publication. The claim shipped in the previous commit — "a singleton ordinal domain provably cannot alias" — is wrong, and it is wrong in exactly the way DD-021 was wrong. It reasons from the one theorem that happens to be proven rather than from what aliasing is, and a proof of ONE sufficient condition does not enumerate them. The counterexample, 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. 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. Measured on the fixture: an unproven `div_s` deleted with its block, the proven-safe `div_s` from the next block inheriting its identity, reported ordinal_stable=1 and counted as an attributable change. From the keys alone, an obligation removed by deleting its region is indistinguishable from one that was fixed. That is survivor_inherits_deleted_identity one level up the key — the same failure class that got #120 withdrawn. Changes: * `AliasFree` → `OrdinalStable`, `alias_free()` → `ordinal_stable()`, `attributable_changes()` → `ordinal_stable_changes()`. The name now states the scope: sibling-ORDINAL donation is excluded, and nothing else is. * The page says plainly that this is NOT a certificate that identity held, and explains the region-path shift that defeats it. * The grep gate now asserts the DISCLOSURE is present, not only that the over-claim is absent. A number a reader cannot calibrate is worse than none. * The limitation is pinned by a characterization test rather than hidden: if a future change makes that count 0, the test fails so the page's disclosure is updated in the same commit instead of warning about a hazard that is gone. Also corrected a public claim I had just introduced. The obligation anchor's tooltip read "stable obligation id — survives edits elsewhere in the module" — precisely what scry#123 falsified for Rust-produced modules, rendered into the published dashboard. Now scoped, and it cites #123. Swept README, docs/ and render_scope for other identity-stability wording: none found (FEAT-064 has no public documentation yet). DD-022 records this as a PATTERN, which is the durable part: every attempt to certify identity from the KEYS ALONE has now 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. 136 tests pass; clippy -D warnings clean; rivet validate PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc
avrabe
added a commit
that referenced
this pull request
Aug 21, 2026
…easured (#124) * plan: split REQ-020, unblock v3.3.0, and add the dogfood + visualization features 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc * FEAT-068/072/073: make obligation identity visible, citable, and measured 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-<obligation_id>"` 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 <before.wasm> <after.wasm>` 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc * FEAT-072/073: publish the delta view, wire the harness into CI, record scry#123 CI (observation mode). The harness runs on every build over the last 3 commits and uploads its report. It never gates: the script exits 0 by construction and `continue-on-error` is belt to that braces. `if-no-files-found: warn`, not `error` — an observation that produced nothing is a fact to report, and `error` would turn a non-gating harness into a gate through the back door. Pages. The self-analysis page now carries obligation anchors automatically, and release.yml renders a release-over-release delta against the previous tag, linked from the landing page when present. `continue-on-error`: an unbuildable previous tag is a fact about the history, not a reason to block a release. Fixed a defect in my own page before it shipped. The moved-sites table filtered on `changed()` — true for gone and new rows too — while the summary counted in-place changes only, so the page could announce "7633 changed" directly above a summary saying "0 changed". Conflating vanished / new / changed-in-place is precisely how a delta misleads, so the table now carries an explicit `fate` column and a reconciliation test asserts moved == gone + new + changed with the three buckets disjoint. MEASURED — scry#123, and it reorders the rework. The harness's first run found a defect on NEITHER scry#122's nine items nor DD-020's limitations: 43-45% of function identities churn per build. Rust legacy mangling ends in `17h<16 hex>E`, a symbol disambiguator derived from crate metadata and instantiation rather than from the function body, and FEAT-064 prefers the name-section name. Across 582cfb0→524b3e0b, 334 of 744 functions carrying advisories lost EVERY obligation identity, 410 kept every one, and ZERO were partial. That is upstream of scry#122: content-corroborating `site_key` cannot help while `func_ident` — hashed in first — churns. Both repairs fail in opposite directions (raw: 1.2% collision / 43% churn; stripped: 0% churn / 36% collision, max 36 functions per name), so #123 states the measured trade and deliberately recommends nothing. FEAT-064's AC#1 — "an edit in an unrelated function leaves every obligation ID outside it unchanged" — is recorded as FALSIFIED IN PRACTICE on Rust-produced modules. It passes the hand-written WAT fixture and fails on real toolchain output. Third FEAT-064 claim refuted after being written, and the first the fixture suite structurally could not have caught, because the defect is in the producer's output rather than in scry's logic. This blocks calling REQ-020 verified; it does not affect what has landed. The harness also KILLED one of my own explanations before it was published: I expected ordinal shifts inside surviving functions to masquerade as gone+new. The discriminating probe found zero partial-overlap functions, so ordinal shift contributed nothing. "A fix cannot present as `changed`" is therefore recorded as an OPEN HYPOTHESIS with a named probe, not as a finding — across 7 pairs zero shared sites changed, but that may be a fact about the sample rather than a structural one. DD-022 and FEAT-072 corrected from "adjudicable fraction" to "alias-free fraction": nothing here certifies adjudicability, but a singleton ordinal domain provably cannot alias. Strictly stronger than DD-021's refuted rule. 135 tests pass; clippy -D warnings clean; rivet validate PASS; both workflows parse. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc * FEAT-072: the alias-free claim was unsound — rename to OrdinalStable and disclose Caught in review before publication. The claim shipped in the previous commit — "a singleton ordinal domain provably cannot alias" — is wrong, and it is wrong in exactly the way DD-021 was wrong. It reasons from the one theorem that happens to be proven rather than from what aliasing is, and a proof of ONE sufficient condition does not enumerate them. The counterexample, 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. 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. Measured on the fixture: an unproven `div_s` deleted with its block, the proven-safe `div_s` from the next block inheriting its identity, reported ordinal_stable=1 and counted as an attributable change. From the keys alone, an obligation removed by deleting its region is indistinguishable from one that was fixed. That is survivor_inherits_deleted_identity one level up the key — the same failure class that got #120 withdrawn. Changes: * `AliasFree` → `OrdinalStable`, `alias_free()` → `ordinal_stable()`, `attributable_changes()` → `ordinal_stable_changes()`. The name now states the scope: sibling-ORDINAL donation is excluded, and nothing else is. * The page says plainly that this is NOT a certificate that identity held, and explains the region-path shift that defeats it. * The grep gate now asserts the DISCLOSURE is present, not only that the over-claim is absent. A number a reader cannot calibrate is worse than none. * The limitation is pinned by a characterization test rather than hidden: if a future change makes that count 0, the test fails so the page's disclosure is updated in the same commit instead of warning about a hazard that is gone. Also corrected a public claim I had just introduced. The obligation anchor's tooltip read "stable obligation id — survives edits elsewhere in the module" — precisely what scry#123 falsified for Rust-produced modules, rendered into the published dashboard. Now scoped, and it cites #123. Swept README, docs/ and render_scope for other identity-stability wording: none found (FEAT-064 has no public documentation yet). DD-022 records this as a PATTERN, which is the durable part: every attempt to certify identity from the KEYS ALONE has now 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. 136 tests pass; clippy -D warnings clean; rivet validate PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc * rivet: give FEAT-073 a typed link to DD-022 CI's artifact validation flagged a trace gap this branch introduced: FEAT-073's prose names DD-022 as the decision that makes it observation-only, but nothing in `links:` said so. Prose is not traceability — a mention the graph cannot see does not re-open the right decision when the feature regresses. Also tried a reverse `verified-by` edge from REQ-021 and reverted it: the type is not in the schema, and FEAT-073 already declares `traces-to: REQ-021`, which is the direction the schema models. Inventing vocabulary to silence a nag would have recorded a relation the tooling cannot check. rivet validate: PASS, 130 warnings (was 131). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes the loop REQ-018 promised. v3.1 shipped a verification oracle as prose; this makes it a machine verdict, so an agent's edit is gated by a sound checker rather than by tests.
verify_against(before, after)→discharged | still-open | regressed | moved | removed-with-code | uncertain.Two findings forced the design (DD-021, new)
1. The id can't be the matching key.
obligation_idincludes the advisory code — the clean-room required it, since onei32.div_sraises two obligations at one pc. But fixing an obligation changes its code (div-by-zero→proven-safe) and therefore its id — exactly the transition we must detect. Matching on it would render every genuine discharge as "one id vanished, an unrelated one appeared."So three keys, each with one job:
obligation_id(cite),site_key(match — excludes code),group_key(the ordinal domain — the conservatism signal).2.
dischargedhas to be a certainty claim.ObligationId.vproves identity can alias (survivor_inherits_deleted_identity), which admits a false discharge: delete an open site, and a proven-safe same-kind sibling inherits its identity — the deleted obligation looks fixed. Sodischargedis withheld unless the ordinal domain's site set is unchanged; otherwiseuncertain.I verified the rule actually fires
Rather than trust a green test (the aliasing oracle accepts two outcomes), I probed the real verdict:
Without the conservatism rule this case reports
dischargedfor an obligation that was never fixed.removed-with-codestays strictly distinct fromdischarged: deleting the code that carried an obligation proves nothing, and an agent rewarded for conflating them learns to delete rather than fix.Honest residual (in DD-021)
A pure reordering of two same-kind operators in one region preserves the group's site set while swapping which site each key denotes — that shape can still mis-attribute a verdict. Disclosed; closing it needs content corroboration beyond the key.
Verification
4 FEAT-065 oracles (real fix →
Discharged; deletion →RemovedWithCode, neverDischarged; aliasing →Uncertain; lost fact →Regressed). core 106, viz 25, segment 10, poly 9, interval 8, octagon 26. clippy-D warningsclean across CI's package set; fmt clean;rivet validatePASS.Scope: the pure adjudicator. CLI/MCP surfacing is FEAT-066/067. FEAT-065 stays
proposedpending clean-room + CI.🤖 Generated with Claude Code