amadan
Box identity spec rev 3: answer Astra's round 2
Four P1s: the effective edges file and the sweep decide by the fresh snapshot's key shape, never by generation, and snapshot-less readers discard nothing; Step A records a proven id-to-label alias the join matches through; the steering identifier moves in two releases (labels at N except a contested pair, ids at N+1 with the rename rule) so an old converger is never handed a mass rename; the claim's fencing claim is withdrawn, uniqueness is a prerequisite and a twin latch refuses authority-bearing work. Three P2s: durable twin evidence under status/identity/, webhook delivery through the lease holder's metrics sinks, architecture cards from the snapshots with separate unread flags. Findings committed unedited as CODEX-FINDINGS-BOX-IDENTITY-R2.md. Rev 3 is not yet reviewed.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
2 files changed,
+272
−137
docs/superpowers/specs/2026-10-06-box-identity-collisions-design.md+232 −137docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-R2.md+40 −0
CI passed — run details
diff --git a/docs/superpowers/specs/2026-10-06-box-identity-collisions-design.md b/docs/superpowers/specs/2026-10-06-box-identity-collisions-design.md| index f478a11a1..e4d8376a5 100644 |
| --- a/docs/superpowers/specs/2026-10-06-box-identity-collisions-design.md |
| +++ b/docs/superpowers/specs/2026-10-06-box-identity-collisions-design.md |
| @@ -1,15 +1,19 @@ |
| # Box identity: key box objects by a collision-resistant id, keep the label for people |
| **Date:** 2026-10-06 |
| -**Revision:** 2 |
| +**Revision:** 3 |
| - Rev 1 (71112c9e) went to Astra (GPT-6, via codex); the findings are in |
| `CODEX-FINDINGS-BOX-IDENTITY-R1.md`. Four P1s, five P2s, one P3, all |
| - checked against the code and accepted. Changes are marked "(codex N)" and |
| - §11 records each disposition. |
| + checked against the code and accepted. Changes are marked "(codex N)". |
| +- Rev 2 (d668281f) went back; the findings are in |
| + `CODEX-FINDINGS-BOX-IDENTITY-R2.md`. Four P1s (three of them round-1 |
| + P1s judged still open), three P2s, all checked and accepted. Changes are |
| + marked "(codex R2-N)". Rev 3 has not been reviewed. §11 records every |
| + disposition. |
| **Discussion:** amadan carlos/platform #212 |
| -**Status:** draft, for Paul's review after Astra's second round. |
| +**Status:** draft. Rev 3 needs Astra's third round before Paul's review. |
| **Builds on:** the fleet status page (`internal/status`), the multi-region |
| ingress edges file (2026-08-20, Part 3), the steering converger |
| (`internal/steering`), nearest-region placement |
| @@ -154,14 +158,19 @@ func LabelForID(id string) (label string, ok bool) |
| - **Machine ids are assumed unique.** A cloned image that keeps |
| `/etc/machine-id` produces two boxes with one id, and they overwrite one |
| key rather than producing two objects, so §3.4's duplicate check cannot |
| - see it (codex 9). The writer checks instead: `WriteBox` already reads the |
| - current object for its etag; it now also parses it, and if that object is |
| - fresh and carries a non-empty `instance_id` different from this box's, |
| - this box has a twin. It logs, publishes the `identity` alert (§3.4) and |
| - keeps writing, so the twin is visible rather than silent. A box with no |
| - instance id (off-cloud) cannot make this check. The image build must |
| - clear `/etc/machine-id` so systemd regenerates it on first boot; the |
| - rollout checks the flagship's AMI recipe does (§9). |
| + see it (codex 9). Uniqueness is a **safety prerequisite**, not something |
| + the design recovers from (codex R2-4): the image build must clear |
| + `/etc/machine-id` so systemd regenerates it on first boot, and the |
| + rollout checks the flagship's and Tito's recipes do (§9). What the |
| + design adds is detection: `WriteBox` already reads the current object |
| + for its etag; it now also parses it, on the first read and on the CAS |
| + retry read (codex R2-5), and if that object is fresh and carries a |
| + non-empty `instance_id` different from this box's, this box has a twin. |
| + It keeps writing, so the twin stays visible, writes durable evidence for |
| + the alert (§3.4), and sets a process-wide **twin latch**: while set, the |
| + box refuses to arm or continue any authority-bearing work that names a |
| + box (the claim, §5), and `edgesFilePass` keeps publishing. A box with no |
| + instance id (off-cloud) cannot make this check. |
| - The label is unchanged. `Label` keeps its function and its table so the |
| public label of every existing box is stable through the roll. |
| @@ -187,10 +196,10 @@ to `Box`. `edgesFileKey` takes the id when present, else the label. `Box` |
| keeps the label for every surface that shows a box to a person. The new |
| field is part of the change gate like every field but `Generation`. |
| -Steering. `steering.edgesFileView` gains `BoxID`; `desiredRecord.Box` |
| -becomes `BoxKey(file)` (the id when present, else the label), so the |
| -Route53 `SetIdentifier` and the `dedupeRecords` key become the id (codex 1). |
| -The converger's handling of the identifier change is §3.5. |
| +Steering. `steering.edgesFileView` gains `BoxID`. The Route53 |
| +`SetIdentifier` and the `dedupeRecords` key move to the id in two |
| +releases, not one, so a rollback never hands an old converger a mass |
| +rename (codex 1, R2-3); the rule is §3.5. |
| A `BoxKey` helper, in `internal/edgesfile` for files and `internal/status` |
| for snapshots, returns the id if set, else the label. Both objects carry |
| @@ -201,7 +210,8 @@ both names; which one a reader matches on is §3.3. |
| Three steps, each in one package, each with one owner. |
| **Step A: snapshots** (`status.loadBoxesReport`, `fleet.go:238`). Returns |
| -the boxes plus a `Report{Duplicates, Superseded, Contested []string}`. |
| +the boxes plus a `Report{Duplicates, Superseded, Contested []string; |
| +Aliases map[string]string}`. |
| 1. Group by `box_id`. Two objects (two keys) with one id is a |
| **duplicate**: both are returned and flagged; `complete` is false. |
| @@ -210,45 +220,54 @@ the boxes plus a `Report{Duplicates, Superseded, Contested []string}`. |
| the same non-empty `metrics.instance_id`, they are one box seen through |
| an old key and a new key (a roll or rollback in progress). The fresher |
| is kept; the other is **superseded** and dropped from the returned |
| - slice, so nothing downstream counts it. If instance ids differ, or |
| - either is empty, both stand and the label is **contested** (two boxes, |
| - one old writer, or an off-cloud box mid-rollback); `complete` is false |
| - for the completeness readers. Contested is not Duplicate: the public |
| - feed shows both rows, because both are boxes. |
| + slice, so nothing downstream counts it. The pairing is recorded as a |
| + proven **alias** `id -> label` in `Report.Aliases`, whichever way the |
| + supersession went, so the join (Step C) keeps the identity evidence |
| + the dedupe removed from the rows (codex R2-2). If instance ids differ, |
| + or either is empty, both stand and the label is **contested** (two |
| + boxes, one old writer, or an off-cloud box mid-rollback); `complete` |
| + is false for the completeness readers. Contested is not Duplicate: the |
| + public feed shows both rows, because both are boxes. |
| 3. Everything else passes through unchanged. |
| -**Step B: edges files** (`edgesfile.Effective(files []Ident) (keep |
| -map[string]bool, contested []string)`, where `Ident` is `{Key, Box, BoxID, |
| -EIP, Generation}`). Every reader of `control/edges/` applies it to its |
| -listing before folding: homemap, steering's loader, the console's |
| -`readEdgesSnapshot`, `moveTargets`, `EdgeIPs`, `DeploymentRoutes`. This is |
| -what makes the object key not load-bearing; in rev 1 it was asserted, now |
| -it is a function (codex 3). |
| +**Step B: edges files** (`edgesfile.Effective(files []Ident, ev |
| +Evidence) (keep map[string]bool, contested []string)`, where `Ident` is |
| +`{Key, Box, BoxID, EIP, Generation}` and `Evidence` is Step A's aliases |
| +and the key shape of each box's fresh snapshot, or nil for a reader that |
| +has no snapshots). Every reader of `control/edges/` applies it to its |
| +listing before folding. This is what makes the object key not |
| +load-bearing; in rev 1 it was asserted, now it is a function (codex 3). |
| 1. Two files with one `box_id`: both kept, flagged duplicate. |
| 2. A file with no `box_id` and a file with one, same `box` label and the |
| - same non-empty `eip`: one box, old and new key. Two boxes never share an |
| - EIP. The newer `generation` is effective; the other is dropped. The |
| - dropped file's hosts do not fold, so the effective file alone decides |
| - what the box serves. On rollback the legacy file is rewritten by the |
| - box's first tick (§6), so it is the newer one. |
| + same non-empty `eip`: one box, old and new key. Two boxes never share |
| + an EIP. **Which is effective is decided by the snapshot, never by |
| + `generation`** (codex R2-1): the snapshot is written unconditionally |
| + every tick (`statusTick`), the edges file only on change, so a legacy |
| + file seeded into an old release's memory gate (`edgesfile.go:529`) can |
| + be the live writer's and still carry the older stamp. With evidence: |
| + the file whose key shape matches the box's fresh snapshot (by alias) |
| + is effective; the other is dropped and its hosts do not fold. Without |
| + evidence (homemap, steering): both are kept and both fold. They name |
| + one EIP, so every dial target is the same; only a host set can differ, |
| + and then the union is served, which is the behaviour an old reader has |
| + today. No snapshot-less reader ever discards a file. |
| 3. Same label, no `box_id` on one side, EIPs differ or either is empty: |
| both kept, label contested. |
| 4. Everything else kept. |
| **Step C: the join** (`EdgeIPs`, `DeploymentRoutes`, |
| `readLiveEdgesSnapshot`, `foldHomes` self-skip, `moveTargets`). After A and |
| -B, with `snapshots` and `files`: |
| - |
| -1. A file with a `box_id` matches the snapshot with that `box_id`. It never |
| - falls back to the label: a box writes both objects from one process, so |
| - its snapshot carries the id within one tick of its file, and a legacy |
| - snapshot under its label during that minute is either its own |
| - not-yet-deleted old object (superseded or about to be) or a colliding |
| - sibling's, which must not vouch for it. |
| -2. A file with no `box_id` matches by label, and only when exactly one |
| - snapshot carries that label after Step A. Two or more is ambiguous: no |
| - match, label contested. |
| +B, with `snapshots`, `files` and `Aliases`: |
| + |
| +1. A file with a `box_id` matches the snapshot with that `box_id`, or the |
| + snapshot whose label is `Aliases[box_id]` (a proven alias from Step A, |
| + codex R2-2). It never falls back to an unproven label: a legacy |
| + snapshot under its label that shares no instance id is either a |
| + colliding sibling's or unprovable, and must not vouch for it. |
| +2. A file with no `box_id` matches the snapshot carrying its label when |
| + exactly one does after Step A, or the snapshot whose id aliases to that |
| + label. Two or more candidates is ambiguous: no match, label contested. |
| 3. A snapshot with no file, or a file with no snapshot, keeps today's |
| meaning (`instancesplacement.go:120-150`: incomplete evidence for |
| eligibility, not live for `EdgeIPs`). |
| @@ -261,34 +280,49 @@ Contested, duplicate and flagged all make `BoxesComplete` false for |
| automatic eligibility, which is the posture `readLiveEdgesSnapshot` |
| already takes for anything it cannot prove. |
| -**The architecture page** (codex 6). `buildBoxCards` stops unioning |
| -`FleetBox` rows with `HostRow`s. It builds cards from `HostRows` alone |
| -(`Box` carries every field `FleetBox` has, and `Stale` is computed the |
| -same way), keyed by `BoxKey`, node id `"box:"+BoxKey`, `claimed` and |
| -`targetOf` likewise. `HostRow` gains `ID`. When the host read failed |
| -(`ArchBoxesUnread`) the page falls back to `FleetBox` rows keyed by label, |
| -and a label shared by two rows renders one card marked ambiguous. Card |
| -titles are the label; two cards with one label append the first four hex |
| -characters of the id. |
| +**The architecture page** (codex 6, R2-7). `buildBoxCards` stops |
| +unioning `FleetBox` rows with `HostRow`s by label. `ArchInput` gains |
| +`Boxes []status.Box` from `LoadBoxes`, the private snapshots themselves, |
| +which carry every field a card takes from `FleetBox` today (`Routes`, |
| +`Load`, `Region`, `archgraph.go:594-600`) and the id; `HostRow` |
| +(`view.go:830`) is not widened. Cards are keyed by `BoxKey`, node id |
| +`"box:"+BoxKey`, `claimed` and `targetOf` likewise. `archpage.go:53` |
| +separates the two reads: `fleetUnread` and `hostsUnread`. Only when the |
| +snapshot read failed does the page fall back to `FleetBox` rows keyed by |
| +label, and a label shared by two rows renders one card marked ambiguous. |
| +Card titles are the label; two cards with one label append the first four |
| +hex characters of the id. |
| ### 3.4 Duplicate detection is incomplete evidence, and how it alerts |
| -Three conditions, all from §3.3: a duplicate id; a contested label; a |
| -twin (§3.1). The status lease holder evaluates them in `BuildFleet` and |
| -writes one singly-owned object, `alerts/fleet/identity.json`, in |
| -`metrics.AlertState` shape with `Box: "fleet"` and one rule per condition, |
| -**every publish tick**, firing or not (codex 7). Ownership follows the |
| -status lease: whichever box publishes writes it, so a lease transfer |
| -cannot strand a firing rule, and clearing is just the next tick's write. |
| -The alert watcher (`alertwatch.go:97`) reads this one key alongside |
| -`alerts/boxes/*.json`, and treats an object older than three snapshot |
| -periods as all-clear, the same `BoxStale` rule the boxes use. Delivery is |
| -the existing path: operators holding a keymail grant are mailed |
| -(`alertwatch.go:187`), and the webhook when `CARLOS_ALERT_WEBHOOK` is set. |
| -The existing limitation stands and is named: with no grant and no webhook |
| -the transition is logged and dropped (`alertwatch.go:194`, amadan #192). |
| -The fleet page and `carlos status -live` show the condition as a chip on |
| -the rows involved. Nothing reaches fleet.json. |
| +Three conditions: a duplicate id and a contested label (§3.3, visible to |
| +whoever reads the prefix) and a twin (§3.1, visible only to the box that |
| +saw the foreign object before overwriting it). The twin needs durable |
| +evidence (codex R2-5): the detecting box writes |
| +`status/identity/<box_id>.json` `{instance_ids, seen_at}` on every tick |
| +it sees the twin, and the lease holder treats an entry older than three |
| +snapshot periods as cleared. The status lease holder evaluates all three |
| +in `BuildFleet` and writes one singly-owned object, |
| +`alerts/fleet/identity.json`, in `metrics.AlertState` shape with |
| +`Box: "fleet"` and one rule per condition, **every publish tick**, firing |
| +or not (codex 7). Ownership follows the status lease: whichever box |
| +publishes writes it, so a lease transfer cannot strand a firing rule, and |
| +clearing is the next tick's write. |
| + |
| +Delivery (codex R2-6) is two paths, both existing. Keymail: the console's |
| +alert watcher (`alertwatch.go:97`) reads this one key alongside |
| +`alerts/boxes/*.json`, treats an object older than three snapshot periods |
| +as all-clear, and mails operators holding a grant (`alertwatch.go:187`); |
| +with no grant the transition is logged and dropped (`alertwatch.go:194`, |
| +amadan #192). Webhook: the watcher has no webhook path; `CARLOS_ALERT_ |
| +WEBHOOK` is delivered from the box by the metrics loop's sinks |
| +(`metrics_loop.go:510`). The lease holder reuses those sinks: before it |
| +writes the identity object it reads the previous one, and a rule whose |
| +`Firing` changed is one `metrics.Event` delivered through the same |
| +`sinks.deliver`. The previous object is what dedupes a takeover: a new |
| +holder sees the state the old holder last wrote, not a blank. The fleet |
| +page and `carlos status -live` show the condition as a chip on the rows |
| +involved. Nothing reaches fleet.json. |
| ### 3.5 Writers |
| @@ -309,30 +343,50 @@ the rows involved. Nothing reaches fleet.json. |
| delete changes the etag and the delete refuses. A store that cannot |
| enforce the condition refuses too, and the object is left for the sweep. |
| Positive, non-empty evidence or nothing: an off-cloud box with no |
| - instance id leaves its legacy snapshot for the sweep. The check runs once |
| - per process start. |
| + instance id leaves its legacy snapshot for the sweep. The check runs on |
| + every tick until it ends in a delete, a not-found, or a mismatch (codex |
| + R2-1): a transient failure must not leave a legacy object behind to be |
| + seeded into an old release's gate on a later rollback. |
| - **The edges gate verifies against the bucket.** Every tenth tick with |
| no local change, `edgesFilePass` reads its own key. Missing, or different |
| from `*last` with Generation cleared: republish. Nothing else should |
| write an id key, so this is defence in depth, and it is also how a file |
| removed by the sweep or by hand comes back without waiting for a route |
| change. It does not fix the old release's gate; nothing can. |
| -- **The steering identifier change** (codex 1). When `SetIdentifier` moves |
| - from label to id, a box's records are deleted under one identifier and |
| - upserted under another in one pass. The converger learns a **rename**: a |
| - managed-but-unwanted record whose `(Name, Value, Region)` is also being |
| - upserted under a wanted identifier is a rename, applied as upsert then |
| - delete in the same change batch and exempt from the shrink count |
| - (`route53.go:207-214`). Without this a single-armed-box deployment |
| - could never flip: all its records would count as a shrink of 100%. |
| - While old and new boxes alternate holding the housekeeper lease, an old |
| - holder renames back to labels and a new one forward to ids. Each flip is |
| - one upsert-and-delete per record with a 60-second TTL, bounded by the |
| - roll. Rollback is the same flip once, in reverse, by the old release's |
| - converger, which sees the id-identified records as managed and unwanted; |
| - for a single-box deployment the old converger's shrink guard refuses |
| - that, and the records simply stay under id identifiers, still resolving, |
| - until an operator deletes them or the box rolls forward again. |
| +- **The steering identifier change** (codex 1, R2-3), in two releases. |
| + An old converger that finds every record under an identifier it does |
| + not want refuses the whole pass before any write (`route53.go:209`): |
| + three id-identified records against a shrink limit of two freezes DNS |
| + for that release, additions included. So no release may hand an old |
| + converger a mass rename, which rules out flipping in the release a box |
| + can be rolled back from. |
| + - **Release N (this spec).** The converger recognises both identifier |
| + shapes as owned. It keeps writing the **label** as `SetIdentifier` |
| + for every file whose label is unique in the fold, and uses the |
| + **id** only for files whose label is shared (a contested pair), where |
| + today one box's records are lost anyway. A rollback from N finds |
| + label identifiers everywhere except a live collision, and the old |
| + converger converges as before. If a collision is live at rollback, |
| + the old converger sees the pair's id-identified records as unwanted; |
| + for a fleet of four or more that is within the shrink limit and it |
| + renames them back (losing one box's records, as before this spec); |
| + for a smaller fleet it refuses, DNS stays as it is, still resolving, |
| + until the roll forward or an operator deletes those records. That is |
| + the one steering cost of rolling back with a live collision, and the |
| + runbook names it. |
| + - **Release N+1**, after every box is on N and N-1 is no longer a |
| + rollback target: `SetIdentifier` is the id for every file. The |
| + converger learns a **rename**: a managed-but-unwanted record whose |
| + `(Name, Value, Region)` is also being upserted under a wanted |
| + identifier is applied as upsert then delete in the same change batch |
| + and exempt from the shrink count (`route53.go:207-214`), so a |
| + single-armed-box deployment can flip. Rolling back from N+1 to N is |
| + safe because N owns both shapes and renames back the same way. |
| + - Old readers during the N roll keep today's faults for a colliding |
| + pair until they roll: an old converger dedupes the pair's records by |
| + label (`steering.go:318`), and an old home map skips the sibling's |
| + file as self (`homemap.go:547`). Nothing on the new release can fix |
| + an old reader; the roll fixes it. |
| - **The identity sweep** (codex 2, 3). The status lease holder runs it on |
| its publish tick, and `carlos fleet sweep` runs the same code from an |
| operator's machine with bucket credentials, for the case where no box is |
| @@ -341,12 +395,16 @@ the rows involved. Nothing reaches fleet.json. |
| days) is deleted with the edges file that matches it under §3.3 (by id, |
| else unambiguous label); a snapshot that Step A marked superseded is |
| deleted at once, in either direction (legacy superseded by id, or id |
| - superseded by legacy after a rollback), with the edges file Step B |
| - marked non-effective for the same box; an edges file with no snapshot at |
| - all is reported, never deleted automatically, because nothing can date |
| - it. `carlos fleet retire <id|label>` deletes both objects by hand after |
| - printing what it found. The deployment bucket is versioned, which makes |
| - a wrong delete recoverable but is not a substitute for the condition. |
| + superseded by legacy after a rollback), and with it the edges file of |
| + the **same key shape as the superseded snapshot**, when that file |
| + shares the effective file's EIP. The sweep never chooses an edges file |
| + by `generation` (codex R2-1): the superseded snapshot's shape says which |
| + writer has stopped, and only that writer's file goes. An edges file with |
| + no snapshot at all is reported, never deleted automatically, because |
| + nothing can date it. `carlos fleet retire <id|label>` deletes both |
| + objects by hand after printing what it found. The deployment bucket is |
| + versioned, which makes a wrong delete recoverable but is not a |
| + substitute for the condition. |
| ### 3.6 Step 2: the other per-box keys |
| @@ -394,12 +452,13 @@ Roll order does not matter. Each pair: |
| | new box | new reader | by id | |
| | colliding pair, both old | any | still collides until one rolls | |
| | colliding pair, one rolled | new reader | the rolled box has its own key and joins by id. The legacy objects are the sibling's: its `instance_id`/`eip` differ, so the guard leaves them and Step A marks the label contested. Eligibility is incomplete and the `identity` alert fires until the sibling rolls | |
| -| colliding pair, one rolled | old reader | the legacy objects are now the sibling's alone, so the old reader sees two boxes correctly for the first time | |
| -| one box, first minutes after roll | new reader | id snapshot and legacy snapshot share `instance_id`: superseded (A2). Legacy file and id file share `eip`: the newer is effective (B2). Then the guard deletes both legacy objects | |
| +| colliding pair, one rolled | old reader | the status feed and fleet page show two boxes correctly for the first time: the legacy snapshot is the sibling's alone. Old steering and an old home map still collapse the pair (§3.5) until they roll (codex R2-3) | |
| +| one box, first minutes after roll | new reader | id snapshot and legacy snapshot share `instance_id`: superseded, alias recorded (A2). Legacy file and id file share `eip`: the id file is effective because the fresh snapshot is id-shaped (B2). Then the guard deletes both legacy objects | |
| One release of readers accepting both shapes is this release. The label |
| path (A2, B2, C2) stays for at least one more release and is removed only |
| -when the sweep reports no legacy key in production. |
| +when the sweep reports no legacy key in production. The steering |
| +identifier has its own two-release boundary (§3.5). |
| Nothing customer-visible changes. The public label is the same string. |
| fleet.json's shape is unchanged. The instances API's `served_by.box` keeps |
| @@ -428,10 +487,15 @@ widened it): |
| label through the fleet page; |
| - a box whose id is empty (§3.1) refuses to arm any claim-driven work, the |
| same way `resolveFleetIdentity` refuses an invalid fleet identity; |
| -- the claim relies on machine-id uniqueness, which §3.1 states, the image |
| - recipe enforces, and the twin check detects but cannot prevent. The |
| - claim's own fencing (execution lease, self-fence) is what bounds a twin's |
| - damage, not the id; |
| +- a box whose twin latch is set (§3.1) refuses the same work, and drops |
| + any execution lease it holds, until the latch clears; |
| +- the claim relies on machine-id uniqueness as a **prerequisite** (codex |
| + R2-4). Nothing in the claim distinguishes twins: `generation.go:31` |
| + compares the box string both twins hold, the execution lease is keyed |
| + by it and is liveness only (claim spec lines 1397-1408), and ordinary |
| + serving holds no lease at all (line 1446). The twin check and latch are |
| + detection and refusal, not fencing, and this spec makes no clone-safety |
| + promise; |
| - step 1 of this spec lands first so the identity exists when the claim's |
| plans build on it. |
| @@ -443,40 +507,46 @@ after a while may disagree with the legacy ones (codex 3). The protocol: |
| 1. Roll the box back. Its first status tick writes the legacy snapshot |
| (unconditional, `statusTick`). Its first edges tick finds no legacy |
| - file (the forward run deleted it) and publishes one, newer than the |
| - id-keyed file; or finds the undeleted legacy file, seeds its gate from |
| - it, and leaves it, in which case the legacy file is the older one until |
| - a route changes. |
| -2. On any box still on the new release, the next publish tick's sweep |
| - marks the id-keyed snapshot superseded (A2, same `instance_id`, legacy |
| - fresher) and the id-keyed file non-effective (B2, same `eip`) or, in |
| - the seeded-gate case above, keeps the id file effective until the |
| - legacy one is rewritten. Both id-keyed objects are then deleted |
| - conditionally. |
| + file (the forward run deleted it, and keeps trying until it has) and |
| + publishes one; or, if a legacy file somehow survived, seeds its gate |
| + from it (`edgesfile.go:529`) and leaves it unchanged until a route |
| + changes. Either way the legacy file is the live writer's, whatever its |
| + `generation` says, and that is why §3.3 B2 and the sweep decide by the |
| + snapshot's shape (codex R2-1). |
| +2. On any box still on the new release, the next publish tick marks the |
| + id-keyed snapshot superseded (A2: same `instance_id`, legacy fresher), |
| + records the alias, and so makes the legacy file effective (B2) and |
| + joinable (C1 by alias, C2). The sweep then deletes the id-keyed |
| + snapshot and the id-keyed edges file, conditionally. The live writer's |
| + legacy file is never a candidate. |
| 3. If every box rolled back, nothing on a box runs the sweep. The rollback |
| runbook step is `carlos fleet sweep` from the operator's machine, with |
| the new CLI and bucket credentials, once after the last box. Until it |
| runs, an old console shows the id-keyed snapshot as a stale second row |
| - and `sumInstances` counts it; an old home map and steering see two |
| - files with one EIP and fold both, and on a host conflict pick by sorted |
| - key, which is wrong only if the two files disagree, which the sweep |
| - step bounds to minutes. |
| + and `sumInstances` counts it; an old home map and steering fold both |
| + files, which name one EIP, so every dial target is right and only a |
| + host set can be over-served. Steering identifiers are labels at N |
| + (§3.5), so the old converger converges; the one exception is a live |
| + collision, named there. |
| 4. An off-cloud box (no `instance_id`) cannot be deduped by A2. Its stale |
| id-keyed snapshot stays until `retiredAfter` or `carlos fleet retire`. |
| - Its edges file is still deduped by B2 (EIP). This is the one case §6 |
| - does not make automatic, and the runbook says so. |
| + Its edges files are both kept by B2 (no evidence), both fold, same EIP. |
| + This is the one case §6 does not make automatic, and the runbook says |
| + so. |
| The rolled-back box's objects are readable by every reader: `label`, |
| `box`, `eip`, `hosts` are unchanged. Nothing on the new release writes a |
| -shape the old release cannot parse. Steering on rollback is §3.5. |
| +shape the old release cannot parse. |
| ## 7. Rollback and roll: the invariant |
| Across every state in §4 and §6: a live box is counted for at most one |
| -row, its EIP is in the edge set, and its hosts fold from exactly one file; |
| -a retired or superseded object counts for nothing; and anything the |
| -readers cannot prove makes automatic eligibility incomplete rather than |
| -wrong. §8's simulation asserts exactly this. |
| +row and its EIP is in the edge set; every file that folds for it names |
| +its own EIP, and a snapshot-aware reader folds exactly one; a retired or |
| +superseded object counts for nothing; no reader ever deletes or discards |
| +the live writer's object; and anything the readers cannot prove makes |
| +automatic eligibility incomplete rather than wrong. §8's simulation |
| +asserts exactly this. |
| ## 8. Test plan |
| @@ -500,19 +570,31 @@ Unit, `internal/status`: |
| Unit, `internal/edgesfile`, `internal/host`: |
| -- `Effective`: duplicate id; legacy-plus-id same EIP, newer generation |
| - wins in both directions; different EIPs both kept and contested; a |
| - mismatched `box`/`box_id` flagged. |
| +- `Effective`: duplicate id; legacy-plus-id same EIP with evidence, the |
| + snapshot's shape wins in both directions and an older-generation legacy |
| + file still wins after a rollback; the same pair without evidence keeps |
| + both; different EIPs both kept and contested; a mismatched |
| + `box`/`box_id` flagged. |
| - `edgesFilePass` writes the id key; `box_id` is in the gate; the |
| tenth-tick verify republishes a missing or foreign body. |
| - Legacy cleanup: deletes only on non-empty matching evidence; refuses |
| when the etag changed between read and delete (a fake |
| `ConditionalDeleter`); refuses on a store without conditional delete; |
| - runs once per start. |
| + retries each tick after a transient failure and stops after a delete, |
| + a not-found or a mismatch. |
| - `EdgeIPs`, `DeploymentRoutes`, `moveTargets`: the §4 matrix, plus the |
| - ambiguous-label case (two snapshots, one legacy file: no match). |
| -- Steering: a rename is one upsert-and-delete batch, exempt from the |
| - shrink count; a single-box flip converges; `dedupeRecords` keys by id. |
| + ambiguous-label case (two snapshots, one legacy file: no match), plus |
| + the alias case (id file, legacy snapshot, proven alias: match). |
| +- Steering at N: labels for unique files, ids for a contested pair, both |
| + shapes owned, an old-shape fixture converges with no shrink refusal. |
| + At N+1: a rename is one upsert-and-delete batch exempt from the shrink |
| + count; a single-box flip converges; `dedupeRecords` keys by id. |
| +- The twin check: fires on the first read and on the CAS retry read; |
| + writes `status/identity/<id>.json`; sets the latch; the latch refuses |
| + claim work and clears when the evidence expires. |
| +- The sweep deletes the superseded shape's edges file and never the |
| + effective one, in a rollback fixture where the legacy file carries the |
| + older generation. |
| Unit, `internal/console`, `internal/edge`: |
| @@ -520,11 +602,14 @@ Unit, `internal/console`, `internal/edge`: |
| flagged each set `BoxesComplete=false` and log once. |
| - `foldHomes`: self-skip by id; two same-label files with different ids |
| both fold; a non-effective file does not. |
| -- `buildBoxCards`: two boxes with one label give two cards from |
| - `HostRows`; the `FleetBox` fallback gives one ambiguous card; `targetOf` |
| - and `claimed` resolve to `"box:"+id`. |
| +- `buildBoxCards`: two boxes with one label give two cards from the |
| + snapshots, with counts and load; the `FleetBox` fallback gives one |
| + ambiguous card only when the snapshot read failed; `targetOf` and |
| + `claimed` resolve to `"box:"+id`. |
| - The alert watcher reads `alerts/fleet/identity.json`, mails on a |
| - transition, clears on an all-clear or a stale object. |
| + transition, clears on an all-clear or a stale object. The lease holder |
| + delivers a transition through the metrics sinks once, and a new holder |
| + taking over a firing state does not deliver it again. |
| Mixed-version goldens: a committed legacy-shape object for each prefix, |
| parsed by every new reader; a committed new-shape object asserted to keep |
| @@ -549,15 +634,18 @@ thousands of seeds, asserting §7's invariant at every step. |
| box, no `duplicate` or `contested` chip once its sibling, if any, has |
| rolled. |
| 4. Watch the lease holder's log for the sweep's first pass: the rolled |
| - boxes' legacy keys disappear, nothing else does. Watch the steering log |
| - for renames, not shrink refusals. |
| + boxes' legacy keys disappear, nothing else does. Steering identifiers |
| + do not move at N unless a collision is live. |
| 5. Roll the console. Nearest-region eligibility keeps reading, now by id. |
| 6. After every box is on the release and the sweep reports no legacy key, |
| file the step-2 plan (registry snapshots first) and record the §5 |
| ruling on the claim branch. |
| -7. One release later, remove the label path from §3.3. |
| +7. Release N+1, once N-1 is no longer a rollback target: steering |
| + identifiers move to the id with the rename rule (§3.5). |
| +8. One release later again, remove the label path from §3.3. |
| -Rollback is §6; its runbook step is `carlos fleet sweep`. |
| +Rollback is §6; its runbook step is `carlos fleet sweep`, and the one |
| +cost it cannot remove is a live collision's steering records (§3.5). |
| ## 10. Open questions for Paul |
| @@ -589,3 +677,10 @@ Rollback is §6; its runbook step is `carlos fleet sweep`. |
| | R1-8 step 2 contradicts bucket-private | P2 | accepted. Store-door read scope corrected; step 2 split and gated on a ruling; `metricsview` and the cursor named (§2.4, §3.6, §10) | |
| | R1-9 claim ruling incomplete; clones overwrite | P2 | accepted. Every box-naming field listed; empty id refuses to arm; uniqueness assumed, enforced by the image recipe, detected by the twin check (§3.1, §5, §9) | |
| | R1-10 store-door readability, `ValidTunnelName`, 11% | P3 | accepted. All three corrected (§1, §2.4, §3.1) | |
| +| R2-1 the sweep can delete the live writer's edges file when rollback seeds an older legacy file | P1 | accepted. Effective-file choice and the sweep decide by the fresh snapshot's key shape, never by `generation`; snapshot-less readers discard nothing; the forward guard retries until done (§3.3 B2, §3.5, §6) | |
| +| R2-2 snapshot dedupe breaks the join | P1 | accepted. Step A records a proven `id -> label` alias; C1 and C2 match through it (§3.3) | |
| +| R2-3 an old converger freezes on id identifiers; old readers still collapse a pair | P1 | accepted. Two-release boundary: N writes labels except for a contested pair and owns both shapes; N+1 flips with the rename rule; old readers' faults during the roll named (§3.2, §3.5, §4, §9) | |
| +| R2-4 claim fencing does not bound twins | P1 | accepted. The fencing claim is withdrawn; uniqueness is a prerequisite; the twin latch refuses authority-bearing work; no clone-safety promise (§3.1, §5) | |
| +| R2-5 twin observations do not reach the alert writer | P2 | accepted. Durable `status/identity/<id>.json` evidence with expiry; the check runs on the CAS retry read too (§3.1, §3.4) | |
| +| R2-6 the watcher has no webhook path | P2 | accepted. Keymail via the watcher; webhook via the lease holder's own metrics sinks on a transition, deduped against the previous object (§3.4) | |
| +| R2-7 architecture cards need snapshot fields; one unread flag covers two reads | P2 | accepted. Cards from `status.Box` via `LoadBoxes`; `fleetUnread` and `hostsUnread` separated (§3.3) | |
diff --git a/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-R2.md b/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-R2.md| new file mode 100644 |
| index 000000000..bd0956ef1 |
| --- /dev/null |
| +++ b/docs/superpowers/specs/CODEX-FINDINGS-BOX-IDENTITY-R2.md |
| @@ -0,0 +1,40 @@ |
| +Reviewed revision 2 at `d668281f` against code at `04cd2d78`, plus both claim branches via `git show`. No files changed. |
| + |
| +Round-1 dispositions: **R1-1, R1-3 and R1-4 remain open.** R1-2 closes the original read/delete race: `DeleteIfMatch` enforces the observed revision and refuses unsupported stores. R1-5, R1-8 and R1-10 are addressed. R1-6, R1-7 and R1-9 are only partially addressed. |
| + |
| +1. **P1 — The rollback sweep can delete the live writer’s edges file.** |
| + **Claim:** §3.3B selects by generation; §3.5 deletes the non-effective file; §6 says both ID objects are deleted. These disagree when rollback seeds an older legacy file. |
| + **Evidence:** [host/edgesfile.go:529](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/edgesfile.go:529) seeds that file; [line 491](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/edgesfile.go:491) suppresses unchanged writes indefinitely. The legacy snapshot becomes newest while the ID edges file remains newest. Following §3.5 deletes the live legacy edges file and leaves the obsolete ID file orphaned. Conditional deletion succeeds because the legacy file has not changed. |
| + **Fix:** establish the active writer’s format before deleting either edges object. Rollback must force and verify a legacy publication, then remove the ID pair. A generation timestamp alone cannot establish supersession. |
| + |
| +2. **P1 — Snapshot deduplication still breaks the mixed-shape join.** |
| + **Claim:** §3.3A drops the superseded snapshot; C1 requires an exact ID match. |
| + **Evidence:** After the rollback above, A retains only the legacy snapshot while B retains the ID edges file. C cannot join them. Unmatched files lose their addresses in [edgesfile/fold.go:84](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/edgesfile/fold.go:84) and their deployment-route protection at [line 158](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/edgesfile/fold.go:158). This can persist until a route changes, contradicting §7. |
| + **Fix:** preserve a proven ID alias when snapshots share a non-empty instance ID. Deduplicate displayed rows without discarding identity evidence needed by the join. |
| + |
| +3. **P1 — DNS rollback can freeze convergence, and mixed old readers still collapse collisions.** |
| + **Claim:** §3.5 describes reverse renames or harmless surviving records; §4 says old readers see the colliding pair correctly. |
| + **Evidence:** With three ID-keyed managed records, an old converger wants three label-keyed replacements. All three are unwanted; the limit is two. [route53.go:209](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/steering/route53.go:209) returns **before every write**, blocking subsequent additions and updates too. Separately, old [steering.go:318](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/steering/steering.go:318) still deduplicates colliding labels, and old [homemap.go:547](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/edge/homemap.go:547) skips the sibling as self. |
| + **Fix:** define a compatible-reader rollout boundary and an executable reverse DNS migration before handing convergence back to an old release. Bucket sweeping does not repair DNS identifiers. |
| + |
| +4. **P1 — Claim fencing does not bound damage from identical machine IDs.** |
| + **Claim:** §5 says execution leases and self-fencing bound a twin’s damage. |
| + **Evidence:** `feat/hostclaim-library:internal/hostclaim/generation.go:31` checks executor equality using the same box string both twins possess. On `design-replica-ownership`, `2026-10-02-host-lifecycle-claim-design.md:1397` keys the execution lease by that string; lines 1406–1408 explicitly describe it as liveness-only, and line 1446 exempts ordinary serving from leases. Neither mechanism distinguishes twins. |
| + **Fix:** remove the claimed fencing guarantee. Either make uniqueness an explicit safety prerequisite with no clone-safety promise, or introduce independently fenced writer ownership. Detected twins should refuse authority-bearing work. |
| + |
| +5. **P2 — Twin observations have no defined route to the sole alert writer.** |
| + **Claim:** `WriteBox` detects twins, while only the status lease holder evaluates and writes the fleet alert. |
| + **Evidence:** [snapshot.go:742](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/status/snapshot.go:742) returns only an error and overwrites the observed object. [agent.go:2931](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/agent.go:2931) exits for non-publishers; `BuildFleet` subsequently reads only surviving snapshots. A third box holding the lease cannot recover the overwritten observation. |
| + **Fix:** specify durable, private twin evidence that the lease holder consumes, including expiry and clearing. Check both reads in `WriteBox`’s CAS retry path. |
| + |
| +6. **P2 — The claimed webhook delivery path does not exist.** |
| + **Claim:** §3.4 says the existing watcher delivers identity alerts through `CARLOS_ALERT_WEBHOOK`. |
| + **Evidence:** [alertwatch.go:103](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/alertwatch.go:103) requires mail delivery; its transition handler sends keymail only. Webhooks run separately through [metrics_loop.go:510](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/host/metrics_loop.go:510). Writing another `AlertState` object does not invoke that path. |
| + **Fix:** explicitly connect identity transitions to webhook delivery, including takeover deduplication, or state that delivery is keymail-only. |
| + |
| +7. **P2 — The architecture-page inputs remain insufficient.** |
| + **Claim:** §3.3 needs only `HostRow.ID` to build complete cards and uses `ArchBoxesUnread` to detect a failed host read. |
| + **Evidence:** [view.go:830](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/view.go:830) carries neither route counts nor `Load`; cards currently obtain both from `FleetBox` at [archgraph.go:594](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/archgraph.go:594). [archpage.go:53](/home/paulca/amadan.net/carlos/platform-design-box-identity/internal/console/archpage.go:53) sets `ArchBoxesUnread` when **either** read fails, and passes it only to the rendered page. |
| + **Fix:** extend the private card input with the required snapshot fields and separate host-read completeness from fleet-read failure. |
| + |
| +**Verdict: not ready. P1s: rollback sweep deletion, mixed-shape joins, steering rollout/rollback, and the twin-fencing guarantee.** |
| \ No newline at end of file |