From a5ff873d3c7dc48169bd73738aff565169433546 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 21:03:35 +0200 Subject: [PATCH] lift-guard: eleven more classes, two of them regressions I introduced MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-9 review (Claude, N1). The brief said "assume there are more"; there were eleven, and two were introduced by the round-8 fix itself. INTRODUCED BY THE ARITHMETIC TOKENISATION — the round-8 fix for a false NEGATIVE created two false POSITIVES. The interior of `$(( ))` was tokenised with `[A-Za-z_][A-Za-z0-9_]*`, which starts matching at the letter-bearing tail of a numeric literal: echo $((0x1F)) -> FATAL: reads x1F echo $((1e3)) -> FATAL: reads e3 Now anchored so a match cannot begin after a digit or word character. INTRODUCED BY THE INDIRECT-EXPANSION REFUSAL, and this is the one that matters. `${!...}` has three meanings and `re.search(r'\$\{!')` cannot tell them apart: ${!name} indirect expansion — genuinely unanalysable ${!arr[@]} ${!arr[*]} array KEY expansion — ordinary ${!prefix*} ${!prefix@} variable-NAME listing — ordinary A refusal is the most expensive verdict this tool has — it hard-fails the lift — and it was firing on two ordinary constructs with a diagnostic naming a feature they do not use. The reviewer found it LIVE: ltl-accumulator check.sh:274 is `for cert in "${!CONES[@]}"`, so the day lift-guard is ported there, any lift covering that line would have refused. The four forks carry five arrays each, so it was one ordinary edit away from firing there too. Now matched only for genuine `${!name}`. SEVEN MORE BINDING FORMS the driver uses and the guard demanded anyway: let FOO=1 · (( FOO = 1 )) · BAR+=b · FOO[0]=x for (( i=0; i<3; i++ )) · select FOO in · getopts "o" FOO Arithmetic contexts bind as well as read, so `(( i++ ))` and the C-style `for` now contribute to assigns — without that, the reads-extraction added by the round-8 fix demanded the very names those expressions assign. Verified: all eleven silent, genuine `${!n}` still refuses, `$((X+1))` and `((Y>0))` still caught by name, the whole round-8 matrix unchanged, a genuine missing variable still fails, and the four lifting self-tests green in all four forks. The reviewer also discarded one candidate rather than report it — `i=0; (( i++ ))` looks like a demand but is silent under driver ⊇ payload, which is how the self-tests invoke it. That restraint is worth recording: a guard edited twice for false alarms should not be handed a false alarm by its reviewer. Co-Authored-By: Claude Opus 4.8 --- verification/HARNESS.sha256 | 2 +- verification/lift-guard.sh | 39 +++++++++++++++++++++++++++++++++++-- 2 files changed, 38 insertions(+), 3 deletions(-) diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256 index 8318f00..f5ffeaf 100644 --- a/verification/HARNESS.sha256 +++ b/verification/HARNESS.sha256 @@ -8,7 +8,7 @@ a0082f3f5cad2feb8527edcb6efc50c211855eccffade29690d90bc78be8a945 inventory-allo 80cdd232c9a0f3078b2b712957e34797add5421b51bd695a151bf64a7855687a inventory-allowlist.txt 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard -2b78361105984aa8e859758849a0886b5b768766fe9bb39dd04aa8ee24d38b6c lift-guard.sh +cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh 1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py cf86c955dd5b637bc9d673c4222684979f507a4e11e488ab514e654c49f4e569 MODEL-CORRESPONDENCE.txt 34c102ca7a38719ef8890b8dedd3f07c3f92e10ae4a1ce2c47a7db4d53523354 Proofs/Audit.lean diff --git a/verification/lift-guard.sh b/verification/lift-guard.sh index 0ef0a9c..c670242 100755 --- a/verification/lift-guard.sh +++ b/verification/lift-guard.sh @@ -90,7 +90,13 @@ reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload)) # 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'(?