Skip to content

Record the coverage join: detection power and cost refusal are orthogonal axes - #8441

Merged
briansrls merged 1 commit into
mainfrom
session/sharp-raven-273-coverage
Aug 18, 2026
Merged

briansrls merged 1 commit into
mainfrom
session/sharp-raven-273-coverage

Conversation

@gunbai-bot

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

Copy link
Copy Markdown
Contributor

One annotation on gunbc.witness_row_cost. No behaviour change.

What it records

Two instruments were run against the same corpus on the same day and disagreed completely about one cluster:

  • A mutation battery answers does this row red when its subject breaks — run in a session, where rows run to completion. Result: across four clusters, exactly one mutation reds nothing where its cluster should discriminate it (a dangling DeclarationRef bind).
  • A budget-refusal census answers which enrolled rows were killed on cost before they finished. Result on the same day's main run: 131 BUDGET-REFUSED identities — including all 28 rows of the decl_facts reflection cluster the battery had just measured.

A row that is sharp in a dispatch and killed on budget in CI is undiscriminating in CI, however good the row is. So a battery alone overstates coverage, and a budget census alone says nothing about whether the surviving rows discriminate anything. The coverage claim is the join: rows that both complete and red when their subject breaks.

Two disciplines the battery half needs

Both learned by getting them wrong first, and recorded so the next reader doesn't:

  • An empty run is not a green run. An entry passed with no function selector runs zero rows and reports zero failures, which is indistinguishable from a cluster that survived every mutation. It produced three false lines before being caught.
  • Reds-nothing is not fails-to-discriminate. A construction census that ignores a changed field value, or an edge claim that ignores a changed body, is answering the question it declared. Four of the seven measured zeros were scope, not gaps — counting them would have inflated a one-entry list into five, four of them inventions.

What it deliberately does not do

It does not restate the threshold number. witness_row_cost_migration_threshold_note already derives it from gunbc_ci_fast_lane_eval_budget_ms, and a second hand-maintained copy is the duplicate authority DESIGN §3 forbids. This row asserts only that cost refusal and detection power are orthogonal axes and a coverage claim needs both.

Note on CI: main's witnesses job is currently red for reasons that predate this branch (#8423 un-masked budget-refused rows), so this PR's checks will inherit that. This diff is a single data annotation and cannot reach any executing row.

… to try are different facts

Derived from two instruments run against the same corpus on the same day, which
disagreed completely about one cluster.

A MUTATION BATTERY answers "does this row red when its subject breaks" -- run in
a session, where rows run to completion. A BUDGET-REFUSAL CENSUS answers "which
enrolled rows were killed on cost before they finished". A row that is sharp in
a dispatch and killed on budget in CI is UNDISCRIMINATING IN CI however good it
is, so a battery alone overstates coverage and a budget census alone says
nothing about whether the surviving rows discriminate anything. The coverage
claim is the join: rows that both complete AND red when their subject breaks.

Measured, both halves: a four-cluster battery found exactly ONE mutation that
reds nothing where its cluster should discriminate it (a dangling
DeclarationRef bind), while the same day's main run reported 131 BUDGET-REFUSED
identities -- including all 28 rows of the decl_facts reflection cluster. That
cluster's battery result and its CI coverage disagree completely, which is why
the row exists.

Two disciplines the battery half needs, both learned by getting them wrong
first and recorded so the next reader does not:

  - an entry passed with no function selector runs ZERO rows and reports zero
    failures, which is indistinguishable from a cluster that survived every
    mutation. An empty run is not a green run; it produced three false lines
    here before it was caught.
  - reds-nothing is not fails-to-discriminate. A construction census ignoring a
    changed field value, or an edge claim ignoring a changed body, is answering
    the question it declared. Four of the seven zeros measured were scope, not
    gaps, and counting them would inflate the artifact with defects nobody
    claimed.

The threshold number is deliberately NOT restated here --
witness_row_cost_migration_threshold_note already derives it from
gunbc_ci_fast_lane_eval_budget_ms, and a second hand-maintained copy is what
DESIGN §3 forbids. This row asserts only that cost refusal and detection power
are orthogonal axes, and that a coverage claim needs both.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Aug 18, 2026

Copy link
Copy Markdown
Contributor Author

CI red at a92eb24 is not this PR's, and the one PR-only entry was budget noise, proven by re-execution rather than argued.

First run (32155779798): 137 failing identities -- 130 BUDGET-REFUSED, 6 STALE-QUARANTINE, and exactly 1 FAIL not present on main:
where_refinement_enforcement_witness.where_refinement_cast_literal_oci_other_digest_algorithm_accepts, "cost is exactly 1505ms against 1500ms" -- 0.3% over.

Same row, other observations of the same bytes: 1364ms on the #8440 run, and 1274ms on the rerun of this exact frozen merge ref. So it sits at ~85-100% of ceiling with ~15% run-to-run variance, and this PR adds one String annotation to a different module.

After the rerun: 136 failing identities, set difference PR-minus-main is EMPTY. Every remaining failure is the enrolled-row/budget-refusal join un-masked by #8423.

I did not tune anything toward 1500ms. The ceiling is a declared rung drop against the operator's 500ms hard / 100ms warn rule, not a target to fit under, and a row that flips on noise is a cost fact to report, not a diff to absorb.

— sent from sharp-raven-273

@briansrls
briansrls merged commit 38c4484 into main Aug 18, 2026
0 of 2 checks passed
@briansrls
briansrls deleted the session/sharp-raven-273-coverage branch August 18, 2026 22:43
briansrls pushed a commit that referenced this pull request Aug 18, 2026
#8472 made the rung drop's bounded population exact (358, 111, 429, 207) and #8470/#8441
moved floor preparation and coverage-join facts. The only conflict is the roster, and the
resolution is the same as the previous merge: take main's file, apply the 52
STALE-QUARANTINE removals on top. 358 -> 306.

Both edits are removals for different, non-overlapping reasons -- relocation of over-budget
rows on main, observed passes here -- so the merge is their union. The two later sentences
in main's header that assert the roster sits at 358 are corrected in place rather than left
to contradict the count above them.

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