Skip to content

Discriminate LocalRead from Refused in the G2 under-selection control - #8148

Merged
briansrls merged 1 commit into
mainfrom
session/gentle-dove-143-g2-discriminator
Aug 11, 2026
Merged

briansrls merged 1 commit into
mainfrom
session/gentle-dove-143-g2-discriminator

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

Follow-up to #8142 (merged): makes that control's red discriminating.

The gap

specimen_classifies_as_runtime_read returns false in two states that are opposites on the safety axis:

  • Classified{LocalRead} — the strongest safe-to-skip verdict the selection seam has, so it licenses a skip. This is the harm: a skipped witness presents as a faster green floor rather than a failure (under-selection).
  • Refused{cause} — fail-closed, licenses nothing.

One Bool cannot separate them, so on its own the under-selection claim rested on the note beside it. DESIGN §4c: an annotation is never evidence that a machine claim holds, because no Accepted program can read one. #8142's note says outright that the discriminating LocalRead-vs-Refused receipt "is NOT enrolled here."

The repair

specimen_does_not_classify_as_local_read carries the other bit. The pair has a unique signature per reachable state:

state pair reads
Classified{LocalRead} (today) (false, false) — both red, so the red is agreement
Classified{RuntimeRead} (after the traversal repair) (true, true) — both rows delete together
Refused{cause} (false, **true**) — this claim greens alone

That third row is what earns the second evaluation. A drift from LocalRead to Refused is a real change of state with a different remedy, and today it is invisible because the first claim stays red either way. Greening alone makes it a StaleKnownRed refusal against its own admission row — the loud, typed, located signal the floor already routes.

Why expected-red rather than an ordinary green witness

It shares its sibling's evaluation cost, and the long-eval budget is coupled to expected-red across today's population (exact_witness_admission_witness_test every_declared_long_budget_row_is_also_expected_red_today). Asserting the desired state keeps this inside that population instead of retiring that claim, which would have widened scope. Both rows carry one dissolution obligation deliberately: same terminal construction, same trigger, neither survives the other.

Evidence

Release claim_batch, source roots dag + src/v2:

FAIL specimen_classifies_as_runtime_read        cpu=14182ms
FAIL specimen_does_not_classify_as_local_read   cpu=5689ms

(false, false) is the LocalRead signature. Refused would have made the second claim PASS, so the pair establishes by execution what the note previously only asserted.

Admission walls: 18/18 PASS on this change, including the four that could have rejected the new row — every_declared_long_budget_row_is_also_expected_red_today, each_budget_roster_is_homogeneous_in_declared_budget, no_batch_mixes_a_pre_verdict_row_with_an_assertion_false_row, and every_live_admission_is_reached_by_its_own_row (the last confirming the row reaches the new function rather than dangling).

Cost: the discriminator is 5.7s, not a second full 14s — the manifest memoizes across the two witnesses — leaving the pair near 20s against the 180000ms long-lane ceiling.

Scope

Two files, +46/-1. No production code, no traversal change. The G2 traversal repair itself (following data initializers as well as function bodies) is a separate lane and is not in this PR.

specimen_classifies_as_runtime_read is false in two states that are
opposites on the safety axis: Classified{LocalRead}, which is the
strongest safe-to-skip verdict the selection seam has and therefore the
harm, and Refused, which is fail-closed and licenses nothing. One Bool
cannot separate them, so on its own the UNDER-selection claim rested on
the note beside it -- and no Accepted program can read a note (DESIGN
4c). The measured LocalRead-vs-Refused receipt the note cites was
explicitly not enrolled.

specimen_does_not_classify_as_local_read carries the other bit. The pair
has a unique signature per reachable state:

  Classified{LocalRead}   (false, false)  today; both red, red is agreement
  Classified{RuntimeRead} (true,  true)   after the repair; both rows delete
  Refused{cause}          (false, TRUE)   this claim greens ALONE

The third row is what earns the second evaluation. A drift from LocalRead
to Refused is a real change of state with a different remedy, and today
it is invisible because the first claim stays red either way. Greening
alone makes it a StaleKnownRed refusal against its own admission row --
the loud, typed, located signal the floor already routes.

Admitted expected-red rather than landing as an ordinary green witness
because it shares its sibling's evaluation cost and the long-eval budget
is coupled to expected-red across today's population
(exact_witness_admission_witness_test
every_declared_long_budget_row_is_also_expected_red_today). Asserting the
desired state keeps this inside that population instead of retiring that
claim. Both rows carry one dissolution obligation deliberately: same
terminal construction, same trigger, neither survives the other.

Measured on this branch, release claim_batch, source roots dag + src/v2:

  FAIL specimen_classifies_as_runtime_read        cpu=14182ms
  FAIL specimen_does_not_classify_as_local_read   cpu=5689ms

(false, false) is the LocalRead signature; Refused would have made the
second claim PASS. So the pair establishes by execution what the note
previously only asserted. The discriminator costs 5.7s rather than a
second full 14s because the manifest memoizes across the two witnesses,
leaving the pair near 20s against the 180000ms long-lane ceiling.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01XxLzhuMisV3GAPpP2mBtSG
@briansrls
briansrls merged commit 2b5ed94 into main Aug 11, 2026
5 checks passed
@briansrls
briansrls deleted the session/gentle-dove-143-g2-discriminator branch August 11, 2026 21:05
briansrls pushed a commit that referenced this pull request Aug 12, 2026
…brace that broke every gate

DISCOVERY/ENROLLMENT REPAIR, and the roster is now one authority. The five
overlay-dependent claims were inline in the transport's call, so the function
names existed only inside an expression no coverage accounting can read. They are
now `module_binding_supply_claims`, one declared List<ClaimRun> the transport
consumes, so execution and any consumer census read the SAME rows rather than two
lists that can drift. The names are not duplicated anywhere.

Discovery no longer executes them. The corpus walk picks up any *_test.dag under
a source root -- not only the three scan dirs -- and outside the overlay
host_module_bindings is the committed Empty stub, so the vacuity guard refuses
and every row returns false. Selection is removed with a WitnessExclusionRow in
exactly the crate_layout posture (same manifest, same Empty read, same refusal);
scan dirs are NOT broadened and no vacuity guard is weakened.

TWO CONTROLS I DELETED, RESTORED. Rewriting the dag/-root comment in the previous
commit replaced a span that swallowed msrs_an_absent_module_is_not_projected and
msrs_a_real_module_is_not_bound_to_the_wrong_file. It surfaced as `no such
function` when the roster called them, which is the one way it could surface --
the file still parsed and the remaining three still passed, so nothing else would
have said so. Both are back with their arguments intact.

A BRACE THAT BROKE EVERY GATE. #8148 landed a reason string containing
`Classified{LocalRead}`, and `{` opens interpolation in .dag, so the module
raised `undefined variable 'LocalRead'` and nothing that resolves
explicit_witness_admission could run -- which is every gate I needed. Escaped to
`\{LocalRead\}`. One character, no semantic change, and it is a base-side defect
fixed here only because it blocks this branch entirely.

Executed: transport gate true (11 claims, mine among them); bridge witness 21/21;
main_wet to a no-op fixed point; regen_stage0 re-emitted and the seed rebuilt
clean; regen --verify divergence 0.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls pushed a commit that referenced this pull request Aug 12, 2026
…ason (#8170)

main has been red on the fleet job since #8148 landed. The refusal:

  dag/gunbc/explicit_witness_admission.dag:192:181:
    error: undefined variable 'LocalRead'

The row's reason prose contains Classified{LocalRead}. In .dag, `{ident`
opens a string interpolation, so the compiler read LocalRead as a variable
reference and correctly refused an undefined name. The brace is literal
here, and a literal brace is written `\{` -- the escape the language
already provides, rather than respelling the prose to dodge the parser.
This is the only such site in the file.

Discriminating control, run in both directions rather than green-only:

  brace unescaped -> exit 1, "undefined variable 'LocalRead'" x1
  brace escaped   -> exit 0 occurrences; compile.reconcile and
                     compile.analyses complete

(The fixed run still exits 1 on "scoped run function ... has no unique
runtime-selected declaration identity" -- an artifact of probing a
row-producer as a run entry, unrelated to resolution of this file.)

Not addressed here, and worth its own change: #8148's per-PR CI passed
with this defect present. The `ci` job is green on the same commit that
the `fleet` job refuses, so this parse-level class survives a full PR run
and only detonates post-merge on the deploy path.


Claude-Session: https://claude.ai/code/session_01XxLzhuMisV3GAPpP2mBtSG

Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant