amadan

carlos / platform Public

Box identity Option B rev 6 and plan rev 4: answer Astra's round 5

Two P1s: a stale snapshot was not a lock against its own holder, so
--retire-label now replaces it with the tombstone by CAS on the etag it
read before touching the edges file, and a renewal or acquisition that
wins that CAS stops the command with nothing deleted; and a label with a
region HA box record is bound to one instance for good, so retirement
frees a label only for the instance the record names and "the operator
rebinds" is withdrawn. Six P2s: the barrier is stated as conditional on
S3 landing an in-flight request within requestGrace and a call admitted
with a passed deadline is refused; the plan's snippets use the real
sampler, newAlertSinks arguments, a root-package env helper, an S3
opener adapter and a create body with host; every snapshot field is
round-tripped, the per-tick functions run through Gated with an inner
mutation counter, the relay fake forces a first-attempt CAS conflict,
the prefixed key is asserted on the opener's store; operator surfaces
project all three contention rules; the simulation retires by the
stored snapshot with deterministic stopped and fresh-legacy cases; a
fresh machine id comes from systemd-id128 new and the change is proved.
Findings committed unedited as CODEX-FINDINGS-BOX-IDENTITY-B-R5.md.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude a658e5b8d1c714b6ed18e6cc5a6966cbfcdb32d2 parent db5e189
3 files changed, +482 −89
  • docs/superpowers/plans/2026-10-06-box-identity-detect.md +305 −36
  • docs/superpowers/specs/2026-10-06-box-identity-detect-design.md +107 −53
  • docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-B-R5.md +70 −0

CI passed — run details

diff --git a/docs/superpowers/plans/2026-10-06-box-identity-detect.md b/docs/superpowers/plans/2026-10-06-box-identity-detect.md
index 98548bbd6..a928ede84 100644
--- a/docs/superpowers/plans/2026-10-06-box-identity-detect.md
+++ b/docs/superpowers/plans/2026-10-06-box-identity-detect.md
@@ -8,7 +8,7 @@
**Tech Stack:** Go 1.25, `release.Store` (S3 and DirStore), `internal/status`, `internal/host`, `internal/edgesfile`, `internal/console`, `internal/relay`, `internal/metrics`.
-**Spec:** `docs/superpowers/specs/2026-10-06-box-identity-detect-design.md` (rev 5). §2.1 (the verdict table), §2.2 (the gate, absolute deadline, `retireAfter`), §2.3 (recovery and the retire order), §2.6 (the namespace rule, inside the decision) and §3 (reader rules, monotonic completeness, four reads before any return) are normative. Line numbers are against the branch after its merge of main (`fb59cb23`). Region HA's `box_id` (`internal/host/edgesfile.go:277`, `internal/console/boxchoice.go`) is a different field with a different meaning and is **not touched**; this plan adds `machine`.
+**Spec:** `docs/superpowers/specs/2026-10-06-box-identity-detect-design.md` (rev 6). §2.1 (the verdict table), §2.2 (the gate, absolute deadline, `retireAfter`), §2.3 (recovery and the retire order), §2.6 (the namespace rule, inside the decision) and §3 (reader rules, monotonic completeness, four reads before any return) are normative. Line numbers are against the branch after its merge of main (`fb59cb23`). Region HA's `box_id` (`internal/host/edgesfile.go:277`, `internal/console/boxchoice.go`) is a different field with a different meaning and is **not touched**; this plan adds `machine`.
**Landing** (`AGENTS.md:108-130`): the task commits are not independently shippable (Task 2 arms snapshot refusal before Task 4 gates the other publishers and before Task 8's recovery tooling exists). When every task is done and reviewed: squash to one commit on the branch, push, `amadan branch describe carlos/platform design-box-identity -body -`, wait for `amadan ci status carlos/platform -branch design-box-identity` to pass on that tip, then `amadan branch merge carlos/platform design-box-identity -expect <tip> -message "..."`.
@@ -16,7 +16,7 @@
- No object key, prefix, Route53 `SetIdentifier` or region-HA `box_id` changes (spec §1).
- `machine` and `instance_id` never appear in `status/fleet.json`, `status/index.html`, any account page, the instances API response, or an alert mail body (spec §1, §3, §7).
-- A label is never reassigned automatically; only `carlos status --retire-label` deletes a label's objects, only when its snapshot is older than `retireAfter = 3*status.SnapshotPeriod + mutationTTL + requestGrace` (17 minutes), edges file first and snapshot last, with a create-only tombstone when the snapshot is absent (spec §2.3).
+- A label is never reassigned automatically; only `carlos status --retire-label` deletes a label's objects, only when its snapshot is older than `retireAfter = 3*status.SnapshotPeriod + mutationTTL + requestGrace` (17 minutes), and only after replacing that snapshot with a tombstone by CAS on the etag it read (create-only when absent); then the edges file, then the tombstone last. A label with a verified region HA box record is freed only for the instance the record names (spec §2.3, §4).
- `owned` is recorded only after a successful conditional write; each decision attempt starts fresh; a failed `Put` is `unknown` (spec §2.1).
- The namespace rule (spec §2.6) runs inside `decideIdentity` on every call.
- Every `Put`, `Delete` and `DeleteIfMatch` under a label-keyed key goes through `host.Gated`, which refuses past the verdict's expiry and sets an absolute deadline `min(now, expiry) + mutationTTL`, `mutationTTL = 60 * time.Second` (spec §2.2).
@@ -1069,6 +1069,14 @@ func Gated(s release.Store, label string) release.Store {
}
func (g *gatedStore) admit(ctx context.Context) (context.Context, context.CancelFunc, error) {
+ // A caller paused across its own deadline (spec 2.2, B5-3): nothing is
+ // sent on its behalf.
+ if err := ctx.Err(); err != nil {
+ return nil, nil, err
+ }
+ if d, has := ctx.Deadline(); has && !g.now().Before(d) {
+ return nil, nil, context.DeadlineExceeded
+ }
deadline, ok := admitted(g.dir(), g.me(), g.label, g.target(), g.now())
if !ok {
return nil, nil, ErrNotPublishable
@@ -1076,6 +1084,11 @@ func (g *gatedStore) admit(ctx context.Context) (context.Context, context.Cancel
ctx, cancel := context.WithDeadline(ctx, deadline)
return ctx, cancel, nil
}
+```
+
+Task 3's gate test gains one case: a `ctx` whose deadline is already in the past is refused with `context.DeadlineExceeded` before the identity file is read (count `readIdentity` calls through `dir()`).
+
+```go
func (g *gatedStore) Put(ctx context.Context, key string, body []byte, ifMatch string) (string, error) {
ctx, cancel, err := g.admit(ctx)
@@ -1265,18 +1278,53 @@ func TestDirectoryDeploymentIsConfiguredAndDoesNotExpire(t *testing.T) {
}
func TestCollectSnapshotCarriesRoutesAliasesAndVersions(t *testing.T) {
+ // Every route-derived field spec 2.1 names must round-trip through the
+ // decision's write (B5-5): counts, a sidecar, a stamped version, an
+ // alias reading and a database size.
reg := restartTestRegistry(t)
seedRoute(t, reg, "a.example")
- b, routes, err := collectSnapshot(reg, status.Probes{MachineID: "m", InstanceID: "i-m"}, time.Now())
- if err != nil || len(routes) == 0 {
+ if err := reg.SetVersion("a.example", "abc1234"); err != nil { // the registry's version stamp, as the adopt pass does
+ t.Fatal(err)
+ }
+ seedRoute(t, reg, "worker.example")
+ if err := reg.SetSidecar("worker.example", true); err != nil { // the column registry.Route.IsSidecar reads
+ t.Fatal(err)
+ }
+ if err := reg.UpsertAlias(registry.Alias{Host: "www.example", Route: "a.example", DNSStatus: "pointing"}); err != nil {
+ t.Fatal(err)
+ }
+ probes := status.Probes{MachineID: "m", InstanceID: "i-m", RouteDBBytes: map[string]int64{"a.example": 4096}}
+ b, routes, err := collectSnapshot(reg, probes, time.Now())
+ if err != nil || len(routes) != 2 {
t.Fatalf("collect: %v routes=%d", err, len(routes))
}
- if b.Routes.Resident+b.Routes.Static+b.Routes.Hibernating == 0 || b.Machine != status.Machine("m") {
- t.Fatalf("the snapshot must carry the registry's routes and this machine: %+v", b)
+ s := release.NewDirStore(t.TempDir())
+ if _, err := status.DecideLabel(context.Background(), s, b, b.GeneratedAt); err != nil {
+ t.Fatal(err)
+ }
+ raw, _, _ := s.Get(context.Background(), "status/boxes/"+b.Label+".json")
+ var got status.Box
+ _ = json.Unmarshal(raw, &got)
+ switch {
+ case got.Machine != status.Machine("m"):
+ t.Fatalf("machine: %+v", got)
+ case got.Routes.Resident+got.Routes.Static+got.Routes.Hibernating != 1 || got.Sidecars != 1:
+ t.Fatalf("one route and one sidecar: %+v", got)
+ case got.Metrics == nil || got.Metrics.RouteVersions["a.example"] != "abc1234":
+ t.Fatalf("version: %+v", got.Metrics)
+ case got.Metrics.Aliases["www.example"].DNSStatus != "pointing":
+ t.Fatalf("alias reading: %+v", got.Metrics.Aliases)
+ case got.Metrics.RouteDBBytes["a.example"] != 4096:
+ t.Fatalf("db size: %+v", got.Metrics.RouteDBBytes)
}
}
```
+(`SetVersion`, `SetSidecar` and `UpsertAlias` stand for whatever the registry's real write methods for the version column, the sidecar column and `route_aliases` are called; the existing `statusTick` tests in `agent_test.go` seed the same columns and are the reference.)
+
+```go
+```
+
```go
// internal/host/edgesfile_test.go
func TestSeedEdgesFileGateKeepsOnlyOurOwnSeed(t *testing.T) {
@@ -1384,8 +1432,8 @@ func TestEveryPublisherStopsWhenTheLabelIsLost(t *testing.T) {
return edgesFilePass(ctx, s, edgesTestRegistry(t), edgesFile{Box: me.Label, Machine: me.ID}, "1.2.3.4", &last)
}},
{"metrics flush", func(ctx context.Context, s release.Store) error {
- sm := newSampler(nil) // the sampler the existing metricsFlush tests build
- sm.record(now, metrics.Sample{At: now})
+ sm := &sampler{} // metrics_loop.go:60; seed buf the way the existing metricsFlush tests do
+ sm.buf = append(sm.buf, metrics.Sample{At: now})
return metricsFlush(ctx, s, me.Label, sm, now)
}},
{"alert state", func(ctx context.Context, s release.Store) error {
@@ -1408,20 +1456,50 @@ func TestEveryPublisherStopsWhenTheLabelIsLost(t *testing.T) {
return s.Delete(ctx, key)
}},
}
+ // usage, error shipping and analytics go through the same shape: their
+ // per-tick functions (usageFlush, the errship flush, the analytics
+ // meter's Flush) are added to entries with a seeded sink, the way the
+ // existing tests for each build one.
for _, e := range entries {
t.Run(e.name, func(t *testing.T) {
- g := Gated(release.NewDirStore(t.TempDir()), me.Label)
+ inner := &mutationCounter{Store: release.NewDirStore(t.TempDir())}
+ g := Gated(inner, me.Label)
own(status.VerdictOwned)
- if err := e.write(context.Background(), g); err != nil {
- t.Fatalf("owned: %v", err)
+ if err := e.write(context.Background(), g); err != nil || inner.n == 0 {
+ t.Fatalf("owned: %v, %d underlying mutations", err, inner.n)
}
+ before := inner.n
own(status.VerdictForeign)
if err := e.write(context.Background(), g); !errors.Is(err, ErrNotPublishable) {
t.Fatalf("foreign: %v, want ErrNotPublishable", err)
}
+ if inner.n != before {
+ t.Fatalf("no underlying mutation may reach the store after revocation: %d -> %d", before, inner.n)
+ }
})
}
}
+
+// mutationCounter counts Put, Delete and DeleteIfMatch that reach the store.
+type mutationCounter struct {
+ release.Store
+ n int
+}
+
+func (m *mutationCounter) Put(ctx context.Context, key string, body []byte, ifMatch string) (string, error) {
+ m.n++
+ return m.Store.Put(ctx, key, body, ifMatch)
+}
+
+func (m *mutationCounter) Delete(ctx context.Context, key string) error {
+ m.n++
+ return m.Store.Delete(ctx, key)
+}
+
+func (m *mutationCounter) DeleteIfMatch(ctx context.Context, key, etag string) error {
+ m.n++
+ return release.DeleteIfMatch(ctx, m.Store, key, etag)
+}
```
```go
@@ -1431,11 +1509,19 @@ func TestMeterFlushRetriesAndPreservationAreRefused(t *testing.T) {
now := time.Unix(1_700_000_000, 0)
m := NewMeter("annie", func() time.Time { return now }, nil)
m.SetAllocsAll(map[Identity]int{{Account: "a", App: "x"}: 1})
- if err := m.Flush(context.Background(), &refuseAfterGet{Store: inner}); !errors.Is(err, errRefused) {
- t.Fatalf("flush = %v, want the refusal surfaced", err)
+ // First attempt: a real CAS conflict (another writer landed a chunk
+ // between the read and the write), so meter.go:167's retry runs; the
+ // retry's Put is then refused (ownership flipped). B5-5.
+ s := &conflictThenRefuse{Store: inner, key: MeterKey("annie", metrics.HourOf(now))}
+ if err := m.Flush(context.Background(), s); !errors.Is(err, errRefused) {
+ t.Fatalf("flush = %v, want the refusal surfaced on the retry", err)
+ }
+ if s.puts != 2 {
+ t.Fatalf("one conflicting attempt and one refused retry, got %d puts", s.puts)
}
- if keys, _ := inner.List(context.Background(), "metrics/relay/"); len(keys) != 0 {
- t.Fatalf("nothing may be written after refusal, got %v", keys)
+ body, _, _ := inner.Get(context.Background(), s.key)
+ if !strings.Contains(string(body), "other-writer") {
+ t.Fatal("the other writer's chunk must stand; nothing of ours may have landed")
}
key := MeterKey("annie", metrics.HourOf(now))
if _, err := inner.Put(context.Background(), key, []byte("{bad"), ""); err != nil {
@@ -1449,6 +1535,25 @@ func TestMeterFlushRetriesAndPreservationAreRefused(t *testing.T) {
var errRefused = errors.New("refused")
+// conflictThenRefuse: the first Put to key loses a CAS race to a chunk
+// written behind the meter's back; every later Put is refused.
+type conflictThenRefuse struct {
+ release.Store
+ key string
+ puts int
+}
+
+func (c *conflictThenRefuse) Put(ctx context.Context, key string, body []byte, ifMatch string) (string, error) {
+ c.puts++
+ if c.puts == 1 && key == c.key {
+ if _, err := c.Store.Put(ctx, key, []byte(`{"v":1,"box":"other-writer","samples":[]}`), ifMatch); err != nil {
+ return "", err
+ }
+ return "", release.ErrCASConflict
+ }
+ return "", errRefused
+}
+
type refuseAfterGet struct {
release.Store
got bool
@@ -1625,7 +1730,7 @@ func TestRefuserLogsAndDeliversOncePerTransition(t *testing.T) {
func TestRefuserDeliversThroughAlertSinks(t *testing.T) {
var posted []string
post := func(url string, body []byte) error { posted = append(posted, string(body)); return nil }
- sinks := newAlertSinks("https://hook.example/x", post, nil, nil, &alertCounters{}) // alertsink.go:89's parameters; nil SNS
+ sinks := newAlertSinks("https://hook.example/x", post, "", nil, &alertCounters{}) // alertsink.go:89: webhook URL, poster, SNS topic (""), SNS client (nil), counters
rules := metrics.RulesFromEnv(envFunc(map[string]string{}))
r := &refuser{logf: func(string, ...any) {}, deliver: func(e metrics.Event) { sinks.deliver(context.Background(), rules, time.Now(), e) }}
d := status.Decision{Verdict: status.VerdictForeign, Label: "edsger-knitting", Machine: status.Machine("b"), HolderMachine: status.Machine("a"), DecidedAt: time.Now()}
@@ -2346,11 +2451,21 @@ func TestResolveLabelStoresFollowsEachWritersRule(t *testing.T) {
if st.statusWhere != "s3://s/fleets/pi/" || st.deployWhere != "s3://d/" || !opened["s"] || !opened["d"] {
t.Fatalf("locations = %q %q", st.statusWhere, st.deployWhere)
}
- // The prefixed status store really is prefixed: a snapshot written through it lands under the prefix.
+ // The prefixed status store really is prefixed: a snapshot written through
+ // it lands under fleets/pi/ in the opener's store for bucket "s" (B5-5).
+ stores := map[string]release.Store{}
+ open = func(_ context.Context, bucket string) (release.Store, error) {
+ if stores[bucket] == nil {
+ stores[bucket] = release.NewDirStore(t.TempDir())
+ }
+ return stores[bucket], nil
+ }
+ st, _ = resolveLabelStores(context.Background(), envFunc(map[string]string{"CARLOS_DEPLOYMENT_BUCKET": "d", "CARLOS_STATUS_BUCKET": "s", "CARLOS_STATUS_PREFIX": "fleets/pi/"}), open)
_ = status.WriteFleetBox(context.Background(), st.status, status.Box{GeneratedAt: time.Now(), Label: "desk"})
- // (resolveLabelStores wraps with release.NewPrefixStore; the test's opener returns a fresh DirStore per bucket,
- // so list the inner store through a second resolve with no prefix to see the full key.)
- st2, _ := resolveLabelStores(context.Background(), envFunc(map[string]string{"CARLOS_DEPLOYMENT_BUCKET": "d"}), func(_ context.Context, b string) (release.Store, error) { return release.NewDirStore("/nonexistent"), nil })
+ if _, _, err := stores["s"].Get(context.Background(), "fleets/pi/status/boxes/desk.json"); err != nil {
+ t.Fatalf("the snapshot must land under the prefix in bucket s: %v", err)
+ }
+ st2, _ := resolveLabelStores(context.Background(), envFunc(map[string]string{"CARLOS_DEPLOYMENT_BUCKET": "d"}), open)
if st2.statusWhere != "s3://d/" || st2.deployWhere != "s3://d/" {
t.Fatalf("default: status store is the deployment bucket at the root: %q %q", st2.statusWhere, st2.deployWhere)
}
@@ -2452,10 +2567,93 @@ func TestRetireLabelRefusesWhenTheObjectChangedUnderIt(t *testing.T) {
if !errors.Is(err, release.ErrCASConflict) {
t.Fatalf("an etag change between read and delete must surface as a CAS conflict, got %v", err)
}
+ body, _, gerr := s.Get(ctx, "status/boxes/"+holder.Label+".json")
+ if gerr != nil || !strings.Contains(string(body), status.TombstoneMachine) {
+ t.Fatal("the tombstone (the lock) must still be in place after a lost edges race, for the operator to re-run")
+ }
+}
+
+// B5-1: the holder renews its stale snapshot between retire's read and its
+// tombstone write; the CAS loses and nothing is deleted, both live objects
+// preserved.
+func TestRetireLabelStopsWhenTheHolderRenewsBetweenReadAndTombstone(t *testing.T) {
+ st, s := oneStore(t)
+ ctx := context.Background()
+ now := time.Now()
+ holder := status.CollectBox(nil, status.Probes{MachineID: "a", InstanceID: "i-a"}, now)
+ _ = status.WriteBox(ctx, s, holder)
+ _, _ = s.Put(ctx, edgesfile.Prefix+holder.Label+".json", []byte(`{"v":1,"box":"`+holder.Label+`","eip":"1.2.3.4","hosts":{}}`), "")
+ later := now.Add(retireAfter + time.Second)
+ renew := &renewBetween{Store: s, key: "status/boxes/" + holder.Label + ".json", renewed: status.CollectBox(nil, status.Probes{MachineID: "a", InstanceID: "i-a"}, later)}
+ st.status, st.deploy = renew, renew
+ var out bytes.Buffer
+ if err := retireLabel(ctx, st, holder.Label, later, &out); !errors.Is(err, release.ErrCASConflict) {
+ t.Fatalf("the tombstone write must lose to the renewal: %v", err)
+ }
+ if _, _, err := s.Get(ctx, edgesfile.Prefix+holder.Label+".json"); err != nil {
+ t.Fatal("the live holder's edges file must be untouched")
+ }
+ body, _, _ := s.Get(ctx, "status/boxes/"+holder.Label+".json")
+ var got status.Box
+ _ = json.Unmarshal(body, &got)
+ if got.Machine != holder.Machine || !got.GeneratedAt.Equal(later) {
+ t.Fatalf("the renewed snapshot must stand: %+v", got)
+ }
+}
+
+// renewBetween replaces key with renewed after retire's first read of it,
+// standing in for the holder's own DecideLabel renewing a stale snapshot.
+type renewBetween struct {
+ release.Store
+ key string
+ renewed status.Box
+ done bool
+}
+
+func (r *renewBetween) Get(ctx context.Context, key string) ([]byte, string, error) {
+ body, etag, err := r.Store.Get(ctx, key)
+ if err == nil && key == r.key && !r.done {
+ r.done = true
+ raw, _ := json.Marshal(r.renewed)
+ _, _ = r.Store.Put(ctx, key, raw, etag)
+ }
+ return body, etag, err
+}
+
+func (r *renewBetween) DeleteIfMatch(ctx context.Context, key, etag string) error {
+ return release.DeleteIfMatch(ctx, r.Store, key, etag)
+}
+
+// B5-2: a label with a region HA box record bound to another instance is
+// never freed for a different machine.
+func TestRetireLabelRefusesABoundLabelForAnotherInstance(t *testing.T) {
+ st, s := oneStore(t)
+ ctx := context.Background()
+ now := time.Now()
+ holder := status.CollectBox(nil, status.Probes{MachineID: "a", InstanceID: "i-a"}, now)
+ _ = status.WriteBox(ctx, s, holder)
+ publishTestBoxRecord(t, s, holder.Label, "i-a") // a record and bind for instance i-a, built with boxid's test helpers
+ _ = status.WriteEvidence(ctx, s, status.Evidence{V: 1, Label: holder.Label, Machine: status.Machine("b"), InstanceID: "i-b", Verdict: status.VerdictForeign, HolderInstanceID: "i-a", SeenAt: now})
+ var out bytes.Buffer
+ err := retireLabel(ctx, st, holder.Label, now.Add(retireAfter+time.Second), &out)
+ if err == nil || !strings.Contains(err.Error(), "bound to instance i-a") {
+ t.Fatalf("a bound label must not be freed for i-b: %v", err)
+ }
if _, _, gerr := s.Get(ctx, "status/boxes/"+holder.Label+".json"); gerr != nil {
- t.Fatal("the snapshot (the lock) must still be there after a lost race")
+ t.Fatal("nothing deleted")
+ }
+ // The same label, reclaimed by the instance the record names, is allowed.
+ _ = status.WriteEvidence(ctx, s, status.Evidence{V: 1, Label: holder.Label, Machine: status.Machine("a2"), InstanceID: "i-a", Verdict: status.VerdictForeign, HolderInstanceID: "i-b", SeenAt: now})
+ out.Reset()
+ if err := retireLabel(ctx, st, holder.Label, now.Add(retireAfter+time.Second), &out); err != nil {
+ t.Fatalf("returning a bound label to its own instance is allowed: %v", err)
}
}
+```
+
+(`publishTestBoxRecord` builds a record whose signed identity document names the given instance, using the fixtures `internal/boxid/boxid_test.go` already has for a signed document and the embedded certificate; copy that fixture's constructor.)
+
+```go
// putBetween rewrites key after the first Get so the etag no longer matches,
// and FORWARDS DeleteIfMatch so the condition is actually exercised (B4-7).
@@ -2493,6 +2691,9 @@ func TestRetireLabelLoneEdgesFileUsesATombstone(t *testing.T) {
if !spy.sawTombstone {
t.Fatal("a lone edges file is retired under a create-only tombstone snapshot")
}
+ if spy.deletes[0] != edgesfile.Prefix+"annie-welding.json" {
+ t.Fatalf("edges first, tombstone last: %v", spy.deletes)
+ }
if _, _, err := s.Get(ctx, edgesfile.Prefix+"annie-welding.json"); !errors.Is(err, os.ErrNotExist) {
t.Fatal("the lone edges file must be gone")
}
@@ -2507,6 +2708,7 @@ func TestRetireLabelLoneEdgesFileUsesATombstone(t *testing.T) {
type tombstoneSpy struct {
release.Store
sawTombstone bool
+ deletes []string
}
func (t *tombstoneSpy) Put(ctx context.Context, key string, body []byte, ifMatch string) (string, error) {
@@ -2517,7 +2719,11 @@ func (t *tombstoneSpy) Put(ctx context.Context, key string, body []byte, ifMatch
}
func (t *tombstoneSpy) DeleteIfMatch(ctx context.Context, key, etag string) error {
- return release.DeleteIfMatch(ctx, t.Store, key, etag)
+ if err := release.DeleteIfMatch(ctx, t.Store, key, etag); err != nil {
+ return err
+ }
+ t.deletes = append(t.deletes, key)
+ return nil
}
func TestRetireLabelStopsWhenABoxAcquiresBetweenTheReads(t *testing.T) {
@@ -2613,15 +2819,22 @@ Expected: FAIL, undefined.
- [ ] **Step 3: Implement `status_identity.go`**
-`resolveLabelStores(ctx, getenv, open)`: status store is `open(host.ResolveStatusBucket(getenv))` wrapped with `release.NewPrefixStore` when `CARLOS_STATUS_PREFIX` is set, `statusWhere = "s3://<bucket>/<prefix>"`; the deployment store is `open(CARLOS_DEPLOYMENT_BUCKET)` or `release.NewDirStore(CARLOS_DEPLOYMENT_DIR)` with `deployWhere` accordingly; `RunStatus` passes `release.NewS3Store` as `open`. Both commands print both locations first.
+`resolveLabelStores(ctx, getenv, open)`: status store is `open(host.ResolveStatusBucket(getenv))` wrapped with `release.NewPrefixStore` when `CARLOS_STATUS_PREFIX` is set, `statusWhere = "s3://<bucket>/<prefix>"`; the deployment store is `open(CARLOS_DEPLOYMENT_BUCKET)` or `release.NewDirStore(CARLOS_DEPLOYMENT_DIR)` with `deployWhere` accordingly; `RunStatus` passes an adapter, `func(ctx context.Context, b string) (release.Store, error) { return release.NewS3Store(ctx, b) }`, because `NewS3Store` returns `*S3Store` (`store.go:557`). Both commands print both locations first. The root package has no `envFunc`; `status_identity_test.go` defines `func envFunc(m map[string]string) func(string) string { return func(k string) string { return m[k] } }`.
`checkLabel`: `label, machine := status.Label(machineID), status.Machine(machineID)`; print `label <label>, machine <machine>`; `Get` the snapshot from `st.status` and the edges file from `st.deploy`; print each as absent or `machine`, `instance_id`, `fresh`/`stale` (snapshot via `BoxStale`), `machine`, `box_id`, `eip` (edges); print each unexpired evidence entry naming the label with holder and refuser instance ids; print whether `boxid.Key(label)` and `boxid.BindKey(label)` exist (`control/boxes/`, informational); print `claim references: not checked (hostclaim is not on main)`. Exit 0 when both objects are absent or every present object's `machine == machine`; exit 1 otherwise, printing `verdict: foreign` or `verdict: unproven` (an object with no `machine`).
-`retireLabel`: read the snapshot (`st.status`) with etag. Present: parse; if `now.Sub(GeneratedAt) < retireAfter` return `label <label>: snapshot is <age> old, younger than retireAfter (<retireAfter>); a mutation may still be in flight, refusing`. Absent: write the tombstone create-only (`status.Box{GeneratedAt: time.Time{}, Label: label, Machine: status.TombstoneMachine}`, `Put(key, body, "")`); on `ErrCASConflict` print `a box took label <label> between the reads; nothing deleted` and return the error; remember the tombstone's etag; print `snapshot: already gone (tombstone written)`. Read the edges file (`st.deploy`) with etag; present: print its `machine`/`box_id`/`eip` and `release.DeleteIfMatch` it (a failed condition returns the error, snapshot untouched); absent: print `edges file: already gone`. Finally `release.DeleteIfMatch` the snapshot or tombstone on its etag. `ErrConditionalDeleteUnsupported` is returned as is. The doc comment states the claim dependency (spec §4).
+`retireLabel` (spec §2.3, codex B5-1, B5-2), in this order:
+
+1. Region HA check: `boxid.Load(ctx, st.deploy, label)`; when a record exists and verifies (`boxid.Verifier`, the same way `eligibleBoxes`'s callers load it), compare its `InstanceID` with the refuser's instance id from the unexpired evidence naming the label; if there is no such refuser or the ids differ, return `label <label> is bound to instance <id> by its box record (control/boxes/<label>.json) and can only return to that instance; give the new box a fresh machine id instead`.
+2. Read the snapshot (`st.status`) with its etag. Present: parse; if `now.Sub(GeneratedAt) < retireAfter` return `label <label>: snapshot is <age> old, younger than retireAfter (<retireAfter>); a mutation may still be in flight, refusing`. Then **take the lock**: `Put(key, tombstone, etag)` where `tombstone` is `status.Box{GeneratedAt: time.Time{}, Label: label, Machine: status.TombstoneMachine}` and `etag` is the one read (`""` when the snapshot was absent, so the create is create-only). On `ErrCASConflict` print `the holder renewed or a box took label <label> between the read and the write; nothing deleted` and return the error. Remember the tombstone's etag. Print `snapshot: replaced by a tombstone` or `snapshot: already gone (tombstone written)`.
+3. Read the edges file (`st.deploy`) with its etag; present: print its `machine`/`box_id`/`eip` and `release.DeleteIfMatch` it (a failed condition returns the error with the tombstone in place; the operator re-runs); absent: print `edges file: already gone`.
+4. `release.DeleteIfMatch` the tombstone on its etag, last.
+
+`ErrConditionalDeleteUnsupported` is returned as is. The doc comment states the claim dependency (spec §4).
`RunStatus`: `checkFlag := fs.String("check-label", "", "show who holds the label this machine id gives; exit 1 if another machine does")`, `retireFlag := fs.String("retire-label", "", "free a stale label after a collision (spec 2.3)")`; `statusUsage` gains both lines. `printLiveBoxes(w, boxes, evidence, now)`: a label named by unexpired evidence prints ` CONTESTED (holder <instance>, refuser <instance>)`.
-`HostRows` loads evidence (a nil store or a failed load leaves rows uncontested) and sets `Contested`, `HolderInstance`, `RefuserInstance`; `fleet.html`'s Host cell renders `{{if .Contested}}<span class="chip chip-stale">contested</span> holder {{.HolderInstance}}, refuser {{.RefuserInstance}}{{end}}`.
+`HostRows` projects all three contention rules (spec §3, codex B5-6): it loads evidence, the observation file and the edges files (through `edgesfile.Parse`), and marks a row `Contested` when the label is named by unexpired evidence, has an active `contested_until`, or its edges file's `machine` differs from the snapshot's; `HolderInstance` is the snapshot's `Metrics.InstanceID`, `RefuserInstance` the evidence's when there is one, and `Reason` one of `evidence`, `writer change`, `edges mismatch`. A nil store or a failed load leaves rows uncontested. `fleet.html`'s Host cell renders `{{if .Contested}}<span class="chip chip-stale">contested</span> {{.Reason}}{{if .HolderInstance}}, holder {{.HolderInstance}}{{end}}{{if .RefuserInstance}}, refuser {{.RefuserInstance}}{{end}}{{end}}`. `printLiveBoxes` prints the same three sources. `TestHostRowsCarryContestedAndBothInstances` gains two sibling cases, one with only an observation `contested_until` and one with only an edges mismatch, each asserting `Contested` and `Reason`.
`docs/site/cli.md` `### carlos status`, after the `--live` example:
@@ -2704,7 +2917,7 @@ func TestDryRunNeedlesIncludeIdentityAndTheRunPublishesEvidence(t *testing.T) {
func TestInstanceListNeverCarriesMachineOrInstanceID(t *testing.T) {
fx, token := instanceFixture(t, "ie")
enableInstances(t, fx, "titogo", titoManifest())
- st, _, body := rawReq(t, http.MethodPost, instancesURL(fx, OpsAccountID, "titogo"), token, `{"name":"acme"}`)
+ st, _, body := rawReq(t, http.MethodPost, instancesURL(fx, OpsAccountID, "titogo"), token, `{"host":"acme.go.tito.io","region":"ie"}`) // apiinstances.go:642 requires host
if st != http.StatusCreated && st != http.StatusOK {
t.Fatalf("create: %d %s", st, body)
}
@@ -2794,8 +3007,14 @@ func TestDecideLabelSimulation(t *testing.T) {
if rng.Intn(4) == 0 {
ms[n-1].id = ms[0].id // a clone
}
- holder := map[string]string{} // label -> instance holding it, "" = unknown after an old overwrite
+ holder := map[string]string{} // label -> instance holding it, "" = unknown after an old overwrite
lastOwnedAt := map[string]time.Time{}
+ retired := 0
+ defer func() {
+ if seed == 0 && retired == 0 {
+ t.Log("seed 0 retired nothing; the deterministic retirement tests below cover the path")
+ }
+ }()
const retireAfter = 3*status.SnapshotPeriod + 2*time.Minute
for tick := 0; tick < 60; tick++ {
now = now.Add(time.Minute)
@@ -2806,12 +3025,18 @@ func TestDecideLabelSimulation(t *testing.T) {
if rng.Intn(15) == 0 {
ms[rng.Intn(n)].old = !ms[rng.Intn(n)].old // a roll
}
- if rng.Intn(40) == 0 { // an operator retires a stale label
- for label, at := range lastOwnedAt {
- if now.Sub(at) > retireAfter {
- key := "status/boxes/" + label + ".json"
- if _, etag, err := inner.Get(context.Background(), key); err == nil {
- _ = release.DeleteIfMatch(context.Background(), inner, key, etag)
+ if rng.Intn(40) == 0 { // an operator retires a stale label, judged from the STORED snapshot (B5-7)
+ for label := range lastOwnedAt {
+ key := "status/boxes/" + label + ".json"
+ raw, etag, err := inner.Get(context.Background(), key)
+ if err != nil {
+ continue
+ }
+ var cur status.Box
+ _ = json.Unmarshal(raw, &cur)
+ if now.Sub(cur.GeneratedAt) > retireAfter {
+ if release.DeleteIfMatch(context.Background(), inner, key, etag) == nil {
+ retired++
delete(holder, label)
delete(lastOwnedAt, label)
}
@@ -2852,6 +3077,47 @@ func TestDecideLabelSimulation(t *testing.T) {
}
}
+// Deterministic retirement cases (B5-7): a writer that stopped is retired
+// once its stored snapshot is older than retireAfter; a legacy writer that
+// keeps refreshing is never retired, however long ago a new writer last
+// owned the label.
+func TestRetirementJudgesTheStoredSnapshot(t *testing.T) {
+ s := release.NewDirStore(t.TempDir())
+ ctx := context.Background()
+ now := time.Now()
+ const retireAfter = 3*status.SnapshotPeriod + 2*time.Minute
+ stopped := boxFor("stopped", "i-s", now)
+ if _, err := status.DecideLabel(ctx, s, stopped, now); err != nil {
+ t.Fatal(err)
+ }
+ legacyLabel := status.Label("legacy")
+ key := "status/boxes/" + legacyLabel + ".json"
+ later := now.Add(retireAfter + time.Minute)
+ raw, _ := json.Marshal(status.Box{GeneratedAt: later, Label: legacyLabel, Metrics: &status.BoxMetrics{InstanceID: "i-l"}})
+ if _, err := s.Put(ctx, key, raw, ""); err != nil {
+ t.Fatal(err)
+ }
+ retire := func(label string) bool {
+ k := "status/boxes/" + label + ".json"
+ body, etag, err := s.Get(ctx, k)
+ if err != nil {
+ return false
+ }
+ var cur status.Box
+ _ = json.Unmarshal(body, &cur)
+ if later.Sub(cur.GeneratedAt) <= retireAfter {
+ return false
+ }
+ return release.DeleteIfMatch(ctx, s, k, etag) == nil
+ }
+ if !retire(stopped.Label) {
+ t.Fatal("a stopped writer's old snapshot is retired")
+ }
+ if retire(legacyLabel) {
+ t.Fatal("a legacy writer that keeps refreshing is never retired")
+ }
+}
+
// A deterministic old-overwrite-then-upgrade case: permitted, and owned.
func TestOldWriterThatOverwroteThenUpgradedIsOwned(t *testing.T) {
s := release.NewDirStore(t.TempDir())
@@ -2917,9 +3183,12 @@ Under the fleet status section, after the `CARLOS_FLEET_BOX` bullet:
- Before a new box joins: `carlos status --check-label <machine-id>`
(read the id with `cat /etc/machine-id` over SSM after first boot,
before bootstrapping the agent). Exit 1 means another machine holds
- that label: give the box a new machine id
- (`rm /etc/machine-id && systemd-machine-id-setup && reboot`) and it
- comes back under a new label. Nothing else is needed.
+ that label: give the box a fresh machine id and prove it changed
+ (`old=$(cat /etc/machine-id); systemd-id128 new | tr -d '\n' >
+ /etc/machine-id; rm -f /var/lib/dbus/machine-id; test "$(cat
+ /etc/machine-id)" != "$old" && reboot`; `systemd-machine-id-setup`
+ alone may reuse an id), then `--check-label` on the new id must exit
+ 0. It comes back under a new label. Nothing else is needed.
- If an established box was displaced during a roll (it refuses and the
newer box holds its label): `--check-label` on the newer box (stop if
it names an open claim operation); `systemctl stop carlos-edge.service`
diff --git a/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md b/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md
index a11571015..84ec479f1 100644
--- a/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md
+++ b/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md
@@ -1,7 +1,7 @@
# Box identity, Option B: detect and refuse, no key migration
**Date:** 2026-10-06
-**Revision:** 5
+**Revision:** 6
- Rev 1 (7ff690c5) went to Astra (GPT-6, via codex); findings in
`CODEX-FINDINGS-BOX-IDENTITY-B-R1.md`: seven P1s, five P2s, accepted.
@@ -17,7 +17,13 @@
different meaning, the claim's box name bound by a signed box record.
This spec's digest is now called **`machine`**, and §4 defers the claim
reference to region HA.
-- **Rev 5 has not been reviewed.** Code line references are against the
+- Rev 5 (db5e1897): `CODEX-FINDINGS-BOX-IDENTITY-B-R5.md`, two P1s and
+ six P2s, accepted; changes marked "(codex B5-N)". The P1s: a stale
+ snapshot was not a lock against its own holder's renewal, so retirement
+ now replaces it with a tombstone by CAS before touching anything; and a
+ label with a region HA box record is bound to one instance for good, so
+ retirement hands a label only back to that instance.
+- **Rev 6 has not been reviewed.** Code line references are against the
branch after its merge of main (`fb59cb23`) unless marked otherwise.
**Discussion:** amadan carlos/platform #212
@@ -142,17 +148,24 @@ its corrupt-chunk preservation write, `internal/relay/meter.go:167-190`)
is therefore re-admitted at each call and aborts when the verdict
changes. Reads and lists are not gated.
-**What the deadline buys, honestly.** The production store is S3; the
-AWS SDK aborts an unsent request at the deadline, and a request already
-on the wire completes or fails server-side within seconds. The
-retirement barrier therefore adds a grace for that: `retireAfter = 3 *
-SnapshotPeriod + mutationTTL + requestGrace`, `requestGrace = 60s`,
-seventeen minutes after the label's last owned decision (the snapshot's
-`generated_at`, which every owned decision writes). `DirStore` ignores
-its context (`store.go:340`, `conditional_delete.go:62`) and is a
-one-box, one-process shape; it needs no barrier. Standalone processes
+**What the deadline buys, and what it assumes** (codex B4-3, B5-3). The
+production store is S3; the AWS SDK aborts an unsent request at the
+deadline. A request already on the wire is outside the client's control,
+and S3 publishes no maximum for how long such a request may take to
+land, so the barrier **assumes** it lands or fails within
+`requestGrace = 60s`, and the safety claim below is conditional on that
+assumption: `retireAfter = 3 * SnapshotPeriod + mutationTTL +
+requestGrace`, seventeen minutes after the label's last owned decision
+(the snapshot's `generated_at`, which every owned decision writes). The
+gate also refuses a call whose context deadline has already passed when
+it is admitted (a goroutine paused across expiry), so nothing is sent
+after expiry from this side. `DirStore` ignores its context
+(`store.go:340`, `conditional_delete.go:62`) and is a one-box,
+one-process shape; it needs no barrier. Standalone processes
(`relay serve`, root-side `adopt`) read the same file and expire at the
same instant; the barrier, not stopping the agent, is what drains them.
+An unconditional guarantee would need the store to fence writers, which
+S3's conditional writes do not do; this spec does not claim one.
The entry points, each of which today derives the label from
`metricsBoxLabel`, `BoxLabel` or `status.Label(readMachineID())`, and
@@ -211,10 +224,16 @@ refuser and has published nothing under the label.
1. `carlos status --check-label <newcomer machine id>`; stop here if it
names an open claim operation for the newcomer (§4).
-2. On the newcomer: `rm /etc/machine-id && systemd-machine-id-setup &&
- reboot`. It comes back under a new label and a new `machine`, decides
- that label at arm, and publishes. Nothing is retired; the holder never
- noticed.
+2. On the newcomer, give it a **fresh** machine id and prove it changed
+ (codex B5-8: `systemd-machine-id-setup` may reuse `/run/machine-id`
+ or the D-Bus id rather than generate one):
+ `old=$(cat /etc/machine-id); systemd-id128 new | tr -d '\n' >
+ /etc/machine-id; rm -f /var/lib/dbus/machine-id; test "$(cat
+ /etc/machine-id)" != "$old" && reboot`. After the reboot,
+ `--check-label $(cat /etc/machine-id)` on the new id must exit 0
+ before recovery is declared done. The box comes back under a new label
+ and a new `machine`, decides that label at arm, and publishes. Nothing
+ is retired; the holder never noticed.
**Displaced holder**: an old-release sibling overwrote an established
box's objects during a roll (§5); after the roll the sibling, now stamped
@@ -226,38 +245,52 @@ Here the sibling is the newcomer and its objects block the holder.
2. `systemctl stop carlos-edge.service` on the sibling (the agent's unit,
which runs `carlos agent`), and its relay unit where one is
installed. This starts the label's snapshot going stale.
-3. Regenerate the sibling's machine id and reboot, as above.
+3. Give the sibling a fresh machine id and reboot, as in the ordinary
+ case, and prove it changed.
4. After `retireAfter` (seventeen minutes from step 2),
`carlos status --retire-label <label>` (§2.7). It refuses while the
- snapshot is younger than `retireAfter`.
+ snapshot is younger than `retireAfter`, and it refuses when the label
+ has a region HA box record bound to an instance other than the one
+ that will reclaim it (below).
5. The established box's next tick finds not-found, creates, and is
- owned.
+ owned. Its region HA record, if it has one, names the same instance
+ and still verifies.
**A retired box's label**: a new box collides with a label whose holder
-is gone. `--check-label` shows a stale snapshot; `--retire-label` after
-`retireAfter`; the new box takes it on its next tick.
+is gone. If the label has no region HA box record, `--retire-label`
+after `retireAfter` frees it and the new box takes it. If it has one,
+the label belongs to the gone instance for good (§4): the new box gets a
+fresh machine id instead, as in the ordinary case.
-**How `--retire-label` deletes without a race** (codex B4-4). Acquisition
-needs the snapshot absent (§2.1, first row), so the snapshot is the lock:
+**How `--retire-label` deletes without a race** (codex B4-4, B5-1). The
+snapshot is the lock, but a stale snapshot is not a lock against its own
+holder, which may renew it at any age (§2.1, second row). So retirement
+first **takes** the lock:
1. Read the snapshot with its etag. Present and younger than
- `retireAfter`: refuse. Present and old enough: it stays in place,
- blocking every acquirer, while step 2 runs. **Absent** (a lone edges
- file): write a **tombstone** snapshot create-only,
- `{"generated_at": "0001-01-01T00:00:00Z", "label": "<label>",
- "machine": "retiring"}`; a CAS conflict means a box acquired the label
- in between, and the command stops and says so. The tombstone is
- foreign to every box (§2.1) and stale to every reader, so it blocks
- acquisition and counts for nothing.
+ `retireAfter`: refuse. Present and old enough, or absent: write the
+ **tombstone** snapshot, `{"generated_at": "0001-01-01T00:00:00Z",
+ "label": "<label>", "machine": "retiring"}`, with `ifMatch` on the
+ etag read (create-only when absent). A CAS conflict means the holder
+ renewed or a box acquired the label between the read and the write;
+ the command stops, deletes nothing, and says so. Once the tombstone is
+ in place it is foreign to every box, the former holder included, and
+ stale to every reader, so nothing can acquire or renew the label and
+ it counts for nothing.
2. Read the edges file with its etag and `DeleteIfMatch` it. A failed
- condition stops the command. (An edges file has no freshness of its
- own; `generation` is a change stamp, `edgesfile.go:560`.)
-3. `DeleteIfMatch` the snapshot (or the tombstone) on the etag from step
- 1, **last**. The label is free only now.
-
-Each object's location is resolved by its own rule and printed first
-(§2.7), and the holder's and refuser's `machine` and `instance_id` are
-printed with the result.
+ condition stops the command with the tombstone in place (the operator
+ re-runs). An edges file has no freshness of its own (`generation` is
+ a change stamp, `edgesfile.go:560`).
+3. `DeleteIfMatch` the tombstone on the etag from step 1, **last**. The
+ label is free only now.
+
+Before step 1 the command reads `control/boxes/<label>.json` and its
+bind (region HA §5.1). When a verified record exists, it refuses unless
+the instance id it names equals the instance id of the refuser that will
+reclaim the label (from the evidence, §2.4); a bound label is never
+handed to another instance (codex B5-2, §4). Each object's location is
+resolved by its own rule and printed first (§2.7), and the holder's and
+refuser's `machine` and `instance_id` are printed with the result.
### 2.4 Evidence
@@ -419,9 +452,12 @@ true` mails. Operators holding a grant are mailed; with none the
transition is logged and dropped (`alertwatch.go:194`, amadan #192). The
mail body (`alertMessage`, `alertwatch.go:285`) names the label and the
rule, never a `machine` or `instance_id`; those are on the operator fleet
-page and in `carlos status --live`, which show a `contested` chip, the
-holder's instance id (from the snapshot) and the refuser's (from the
-evidence). **Ruling R4** (§9): fleet.json says nothing.
+page and in `carlos status --live`, which project **all three rules**
+(codex B5-6): a `contested` chip for a label named by evidence, by an
+active `contested_until`, or by a snapshot/edges `machine` mismatch,
+with the holder's instance id (from the snapshot) and the refuser's
+(from the evidence) where known, and the reason otherwise. **Ruling R4**
+(§9): fleet.json says nothing.
## 4. The host lifecycle claim
@@ -444,16 +480,23 @@ Two specs now speak about box names, and this one defers (codex B4-1):
work when it cannot prove uniqueness". A box whose verdict leaves owned
mid-operation drops its execution lease and lets the claim's recovery
owner take over, as for any lost lease.
-- **The two agree on collisions.** Two legacy boxes with one label are
- two instances claiming one region-HA box id; the bind names exactly one
- record version and instance, so at most one of them can ever be bound,
- and this spec's refusal keeps the other from publishing anything the
- claim or the placer would read. A label freed by `--retire-label` and
- taken by another machine is a new instance under an old box id: region
- HA's record for the old instance does not verify for the new one, and
- the operator rebinds (`carlos ops box bind <label>`) as that spec says.
- `--check-label` prints the record and bind state so the operator sees
- both sides at once.
+- **The two agree on collisions, and a bound label is never reused**
+ (codex B5-2). Two legacy boxes with one label are two instances
+ claiming one region-HA box id; the bind names exactly one record
+ version and instance, so at most one of them can ever be bound, and
+ this spec's refusal keeps the other from publishing anything the claim
+ or the placer would read. Region HA's records and binds can never be
+ replaced or deleted (its §5.1 bucket policy), and `boxid.Verify`
+ (`internal/boxid/verify.go:72`) checks the unchanged record, not the
+ current publisher, so a label with a record is that instance's for
+ good. `--retire-label` therefore refuses to free a label with a
+ verified record unless the instance that will reclaim it (the refuser
+ named in the evidence) is the instance the record names: the
+ displaced-holder recovery gives a label back to its own instance, and
+ nothing else moves a bound label. A new box that collides with a bound
+ label, held or retired, gets a fresh machine id (§2.3). `--check-label`
+ prints the record's instance id and the bind state so the operator
+ sees this before acting.
- Twins (one machine id on two machines) share a `machine`; §2.1 detects
them by `instance_id` and refuses the second. Machine-id uniqueness is
a prerequisite (§8); this spec makes no clone-safety promise beyond
@@ -545,8 +588,11 @@ Guarantees, stated per state:
- Steering and the home map do not consume the verdicts (§2.6).
- A platform box with a split or prefixed status store does not arm
(§2.6); none exists today.
-- A label freed and retaken crosses region HA's bind; the operator
- rebinds (§4).
+- A label with a region HA box record can only ever return to the
+ instance the record names (§4); a new box colliding with one gets a
+ fresh machine id, which is the ordinary recovery anyway.
+- The retirement barrier is conditional on S3 landing an in-flight
+ request within `requestGrace` (§2.2).
Operator cost: one alert; a reboot for an ordinary collision, five steps
for a displaced holder; one `--check-label` per new box. No runbook step
@@ -709,3 +755,11 @@ override any of them.
| B4-9 the simulation rejects permitted mixed-version behaviour | P2 | accepted. Old-writer displacement is modelled; exclusivity asserted over all-new intervals; a deterministic old-overwrite-then-upgrade case (§5, §7) |
| B4-10 the recovery procedure cannot finish for an ordinary collision | P2 | accepted. Two procedures: ordinary (reboot the newcomer, nothing retired) and displaced holder (stop, regenerate, wait, retire, reclaim) (§2.3) |
| B4-11 landing and gate instructions inaccurate | P2 | accepted. Squash on the branch, push, describe, CI on the tip, `merge -expect`; `go build ./... && make test` plus cross-compiles (§8) |
+| B5-1 a stale snapshot is not a lock against its own holder | P1 | accepted. Retirement first replaces the snapshot with the tombstone by CAS on the etag read (create-only when absent); a renewal or acquisition winning that CAS stops the command with nothing deleted (§2.3) |
+| B5-2 label reuse breaks region HA's immutable record and bind | P1 | accepted. A label with a verified record is its instance's for good; `--retire-label` refuses unless the reclaiming instance is the record's; "the operator rebinds" withdrawn; a colliding new box gets a fresh machine id (§2.3, §4, §6.2) |
+| B5-3 the barrier rests on an unestablished S3 bound | P2 | accepted. The guarantee is stated as conditional on `requestGrace`; a call admitted with a passed deadline is refused; no unconditional claim (§2.2, §6.2) |
+| B5-4 snippets that fail before testing | P2 | accepted in the plan: the sampler fixture, `newAlertSinks`'s string argument, a root-package env helper, an opener adapter, a create body with `host` |
+| B5-5 integration coverage short of the claim | P2 | accepted in the plan: every snapshot field round-tripped, the real per-tick functions through `Gated` with an inner mutation counter, a first-attempt CAS conflict before relay revocation, the prefixed key asserted on the opener's store |
+| B5-6 operator surfaces omit two contention sources | P2 | accepted. All three rules projected on the fleet page and `--live` (§3) |
+| B5-7 the simulation retires a fresh legacy writer | P2 | accepted in the plan: retirement reads the stored snapshot; deterministic stopped-writer and fresh-legacy-writer cases |
+| B5-8 `systemd-machine-id-setup` may reuse an id | P2 | accepted. A fresh id from `systemd-id128 new`, the D-Bus id removed, the change proved, and `--check-label` on the new id before recovery is done (§2.3) |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-B-R5.md b/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-B-R5.md
new file mode 100644
index 000000000..decd59884
--- /dev/null
+++ b/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-B-R5.md
@@ -0,0 +1,70 @@
+Reviewed `db5e18974f21e9d649acf133a005419fffe15502` read-only. No files changed or tests run; the proposed tests were checked against existing definitions.
+
+| Round-4 finding | Assessment |
+|---|---|
+| B4-1 | Rename corrected; claim-reference recovery remains inconsistent with region HA. |
+| B4-2 | Namespace rule correctly moved inside every decision. Integration test remains incomplete. |
+| B4-3 | Absolute deadlines, expiry refusal and DirStore exclusion corrected. S3 completion bound remains assumed. |
+| B4-4 | Lone-edges acquisition race fixed; existing-holder renewal still races retirement. |
+| B4-5 | Empty-edges early return fixed; snapshots now contribute to completeness. |
+| B4-6 | Independent writes, intervening lease check and explicit `leaseErr` addressed. |
+| B4-7 | Meter, mail and conditional-delete helpers corrected; instance creation remains wrong. |
+| B4-8 | Some coverage added; several tests still cannot establish the claimed integration behavior. |
+| B4-9 | Displacement and deterministic upgrade case corrected; retirement simulation remains inaccurate. |
+| B4-10 | Recovery cases separated correctly; regeneration command does not guarantee a new identity. |
+| B4-11 | Squash/describe/CI/merge sequence and `go build ./... && make test` corrected. |
+
+1. **B5-1 — P1: a stale snapshot is not a lock against its existing owner.**
+
+ Retirement leaves the stale snapshot unchanged while deleting edges ([Spec:243](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md:243), [Plan:2620](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2620)). The same machine can renew that snapshot regardless of age ([Plan:558](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:558)). Sequence: retirement reads stale snapshot → holder renews → retirement reads and deletes edges → snapshot deletion conflicts. A live holder loses its edges file; its unchanged fingerprint can suppress republication ([edgesfile.go:560](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/edgesfile.go:560)).
+
+ **Fix:** conditionally replace the stale snapshot with a retirement reservation before touching edges. A renewal winning that CAS must stop retirement. Test this interleaving, including preservation of both live objects.
+
+2. **B5-2 — P1: label reuse does not invalidate the old region-HA identity, and rebinding is forbidden.**
+
+ The spec says the old record stops verifying and the operator rebinds ([Spec:451](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md:451)). But verification checks the unchanged record and bind, without the current publisher’s instance ID ([verify.go:72](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/boxid/verify.go:72)); placement joins by `BoxID` ([boxchoice.go:42](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/boxchoice.go:42)). Region HA explicitly prohibits replacing or deleting records and binds, including to permit rebinding ([Region-HA spec:215](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-04-region-ha-box-placement-design.md:215)).
+
+ **Fix:** preserve immutable claim identities. Specify checks tying the publishing/executing instance to the verified record, and refuse cross-instance reuse of a bound label unless region HA gains a separately reviewed replacement protocol. Test retirement followed by acquisition by another instance.
+
+3. **B5-3 — P2: the seventeen-minute barrier remains conditional on an unestablished backend bound.**
+
+ “Completes or fails server-side within seconds” is the premise behind `requestGrace` ([Spec:145](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md:145)). The implementation supplies a client context to S3; it establishes no server-completion maximum ([store.go:637](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/release/store.go:637)). [S3’s documented conditions](https://docs.aws.amazon.com/AmazonS3/latest/userguide/conditional-writes.html) check the mutated object, not the ownership snapshot. Task 3’s `DirStore` spy inspects deadlines but never models late completion ([Plan:826](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:826)).
+
+ **Fix:** state the safety guarantee as conditional on this assumption. To retain an unconditional retirement guarantee, require proven writer quiescence or fencing. Add pause-before-dispatch and completion-after-barrier tests.
+
+4. **B5-4 — P2: several exact snippets still fail before testing their intended behavior.**
+
+ | Proposed code | Evidence and fix |
+ |---|---|
+ | `newSampler(nil)` and `sm.record(...)` | Neither exists ([Plan:1387](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:1387)). Use `sampler` and its `tick` fixture, or seed `buf` ([metrics_loop.go:60](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/metrics_loop.go:60)). |
+ | `newAlertSinks(..., nil, nil, ...)` | Third argument is a string ([Plan:1628](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:1628), [alertsink.go:89](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/alertsink.go:89)). Pass `""`. |
+ | Root-package `envFunc(...)` | Helper exists only in package `host` ([Plan:2342](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2342), [fleetidentity_test.go:8](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/fleetidentity_test.go:8)). Define a root-package helper. |
+ | Pass `release.NewS3Store` directly as `open` | Its result is `*S3Store`, whereas the callback returns `release.Store` ([Plan:2616](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2616), [store.go:557](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/release/store.go:557)). Use an adapter closure. |
+ | Create instance with `{"name":"acme"}` | API requires `host`; this reaches a 400 ([Plan:2707](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2707), [apiinstances.go:642](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/apiinstances.go:642)). Use `{"host":"acme.go.tito.io","region":"ie"}` and assert the decoded host. |
+
+5. **B5-5 — P2: the claimed integration coverage still exceeds the tests.**
+
+ The snapshot test seeds one plain route and asserts only counts and machine identity, not aliases, sidecars, versions or database readings ([Plan:1267](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:1267)). The publisher test installs `Gated` itself, substitutes raw store calls for alerts/pruning, and omits usage, analytics, error shipping and relay wiring ([Plan:1378](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:1378)). The relay fake refuses the first Put, so no CAS retry occurs ([Plan:1434](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:1434)). The prefix test never inspects the underlying written key ([Plan:2349](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2349)).
+
+ **Fix:** exercise production wiring with an initially successful publication, then revoke and assert no further underlying mutations. Populate and round-trip every required snapshot field; force a first-attempt CAS conflict before relay revocation; retain the opener’s stores and assert the actual prefixed key.
+
+6. **B5-6 — P2: operator surfaces omit two sources of contention.**
+
+ `HostRows` and `printLiveBoxes` mark contention from evidence alone ([Plan:2622](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2622)). A snapshot/edges mismatch or observation-only `contested_until` can therefore block placement and fire an alert without appearing contested on those surfaces, contrary to [Spec:420](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md:420).
+
+ **Fix:** project all three contention rules into both surfaces. Test each independently; show instance IDs only where known.
+
+7. **B5-7 — P2: simulation retirement can delete a fresh legacy writer’s snapshot.**
+
+ Retirement uses `lastOwnedAt`, updated only by new-writer decisions ([Plan:2810](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2810)). Old writers refresh `GeneratedAt` without updating that timestamp ([Plan:2828](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2828)). After rollback, the simulation can thus “retire” an actively refreshed object.
+
+ **Fix:** evaluate retirement against the current stored snapshot, as the command does. Add deterministic stopped-writer and fresh-legacy-writer cases, and assert that valid retirement actually occurs.
+
+8. **B5-8 — P2: the recovery command can recreate the same machine ID.**
+
+ Both procedures rely on deleting `/etc/machine-id` and running `systemd-machine-id-setup` ([Spec:214](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/specs/2026-10-06-box-identity-detect-design.md:214), [Plan:2921](/home/paulca/amadan.net/carlos/platform-design-box-identity/docs/superpowers/plans/2026-10-06-box-identity-detect.md:2921)). On Debian 13, that tool first reuses `/run/machine-id`, D-Bus identity and other configured sources before generating randomness ([systemd manual](https://manpages.debian.org/trixie/systemd/systemd-machine-id-setup.1.en.html)).
+
+ **Fix:** specify an explicit fresh-ID procedure, verify that the ID changed, and run `--check-label` on its resulting label before declaring recovery complete.
+
+SPEC: NOT READY — P1s: B5-1, B5-2
+PLAN: NOT READY TO BUILD — P1s: B5-1, B5-2
\ No newline at end of file