From dbfa999c0833966b160b08166d2834dbb08806f3 Mon Sep 17 00:00:00 2001 From: OffgridwithJD Date: Fri, 11 Sep 2026 22:56:15 +0000 Subject: [PATCH 1/2] test: the stamp-block extraction anchors on the write, not on file position (#961) Part 460 took the FIRST one-tab 'if (' in run_all_versions.sh. There is exactly one today, so it was unambiguous -- and the premises would have caught it if that stopped being true, since the extracted block would hold zero or two stamp writes. @jdatcmd raised it while approving #961: it was the premises doing the work rather than the anchor. The anchor now finds the stamp write and walks BACK to the 'if (' enclosing it, then forward to the first terminator at or after it. A subshell added anywhere else in the file cannot move the range, because the range is defined by the line it is about. NECESSARY -- identical on today's input, or it changes behaviour while claiming not to: old anchor md5 47b4f1a9193c new anchor md5 47b4f1a9193c SUFFICIENT -- a second one-tab subshell injected ABOVE the stamp block, which is the edit that motivated the change: OLD 4 lines, 0 stamp writes extracted the WRONG block; the 'exactly one stamp write' premise reads 0, so it fails loudly NEW 7 lines, 1 stamp write unchanged and the part run against that injected controller: rc=0, 0 FAILs, all four arms. Either half alone is worthless: md5-only proves the change does nothing that matters, injection-only proves it does something without showing what else moved. THE BOUNDARY THE NEW DESIGN COULD OPEN, and it is not one the old one had. A backward walk has to decide what to do when it runs off the top of the file, and one of the three possibilities would satisfy every guard: walks to line 1, emits everything above a block that parses and is WRONG emits the write alone 1 write: BOTH premises PASS on a block that is not the call site emits nothing premises catch it, same as before Measured on a fixture with two lines above the write and no enclosing 'if (': it emits NOTHING. 'open' is never assigned, so 'start' is empty and the guard 'if (!start || !stamp) exit' fires before the print loop. One premise added -- 'the extraction produced a block at all' -- because an awk whose condition never fires prints nothing, and an empty block would otherwise read as a block with no stamp write in it. Two different failures arriving at the same number. Two writes in SEPARATE subshells is the case the count premise cannot see: the block holds one and the premise passes. The static caller sweep catches it -- injected, it reports got [4] want [3] on both the premise and the arm. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Uf6UoeBRZYLQZa4KxNiw8a --- ...0-the-controller-must-record-the-binary.sh | 50 ++++++++++++++++++- 1 file changed, 49 insertions(+), 1 deletion(-) diff --git a/test/selftest/460-the-controller-must-record-the-binary.sh b/test/selftest/460-the-controller-must-record-the-binary.sh index 832d5ea2..e2e60acf 100644 --- a/test/selftest/460-the-controller-must-record-the-binary.sh +++ b/test/selftest/460-the-controller-must-record-the-binary.sh @@ -45,11 +45,59 @@ check "premise: this part was given an executable pg_config to read the prefix f # The subshell block, from `if (` to `); then`. A LITERAL TAB, not `\t`: GNU grep's # BRE does not read `\t` as a tab, and the first version of this premise counted 0 # and would have let the arms below run against an empty block. +# ANCHORED ON THE STAMP WRITE, NOT ON FILE POSITION. The first version took the +# FIRST one-tab `if (` in the controller. There is exactly one today -- so it was +# unambiguous, and the premises below would have caught it if it stopped being so +# (the extracted block would hold zero or two stamp writes). @jdatcmd raised that +# while approving #961: it is the premises doing the work rather than the anchor. +# +# So the anchor now finds the stamp write and walks BACK to the `if (` that encloses +# it, then forward to the first terminator at or after it. A second subshell added +# anywhere in the file cannot move the range, because the range is defined by the +# line it is about. +# +# `start` BEING UNSET WHEN NOTHING ENCLOSES THE WRITE IS LOAD-BEARING, not an +# oversight to tidy up. A backward walk has to decide what to do when it runs off +# the top, and one of the three possibilities satisfies every guard below: +# +# walks to line 1, emitting everything above a block that parses and is WRONG +# emits the write alone ONE stamp write, so both premises +# PASS on a block that is not the +# call site +# emits nothing the premises catch it +# +# This takes the third because `open` is never assigned, `!start` is true for an +# unassigned awk variable, and the guard exits before the print loop. Defaulting +# `start` to 1 would look like a tidy-up and would buy the first case. Measured on a +# fixture with two lines above the write and no enclosing `if (`: zero lines out. _c961_block="$(awk -v t="$_c961_tab" ' - $0 == t "if (" {f=1} f {print} f && $0 == t "); then" {exit}' "$_c961_rav")" + { line[NR] = $0 } + $0 == t "if (" { open = NR } + /pgc_write_source_stamp/ && !stamp { stamp = NR; start = open } + END { + if (!start || !stamp) exit + for (i = start; i <= NR; i++) { + print line[i] + if (i >= stamp && line[i] == t "); then") exit + } + }' "$_c961_rav")" +check "premise: the extraction produced a block at all" \ + "$([ -n "$_c961_block" ] && echo yes || echo empty)" "yes" check "premise: the controller's stamp block was extracted exactly once" \ "$(printf '%s\n' "$_c961_block" | grep -c "^${_c961_tab}if ($")" "1" +# AND NO SUBSHELL OPENS BETWEEN THE OPENER AND THE WRITE, at any depth. The anchor +# matches `if (` at ONE tab, so a write nested inside a DEEPER subshell leaves `open` +# pointing at the outer block -- and that block holds exactly one one-tab `if (` and +# exactly one stamp write, so every premise above it passes on a block WIDER than the +# call site. Measured on a fixture with the write in a two-tab subshell inside a +# one-tab one: 8 lines out, 1 one-tab `if (`, 1 write, all premises green. +# +# Counting `if (` at ANY indent is what distinguishes them: the real block has one, +# the nested shape has two. Cheaper than teaching the anchor to track depth, and it +# fails closed -- a shape this does not understand is refused rather than driven. +check "premise: nothing opens a deeper subshell inside the extracted block" \ + "$(printf '%s\n' "$_c961_block" | grep -cE '^[[:space:]]*if \($')" "1" check "premise: and it holds exactly one stamp write" \ "$(printf '%s\n' "$_c961_block" | grep -c 'pgc_write_source_stamp')" "1" From 06f6a4bc5329a848f954d6a5f32467768d98bef6 Mon Sep 17 00:00:00 2001 From: OffgridwithJD Date: Fri, 11 Sep 2026 23:01:56 +0000 Subject: [PATCH 2/2] test: the CHANGELOG and ledger for the extraction anchor (#961 follow-up) Two new check names -- the premise that the extraction produced a block at all, and the premise that nothing opens a deeper subshell inside the extracted block. Guarded log, merged, census DERIVED from the file. AND A CORRECTION TO THIS PR'S OWN CLAIM. The first version said a subshell added anywhere else in the file cannot move the range. That is false for a NESTED one: a write inside a deeper subshell leaves the opener pointing at the outer block, which holds exactly one one-tab 'if (' and exactly one stamp write -- so every premise passed on a block wider than the call site. Measured on a fixture with the write two tabs in: eight lines out, all premises green. Found by driving a hole I had named in my own change rather than leaving it for review. The premise counting 'if (' at ANY indent closes it: one in the real block, two in the nested shape. Cheaper than teaching the anchor to track depth, and it fails closed. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01Uf6UoeBRZYLQZa4KxNiw8a --- CHANGELOG.md | 51 ++++++++++++++++++++++++++++++++++++ test/check_ledger.tsv | 2 ++ test/check_ledger_budget.txt | 2 +- 3 files changed, 54 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 6a6e3e3c..720ff606 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1765,6 +1765,57 @@ true until the next version shipped. anywhere in the tree, removed by #917 with their rows left behind. Those are not created by this change and are filed separately rather than tidied away here. +- The controller-stamp extraction anchors on the write rather than on file position + (#961 follow-up). + + Selftest 460 took the **first** one-tab `if (` in `run_all_versions.sh`. There is + exactly one today, so it was unambiguous, and the premises would have caught it if + that stopped being true -- the extracted block would hold zero or two stamp writes. + It was the premises doing the work rather than the anchor. + + The anchor now finds the stamp write and walks back to the `if (` enclosing it, then + forward to the first terminator at or after it. A subshell added elsewhere at the same + indent cannot move the range, because the range is defined by the line it is about. + + **A subshell that NESTS around the write can still widen it, and that is a premise + rather than a fix.** The anchor matches `if (` at one tab, so a write inside a deeper + subshell leaves the opener pointing at the outer block -- which holds exactly one + one-tab `if (` and exactly one stamp write, so every other premise passes on a block + wider than the call site. Measured on a fixture with the write two tabs in: eight lines + out, all premises green. A premise counting `if (` at ANY indent distinguishes them -- + one in the real block, two in the nested shape -- which is cheaper than teaching the + anchor to track depth and fails closed, refusing a shape it does not understand rather + than driving it. + + Proven in both directions, because either half alone says nothing. Identical on + today's input -- the extracted block hashes `47b4f1a9193c` before and after -- and + different on the input that motivated the change: + + a second one-tab subshell injected ABOVE the stamp block + OLD anchor 4 lines, 0 stamp writes, so it extracted the WRONG block and the + `exactly one stamp write` premise reads 0: loudly wrong + NEW anchor 7 lines, 1 stamp write, unchanged + + md5-only would prove the change does nothing that matters; injection-only would prove + it does something without showing what else moved. + + **And it closes a boundary the new design could open rather than one the old one + had.** A backward walk has to decide what to do when it runs off the top of the file, + and one of the three possible behaviours satisfies every guard in the part: emitting + the write alone gives exactly one stamp write, so both premises pass on a block that + is not the call site. This emits nothing instead, because `open` is never assigned and + the guard exits before the print loop -- a property that arrived from the guard's + shape rather than from foresight, now written into the code as load-bearing so the + next reader does not default `start` to 1 as a tidy-up. + + One premise added, `the extraction produced a block at all`, because an awk whose + condition never fires prints nothing and an empty block would otherwise read as a + block with no stamp write in it -- two different failures arriving at the same number. + + Two stamp writes in **separate** subshells is the case the count premise cannot see: + the extracted block holds one and the premise passes. The static caller sweep catches + it -- injected, both the premise and the arm report `got [4] want [3]`. + ## [1.0-alpha3] - 2026-09-02 ### Added diff --git a/test/check_ledger.tsv b/test/check_ledger.tsv index 82fb87f5..29b068c0 100644 --- a/test/check_ledger.tsv +++ b/test/check_ledger.tsv @@ -851,7 +851,9 @@ harness_selftest 460-the-controller-must-record-the-binary control: without that harness_selftest 460-the-controller-must-record-the-binary every caller records the installed library's digest (#961) never - harness_selftest 460-the-controller-must-record-the-binary premise: all three stamp call sites were found with their arguments joined never - harness_selftest 460-the-controller-must-record-the-binary premise: and it holds exactly one stamp write never - +harness_selftest 460-the-controller-must-record-the-binary premise: nothing opens a deeper subshell inside the extracted block never - harness_selftest 460-the-controller-must-record-the-binary premise: the controller's stamp block was extracted exactly once never - +harness_selftest 460-the-controller-must-record-the-binary premise: the extraction produced a block at all never - harness_selftest 460-the-controller-must-record-the-binary premise: the matrix controller is present and parses never - harness_selftest 460-the-controller-must-record-the-binary premise: the mutation removed the installed-digest argument never - harness_selftest 460-the-controller-must-record-the-binary premise: this part was given an executable pg_config to read the prefix from never - diff --git a/test/check_ledger_budget.txt b/test/check_ledger_budget.txt index dadef130..7c63eb23 100644 --- a/test/check_ledger_budget.txt +++ b/test/check_ledger_budget.txt @@ -34,4 +34,4 @@ suites_not_covered 250 # Without that it is a hand-maintained count that drifts, which is the failure # this repository has spent a day proving. It is not a ceiling; it is a # measurement that must be true. -checks_never_observed_red 903 +checks_never_observed_red 905