test/sabotage-f4a.sh

1#!/bin/sh

2# sabotage-f4a.sh -- prove that `test/gate-f4a.sh` can go RED.

3#

4# A gate reported only green has been shown to be quiet, not to work. Every leg

5# below breaks the PRODUCT -- source under `src/`, not the gate's own assertions

6# -- rebuilds, and requires the named arm to fail. A leg that stays green is a

7# finding about the gate, and this script says so in those words rather than

8# exiting 0.

9#

10# WHY THE PRODUCT LAYER

11#

12# Breaking an assertion only proves the assertion is wired to something.

13# Breaking the PRODUCT proves the gate executes the product rather than a mirror

14# of itself. Every leg here plants a defect a reasonable person could actually

15# ship; two are the plan's own named sabotages for this phase.

16#

17# ONE LEG IS INVERTED, AND IT IS THE MOST INFORMATIVE ONE

18#

19# Leg 3 plants a defect in SHARED row construction and requires arm 1 to stay

20# GREEN while arm 2 goes RED. The convergence check compares a rebuild against

21# an incremental run, and both paths call the same code, so a defect in that

22# shared code is invisible to it BY CONSTRUCTION. That is a real limit of the

23# phase's central property and it is better measured and disclosed than left for

24# a reviewer to find. The leg exists to show the limit AND to show which arm

25# covers the gap.

26#

27# RESTORE IS VERIFIED BY HASH, not by `git checkout` reporting success.

29set -u

30repo_dir=$(cd "$(dirname "$0")/.." && pwd)

31cd "$repo_dir" || exit 1

33sigil="${SIGIL:-sigil}"

34redirects="$repo_dir/dev-redirects.sgl"

35export SIGIL_REDIRECTS="$redirects"

37work=$(mktemp -d /tmp/sabotage-f4a.XXXXXX) || { echo "SETUP-FAILED: no temp dir"; exit 3; }

38# Baselines live OUTSIDE $work: the EXIT trap deletes $work, and on an interrupt

39# the restore verification would otherwise read empty baselines and report a

40# false alarm against a tree that is perfectly clean.

41base=$(mktemp -d /tmp/sabotage-f4a-base.XXXXXX) || { echo "SETUP-FAILED: no baseline dir"; exit 3; }

43TOUCHED="src/folio/graph.sgl test/gate-f4a.sh"

45for f in $TOUCHED; do

46 if ! git diff --quiet -- "$f" 2>/dev/null; then

47 echo "SETUP-FAILED: $f has uncommitted changes. This suite restores with \`git checkout --\`" >&2

48 echo " and would DESTROY them. Commit or set them aside first." >&2

49 exit 3

50 fi

51 sha256sum "$f" | cut -d' ' -f1 > "$base/$(echo "$f" | tr / _).base"

52done

54restore_all () { for f in $TOUCHED; do git checkout -- "$f" 2>/dev/null; done; }

56# The trap cleans up and says NOTHING about exit status. (sabotage-f2b.sh

57# records why at length: a cleanup that exits its own status turns a Ctrl-C into

58# a reported success.)

59cleanup () {

60 restore_all

61 "$sigil" build --redirects "$redirects" >/dev/null 2>&1

62 rm -rf "$work" "$base"

63}

64trap cleanup EXIT INT TERM

66legs=0

67bad=0

69echo "=========================================================================="

70echo "sabotage-f4a: can gate-f4a.sh go red?"

71echo "=========================================================================="

72echo "compiler : $("$sigil" --version 2>&1 | sed 's/\x1b\[[0-9;]*m//g' | tail -1)"

73echo "SIGIL_REDIRECTS : $redirects"

74echo "subject : $TOUCHED"

75echo

77# THE BASELINE MUST BE GREEN BEFORE ANY LEG RUNS.

78#

79# Every leg below reads a RED as evidence that the arm detects the plant. If

80# the arm were already red on the clean tree, every leg would score as a success

81# while proving nothing at all.

82echo "baseline: running the full gate on the clean tree..."

83if ! sh test/gate-f4a.sh > "$work/baseline.log" 2>&1; then

84 echo "SETUP-FAILED: gate-f4a.sh is RED on the CLEAN tree. Every leg below would" >&2

85 echo " score a red it did not cause. Fix the gate or the product first." >&2

86 grep 'GATE-F4A' "$work/baseline.log" | head -10 >&2

87 exit 3

88fi

89# THE DENOMINATOR MUST MATCH THE ARMS THAT ACTUALLY RAN.

90#

91# This line used to be `grep -c 'OK$'`, which counts LINES ENDING IN OK -- not

92# arms. It read 10 for most of this suite's life and silently became 11 when

93# arm 1 gained a control line ending in the same two letters. No verdict was

94# affected, but a denominator that drifts without an arm being added is how a

95# suite starts certifying more than it runs, and "count it more carefully"

96# does not catch the next drift. So the count is now CHECKED against the arms

97# the gate announced, and disagreement is fatal.

98passed=$(grep -cE '^arm [0-9]+ OK$' "$work/baseline.log")

99declared=$(grep -c '^--- arm ' "$work/baseline.log")

100if [ "$passed" -ne "$declared" ]; then

101 echo "SETUP-FAILED: the baseline reported $passed arms OK but $declared arms ran." >&2

102 echo " This suite does not know what it is certifying. Fix the count first." >&2

103 exit 3

104fi

105echo "baseline: GREEN -- $passed of $declared arms passed"

106echo

107

108# $1 = label, $2 = arms that must go RED, $3 = arms that must stay GREEN ("" for none),

109# $4 = file, $5 = sed expression

110leg () {

111 label=$1; red_arms=$2; green_arms=$3; file=$4; expr=$5

112 legs=$((legs + 1))

113 echo

114 echo "=========================================================================="

115 echo "LEG $legs: $label"

116 echo " planting in $file"

117 echo " arms that MUST go red : [$red_arms]"

118 [ -n "$green_arms" ] && echo " arms that MUST stay green: [$green_arms]"

119 echo "=========================================================================="

120

121 before=$(sha256sum "$file" | cut -d' ' -f1)

122 sed -i "$expr" "$file"

123 after=$(sha256sum "$file" | cut -d' ' -f1)

124

125 # THE PLANT MUST HAVE LANDED. A sed that matched nothing leaves the file

126 # untouched, the gate then passes for the honest reason, and the leg would

127 # score as "the gate did not catch it" -- convicting a correct gate. This is

128 # the single most important check in the file.

129 if [ "$before" = "$after" ]; then

130 echo "LEG $legs INCONCLUSIVE: the plant did not change $file (the sed matched nothing)."

131 echo " This says NOTHING about the gate. Fix the sed expression."

132 bad=$((bad + 1))

133 git checkout -- "$file" 2>/dev/null

134 return

135 fi

136

137 if ! "$sigil" build --redirects "$redirects" > "$work/build.log" 2>&1; then

138 echo "LEG $legs RED (build): the sabotaged tree does not compile, so the gate cannot run against it."

139 echo " Weaker than an assertion red -- it proves the build catches this, not that the gate discriminates."

140 git checkout -- "$file" 2>/dev/null

141 "$sigil" build --redirects "$redirects" >/dev/null 2>&1

142 return

143 fi

144

145 F4A_NO_BUILD=1 sh test/gate-f4a.sh $red_arms > "$work/gate.log" 2>&1

146 rc=$?

147 if [ "$rc" -eq 0 ]; then

148 echo "LEG $legs STAYED GREEN -- THIS IS A GATE DEFECT, NOT A PASS."

149 echo " The product was broken as described and arm(s) [$red_arms] did not notice."

150 grep -E '^(arm|GATE| )' "$work/gate.log" | tail -8

151 bad=$((bad + 1))

152 elif [ "$rc" -eq 3 ]; then

153 # SETUP-FAILED IS NOT A RED. A gate that could not establish its subject has

154 # said nothing about the product, so scoring exit 3 as a detection would be

155 # scoring the gate's inability to run as evidence that it detects defects.

156 echo "LEG $legs INCONCLUSIVE: the gate exited 3 (SETUP-FAILED) -- it could not establish its"

157 echo " subject, so this says NOTHING about whether the arm detects the planted defect."

158 grep 'SETUP-FAILED' "$work/gate.log" | head -3 | sed 's/^/ /'

159 bad=$((bad + 1))

160 else

161 echo "LEG $legs RED as required (gate exit $rc). NAMED SIGNATURE:"

162 grep 'GATE-F4A FAIL' "$work/gate.log" | head -4 | sed 's/^/ /'

163 fi

164

165 if [ -n "$green_arms" ]; then

166 F4A_NO_BUILD=1 sh test/gate-f4a.sh $green_arms > "$work/gate-green.log" 2>&1

167 grc=$?

168 if [ "$grc" -eq 0 ]; then

169 echo " and arm(s) [$green_arms] stayed GREEN as required."

170 else

171 echo " BUT arm(s) [$green_arms] went RED, which this leg predicted they would NOT."

172 echo " The prediction was wrong; read that as a finding about the leg, not a pass."

173 grep 'GATE-F4A FAIL' "$work/gate-green.log" | head -3 | sed 's/^/ /'

174 bad=$((bad + 1))

175 fi

176 fi

177

178 git checkout -- "$file" 2>/dev/null

179 "$sigil" build --redirects "$redirects" >/dev/null 2>&1

180}

181

182# ==========================================================================

183# LEG 1 -- THE PLAN'S FIRST NAMED SABOTAGE: an edge is wrong on incremental

184# update.

185#

186# `graph-index-document!` stops re-resolving after indexing. Edge resolution is

187# a WHOLE-GRAPH function -- whether a target is resolved, missing or ambiguous

188# depends on which other documents exist -- so an incremental run that skips it

189# freezes each edge's verdict at the moment its own file happened to be touched,

190# while a rebuild sees the finished set. Arm 1's `target-late` and

191# `target-removed` sequences are built for exactly this.

192#

193# THIS PLANT HAD TO BE RE-AIMED IN F4b, AND THE MISS IS WORTH RECORDING. The

194# leg used to patch `(resolve-edges! g)` inside this function. F4b replaced

195# that call with the scoped one, so the sed silently matched NOTHING and the

196# leg stopped testing anything at all -- while still printing as a leg.

197#

198# It was caught only by the "the plant must have landed" hash check, which is

199# the check this file calls its most important line and which had never fired

200# before. A sabotage leg is code that must keep tracking the code it attacks;

201# refactoring the product disarms the instrument aimed at it, quietly, and a

202# suite that trusted its own leg count would have reported eight greens over a

203# leg that no longer existed.

204# ==========================================================================

205leg "incremental update does not re-resolve edges (the plan's 'omit one edge' leg)" \

206 "1" "" \

207 "src/folio/graph.sgl" \

208

    '/define (graph-index-document! g path)/,/^$/ s|(resolve-edges-scoped! g (cons doc-uid doomed) (car acc) (cdr acc))|#t ;; SABOTAGE|'

209

210# ==========================================================================

211# LEG 2 -- a re-index LEAKS the previous version's edges.

212#

213# `delete-document-rows!` stops deleting edges, so re-indexing a document adds

214# its edges again on top of the old ones. The shape a partial cache

215# invalidation leaves, and it grows silently.

216# ==========================================================================

217leg "re-indexing leaves the previous edges behind" \

218 "1" "" \

219 "src/folio/graph.sgl" \

220 's|(run! db "DELETE FROM edges WHERE doc_uid = ?" doc-uid)|(run! db "SELECT 1") ;; SABOTAGE|'

221

222# ==========================================================================

223# LEG 3 -- INVERTED, AND DELIBERATELY SO.

224#

225# One mention edge is dropped in SHARED row construction, so the rebuild and the

226# incremental path lose it identically. Arm 1 must stay GREEN -- the

227# convergence property is blind to a defect both of its arms share, by

228# construction -- and arm 2 must go RED.

229#

230# This is the leg that says what the phase's central property does NOT cover.

231# ==========================================================================

232leg "a mention is dropped in SHARED construction (convergence is blind; backlinks are not)" \

233 "2" "1" \

234 "src/folio/graph.sgl" \

235

    's|(let loop ((names (extract-crosslinks source)) (skipped 0))|(let loop ((names (let ((ns (extract-crosslinks source))) (if (pair? ns) (cdr ns) ns))) (skipped 0)) ;; SABOTAGE|'

236

237# ==========================================================================

238# LEG 4 -- THE PLAN'S SECOND NAMED SABOTAGE: key identity by path.

239#

240# `graph-doc-uid` takes the path into the key. Everything still works inside

241# one mount; the move arm is what notices, which is the whole reason `path` is

242# excluded from the convergence relation.

243# ==========================================================================

244leg "document identity is keyed by path (the plan's 'key identity by path' leg)" \

245 "6" "" \

246 "src/folio/graph.sgl" \

247

    's|(doc-uid (graph-doc-uid (folio-graph-workspace g) slug fmt))|(doc-uid (graph-doc-uid (folio-graph-workspace g) path fmt)) ;; SABOTAGE|'

248

249# ==========================================================================

250# LEG 5 -- unknown edge kinds are admitted to the built-in invariants.

251#

252# `kind_known` is set to 1 unconditionally. The plan requires unknown kinds to

253# be stored AND excluded; this keeps the storing and drops the excluding, which

254# is the version that looks right in a schema dump.

255# ==========================================================================

256leg "every edge kind is treated as built-in" \

257 "8 2" "" \

258 "src/folio/graph.sgl" \

259 's|(if (graph-edge-kind-known? kind-sym) 1 0)|1 ;; SABOTAGE|'

260

261# ==========================================================================

262# LEG 6 -- the cycle detector stops folding `blocks`.

263#

264# It still detects cycles; it just cannot see one spelled from the other end.

265# The corpus's only cycle is closed by a `blocks` edge.

266#

267# WHAT ACTUALLY REDDENS, corrected after reading the signature rather than

268# predicting it. With `from` forced to the source, each `blocks` edge becomes a

269# SELF-LOOP, and self-loops are cycles -- so `CYCLE_COUNT` stays 1 and arm 3's

270# count assertion passes. The red comes from the RING assertion:

271#

272# arm3 FLOOR: the reported cycle is not alpha->beta->gamma->alpha:

273# 'ops::topics/alpha::sgd# -> ops::topics/alpha::sgd#'

274#

275# That is worth stating because the obvious reading -- "the count drops" -- is

276# wrong, and an arm that only counted cycles would have stayed GREEN through

277# this leg. The count is not the discriminator; the SHAPE is. Same lesson as

278# arm 4's reversed supersession: a shape check is not a direction check, and

279# here a count check is not a shape check. Traced by an adversarial review and

280# then confirmed by this leg's own signature.

281# ==========================================================================

282leg "the dependency relation ignores 'blocks'" \

283 "3" "" \

284 "src/folio/graph.sgl" \

285 's|"blocks") d s))|"blocks") s s)) ;; SABOTAGE|'

286

287# ==========================================================================

288# LEG 7 -- ambiguous is reported as missing.

289#

290# The taxonomy's shape 17, planted deliberately: a lookup that answers the same

291# thing for "not there" and "there twice". Downstream this is how a duplicated

292# id gets treated as an absent one and a second gets minted.

293# ==========================================================================

294leg "an ambiguous target is reported as missing" \

295 "5" "" \

296 "src/folio/graph.sgl" \

297 's|((pair? (cdr docs)) (list "" "ambiguous"))|((pair? (cdr docs)) (list "" "missing")) ;; SABOTAGE|'

298

299# ==========================================================================

300# LEG 8 -- the schema probe always says healthy.

301#

302# A guard that cannot fail. Recovery becomes unreachable and a damaged database

303# is read with today's queries against whatever is in the file.

304# ==========================================================================

305leg "the schema probe always reports healthy" \

306 "7" "" \

307 "src/folio/graph.sgl" \

308 's|(define (probe-schema db)$|(define (probe-schema db) #t) ;; SABOTAGE\n (define (probe-schema-unused db)|'

309# ==========================================================================

310# LEG 9 -- F4b: THE SCOPE IS TOO NARROW. A collision forms against a

311# document nobody touched.

312#

313# `merge-snapshot` stops contributing the document's SLUG to the affected set,

314# so the scoped resolver still re-resolves edges by doc_uid and by node id but

315# never by slug. Edges pointing AT a document whose slug just appeared,

316# vanished or became contested keep the verdict they had before -- and those

317# edges live in OTHER FILES, which the incremental pass never opened.

318#

319# This is the defect the whole phase risks: scoping is an argument that the

320# unvisited rows could not have changed, and this plant makes that argument

321# false while leaving every visited row correct. A reviewer reading only the

322# touched document sees nothing wrong.

323# ==========================================================================

324leg "the affected set omits the changed slug (a collision forms against an untouched document)" \

325 "1" "" \

326 "src/folio/graph.sgl" \

327 's|(let ((slugs (add-unique (snapshot-slug snap) slugs)))|(let ((slugs slugs)) ;; SABOTAGE|'

328

329# ==========================================================================

330# LEG 10 -- THE SAME DEFECT, WITH THE ORACLE SCOPED TOO.

331#

332# THIS LEG PASSES WHEN THE GATE GOES GREEN, and that is not a contradiction:

333# the finding IS the green.

334#

335# Leg 9 plants a real scoping defect and arm 1 catches it. This leg plants THE

336# SAME defect -- byte for byte, the same sed -- and additionally narrows the

337# ORACLE so it no longer compares edge VERDICTS, only the declared targets.

338# Nothing about the product's brokenness changes between the two legs. The only

339# variable is whether the thing the incremental result is measured against still

340# looks at the whole corpus.

341#

342# It goes green. So arm 1's power to detect a scoping defect is not a property

343# of arm 1: it is a property of the REBUILD BEING UNSCOPED. The asymmetry is

344# the instrument, and this leg is what makes that sentence a measurement instead

345# of a slogan.

346#

347# I expected arm 1's existing floors to catch a CRUDE version of this and wrote

348# that down before checking. They do not. Dropping EDGE rows from the dump

349# outright leaves 469 of 593 lines -- still well past the "at least 100 lines"

350# control and nowhere near the empty-dump floor -- and all eleven sequences then

351# report CONVERGED. MEASURED, not reasoned: the first draft of this comment

352# asserted the opposite, and it was wrong in the flattering direction.

353#

354# So the finding is broader than this leg needs. Arm 1's controls check that the

355# dump is LONG and that diff can see a one-line change. NOTHING checks that the

356# relation still COVERS edge verdicts. An oracle can be quietly narrowed and

357# every control keeps passing. The truncation used below is the subtle version

358# -- it preserves the line count exactly -- but the crude version works just as

359# well, and that is the part worth being uncomfortable about.

360# ==========================================================================

361leg_oracle_scoped () {

362 legs=$((legs + 1))

363 echo

364 echo "=========================================================================="

365 echo "LEG $legs: the same scoping defect, with the ORACLE scoped as well"

366 echo " planting in src/folio/graph.sgl AND test/gate-f4a.sh"

367 echo " EXPECTED OUTCOME: arm 1 GREEN -- and the green is the finding"

368 echo "=========================================================================="

369

370 gb=$(sha256sum src/folio/graph.sgl | cut -d' ' -f1)

371 ob=$(sha256sum test/gate-f4a.sh | cut -d' ' -f1)

372

373 # (a) the product defect -- identical to leg 9

374

  sed -i 's|(let ((slugs (add-unique (snapshot-slug snap) slugs)))|(let ((slugs slugs)) ;; SABOTAGE|' src/folio/graph.sgl

375 # (b) the oracle defect -- EDGE lines truncated to 9 fields, dropping the

376 # resolved-target uid and the verdict. Line COUNT is untouched.

377

  sed -i "s|cut -f2- > \"\$2\"|cut -f2- \| awk -F'\\\\t' -v OFS='\\\\t' '\$1==\"EDGE\"{NF=9}1' > \"\$2\"|" test/gate-f4a.sh

378

379 ga=$(sha256sum src/folio/graph.sgl | cut -d' ' -f1)

380 oa=$(sha256sum test/gate-f4a.sh | cut -d' ' -f1)

381

382 # BOTH plants must have landed. If the oracle plant silently missed, this leg

383 # degenerates into leg 9 and would report "green is the finding" about a gate

384 # that was never contaminated -- which would be a lie in the flattering

385 # direction. If the product plant missed, the green is just a correct gate

386 # over correct code.

387 if [ "$gb" = "$ga" ]; then

388 echo "LEG $legs INCONCLUSIVE: the PRODUCT plant did not land; a green here would mean nothing."

389 bad=$((bad + 1)); restore_all; return

390 fi

391 if [ "$ob" = "$oa" ]; then

392 echo "LEG $legs INCONCLUSIVE: the ORACLE plant did not land; this is leg 9 again, not a new leg."

393 bad=$((bad + 1)); restore_all; return

394 fi

395 echo " both plants landed (graph.sgl and gate-f4a.sh hashes both moved)"

396

397 if ! "$sigil" build --redirects "$redirects" > "$work/build.log" 2>&1; then

398 echo "LEG $legs INCONCLUSIVE: the sabotaged tree does not compile."

399 bad=$((bad + 1)); restore_all

400 "$sigil" build --redirects "$redirects" >/dev/null 2>&1

401 return

402 fi

403

404 F4A_NO_BUILD=1 sh test/gate-f4a.sh 1 > "$work/gate-oracle.log" 2>&1

405 rc=$?

406 if [ "$rc" -eq 0 ]; then

407 echo "LEG $legs GREEN -- AND THE GREEN IS THE FINDING."

408 echo " Leg 9 proved arm 1 catches this exact defect. Here the defect is UNCHANGED"

409 echo " and the only edit is that the oracle stopped comparing edge verdicts."

410 echo " Arm 1 now certifies a corpus whose cross-document edges are stale."

411 grep -E 'control 1a|CONVERGED' "$work/gate-oracle.log" | head -4 | sed 's/^/ /'

412 echo " Note the controls still pass: the dump is full-length and the comparison"

413 echo " still sees a one-line perturbation. A healthy-looking oracle, measuring less."

414 elif [ "$rc" -eq 3 ]; then

415 echo "LEG $legs INCONCLUSIVE: gate exited 3 (SETUP-FAILED); it never ran."

416 bad=$((bad + 1))

417 else

418 echo "LEG $legs WENT RED, WHICH THIS LEG PREDICTED IT WOULD NOT."

419 echo " Read that as a finding about the leg: the contamination did not actually"

420 echo " blind arm 1, so this leg does not establish what it claims."

421 grep 'GATE-F4A FAIL' "$work/gate-oracle.log" | head -4 | sed 's/^/ /'

422 bad=$((bad + 1))

423 fi

424

425 restore_all

426 "$sigil" build --redirects "$redirects" >/dev/null 2>&1

427}

428leg_oracle_scoped

429

430

431# ==========================================================================

432echo

433echo "=========================================================================="

434echo "RESTORE VERIFICATION"

435echo "=========================================================================="

436restore_all

437"$sigil" build --redirects "$redirects" >/dev/null 2>&1

438notrestored=0

439for f in $TOUCHED; do

440 want=$(cat "$base/$(echo "$f" | tr / _).base")

441 have=$(sha256sum "$f" | cut -d' ' -f1)

442 if [ "$want" != "$have" ]; then

443 echo "NOT RESTORED: $f ($have != $want)"

444 notrestored=$((notrestored + 1))

445 fi

446done

447[ "$notrestored" -eq 0 ] && echo "all $(echo $TOUCHED | wc -w) touched file(s) restored, verified by hash"

448

449echo

450echo "=========================================================================="

451echo "$legs legs run; $bad inconclusive or wrongly green; $notrestored file(s) not restored"

452if [ "$bad" -eq 0 ] && [ "$notrestored" -eq 0 ]; then

453 echo "SABOTAGE-F4A: every leg behaved as predicted."

454 exit 0

455else

456 echo "SABOTAGE-F4A: FINDINGS ABOVE. Read them as statements about the GATE."

457 exit 1

458fi