test: the four PG-log secret-leak claims had no premise (#1032)

[OffgridwithJD]

Closes #1032.

Four secret-leak claims over $PGC_LOGFILE could pass having read nothing. Each now carries its own premise.

The hole is exactly one state

iceberg_rest.sh, iceberg_rest_server.sh (twice) and iceberg_rest_vended.sh assert a token or secret never reaches the PG server log, comparing grep -c "$SECRET" "$PGC_LOGFILE" against 0. Nothing in the tree asserted that file exists, is readable, or holds a line.

I expected the usual fail-open shapes and found only one. Measured over all four states:

the log is	grep -c gives	the claim
a real server log	0	passes, correctly
present and EMPTY	0	PASSES, having read nothing
missing	(nothing)	fails
leaking the secret	1	fails

grep -c prints nothing for a file it cannot open, so a missing path, an unset variable and an unreadable file all fail closed already. Present-and-empty prints the 0 the claim wants. Anything that leaves the log present and empty — a rotation, a log_destination change, a truncating reuse path — turns all four green and says nothing.

The fix

Each claim carries its own premise immediately above it, rather than one per suite, so a claim and its premise cannot drift apart:

_ir_loglines="$(grep -c . "$PGC_LOGFILE" 2>/dev/null)" || _ir_loglines=0
check "premise: the PG server log holds lines to search" \
	"$([ "${_ir_loglines:-0}" -gt 0 ] && echo yes || echo no)" "yes"

Not the grep -c . ... || echo 0 form the issue suggested. grep -c prints 0 and exits 1 on an empty file, so that yields two lines and turns the comparison into a shell error rather than a comparison:

empty log with || echo 0 -> $'0\n0'

That is the same defect I raised on #1102, and it would have put it into the fix for it. The assignment form carries one value.

The two premises in iceberg_rest_server.sh are named distinctly, because a row is keyed on (suite, part, name) and two checks sharing a name share a row (#982).

Removal proof, at suite level

Pointing both reads at a present-and-empty file:

FAIL  premise: the PG server log holds lines to search: got [no] want [yes]
PASS  the token never appears in the server (PG) log
file the claim read: 0 lines

The premise catches precisely what the claim cannot see, and the claim still passes — which is the whole finding.

A first attempt at this proof did not reproduce, and that is worth recording. Truncating $PGC_LOGFILE in place left the premise green, because the running postmaster wrote a line back within the same instant:

MUT-DIAG lines immediately after truncation: 1

The mutation never created the state it claimed to, and an invalid control that reports green looks exactly like a passing one. The valid version points PGC_LOGFILE at a static file nothing writes to.

Verification

All three suites on PG18, unmutated:

iceberg_rest:        rc=0  FAILs=0  iceberg_rest.sh: PASSED
  PASS  premise: the PG server log holds lines to search
  PASS  the token never appears in the server (PG) log
iceberg_rest_server: rc=0  FAILs=0  iceberg_rest_server.sh: PASSED
  PASS  premise: the PG server log holds lines to search, for the mapping token
  PASS  premise: the PG server log holds lines to search, for the client secret
  PASS  the mapping token never appears in the PG server log
  PASS  the client secret never appears in the PG server log
iceberg_rest_vended: rc=0  FAILs=0  iceberg_rest_vended.sh: PASSED
  PASS  premise: the PG server log holds lines to search
  PASS  the vended secret never appears in the PG server log

bash -n and shellcheck -S error -s bash clean on all three. The mutated file was restored byte-exact after each arm.

The ledger is untouched. All three suites hold zero rows, so they are uncovered: no rows move, the new-check refusal does not apply, and suites_not_covered does not change — adding checks to a suite already counted as uncovered leaves that ceiling where it is.

Note on the CHANGELOG

This adds a new ## [Unreleased] section, and so does #1098. They will conflict for no reason related to either change — which is #996, still open.

🤖 Generated with Claude Code

https://claude.ai/code/session_012RSw4qMHS7ByE7PY8Ns4cs

[linuxhikerpm]

The empty-log hole is real: grep -c SECRET against an existing empty file is 0, which is the want. Missing/unreadable already fail closed. A per-claim premise immediately above each absence check is the right pin, and the assignment form (grep -c . ... || var=0) avoids the two-line || echo 0 trap. Distinct names on the two server-suite premises keep the ledger key unique.

CHANGELOG correctly opens ## [Unreleased] after alpha4 closed. That will collide with other Unreleased PRs on merge; that is editorial, not a defect in the premises. Approving, not merging.

[jdatcmd]

Approving. The hole is real, the fix closes exactly it, and I reproduced the state table independently rather than reading it.

What it closes

grep -c prints 0 for a file that exists and is empty, so a leak claim expecting 0 passes having read nothing. A MISSING file prints nothing and already failed the claim, so empty was the only hole. I ran the four states myself:

real     premise=yes  claim=[0]   premise holds
empty    premise=no   claim=[0]   PREMISE CATCHES IT
missing  premise=no   claim=[]    PREMISE CATCHES IT
leak     premise=yes  claim=[1]   premise holds, claim fails

Your table and mine agree, including that missing was never the hole.

The wiring, which is what I actually wanted to check

A premise that guards a different file than the claim greps is decoration. These do not:

110  _ir_loglines="$(grep -c . "$PGC_LOGFILE" ...)"
111  check "premise: the PG server log holds lines to search"
113  check "the token never appears in the server (PG) log"
114      "$(grep -c "$TOKEN" "$PGC_LOGFILE" ...)" "0"

Same variable, and the premise is on the line before the claim rather than after it, so a vacuous claim cannot already have passed.

The note on || echo 0

Worth the space it takes. grep -c prints 0 AND exits 1 on an empty file, so || echo 0 yields two lines and turns the comparison into a shell error. That is the kind of thing that gets "simplified" back in by someone tidying, and the comment is what stops it.

One thing I looked for and found already answered

My first question was whether a non-empty log is a POSITIVE control or only a necessary premise: it proves the file has content, not that the search would find the secret if it were there. Your leaking got=[1] row is that control, and it is in the comment. I would not have found it if the measurement table were not written down.