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 |
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