From cba5fa330123e0ec06bf3c8741ec2d1b01c02f2e Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 13:14:20 +0200 Subject: [PATCH] lift-guard: close all nine classes the reviewer demonstrated MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-8 review (Claude, register key `lift-guard-regex-both-directions`). Every class reproduced here before fixing, and re-tested after. THREE FALSE NEGATIVES — the payload reads a name and the guard stayed silent, which is the direction that costs something, because silence is what the tool exists to prevent: echo $((X + 1)) arithmetic expansion reads X without a `$` before the (( Y > 0 )) name, and the read pattern cannot match it: the character after `$` is `(`. Both contexts are now tokenised. `if [ $((inm + ins)) -eq 0 ]` is already live at check.sh:464 — not lifted today, so latent, not absent. n=Q; ${!n} indirect expansion defeats text analysis outright. The guard now REFUSES the lift rather than passing it. Its contract is "does not miss a dependency"; where it cannot honour that it must say so, not shrug. SIX FALSE POSITIVES — the driver defines the name and the guard cried wolf. This direction matters too: a guard that raises false alarms gets edited away, and then it guards nothing. case x in a) FOO=1 ;; `)` added to the assignment delimiters if …; else FOO=1; fi `else` added ! FOO=1 `!` added mapfile -t FOO binds a name with no `=` at all readarray -t FOO likewise printf -v FOO "x" likewise The banner also over-claimed. It read as a completeness statement about LIFTING; it is a completeness statement about VARIABLES. A lifted payload also inherits functions, shell options, traps and a working directory, and this tool models none of them — loud failures under `set -e`, but the header now says so rather than implying otherwise. Verified: all nine classes behave correctly, a genuine missing variable is still caught by name, and the seven lifting self-tests pass in dalek plus the four fast ones in each ported fork. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 2 +- verification/lift-guard.sh | 77 ++++++++++++++++++++++++++++++------- 2 files changed, 64 insertions(+), 15 deletions(-) diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 9609167..948e487 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ a0fb8a1a99bc991870b493796bf7bfe09463413298d83c6ae73a269712f96b55 inventory-allo 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -b982bd1aa56b0648b10516985a2e0f6a9cacff4e1d19b441dadc5b35d69ec732 lift-guard.sh +2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py 855134c50bc2ce374eb935058f808264ea6de5ee328ef766956e7e54366f75fe MODEL-CORRESPONDENCE.txt 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh index fa13632..0ef0a9c 100755 --- a/verification/lift-guard.sh +++ b/verification/lift-guard.sh @@ -1,7 +1,16 @@ #!/usr/bin/env bash # lift-guard.sh [] # -# Every variable the LIFTED PAYLOAD reads must be one the DRIVER defines. +# Every VARIABLE the LIFTED PAYLOAD reads must be one the DRIVER defines. +# +# VARIABLES ONLY — and the emphasis is a round-8 correction (Claude, N1). A +# lifted payload also inherits FUNCTIONS, shell options, traps and a working +# directory from the script it was cut out of. This tool models none of those. +# A lifted phase calling a function defined in a neighbouring phase fails with +# `command not found`, loud under `set -e`, which is why it is not urgent; but +# the banner used to read as a completeness claim about lifting and it is a +# completeness claim about variables. +# # Prints the offending names and exits 1 if any are missing. # # ─────────────────────────────────────────────────────────────────────────── @@ -42,12 +51,16 @@ # grows a new dependency fails AT LIFT TIME, naming it, instead of dying # mid-run or — worse — passing for the wrong reason. # -# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser: it -# cannot see indirect expansion, `eval`, or a name built at runtime. It is a -# tripwire on the failure mode that actually occurred twice, not a proof of -# closure. Its answer is advisory in one direction only — it can miss a -# dependency, it does not invent one, and every name it reports is a name the -# payload genuinely mentions and the driver genuinely does not set. +# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser. It +# still cannot see a name built at runtime or passed through `eval`, and it +# models variables only — not functions, shell options, traps or the working +# directory a lifted phase also inherits. It is a tripwire on failure modes +# that actually occurred, not a proof of closure. +# +# Where it CANNOT bound the reads it refuses rather than staying silent: +# indirect expansion (`${!name}`) is detected and fails the lift. That is the +# round-8 correction — a guard whose contract is "does not miss a dependency" +# must say so when it cannot honour it, instead of shrugging. # ─────────────────────────────────────────────────────────────────────────── set -euo pipefail @@ -68,14 +81,33 @@ driver = open(sys.argv[2]).read() # comment costs one lifted definition, a name missed costs a broken self-test. reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload)) +# ARITHMETIC CONTEXTS READ NAMES WITHOUT A `$`. Round-8 review (Claude, N1): +# echo $((X + 1)) reads X +# (( Y > 0 )) && ... reads Y +# and the pattern above cannot see either, because the character after `$` is +# `(`. This is the guard's own failure mode — a phase growing a dependency the +# guard is blind to — and `if [ $((inm + ins)) -eq 0 ]` is already live in +# check.sh's Phase 1b. Not lifted today, which made it latent, not absent. +for expr in (re.findall(r'\$\(\((.*?)\)\)', payload, re.S) + + re.findall(r'(?