carlos / platform Public

Finding 1 is not the only open item. Finding 2 still has a model/build mismatch. Reviewed model ded69314 against built HEAD b9092a0c. No P1 established.

1. P2 — The model makes the first serving wake warm; the build requires cold.

The model certifies the stopped probe in ltx_test.go:411, then consumes that certificate for warm admission in protocol_test.go:1644.

Built serving admission instead selects a fresh generation with Mode: "cold" in claimowners.go:423, explicitly refuses PredecessorCertified, and records the predecessor’s writes_lost. N6 reuses the stop receipt; it does not grant warm admission.

Assumption (a) is false; the model needs correction. A successful replication flush does not confer admission certification. Model the fresh generation, changed installation stamp, loss declaration and subsequent cleanup. Extend the N6 witness beyond checking that a process runs.

1. P2 — Finding 1 remains: rollback loses source files protection.

movessources.go:491 still returns the newest admission’s region during restoring. After target admission, source-region parks can consequently lose protection for files needed by rollback. The previous finding remains unchanged, including its latent rather than demonstrated production impact.

1. P3 — The model conflates session closure with the later host admission fence.

regionha_test.go:158 closes relFence before flushing and blocks subsequent source admissions. Built StopWriters closes the current attempt and session’s launch journal first; root’s durable admission fence comes through Collect after flush and position recording at relocationeffects.go:202.

Assumption (b) is not an exact match. Separate these states and exercise wake/restart during the intervening interval before enabling drains. This establishes a modelling limitation, not simultaneous writers in the build.

The other judgments:

• Finding 2: discharge ordering, retries, owned fences, successor barriers and claim-mode completion are now represented. Closure remains blocked by the cold-wake mismatch above.
• Finding 3: the requested catch-up path is implemented and modelled. Ruling 85’s successor-operation residual is acceptable while dormant: a stale ready row can affect availability until park-local, but no second writer was established. It does not prove the full source-hold requirement for activation.
• Finding 4: closed. C1 refusal precedes release effects; C11 refusal precedes attempt counting.
• Ruling 86: sound on the inspected paths. completion_fence.go:61 verifies the exact termination record against roster authority and the completion box. Missing or invalid evidence cannot obtain the exemption. No live-box participation bypass found.
• Assumption (c): matches. Completion follows the journalled probe stop; the former relocation opened phase and settle window are absent.

Targeted tests in both worktrees were blocked when Go tried to create its build directory on the read-only filesystem. These conclusions are from static inspection.

---

FIRST PROMPT: Follow the L18 joint-round review brief against the model and built HEADs.

WHAT: Assess whether relocation may merge dormant after finding 1 lands.

STATUS: Review complete; two P2 findings and one P3 limitation remain.

NEEDED: Nothing for this review.

RECOMMENDED: Fix source protection, correct the model’s first serving wake, and rerun the joint gate.

SESSION: Safe to close; no files changed or background processes started.

Verdict: no—landing finding 1 alone is insufficient for relocation to merge dormant.