FEAT-071 (REQ-021): scry's scope as DATA, from one source - #171
Closed
avrabe wants to merge 1 commit into
Closed
Conversation
The dashboard stated scope in hand-written prose, and `render_scope` ignored its AnalysisResult entirely (the parameter was `_r`), so it said the same thing about every module. An agent deciding whether to trust a verdict got paragraphs. THE DRIFT THIS REPLACES IS MEASURED, not hypothetical. The old not-proven list named only PROVENANCE limits -- WasmCert not imported, the memory-content model, not a qualified tool -- and NONE of the dominant practical ones. Measured on a real module: unmodeled-control-flow 15.6% of advisories and unsupported-op 5.9%, against a proven-safe rate of 0.6%. A reader would have formed a materially more optimistic picture than the numbers support. The enumerated list now names the if/else region havoc, the unsupported-op function scrub, and the disequality limit that makes a correct div-by-zero fix invisible (#165). SINGLE SOURCE: the page and the feed are both rendered from SCOPE_EVIDENCE and SCOPE_NOT_PROVEN, so a limitation cannot be stated on one and omitted from the other. The oracle requires every not-proven item in BOTH surfaces, and is mutation-checked: emitting empty strings in the FEED while the page still lists them (asserted a single matching line before applying) kills it with "not-proven item missing from the FEED". Red-first: "the feed must carry a scope manifest, not leave scope to the page", after the non-vacuity assertion on the constants had passed. Human legibility is NOT traded away: `hero_and_scope_copy_finalized` still passes unchanged, because each kind renders its human phrasing AND its machine tag. A manifest a human cannot read is a different failure from prose a machine cannot read, not a fix for it. Schema 5 -> 6. Three sibling tests pinned the version by EQUALITY and broke at once on a bump unrelated to the field each guarded; they now assert a LOWER BOUND parsed from the document, which still fails if a field ships without a bump. Mutation-checked: regressing the constant to 4 kills exactly those three. tests=0 clippy=0 fmt=0 rivet=0 claim-check=0 gate-coverage=0. Refs: FEAT-071 Claude-Session: https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
📐 rivet artifact deltaPR: #171 Base SHA: Validationhead — `rivet validate` resultbase — `rivet validate` result (for comparison)Artifact stats
full stats — headDiff (base → head)AADL model — headPosted by the |
Contributor
Author
|
Superseded by #174 — same branch, rebased onto main. Auto-closed by GitHub when I deleted |
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.
Stacked on #170 — it carries the 12-entry
required-checks.txt, without which thedrift gate correctly fails here. GitHub will retarget this to
mainwhen #170 merges.The drift this replaces is measured
The dashboard stated scope in hand-written prose, and
render_scopeignored itsAnalysisResultentirely (the parameter was_r) — it said the same thing aboutevery module.
Worse, its "what scry does NOT prove" list named only provenance limits (WasmCert
not imported, memory-content model, not a qualified tool) and none of the dominant
practical ones:
unmodeled-control-flow— anif/elsehavocs its regionunsupported-op— scrubs the whole functionAn agent reading that would form a materially more optimistic picture than the numbers
support. The enumerated list now names the region havoc, the function scrub, and the
disequality limit that makes a correct div-by-zero fix invisible (#165).
Single source, so page and feed can't drift
Both are rendered from
SCOPE_EVIDENCE/SCOPE_NOT_PROVEN. The oracle requires everynot-proven item to appear in both surfaces.
Mutation-checked on exactly that property: emitting empty strings in the feed
while the page still lists them — asserted a single matching line before applying —
kills the test with
not-proven item missing from the FEED.Red first:
the feed must carry a scope manifest, not leave scope to the page, afterthe non-vacuity assertion on the constants had already passed.
Human legibility is not traded away
hero_and_scope_copy_finalized— a pre-existing gate on the prose — still passesunchanged, because each evidence kind renders its human phrasing and its machine
tag. A manifest a human can't read is a different failure from prose a machine can't
read, not a fix for it.
Schema 5 → 6, and a pin that kept rotting
Three sibling tests pinned the version by equality and broke at once on a bump
unrelated to the field each guarded. They now assert a lower bound parsed from the
document — still fails if a field ships without a bump, but doesn't rot on unrelated
ones. Mutation-checked: regressing the constant to 4 kills exactly those three.
tests=0 clippy=0 fmt=0 rivet=0 claim-check=0 gate-coverage=0🤖 Generated with Claude Code
https://claude.ai/code/session_01KkNzkNYzPh7366DkNijeNc