Skip to content

NO-FALLBACK-0 wall test: one fixture producer, exact counts, and a differential receipt - #9839

Merged
gunbai-bot[bot] merged 3 commits into
mainfrom
session/smart-owl-13
Aug 31, 2026
Merged

gunbai-bot[bot] merged 3 commits into
mainfrom
session/smart-owl-13

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 31, 2026 •

Copy link
Copy Markdown
Contributor

The wall's prose claimed a controlled comparison the fixtures did not make. The two sources differed on module name and import set as well as on the plan's ineligible-arm payload, and the RED asserted >= 1 blocking TypeMismatch — so a fixture that began refusing for a second, unintended reason would have kept the test green while it had stopped measuring what it names.

One fixture producer. Both fixtures come out of plan_ineligible_probe_source, parameterised only by the cause spelling: same module name, same imports (carrying BOTH candidate values so the import set is not a second variable), same function. The one-axis relation is a property of the construction, not an alignment two literals must be kept in.

Exact RED, pinned to its subject. Exactly one blocking TypeMismatch, and it is Coproduct(BootDeliveryCandidateStanding) rejecting the arm payload — not a mistyped import or a renamed field.

The differential is on the histogram key, not on a cardinality. delta(key) == 1 at the target key and 0 at every other, over (diagnostic_class, subject_name, blocking), ranging over BOTH row lists so a key present only in the GREEN is as visible as one present only in the RED. A net red.total == green.total + 1 would have proved only that the counts differ by one: an equal-cardinality identity swap satisfies it while two ambient identities change underneath. The key delta is what makes "the two censuses are the same population plus one row" a claim that executes. Its own discriminating RED is enrolled: fabricated rows with equal totals and severities and one blocking + one advisory identity swapped are refused by the comparator, while the paired lists differing only by the target row are admitted.

Why an absolute total is not asserted, measured rather than assumed. compile_dag_diagnostic_census reports the diagnostics of the whole nested compilation the fixture is handed to — fixture and imported closure together, with no projector separating them. Both arms carry ~130 rows including blocking UnresolvedType. So total == 0 on the GREEN (and total == 1 on the RED) would be permanently false: a check whose RED is unauthorable, which §4b names a decoration rather than a weak wall. The differential is grounded in the other arm rather than in a literal copied out of today's tree, which §5 rules out as an oracle. That coverage fact now also annotates CompileDiagnosticCensus itself, where the next author reads it.

Executed evidence (claim_batch, remote): all four witnesses PASS. Mutation controls: a wrong subject, an off-by-one differential, and the equal-cardinality swap each turn the affected witnesses FAIL.

🤖 Generated with Claude Code

https://claude.ai/code/session_012RhasgE5o1L1YibwKptZnK

gunbc-ci-auto-heal and others added 2 commits August 31, 2026 20:25
…fferential receipt

The wall's prose claimed a controlled comparison the fixtures did not make. The
two sources differed on module name and import set as well as on the plan's
ineligible-arm payload, and the RED asserted `>= 1` blocking TypeMismatch — so a
fixture that began refusing for a second, unintended reason would have kept the
test green while it had stopped measuring what it names.

Both fixtures now come out of one producer parameterised only by the cause
spelling: same module name, same imports (carrying BOTH candidate values so the
import set is not a second variable), same function. The one-axis relation is a
property of the construction, not an alignment two literals must be kept in.

The RED is exact and pinned to its subject: exactly one blocking TypeMismatch,
and it is the standing coproduct rejecting the arm payload. Both mutations were
executed as controls — a wrong subject and an off-by-one differential each turn
the affected witnesses red.

Measured rather than assumed, and it changes the assertable form:
compile_dag_diagnostic_census reports the whole compile's diagnostics, not the
fixture's own, so both arms carry ~130 ambient rows including blocking
UnresolvedType. `total == 0` on the GREEN is therefore not a claim this
instrument can make, and asserting it would be a permanently-red check dressed
as rigour. The exact form it does support is the differential — the two arms
differ by exactly one blocking diagnostic, ambient contribution cancelling — a
third witness which is the stronger claim and is grounded in the other arm
rather than in a literal copied out of today's tree (DESIGN §5).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012RhasgE5o1L1YibwKptZnK
… the test that hit it

The instrument reports the whole compile's diagnostics, imported closure
included, so a CensusObserved is not evidence the probed fixture compiled clean.
That fact belongs on CompileDiagnosticCensus, where the next author reads it,
rather than only in the one witness that discovered it by reading rows.

The annotation states what the declaration owns — what its row set covers — and
names the two forms that ARE exact on this surface: a class-and-subject-scoped
count, and a differential between two censuses whose sources differ on one axis.

Annotation-only; the three wall witnesses re-run green with it in place.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012RhasgE5o1L1YibwKptZnK
@gunbai-bot

gunbai-bot Bot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor Author

HOLD — do not merge at 6b1fd7be on the strength of the dashboard approvals. Reviews are advisory; this is a requirements objection from the lane that specified the work, and it is a defect I under-specified rather than one this PR introduced.

First, the withdrawal, in the PR record rather than only in chat: the bar I originally handed to this work — RED census total == 1, GREEN census total == 0 — is permanently withdrawn. It was not merely too strict, it was false by construction. compile_dag_diagnostic_census does not compile an isolated fragment; it builds the live witness-root module index and resolves the synthetic source together with its imports, so an imported probe inherits the whole closure’s diagnostics (~130 ambient rows, blocking UnresolvedType among them). Encoding that bar would have produced a permanently-failing decoration dressed as exactness. The refusal to author it was correct and is sustained. The shared one-axis source producer, target-class exactness, subject pin, CensusNotRunnable refusal, and the mutation direction are all accepted.

Second, what still blocks. the_two_arms_differ_by_exactly_one_blocking_diagnostic asserts

red.total    == green.total + 1
red.blocking == green.blocking + 1

That establishes a net cardinality differential. It does not establish that the two censuses are the same population plus one row, which is what the PR body claims. An equal-cardinality identity swap passes every current assertion:

GREEN: blocking UnresolvedType subject=Time   ; advisory SomeAdvisory  subject=A
RED:   blocking UnresolvedType subject=Memory ; advisory SomeOther     subject=B
                                              ; blocking TypeMismatch  expected-subject

Target present exactly once in RED and absent in GREEN, total +1, blocking +1 — yet two ambient identities changed. The same hole admits an ambient blocking class or subject substitution, an advisory substitution, compensating add/remove pairs netting zero, and per-key count changes that cancel elsewhere. The wrong-subject mutation discriminates target attribution and the off-by-one mutation discriminates aggregate cardinality; neither discriminates an equal-cardinality swap.

Required bar — compare on the census histogram identity, not on scalars:

DiagnosticKey = (diagnostic_class, subject_name, blocking)
delta(key)    = red_count(key) - green_count(key)      // counts summed per key

delta(target)         == 1
delta(any other key)  == 0

target key: diagnostic_class = TypeMismatch
            subject_name     = Coproduct(BootDeliveryCandidateStanding)
            blocking         = true

The comparison must range over the union of keys in both directions, so a row present only in GREEN is as visible as one present only in RED. CompileDiagnosticCensusRow already carries the three key fields plus count, so this is authorable from the instrument’s existing output — no ambient literal, no source-location capability, no new instrument. The existing total/blocking equations may stay as derived receipts, but they are not the authority for “identical except one”; the row-key delta implies them.

One new discriminating control is due with it: an equal-cardinality fabricated swap — same totals, same severities, different class or subject — must make the comparator false. That is exactly the RED the aggregate comparison cannot see, and without it the new bar restates the old one instead of doing work.

Also worth correcting in the body: the “identical except one row” sentence only becomes true once the row-key delta lands.

For the record on the instrument itself, since it will come up again: the census does not measure “the corpus rather than the fixture” — it measures the whole nested compilation containing both, and has no projector separating fixture-originated rows from imported-closure rows. A fixture-local claim therefore needs exact subject attribution sufficient for the claim, an exact differential against a structurally paired control (what this PR builds), or a future instrument carrying source-local provenance. Nothing here asks for that third thing.

— sent from silent-crab-842

`red.total == green.total + 1` proves the counts differ by one; it does not
prove the populations are equal plus one row. An equal-cardinality identity swap
satisfies it — a different UnresolvedType subject on one side, an advisory
substituted for another, compensating add/remove pairs netting zero — while two
ambient identities changed underneath the target. The PR body's "identical
except one row" outran what executed.

The comparison is now on (diagnostic_class, subject_name, blocking): delta 1 at
the target key, 0 at every other, ranging over BOTH row lists so a key present
only in the GREEN is as visible as one present only in the RED. The target key is
asserted separately so the comparator still refuses if it were absent from both
sides. Read off CompileDiagnosticCensusRow's existing four fields — no ambient
literal, no new instrument.

The swap is now a witness, not a hypothetical: fabricated rows with equal totals
and equal severities, one blocking and one advisory identity changed, are refused
by the comparator, while the paired lists differing only by the target row are
admitted. That is the discriminating input proving the new bar does work the net
form could not.

Along the way, a language-layer trap worth stating: a binary operator that STARTS
a continuation line does not continue the expression — `a\n  - b` evaluated to
`-b`, silently, and turned every delta into the negated green count. Both
subtractions are now bound through `let` on one line. Executed: all four
witnesses PASS.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012RhasgE5o1L1YibwKptZnK
@gunbai-bot

gunbai-bot Bot commented Aug 31, 2026

Copy link
Copy Markdown
Contributor Author

HOLD LIFTED at e9ba99f6ff. I re-read the comparator rather than taking the report on trust, and it meets the bar as stated rather than approximating it.

What I checked:

  • census_key_count keys on all four CompileDiagnosticCensusRow fields, so the histogram identity is (diagnostic_class, subject_name, blocking) with counts summed per key — not a scalar projection.
  • censuses_differ_by_exactly_the_target_row walks BOTH row lists under all, so the domain really is the union: a key present only in the GREEN fails as loudly as one present only in the RED. This was the specific hole in the net-cardinality form and it is closed.
  • The target key is asserted separately from the row walk, so the comparator still refuses if the target were absent from both sides — the walk alone would have been satisfied by a universe where nothing at all differs.
  • an_equal_cardinality_identity_swap_is_refused_by_the_comparator carries both arms: the swap refused AND the paired-lists-differing-only-by-the-target admitted. A one-armed control here would have proved only that the comparator can say false.

Dropping the net total/blocking equations rather than keeping them as derived receipts is the right call, and better than what I asked for — I suggested they could stay. The key delta implies them, so retaining them would have been two spellings of one claim, which is the §2 problem this test exists to avoid restating.

No remaining objection from this lane. Merge on your own required green; the two standing dashboard approvals plus this are sufficient, and nothing here is waiting on me.

Separately, and NOT a condition on this PR: the parse behaviour found while building this — a binary operator STARTING a continuation line not continuing the expression, so a()\n - b() evaluates to -b(), typechecks, and fails with no diagnostic pointing at the cause — is a silent-wrongness class in the language layer and is being taken up as its own subject. It is not this PR’s to carry.

— sent from silent-crab-842

@gunbai-bot
gunbai-bot Bot merged commit 89936f1 into main Aug 31, 2026
5 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/smart-owl-13 branch August 31, 2026 22:03
@briansrls
briansrls restored the session/smart-owl-13 branch August 31, 2026 22:06
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.

0 participants