mirror of
https://github.com/saymrwulf/anza-ed25519-verified.git
synced 2026-09-03 20:13:46 +00:00
mrwulf
a5ff873d3c
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 <noreply@anthropic.com>
196 lines
11 KiB
Bash
Executable file
196 lines
11 KiB
Bash
Executable file
#!/usr/bin/env bash
|
|
# lift-guard.sh <payload> <driver> [<phase-label>]
|
|
#
|
|
# 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.
|
|
#
|
|
# ───────────────────────────────────────────────────────────────────────────
|
|
# WHY THIS EXISTS — 2026-08-02
|
|
#
|
|
# Five of this repository's self-tests work by lifting one phase out of
|
|
# check.sh and running it standalone against a deliberately corrupted tree.
|
|
# That is the right design: the test then attacks the SHIPPING gate rather
|
|
# than a re-implementation of it. But a lifted phase is a fragment, and it
|
|
# reads variables its neighbours defined. Each self-test therefore carries a
|
|
# hand-written preamble supplying them.
|
|
#
|
|
# A hand-written preamble is a hand-kept list, and hand-kept lists drift. Twice
|
|
# in two days a phase grew a dependency and no preamble was told:
|
|
#
|
|
# · Phase 2c grew an accounting block reading $KERNLOG, a file Phase 2b
|
|
# creates. selftest-shapes.sh died on its first expansion under `set -u`.
|
|
# It could not pass on any fork from the moment that block was added.
|
|
#
|
|
# · Phase 2b changed from globbing Proofs/*.lean to reading the $PROOFS
|
|
# membership manifest — the spelling-versus-ownership fix ScalarPackSpec
|
|
# forced. selftest-axgate.sh's preamble was never told. Bash does NOT
|
|
# error on an unset array expansion under `set -u`; it expands to nothing,
|
|
# so `printf '"%s.olean", ' "${PROOFS[@]}"` silently produced
|
|
# expected := [".olean"]
|
|
# — one entry, empty name — and the gate's own fail-closed absence check
|
|
# rejected it. The baseline went red and both attack cases were then
|
|
# rejected for the WRONG REASON.
|
|
#
|
|
# Both failed loudly rather than passing vacuously, which is the only reason
|
|
# they were not false assurance. That is luck, not design: a missing variable
|
|
# that happens to make an ATTACK case die still looks like the attack being
|
|
# caught, and only the substring assertions in each `expect` helper stand
|
|
# between that and a green test measuring nothing.
|
|
#
|
|
# The fix for the CLASS is to stop maintaining the list by hand. This tool
|
|
# derives the requirement from the two artifacts themselves, so a phase that
|
|
# 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
|
|
# 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
|
|
|
|
PAYLOAD="${1:?usage: lift-guard.sh <payload> <driver> [phase-label]}"
|
|
DRIVER="${2:?usage: lift-guard.sh <payload> <driver> [phase-label]}"
|
|
LABEL="${3:-the lifted phase}"
|
|
|
|
for f in "$PAYLOAD" "$DRIVER"; do
|
|
[ -s "$f" ] || { echo "FATAL: lift-guard: '$f' is missing or empty."; exit 1; }
|
|
done
|
|
|
|
UNBOUND=$(python3 - "$PAYLOAD" "$DRIVER" <<'PYGUARD'
|
|
import re, sys
|
|
payload = open(sys.argv[1]).read()
|
|
driver = open(sys.argv[2]).read()
|
|
|
|
# What the payload READS. Deliberately over-approximates: a name mentioned in a
|
|
# 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'(?<!\$)\(\((.*?)\)\)', payload, re.S)):
|
|
# NOT PRECEDED BY A DIGIT OR WORD CHARACTER. Round-9 review (Claude, N1):
|
|
# `$((0x1F))` was read as a variable `x1F`, and `$((1e3))` as `e3`, because
|
|
# the pattern happily starts matching at the letter-bearing tail of a
|
|
# numeric literal. Two false alarms introduced by the round-8 fix for a
|
|
# false NEGATIVE — the guard was made to see more and started seeing things
|
|
# that are not there, which is the failure mode that gets a guard deleted.
|
|
for tok in re.findall(r'(?<![0-9A-Za-z_])[A-Za-z_][A-Za-z0-9_]*', expr):
|
|
reads.add(tok)
|
|
|
|
# What the DRIVER defines, in every form these scripts actually use.
|
|
# `TIMEOUT=$T; CORES="$C"` is one line with two assignments, and a
|
|
# start-anchored pattern sees only the first.
|
|
# An assignment may open a line or follow `;`, `&&`, `||`, `then`, `do`, `{`,
|
|
# and — round-8 review (Claude, N1) — `else`, a `case` branch's `)`, and `!`.
|
|
# Six false-positive classes were demonstrated. A guard that cries wolf gets
|
|
# edited away, so over-strictness here is not the safe direction.
|
|
assigns = set(re.findall(
|
|
r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
|
|
r'([A-Za-z_][A-Za-z0-9_]*)=', driver, re.M))
|
|
# `mapfile`/`readarray` and `printf -v` bind a name without an `=` at all.
|
|
assigns |= set(re.findall(
|
|
r'\b(?:mapfile|readarray)\b(?:\s+-[A-Za-z]\s*\S*)*\s+([A-Za-z_][A-Za-z0-9_]*)',
|
|
driver))
|
|
assigns |= set(re.findall(r'\bprintf\b[^\n]*?\s-v\s+([A-Za-z_][A-Za-z0-9_]*)', driver))
|
|
# SEVEN MORE BINDING FORMS — round-9 review (Claude, N1). Each was a false
|
|
# alarm: the driver binds the name and the guard demanded it anyway. Listed in
|
|
# the order reported, so the next reader can check the list against that report.
|
|
assigns |= set(re.findall(r'\blet\s+([A-Za-z_][A-Za-z0-9_]*)\s*=', driver))
|
|
assigns |= set(re.findall(r'\bselect\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver))
|
|
assigns |= set(re.findall(r'\bgetopts\b\s+\S+\s+([A-Za-z_][A-Za-z0-9_]*)', driver))
|
|
assigns |= set(re.findall(r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
|
|
r'([A-Za-z_][A-Za-z0-9_]*)\+=', driver, re.M)) # BAR+=b
|
|
assigns |= set(re.findall(r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
|
|
r'([A-Za-z_][A-Za-z0-9_]*)\[[^]]*\]=', driver, re.M)) # FOO[0]=x
|
|
# Arithmetic CONTEXTS BIND TOO — `(( FOO = 1 ))`, `(( i++ ))`, and the C-style
|
|
# `for (( i=0; i<3; i++ ))`. The reads-extraction above adds every identifier it
|
|
# finds inside `(( ))`, so without this the guard demands the very names those
|
|
# expressions assign.
|
|
for expr in (re.findall(r'\$\(\((.*?)\)\)', driver, re.S)
|
|
+ re.findall(r'(?<!\$)\(\((.*?)\)\)', driver, re.S)):
|
|
assigns |= set(re.findall(r'(?<![0-9A-Za-z_])([A-Za-z_][A-Za-z0-9_]*)\s*(?:=[^=]|\+\+|--)', expr))
|
|
assigns |= set(re.findall(r'\b(?:export|declare|local|readonly)\s+(?:-\w+\s+)*'
|
|
r'([A-Za-z_][A-Za-z0-9_]*)', driver))
|
|
assigns |= set(re.findall(r'\bfor\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver))
|
|
# `read` binds names too, and it is almost never at end of line: the shape that
|
|
# matters here is `while read -r n; do`. An end-anchored pattern misses it and
|
|
# the guard then demands a definition for a loop variable the payload binds
|
|
# itself — a false alarm, which is the one failure a guard cannot afford.
|
|
for m in re.finditer(r'\bread\b((?:\s+-\w+)*(?:\s+[A-Za-z_][A-Za-z0-9_]*)+)', driver):
|
|
assigns |= set(re.findall(r'[A-Za-z_][A-Za-z0-9_]*', m.group(1)))
|
|
|
|
# Names the driver INHERITS rather than defines: the shell's own, and the ones
|
|
# `source ~/aeneas-toolchain/env.sh` puts in the environment. Keep this list
|
|
# short and justified — every entry is a hole in the guard.
|
|
ENV = {'PWD', 'HOME', 'PATH', 'IFS', 'PIPESTATUS', 'BASH_SOURCE', 'FUNCNAME',
|
|
'LINENO', 'RANDOM', 'SECONDS', 'OSTYPE', 'HOSTNAME', 'USER', 'SHELL',
|
|
'TMPDIR', 'LC_ALL', 'LANG', 'BASH_REMATCH', 'REPLY', 'PS4',
|
|
'AENEAS_HOME', 'LEAN_PATH', 'LEAN_MEM_MB', 'LEAN_TIMEOUT',
|
|
'LEAN_MAX_CORES'}
|
|
|
|
# INDIRECT EXPANSION DEFEATS TEXT ANALYSIS, so say so instead of staying
|
|
# silent. `n=Q; echo "${!n}"` reads Q, and no amount of pattern-matching
|
|
# recovers that from the source. The guard's contract is that it does not miss
|
|
# a dependency; where it cannot honour that it must refuse, not shrug.
|
|
# `${!...}` HAS THREE MEANINGS IN BASH and only one of them is indirection:
|
|
# ${!name} indirect expansion — genuinely unanalysable
|
|
# ${!arr[@]} ${!arr[*]} array KEY expansion — ordinary, and LIVE at
|
|
# ltl-accumulator check.sh:274, `for cert in
|
|
# "${!CONES[@]}"`
|
|
# ${!prefix*} ${!prefix@} variable-NAME listing — ordinary
|
|
# Round-9 review (Claude, N1). The round-8 refusal tested for `${!` and could
|
|
# not tell them apart, so a legitimate construct would have hard-failed a lift
|
|
# with a diagnostic naming a feature it does not use. A refusal is the most
|
|
# expensive verdict this tool has; it must be reserved for the case it is
|
|
# actually about.
|
|
INDIRECT = re.compile(r'\$\{!\s*[A-Za-z_][A-Za-z0-9_]*\s*\}')
|
|
if INDIRECT.search(payload):
|
|
print('INDIRECT-EXPANSION')
|
|
else:
|
|
print(' '.join(sorted(n for n in reads - assigns - ENV if not n.isdigit())))
|
|
PYGUARD
|
|
)
|
|
|
|
if [ "$UNBOUND" = "INDIRECT-EXPANSION" ]; then
|
|
cat <<EOF
|
|
FATAL: $LABEL uses indirect expansion (\${!name}).
|
|
The set of variables it reads cannot be derived from its text, so this
|
|
guard cannot certify that the lift carries them. Rewrite the phase
|
|
without indirection, or lift it with a driver that is known-complete by
|
|
other means and say so in the self-test.
|
|
EOF
|
|
exit 1
|
|
fi
|
|
if [ -n "$UNBOUND" ]; then
|
|
cat <<EOF
|
|
FATAL: $LABEL reads variables this lift does not define: $UNBOUND
|
|
Either lift their definitions too — VERBATIM from check.sh, with a
|
|
sed range, so this test cannot drift away from the button's idea of
|
|
them — or end the lift range before the block that uses them.
|
|
Do NOT stub them: a stub makes the test measure something the button
|
|
never runs, which is how a self-test becomes decoration.
|
|
EOF
|
|
exit 1
|
|
fi
|