test: an unrunnable record names the check it stands in for (#1040)

[OffgridwithJD]

What this changes

Two of the four check_unrunnable calls in one loop in test/hilbert_locality.sh carried
a shortened name; the other two matched their runnable twins exactly:

:574  check_unrunnable "box $box: groups read, Z-order"
:597  check_num        "box $box: groups read over $PLACEMENTS placements, Z-order"

:578  check_unrunnable "box $box: Hilbert reads fewer groups than Z-order"
:602  check_text       "box $box: Hilbert reads fewer groups than Z-order"     <- same name

So the property had two ledger keys, and which one appeared depended on whether that
box's two partitions came out different that day. The key was a function of the data.

Scope, stated rather than implied: hilbert_locality is not a ledger-covered suite
(covered = differential, harness_selftest, native_join_runtime_filter,
native_join_vector_agg), so this is a wrong key waiting to be seeded, not a wrong number
in check_ledger.tsv today.

This is half B of the split agreed with @jdatcmd on #1040. They hold half A, the
grader. B lands first so A lands green.

Why a guard and not just the two-line rename

The convention is already near-universal, and that is exactly what made the lapse
invisible. Of the 25 check_unrunnable call sites in test/*.sh, 23 carry the runnable
name — hilbert_cluster 9 of 9, projection_rewrite 11 of 11 counting its pgc_pass
twin. A shorter name in a new refusal branch reads as ordinary, and both halves of a
two-branch site are rarely read together.

Selftest part 480 drives .github/scripts/unrunnable-arm-names.py over test/*.sh. It is
part 470's property one helper over: 470 asks whether a skip loop still names the arms its
sibling branch emits, this asks whether an unrunnable record names a check the same file
asserts anywhere.

The tool derives three things a list of them got wrong first

derived	because
which functions record	from the pgc_record call in the body. Two hand-written lists omitted pgc_pass, and projection_rewrite.sh then read as a false orphan: its twin records through pgc_pass, not a check_* helper.
which argument is the name	pgc_skip records pgc_record FAIL "$2". Argument one is the CAPABILITY, so reading it takes arrow where the check is called arrow support is present — the bash-side mirror of the name-position defect #1036 and #1038 closed on the python side, across 22 call sites. pgc_require_tools records a FIXED name and takes none.
what counts as a refusal	from the verdict recorded, not the helper's spelling. check_unrunnable records FAIL when the reason code is not in the closed list, which made it its own twin in a draft and blocked wrapper detection.

check_skip is deliberately not swept, and that is a finding rather than an omission.
A skipped arm has no runnable counterpart by construction — the name IS the arm — so 21 of
its 23 call sites have no twin and always will. Sweeping it would report 21 mismatches
that are all correct code.

The positive control is the point of the part

This guard's steady state is zero mismatches, and a sweep that matched nothing reports zero
too. Two arms drive the real tool over a fixture whose refusal branch names something the
file never records, and over a control where the names agree. Three further arms pin values
that were wrong in a draft of the tool rather than restating the code: the refusal set,
pgc_skip:2, and pgc_pass/pgc_fail being twins.

The removal proof

The rename is the only variable between the two runs. Both on this branch, db74d9e base.

BEFORE the rename   harness_selftest RC=1, 943 checks, exactly ONE FAIL:

  FAIL  every unrunnable record names a check its own suite asserts (#1040):
        got [hilbert_locality.sh:574 box $box: groups read, Z-order
             hilbert_locality.sh:576 box $box: groups read, Hilbert] want []

        the other 8 arms of the new part all PASS, including both control arms

AFTER  the rename   harness_selftest RC=0, 943 checks

Also in this PR, and why it is not a separate one

The census re-derivation printed in check_ledger_budget.txt reads the wrong field and
returns zero:

awk -F'\t' '$4=="never"' test/check_ledger.tsv | wc -l     -> 0
awk -F'\t' '$5=="never"' test/check_ledger.tsv | wc -l     -> 1189   on db74d9e
stated in the budget                                          1189

#1010 inserted the majors a row claims as field 4, moving the last-red to field 5, and the
recipe stayed on field 4. The CHANGELOG entry for #1010 states that
check_ledger_budget.txt carries the corrected form — it does not. The gate is
unaffected: it computes the census itself and never runs this command. So the harm is a
reviewer re-deriving the number by the printed method, getting 0, and "correcting" a budget
that was right — the same fail-closed direction as #1004, and the same reason to remove it.

Fixed here rather than filed because this change moves that very number (1189 -> 1198),
and a wrong recipe beside a number nobody can check is worse than no recipe. The two
historical $4 forms in CHANGELOG.md are left alone: they are deliberately preserved wrong
instructions, not live ones.

Verified

harness_selftest    RC=0, 943 checks              (red/green above, PG18a)
sweep               25 sites, 24 compared, 1 dynamic, 0 mismatches
                    unchanged with --keep-heredocs, so the answer does not depend on it
shellcheck -S error over test/*.sh test/selftest/*.sh    clean
docs_style          14/14 PASSED
ledger              rows 1197 -> 1206 (+9, the new part)
                    census 1189 -> 1198, re-derived by the CORRECTED command
                    ceiling 249 -> 249, does not rise
                    orphans 0, unprunable 0
                    gate rc=0 against db74d9e
widened extractor   all 7 ported pairs rc=0 missing=0

That last line is the one that matters for #1040's other half: with these two names fixed,
widening compare_to_bash.py to all eight helpers lands green, with no change to the
port and none to pgc_vacuity.py.

Closes nothing on its own — #1040 stays open for the grader half.

🤖 Generated with Claude Code

https://claude.ai/code/session_012RSw4qMHS7ByE7PY8Ns4cs

[OffgridwithJD]

Head moved to 75a3447c7c699688e42591cb2f0e67c2364a94b3 — the sweep's exit code was a lie

@jdatcmd found that the tool prints MISMATCH and returns 0. I reproduced it unpiped before
changing anything, because $? after a pipeline is the last stage's:

on main    2 mismatches   rc=0
on branch  0 mismatches   rc=0

Part 480 gates on the parsed output, so it was never fooled. That is a fact about the
wiring in this PR, not about the tool: anyone who runs it in CI and trusts $? gets a gate
that cannot fail. So it is fixed here rather than left as an observation.

Three arms, not one. "Exits non-zero on a mismatch" alone passes on a tool that always
exits 1; "exits zero when clean" alone passes on a corpus with nothing to look at. The clean
run therefore uses a second fixture directory holding only the agreeing file, with a
premise asserting that directory really has a refusal site:

PASS  the sweep EXITS non-zero when it reports a mismatch
PASS  and exits zero on a corpus that has refusal sites and no mismatch
PASS  premise: that clean run had a refusal site to be silent ABOUT

Neither fixture run is piped, and the comment records why.

The delta, so the previous verification does not have to be redone from scratch

.github/scripts/unrunnable-arm-names.py   |  8 +   one-line return, plus its comment
test/selftest/480-...                     | 28 +   three arms, second fixture dir
test/check_ledger.tsv                     |  3 +   the three new checks
test/check_ledger_budget.txt              |  2 +-  census 1198 -> 1201
CHANGELOG.md                              |  9 +   one paragraph

Nothing else moved between b3433be and 75a3447; that stat is the whole difference.
test/hilbert_locality.sh and test/selftest/parts.manifest are untouched by this commit,
so the rename and its removal proof stand exactly as reviewed.

Re-verified on the new head

harness_selftest    RC=0, 946 checks (943 + 3), 0 FAIL
part 480            12 checks, all pass
sweep unpiped       main 2 mismatches rc=1 | branch 0 mismatches rc=0
shellcheck -S error over test/*.sh test/selftest/*.sh   clean
docs_style          14/14
ledger              rows 1206 -> 1209 (+3), census 1198 -> 1201 re-derived by
                    the corrected $5 command, ceiling 249 -> 249, orphans 0,
                    gate rc=0 against db74d9e

One thing the guard caught on me: an em dash reached the changelog and docs_style refused
it. That is the guard doing its job, and worth saying rather than quietly fixing.

Also filed while here: #1042, the same body-extraction defect in skip-loop-arms.py,
A/B'd as latent (byte-identical output on db74d9e9c). Not fixed in this PR — different
tool, different caller, and its own arm is worth more than the fix.

[OffgridwithJD]

Head 3a640b00eda2f3041e6dde0650513d8cde2b195c — the PG17 red was one field

suites (PG 17) failed on 75a3447 while suites (PG 18) passed. Every suite PASSED in the
failing leg. The census agreed at 1201, the ceiling did not rise, the population reconciled at
253. The only failing condition was the majors field on my twelve new rows:

major field across harness_selftest rows
  934   15;16;17;18;19
   12   18            <- part 480's, and only part 480's

PG17: not in the ledger: harness_selftest 480-... (x12, on major 17)
      PG17 has a check the ledger has never seen, which is not a pass

pgc_ledger.py merge stamps the majors of the log it is given, and I merged one PG18 run.

Not fixed by setting the field

@jdatcmd spotted it independently and proposed writing 15;16;17;18;19 into the twelve rows to
match their 934 neighbours. That goes green, and it is the wrong fix: the value would be
consistent, plausible and unobserved. This field is what the gate compares against, so a
hand-written row is a claim the gate can never catch being wrong — the standard rather than a
measurement checked against one. They withdrew it on that reasoning; their summary is better
than mine, that copying the neighbours is the version which looks like diligence.

The stronger reason is the second one: this answers whether part 480 passes on 15 and 19 at
all. Nobody had asked. The red-then-green removal proof for this whole PR was PG18a, and a
defect in the major field is invisible there by construction.

So harness_selftest ran on all five assert builds and all five logs were merged. The majors
field accumulates as a set (pgc_ledger.py:283), checked in the source before relying on it.

Agreed with @jdatcmd before the runs, so it was not decided after seeing the number: if a
major produced fewer checks, the rows would say what each run observed. A check existing on
four majors and not the fifth is a finding about the part, not a number to smooth.

Measured

PG15  rc=0  946 checks  0 FAIL  12 rows from part 480
PG16  rc=0  946 checks  0 FAIL  12
PG17  rc=0  946 checks  0 FAIL  12
PG18  rc=0  946 checks  0 FAIL  12
PG19  rc=0  946 checks  0 FAIL  12

(part, name) sets: 45 on each major, and PG18 differs from 15, 16, 17 and 19 by ZERO lines,
so no check exists on some majors and not others and the four new logs added no row

ledger gate, once per major's log:   rc=0 on all five, zero "never seen" lines
rows 1209 unchanged | census 1201 unchanged | ceiling 249 -> 249
diff: 12 insertions, 12 deletions in check_ledger.tsv and nothing else
every changed row differs ONLY in field 4 -- checked by normalising that field and
  asserting each line then appears exactly twice
the ledger is now uniform: 1209 of 1209 rows carry 15;16;17;18;19

The delta from 75a3447 is test/check_ledger.tsv alone, so every earlier verification on that
head stands: the rename, its removal proof, the exit-code arms, shellcheck, docs_style, and
the widened-extractor result.

The lesson worth more than the fix

A green on the major you develop on is not a green on the matrix, and this defect is invisible
there by construction. CI runs suites on 17 and 18 only, so 17 was the only place it could
surface before merge — and it did.

[jdatcmd]

APPROVE at 3a640b0. 14/14, both suites legs green, read on this sha at 18:04:36Z and not from any earlier rollup. Everything below was re-run here rather than taken from the PR.

The guard reddens and greens, both directions, unpiped

sweep on main db74d9e    rc=1   2 mismatches
sweep on 3a640b0         rc=0   0 mismatches
buckets                  sites 25 = dynamic 1 + compared 24

rc is the verdict now, and that matters beyond this PR: the first version printed MISMATCH and exited 0. Part 480 was never fooled, because it gates on the parsed output — but the next caller is the one that trusts $?, and a tool whose exit code cannot fail is a trap regardless of today's only consumer.

Three arms, not one, which is the part I would point a reader at. "Exits non-zero on a mismatch" alone passes a tool that always exits 1. "Exits zero on a clean corpus" alone passes a corpus with nothing to find. The third arm is what separates them, and it has its own premise:

check "premise: that clean run had a refusal site to be silent ABOUT"   compared == 1

A clean corpus and an empty corpus both report rc=0; only one is evidence.

The ledger fix was derived, not written

The previous head failed suites (PG 17) because its 12 new rows carried major 18 while every other row carried 15;16;17;18;19. I proposed setting the field by hand and that was wrong — the field is what the gate compares against, so a hand-written row is a claim the gate can never catch being wrong. Running all five majors and merging the logs is the right answer, and it answered a question neither of us had asked: whether part 480 runs at all on 15 and 19. Five (part, name) sets of 45, PG18 differing from the other four by zero lines.

Verified here:

diff 75a3447 -> 3a640b0   test/check_ledger.tsv alone, 12 insertions 12 deletions
                          normalise field 4: 12 distinct lines, each exactly twice,
                          ZERO asymmetric -- so the rows differ only in the major
major field, WHOLE ledger 1209 of 1209 carry 15;16;17;18;19 -- no straggler anywhere
census                    stated 1201, $5-re-derives 1201, 1209 rows, 12 for part 480
part 480                  12 real checks == 12 ledger rows
                          (16 code invocations minus 4 that are FIXTURE CONTENT
                           written into offender.sh/control.sh for the tool to read)

The whole-column check is the one worth keeping as a habit rather than an accident: a fix that corrected these twelve and left a thirteenth row elsewhere at 18 would look identical in the diff.

The census recipe

$4=="never" returned 0 against a stated 1189; $5=="never" returns the stated number. Correct to fix it here rather than separately, because this PR moves that number and a recipe nobody can run beside a number nobody can re-derive is worse than no recipe. Leaving the two historical $4 forms in CHANGELOG.md is right — docs_style.sh's scope note is explicit that landed entries are a record, not a live document.

What this PR unblocks

The widened extractor (#1040's other half) is green on this head: all seven pairs rc=0 missing=0, hilbert_locality at 34 bash names. That half goes up separately once this lands, re-derived against the moved main rather than carried from here.

The methodological point, which outlives the PR

A complete red-then-green removal proof could not see this defect, because the proof ran on one major and the field records the major it ran on. Being more careful locally could not have found it; only the matrix could. Generalised: a mutation proof is evidence about behaviour under the conditions it ran in, so any value that RECORDS those conditions is outside what it can reach — a recorded version, date, environment, or build path. The fix for that is another condition, not more rigour.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NhwXKAgSmYDUjteWkfajHK