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 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"