carlos / platform Public

Reviewed 3c74454f. I found one P1 and seven P2 findings.

1. P1 — Task 1, Step 4: create recovery changes the original one-box behavior. The new cancellation path applies regardless of perRegion. Concrete trace: persist the create’s record, stop its selected box, then run recovery after 15 steps. The baseline waits for a regional box; the new code cancels the incarnation immediately. Identical aggregate counters across 300 seeds do not establish identity for this trace. Fix: preserve the baseline selection/recovery path when perRegion == 1; enable recorded-executor cancellation in the HA shape. Add a deterministic comparison covering this interruption.

1. P2 — Task 2, Step 1: stuck does not refuse source admissions. The new source-admission branch checks phase and row readiness, but neither admits nor admitWriter checks Op.Stuck. An exhausted-target fence during starting deliberately preserves the live source and its ready row. Ordinary wakes can therefore admit another writer while the operation is stuck. Stopping relocate() does not stop that admission path. This misses 1b-next’s relocationAdmission refusal and R1-16. Fix: enforce the stuck refusal at writer admission and add a stuck-source wake test that fails when the guard is removed.

1. P2 — Tasks 2–3, Step 1: the sole-box shortcut bypasses HA eligibility. chooseBoxExcept returns the only live box before checking enrollment, executable, secrets, lost, or outstanding park-local. This affects HA-enabled one-box regions and depleted two-box regions. The unenrolled-reference scenario avoids exposing it because its sole unenrolled box cannot run the fence worker yet; create selection can still choose it. Fix: retain the shortcut only for the original non-HA shape. Apply all eligibility checks in HA worlds, including when one candidate remains, and test each refusal.

1. P2 — Task 2, Step 1: the acknowledgement model does not match requireAcks. The installed transition and probing transition omit acknowledgement checks that 1b-next’s ToInstalled and ToProbing require. Elsewhere, leasesSeen requires current leases, whereas requireAcks checks durable acknowledgement entries and the participant separately checks controller readiness. The model therefore both removes permitted traces and admits forbidden transitions. Fix: represent recorded acknowledgements separately from current controller readiness, mirror each transition’s barrier, and test replacement participants that have not acknowledged.

1. P2 — Tasks 2 and 5A, Step 1: fence deadlines use different evidence from 1b-next. relocPinning skips the delay whenever a release exists. JournalPin checks every retained fence observation even after a release—for example, after replacing a terminated target during a drain. Separately, the dead-target deadline starts at actual termination, rather than the fence record’s observed_at. Delayed observation can consequently make the model mark an operation stuck immediately. Fix: retain observation times independently of termination and fence consumption. Apply the pin delay to all relevant observations and test delayed observation plus target replacement after release.

1. P2 — Task 5, Step 1: the phase tests do not establish their advertised coverage. relocPhase accepts any later phase. Multiple workers can advance the operation within one tick, so a fault labelled pinning can occur during installing. The termination matrix also omits probe-failed and adds a spare before the fault: its one-box case has two live boxes, and its two-box case has three. Fix: stop between individual actor transitions, assert the exact phase and live topology immediately before injection, include probe-failed, and launch replacements through the modeled group after loss.

1. P2 — Tasks 5–6, Step 1: five guards lack mutation-sensitive evidence. The plan explicitly lists five rules for which no direct test fails under mutation: reloc-exec-only-installs, files-pin-exact, reloc-failover-pin-delay, reloc-exec-ack-barrier, and reloc-pin-reaches-release. Their classification as determinism, loss-bound, or redundant guards explains a sweep miss, but does not replace a discriminating test. In particular, the files test lands the held manifest after recovery completes, so reading “latest” during installation produces the same result as reading the pin. Fix: add direct tests for each boundary. Land the newer manifest between pinning and installation; inspect unauthorized writes when only a non-executor acts; assert deadline/barrier states before they pass; inject a pin selection short of the journaled release. These require no additional seed sweep.

1. P2 — Tasks 4–5, Step 1, and Task 7, Step 1: required claim §11 cases remain outside the model. The coverage claim exceeds the scenarios supplied. Missing cases include move landing → source cleanup → target failure with an unchanged file; automatic target loss racing record commit; and failed controller cleanup retaining an update-blocking record. The generic installation-crash test also does not force the prepared-admission → marker → replication-opening boundaries. Calling these Stage B integration work does not satisfy the claim’s separate executable-model requirement. Fix: add explicit model events and witnesses for those boundaries before claiming the milestone complete. Model file-object references sufficiently to exercise unchanged-file recovery after source cleanup.

The past-findings mapping is therefore incomplete:

| Findings or guards | What this model cannot currently establish | |---|---| | R1-2 | Pin selection under a location lease, including loss before publication; selection and journaling are collapsed. | | R1-4 and its follow-ups | Durable automatic-loss evidence surviving operation replacement; timer declarations do not model retained reporting evidence. | | R2-7 | Discovery completion when the final local chore is discharged; filtering obligations does not model that state. | | R11-1 | Origin authorization after admission trimming; manifests carry file content directly and use an untrimmed ancestry map. | | Controller findings across R2–R15 and R18-1 | Cleanup failures, lifetime locks, durable participation, update refusal, and removal during an ongoing operation. | | R18-2 | Host-dependent hash selection; tieHash uses the constant host, and the create test does not exercise two hostnames choosing opposite winners. | | Compilation, adapter, privilege and wiring findings | These remain production-boundary checks; independent model rules cannot detect their reintroduction. |

F1–F3 have explicit mutation paths in Task 5A. F3’s invariant miss is reasonable provided its operation-owned cleanup test remains mutation-sensitive. L21 remains open as instructed; I am not requesting a different ruling or more seeds.

I checked patch application and Go syntax/formatting in memory for the three new Go files through their later revisions. I could not reproduce compilation, tests, or mutation results in this read-only session. No files changed.

---

FIRST PROMPT: Review the two-box plan at 3c74454f using brief 1.

WHAT: Check model fidelity, coverage, mutation strength and one-box identity.

STATUS: Review complete: one P1 and seven P2 findings.

NEEDED: Nothing for this review.

RECOMMENDED: Correct the model guards and coverage, then revise the joint-round evidence mapping.

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

Verdict: not ready.