carlos / platform Public

Reviewed 6b791017.

| Prior verdict / model finding | Disposition | Assessment | |---|---|---| | R16: lost receipt after P opens | Resolved | Receipt verification and stuck handling remain intact. | | R16: crash simulation repairs cleanup faults | Resolved | Crashes preserve faults and durable records; recovery remains separate. | | F2: files pin can lose instance.key | Partly | Missing manifests are refused, but an existing empty manifest bypasses the guard. | | F1: failed probe waits indefinitely without a spare | Partly | The deadline works while the target remains alive; termination bypasses it. | | F3: abandoned prepared generation leaks | Partly | Replacement during installing is covered; replacement from probe-failed can forget P. |

1. P1 — An existing empty manifest still permits key loss. Task 5, Step 4: filesPin, line 7183 returns an existing manifest before checking positive evidence. Stage B explicitly requires a manifest copy before app startup. That copy can lack instance.key: the app then mints its key, replicates dependent database data, and terminates before publishing the key. Recovery still installs a database without its key.

Fix: Refuse recovery without evidence for the required files, including when a manifest exists. Test an empty manifest with an admitted writer and nonempty database. Ruling 25 also needs an upstream durability contract: the continuous-sync window does not make that database recoverable.

1. P2 — Target termination bypasses the no-spare deadline. Task 5, Step 3: Step, line 6737 dispatches a target fence to replace before reaching the phase deadline. When replacements remain, replace returns the chooser’s error indefinitely. Terminating the target after its journaled release therefore leaves the host unserved without marking the operation stuck.

Fix: Add a bounded, fence-consuming transition for a terminated target with no spare. Extend the deadline test by terminating the target after release.

1. P2 — Replacement from probe-failed can discard an unopened P without recording it. Task 1, Step 3: ReplaceTarget, line 2616 deletes prepared in its default branch. This includes a target whose probe deadline expired before any admission, followed by termination. The later install cannot record the forgotten P, so completion queues no retirement.

Fix: Record unopened P before every transition that discards it. Test probe timeout before admission, target termination, replacement, and successful completion.

Rulings 1–24 remain accepted. Ruling 26’s operator-only recovery is reasonable with its stated availability cost. Rulings 25 and 27 need the corrections above. Prior Stage B contracts remain present; the new F2 contract is insufficient.

All 12 embedded patches pass git apply --check; all 47 Go blocks parse with gofmt. Compilation, runtime tests and mutations were not independently reproduced.

---

FIRST PROMPT: “Follow the review brief docs/superpowers/plans/CODEX-PLAN-REGION-HA-1BN-BRIEF-17.md. Review the plan at commit 6b791017.”

WHAT: Review Stage A readiness and Stage B contracts.

STATUS: Three findings: one P1 and two P2s.

NEEDED: Nothing.

RECOMMENDED: Correct the three paths and add the missing regression cases.

SESSION: Safe to close — no files changed or processes left running.

Verdict: not ready.