…production

The stand stopped being a live reproduction at ~16:49 when the S42 card's two
smoke runs reset the cluster, and the worklog kept claiming otherwise for
another hour. Caught only by re-checking the state before teardown rather than
trusting the note: the pool read back fresh.

No evidence lost — everything was captured hours earlier and the mechanism is
mechanised in TLA+ — but the claim was false while it was being repeated, so it
is corrected in place. Records the lesson: holding a stand as evidence has to be
enforced by a mechanism the cards honour, not by a line in a log.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…hour run

User decision: a 20-minute run first to tune the harness, verify every signal is
actually observed and fix what that shakes out, and only then the 4-hour run.
Written in that order deliberately — three harness surfaces were caught silently
under-reporting the product this week, and a long run that reports nothing costs
a day.

The task is concrete rather than aspirational because the gap is concrete: the
soak driver collects no ProfileEvents at all today, so the three signals added
on 2026-07-25 are invisible to it. It also pins stale_edge to the checkpoint's
detail fsck (the counter is detail-mode only) and requires failing closed when
the key is absent, since a missing key means the binary predates the class and
must not read as zero.

Defines stable as two consecutive green runs in which every signal was actually
observed at least once — a green run where a counter was never read is blind,
not stable.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…oundwork)

Task 11 of the publish-confirm plan, under the upstream authorization recorded
in the plan: the CAS parts-exchange portion only, localized as far as possible.

The footprint came out tighter than the constraint asked. `DataPartsExchange` is
purely additive — 59 lines forming one self-contained
`Service::resolveContentAddressedConfirm`, with zero lines removed and no
existing function modified. `processQuery` is deliberately untouched; its
three-line dispatch belongs to Task 13, and the receiver side to Task 14. The
header is in the diff only because the build runs -Weverything -Werror, where a
yet-uncalled function in an anonymous namespace is a -Wunused-function failure;
a private member declaration is not.

The CAS vocabulary crossing into generic code is one opaque enum and two
interface calls. Namespace derivation, ledger rules, token decoding and
lifecycle gating all stay behind `IContentAddressedExchange`, so nothing
CAS-specific reaches MergeTreeData or StorageReplicatedMergeTree.

`ownsNamespace` is the routing predicate, because a pool uuid is shared across
server roots and cannot by itself select the answering mount; it is I/O-free and
answers before startup, live, and after shutdown. The wire token reuses the
existing canonical renderer and gains its exact inverse next to it, parsed as
untrusted input — three decimal fields, no sign, whitespace or partial consume,
ordinal range-checked — with a note on the renderer that the pair is now
wire-load-bearing and must change together.

Rule 6 stays last and `No` is treated as "not proven", never as knowledge:
gate 0's No, gate 1's No and every Unknown reach the same caller outcome. The
enum's doc comment says so and states that any future code treating No as
authoritative must hoist rule 6 first — the carry-forward from Task 10 made
explicit where the next reader will be standing.

Gate: unit_tests_dbms 1356/1356 over 228 suites, and `ninja clickhouse` links
clean — the CA battery alone does not compile the exchange file.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…sk 12 dispatched

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

User instruction. Recorded in the plan rather than kept in conversation, and
placed before Task 21 for a stated reason: a soak is hours of machine time whose
failures are expensive to attribute, so it should run on reviewed code rather
than serve as the first reader.

Scope is the whole of Part B as one change. Each per-task subagent saw only its
own task, so nobody has yet read tasks 9-16 as a single protocol, and that seam
is where a composition defect would sit.

Carries the prompt discipline that made both of today's codex RCAs useful —
facts and artifacts, no hypothesis stated as fact — and lists what must be handed
over because it postdates the spec: the LIST-as-journal finding, the TLA+ config
that mechanises it together with the limit on how the passing main config may be
cited, and the No-vs-Unknown ordering that Tasks 13-16 could quietly break.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…hypothesis

Catch it by the tail first, because the diagnosis is not confirmed: a holey LIST
page was never directly observed, it survives by elimination and is mechanised
in TLA+, which shows the mechanism is sufficient rather than actual.

That qualification changes the design. A detector built for the LIST hypothesis
catches only a LIST hole and would stay silent — while manufacturing confidence
— if the record is instead lost in delta routing, the reducer or the run flush.
So the probes target the effect: the cursor advanced past a transaction that was
never applied. One probe for "the store lied", one for "we dropped it".

Also records why containment was rejected despite being the safe-looking choice,
that id gaps are legitimate and today's Task 18 deliberately creates them, and
the commitment that the real fix still lands before release.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

… 1361/1361

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…d thing

Task 12. The confirm protocol has to interpose between the receiver's `+1`
becoming durable and the promote, so the sender can be asked whether it still
holds the manifest. `publishEntries` did all three in one call, so the split
turns that window from something a caller could forget into a handle that owns
it. `publishEntries` is now prepare-then-promote, so no existing caller moved.

Both failure modes are made impossible rather than discouraged. Forgotten
terminal: the destructor is the guard — non-terminal at destruction logs and
best-effort aborts, noexcept — and the handle is move-only with the source left
terminal, so the duty transfers exactly once and move-assignment onto a live
handle discharges the overwritten one first. Double terminal: an explicit flag,
flipped only AFTER the underlying operation completes, because
`PartWriteTxn::abandon` is deliberately retryable after an append failure and a
premature flag would strand the cleanup.

The `abort`-appends-the-precommit-removal property is MUTATION-VERIFIED, not
asserted and hoped for: `abandon` was commented out, the test failed on exactly
that assertion, and the mutation was reverted. That matters here more than
usual — an abandoned precommit that leaves its `+1` behind is precisely the leak
class root-caused today, and today also produced three separate cases of a check
that passed because it was looking at nothing.

Adds a `livePrecommitsForTest` seam, since the plan requires asserting through
the ledger's precommit view and no accessor existed.

Records two plan defects found: Task 12's heading says `PreparedRelink` while its
own interface block says `PreparedPartWrite`, and the two are different layers —
the receiver's token and decoded entries belong to Task 14's exchange boundary,
not to a CAS-internal facade; and Task 12's file list names two files that belong
to Task 14, which were correctly left alone.

Gate: unit_tests_dbms 1361/1361 over 228 suites. Nothing under `src/Storages`.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

Q2 corrects the framing rather than picking an option: the problem is the
differing server uuid, not whether a tool may read without claiming, so the
answer is a force-claim at mount time and a real read-only mount is a separate
unimplemented task. The design note is superseded as a recommendation; its
verified facts stand. One factual concern is recorded for a single check before
coding — force-claiming against a genuinely live server takes ownership from it,
which is what the refusal exists to prevent.

Q3: stale_edge stays non-fatal, unconditionally.

Q4 redefines S42's green as a consistent state on disk and in memory, which
overrides the window-targeting soundness guard that is zero by construction
today. The generic-fault anti-vacuity guard survives; only the window-specific
targeting is dropped.

Q5: introspection now, in the shape the user specified — each GC phase emits its
own row in the GC log rather than more columns on the per-round row — with the
metric study deferred until after Part B and its soak, so the reproduction rig
is not built until real data can retarget it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…ing phase

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…sender side

Task 13. The sender can now answer "do you still hold exactly this manifest?"
and every relink offer carries the token that names what it offered.

Deliberately half-landed, in the safe direction: the server's advertised clamp
rises to 11, but the client still advertises 10 and the relink-offer gate is
still keyed on 10, so no receiver asks for a confirm and relink behaves exactly
as before. Raising the gate alone would silently disable relink outright, and
bumping the client alone would make the receiver claim it confirms when it does
not — so those two edits land together in Task 14, and a comment at the gate
says so.

A TOCTOU the plan did not anticipate: it assumed the sender could mint the token
from fields the manifest bytes already carry, but decoding a manifest in generic
code means CAS types there, and minting from a SECOND lookup lets a repoint
between the offer and the mint hand the receiver a token naming a manifest whose
entries it never adopted — and a Yes for that protects the wrong blobs. The
lookup now returns the bytes and the token from one resolution.

The wire is deliberately binary: only `yes` authorizes, while `No`, `Unknown`
and an absent cookie all read as `unproven`. Putting `no` on the wire as a
distinct value would invite a receiver to treat it as knowledge, and with rule 6
evaluated last it is not — a fence-lost mount answers `No`. The distinction is
logged where the gate that produced it can be named, never transmitted. Stated
deviation from the spec's literal yes/no/unknown, justified by the enum's own
contract.

Old peers: an old receiver ignores an unknown cookie by name; an old sender
offers relink with no token, and that absence is the capability signal Task 14
keys on, so a new receiver never confirms against one. Fail-closed both ways.

Token codec is strict in both directions — versioned tag, exact field count,
percent-encoded to the unreserved set because namespaces carry `/` and `@` and
the server root id is operator-supplied, with field and total length caps — and
the unparsable-token log prints only a length, never the raw peer text, since a
decoded token is the only form proven free of control characters.

Also removes a re-check the agent had first added: the manifest reader already
enforces it and throws, so the addition would only have converted a loud
corruption error into a silent byte fetch.

Footprint: one function on the sender side as authorized. Within `processQuery`
that is ~21 added lines across eight places, not the plan's "3-line dispatch" —
the confirm must run before the part-name validation, which a confirm request
has no part for, and the offer rename touches its call sites.

Gate: unit_tests_dbms 1363/1363, and `ninja clickhouse` links clean.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…e decisions

Design and 12-task plan for the option-C detector, per-phase GC log rows, S42's
verdict, and force-claim at mount. Three findings correct what I had recorded,
which is why they are called out here rather than buried:

The detector's cheap probe turns out to be free. A round ALREADY enumerates the
ref prefix twice and discards the first result, so comparing the two costs zero
extra backend calls, and an id present in one enumeration, absent from the
other, and below that other's own maximum for the namespace cannot be a
concurrent append — the per-namespace log is append-only and strictly
increasing. A disagreement takes the existing fold-abort path, which is stronger
than the "suppress destructive actions" I wrote: suppression alone still commits
the cursor advance, and that is the permanent half of the damage.

My "count intended-to-fold versus actually-applied and require equality" cannot
be implemented as literally written — at the intake both counts increment in the
same basic block, so the check is vacuous by construction. The same trap S42 fell
into. The plan implements the intent instead, separating an honest control-flow
assertion from the one probe that can actually see loss below the intake, and
labels the former as blind to the suspected defect rather than letting it look
like coverage.

S42's decision describes one guard; there are two rows keyed on the same
zero-by-construction signal, and the second is a `skipped` that outranks `pass`.
Implemented as stated, the card would read skipped, not green.

The CI scrape question is settled and the concern is void: it runs against a
STOPPED server, stated in the code's own comment and confirmed at the call site.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

The remedy was already written and had never once run. `dump_system_tables`
inserts `<readonly>true</readonly>` beside the content_addressed marker so
`clickhouse local` skips mountWritable and never claims server-root ownership —
but it patched config.xml, where that marker does not live, because the CA
storage policy is symlinked into config.d by tests/config/install.sh. sed matched
nothing, silently, and the scrape kept failing on ownership while appearing to be
handled.

Patches both paths, and makes the next no-op loud: if a CA disk is declared and
the marker is absent afterwards, the job prints a warning naming the consequence.
That is the point — a silent no-op is how this survived, and it is the same shape
as three other harness surfaces found today.

Verified by simulating the substitution against the two real config files, not by
reading the sed and believing it.

Also splits the operator-recovery case out to the backlog, since this removes its
CI justification: a server whose local uuid was regenerated still cannot mount its
own pool, and the two readings of "force a new uuid" differ sharply — overwriting
the owner locks the original server out permanently and needs to cover a second
durable object, while adopting the pool's existing uuid reaches the same outcome
with no identity damage and largely exists already. Not decided, not started.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

…ectory

Debris from .claude/tools/cppexpr.sh, which appends its scratch subdirectory to
src/CMakeLists.txt. The directory is untracked, so the line builds fine locally
and breaks cmake everywhere else. Unrelated to the running task; caught by
reading a status listing rather than skimming it.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012UJqPB1gNiKk5AKi91zZyY

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…al rebirth safety)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…rived (task-4 review I2)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ser direction

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…e, README index, narrative rescope)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

CasRefInstallSafetyDeathTest.DenyGuardStopsAnAllocation dispatched on
DEBUG_OR_SANITIZER_BUILD, but DENY_ALLOCATIONS_IN_SCOPE itself is gated
on MEMORY_TRACKER_DEBUG_CHECKS (MemoryTracker.h: defined only under
!NDEBUG). Sanitizer builds define NDEBUG, so there the guard compiles to
static_assert(true) and the death test "failed to die" on all three
sanitizer CI lanes — visible verbatim in the CI error output. (These
lanes only now reached this test at all: the earlier LOGICAL_ERROR
aborts in gtest_ca_wiring / gtest_cas_part_folder_access killed the
process before it, so each fix un-shadows the next tail failure.)

Gate the death test on MEMORY_TRACKER_DEBUG_CHECKS instead, and drop the
throw-only EXPECT_ANY_THROW branch as dead code: MEMORY_TRACKER_DEBUG_CHECKS
implies !NDEBUG implies DEBUG_OR_SANITIZER_BUILD, so whenever the guard
exists its LOGICAL_ERROR aborts — death is the only observable outcome
(the old comment claimed the opposite implication).

Verified: build_debug runs the death test (OK, guard fires); build_asan
compiles it out, remaining CasRefInstallSafety* 21 tests x5 repeats green.

Report: https://altinity-build-artifacts.s3.amazonaws.com/json.html?PR=2073&sha=07f8398acddff2c676aded5f804f122984845a4a&name_0=PR
PR: #2073

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GKmSZa7T87WbRGKkNkSXky

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…old-gen wedge retry / byte-compare sabotages)

Extends `CaCasMountCore` with the consumer side of the mount-fence generation,
per the v9 ref-chain design (`2026-07-27-cas-ref-chain-complete-cut-design.md`
§3 "Recovery ownership" and §9's r9-5): an operation captures the generation at
admission and must re-present it, with a recheck post-I/O immediately before
every publication. The module already owned the generation itself — the durable
writer epoch, its per-actor view and the fenced-pair set.

Three sabotages, each red before any green was run:

- `_sab_staleinstall` — `Install` drops the recheck, so an old recovery's
  result publishes after a self-remount. Reuses the module's own
  `GlobalSupersededWriterMakesNoMutation`.
- `_sab_wedgeretryoldgen` — a wedged lane's one bounded conditional create
  (INV-1's every-attempt rule) fires under the new generation unchecked,
  injecting a dead incarnation's bytes into the successor's live stream. Same
  invariant, independent route.
- `_sab_slotnocompare` — the `slot-occupy` `Occupied` resolution skips the byte
  comparison and acks the lane's own operation while someone else's bytes are
  at the key. This is the one place a new invariant was needed,
  `AckedOpsAreDurable`: nothing in the module recorded what a caller was TOLD,
  only what a writer did.

Also discharges two hand-offs from `CaRefTableSnapshotLogCore`, which cannot
express either: that acked-then-lost direction (it grants the writer perfect
knowledge of `writtenEver`), and INV-2's "`Occupied` with an `EpochSeal`
terminates the walk" branch reached by a concurrent recoverer — pinned by
`_witness_sealrejected`, whose first draft was satisfied by a degenerate
same-generation seal and had to require a strictly later one.

`RecoveryGenOn = FALSE` keeps the layer inert in every pre-existing config; all
twelve keep their colour with byte-identical state counts against a
same-machine baseline of the committed model. `run_mount.sh` becomes a
whole-suite runner asserting violation names, like `run_refcatalog.sh`.

`bash docs/superpowers/models/run_mount.sh` → 18/18 expectations met; the green
gate is exhaustive and stays green at `ADMISSIONS=5`. State counts, traces, the
measured bounds sweep and per-action coverage: `CaCasMountCore_RESULTS.md`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

RCA of the fence cascades on the CA-s3 sanitizer lanes (run for
07f8398, msan 2/3 lane): clickhouse-server logged 351 bursts of
'Connection refused' (e.code() = 111) to rustfs at localhost:11121
spread over the whole run — the service stayed up between bursts, so
this is fd/accept exhaustion, not a crash. rustfs was launched WITHOUT
the open-files-limit raise that start_azurite performs for exactly this
failure mode, while the server under parallel sanitizer load holds 10k+
active Disk-group S3 sessions. Most bursts were absorbed by the CAS
request retries (max_attempts=16 / 90s deadline); the one at ~02:00-02:01
outlived (a) in-flight writes' 90s budgets (Code 210 UNCERTAIN) and
(b) the mount-lease renewal confirm window (TTL 30s), so the mount fence
tripped (fail-closed by design) and every writing test failed with
Code 668/210 from 02:02:52 until remount completed ~02:05:00, with
straggler failures to ~02:10 — ~40 of the run's 66 test failures.

Also add rustfs.log to the uploaded artifacts: it was already written to
ci/tmp/rustfs.log but never uploaded (azurite/kafka/minio logs are),
which was exactly the missing evidence for this class of triage.

Report: https://altinity-build-artifacts.s3.amazonaws.com/json.html?PR=2073&sha=07f8398acddff2c676aded5f804f122984845a4a&name_0=PR
PR: #2073

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GKmSZa7T87WbRGKkNkSXky

…h grace)

Report: https://altinity-build-artifacts.s3.amazonaws.com/json.html?PR=2073&sha=07f8398acddff2c676aded5f804f122984845a4a&name_0=PR

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GKmSZa7T87WbRGKkNkSXky

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…mmitted strict-order constraint

Addresses the task-5 review (Spec pass, Quality needs-fixes).

Important 1 — the operation identity `<< actor, generation >>` aliased two
distinct operations admitted at the same generation, because `WedgeAdmit` is
re-enabled the moment a lane resolves. The reviewer showed the HONEST
configuration reaching a state where `mine` is true for a second operation
sitting on the first one's bytes, with `AckedOpsAreDurable` structurally unable
to see the phantom ack: both operations collapsed to one identity already in
`durable`, so the union was a no-op. The compare the round proved load-bearing
was therefore only its generation half; INV-1's same-generation half — "each
later caller's flush", about multiple callers within ONE incarnation — was not
modelled.

Fixed with a distinct op id per admission, drawn from the already-monotone
`admissions` counter: new `wedgeOp`, an `op` field on `slot` (`None` for a seal),
and `acked`/`durable` as sets of `<< actor, generation, op >>`. The invariant
text is unchanged — the model can now express the damage rather than the
assertion being weakened. `_sab_slotnocompare`'s shortest counterexample becomes
the same-generation case at depth 7, shorter than the cross-generation one it
used to find at 12, so the newly-modelled half is now the primary evidence; the
honest gate stays GREEN and acks no phantom on the reviewer's trace.

Important 2 — the five RED state-count rows were transcribed from a pre-final
revision and never refreshed; my own post-commit logs agreed with the reviewer,
not with the table. Round-1 tables are marked SUPERSEDED with pointers rather
than patched, since the configs they describe no longer exist in that form, and
every number in the fix-round section comes from the logs of the single
full-suite run that produced the verdict.

Also: the `mount = None \/ mount.epoch > 0` strict-order re-check is no longer
uncommitted prose — `StrictOrderMount` plus three `_sab_*_strictorder.cfg`
configs, all still RED on an `AllocEpoch`-first mount, which matters because BFS
finds the generation 0 -> 1 transition first and the product's strict order
never reaches a generation-0 mount. `_witness_ackhappened.cfg` pins
`AckedOpsAreDurable`'s non-vacuity instead of leaning on the coverage table.
`GlobalSupersededWriterMakesNoMutation`'s comment now states the authoritative
per-operation reading. `run_mount.sh` no longer reports FAIL if `rev6_observe`
improves to green under `SLOW=1`.

`bash docs/superpowers/models/run_mount.sh` → 22/22 expectations met; green gate
exhaustive at 82,299,033 / 15,658,147 and still green at `ADMISSIONS=5`
(231,519,697 / 43,330,107); all twelve pre-existing configs byte-identical.
Numbers, traces and coverage: `CaCasMountCore_RESULTS.md` {#fix-round-1}.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ark v9-bounds superseded

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…ges red)

Task 6, the phase-0 gate for the v9 ref-chain design
(`2026-07-27-cas-ref-chain-complete-cut-design.md`). Every runner re-run end to
end from a cleared `tmp/tlc-meta-*` state, sequentially:
**93/93 expectations met across 10 asserted batteries** — 66 configs in the five
models tasks 1-5 wrote or rewrote, plus 27 in the five older models whose
runners this task upgraded. `TLA PHASE: PASS`. Full table, spec-coverage map and
residuals: `docs/superpowers/models/2026-07-28-v9-phase-RESULTS.md`.

Audit of the six models the phase did NOT rewrite, for the premise v9 exists to
remove (a listing treated as complete). None needs rewriting:

- `CaDiskLifecycle` — nothing enumerates anywhere in the module; every
  transition is a point read or a local protocol step.
- `CaErasureProof` — an emptiness-`LIST` IS its subject (`ObsList`), but it
  models it as a hazard, splitting the sample so writers/GC/eraser interleave
  between the `LIST` and the qualification reads. Out of v9's scope (§11), and
  the promotion it gates was excised from the code by lifecycle v1. The premise
  that an empty full-prefix `LIST` verdict is truthful is recorded as a NAMED
  residual rather than left implicit.
- `CaGcAckFloorCore` / `CaGcAckFloorZombie` / `CaGcCondemnMarkerGate` — all
  three assume the fold cut sees everything landed by its instant (`GFold`
  consuming `landed`; `GBegin` latching `snapIndeg` from `refs`;
  `GCut`'s `folded' = (edge = "landed")`). v9 turns that assumption into a
  mechanism — arithmetic `cursor + 1`, a durable hold, the frontier proof — so
  `_sab_skipshard`'s undeclared skip becomes unrepresentable, not merely
  forbidden. Their subjects are orthogonal to discovery.
- `CaRelinkConfirmCore` — the one model that refuses the assumption. Per spec
  §9 `_sab_holeylist` stays as the permanent regression witness; its RESULTS
  gains the note that the fold-side flip lives in the pair
  `CaRefTableSnapshotLogCore_sab_scanistruth` (RED) +
  `CaRefDeltaIntakeCore_v9_hintomission` (GREEN) — neither is evidence alone.

The three audited colours cited were re-observed, not quoted from prose.

Fixes carried by this commit:

- `CaBuildRootPrecommit.tla:300` — `everDangle' = everDangle \/ (...)` parses as
  `(everDangle' = everDangle) \/ (...)`, leaving the ghost unassigned whenever
  the right disjunct is true. Parenthesised. Running the PRE-fix module showed
  the bug was latent, not active (BFS reaches the invariant violation first),
  but one exploration-order change from turning a required red into a harness
  `Error:` that the older runner conventions counted as the expected red. A scan
  of all 23 modules for both shapes of the pattern found exactly this one.
- Runner discipline. `run_disklifecycle.sh` and `run_erasureproof.sh` set
  `overall=1` on any nonzero TLC exit, so their own sabotages and witnesses made
  them FAIL on every run — permanently red suites nobody ran. `run_foldclamp.sh`
  and `run_refwcleanup.sh` accepted `Error:` (or a name-derived expectation) as
  the sabotage's red. All four now assert the NAME of the invariant or property
  each config must break, plus a `temporal <Prop>` kind for liveness reds, which
  TLC reports without a name. `CaBuildRootPrecommit` had no runner at all — its
  colours lived only in prose, which is how the parse bug survived — so
  `run_buildrootprecommit.sh` is new, with 8 named expectations.

The new discipline paid for itself immediately: `run_disklifecycle.sh` failed
its first run because the name pattern `[A-Za-z_]+` cannot match
`I1ForgetTerminal`. The old runner would have called that a PASS. Widened to
`[A-Za-z0-9_]+` and all five re-run, so the recorded output comes from the
scripts as committed. The five phase runners carry the same inert pattern (no
phase config declares a digit-bearing name, checked across all 66) and were
deliberately left untouched so every line of harness output comes from a
byte-identical copy of the script in the tree; recorded as a follow-up.

`models/README.md` and `cas/06-tla-models.md` follow: the `CaBuildRootPrecommit`
runner column said "(inline TLC)", and the how-to-run section had a hand-run
`for cfg in ...` loop that checked no colours at all and silently omitted
`_b2_witness`.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…igation logged

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>