amadan
Spec: replace refuses in-flight ids; compact joins the property alphabet
Addresses the delta review on #5. replace throws on any in-flight id, requires a seq-contiguous run within one lane, and compaction runs only over sendable, not-in-flight entries, otherwise an ack could delete never-sent content. The property test gains compact (overlapping an in-flight batch) and a crash between replace steps 1 and 2. Also: set isExcludedFromBackup on the account directory and pass .completeFileProtection with the write; M6 holds even if K5 ships after K3.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 file changed,
+22
−5
docs/superpowers/specs/2026-09-23-offline-kit.md+22 −5
CI failed — run details
diff --git a/docs/superpowers/specs/2026-09-23-offline-kit.md b/docs/superpowers/specs/2026-09-23-offline-kit.md| index 338e54b..7d24585 100644 |
| --- a/docs/superpowers/specs/2026-09-23-offline-kit.md |
| +++ b/docs/superpowers/specs/2026-09-23-offline-kit.md |
| @@ -218,7 +218,9 @@ Application Support/<bundle id>/accounts/<account.id>/ |
| ``` |
| - Everything is written by `NativeSealedStore` (§3.6). On iOS the file |
| - protection is `.complete`, and files are `isExcludedFromBackup`: the key |
| + protection is `.complete`, passed as `.completeFileProtection` in the same |
| + `write` options. `isExcludedFromBackup` is set on the `accounts/<id>/` |
| + directory, not per file, because atomic writes create new inodes. The key |
| cannot leave the device, so a backed-up copy could never be read anyway. |
| - **"Durable on return" means it survives a process kill** *(L2)*: the file is |
| written with `Data.write(options: .atomic)`, a temporary file renamed into |
| @@ -307,7 +309,17 @@ exercise every method that ships, which is the "one builds, one adopts" bar: |
| 2. delete the other replaced entries. |
| A crash after step 1 leaves duplicates only, never a gap and never |
| - reordering. Only a lane whose payloads tolerate duplicates may use |
| + reordering. |
| + |
| + **`replace` throws if any id is in flight**, exactly as `update` does |
| + (§5). The ids must be a seq-contiguous run within one lane. The merged |
| + entry gets a new UUID and inherits the lane and kind. Compaction runs |
| + only over sendable entries that are not in flight. Without this rule, a |
| + byte-cut batch in flight across a compaction would, on its `ack`, delete |
| + the merged `<oldest seq>.entry`, and with it the content of entries |
| + whose own files step 2 had already removed. |
| + |
| + Only a lane whose payloads tolerate duplicates may use |
| `replace`. Docs qualifies (Yjs integrates duplicates idempotently: docs |
| `internal/docs/handlers.go:879-880`). |
| - **No silent caps.** An app sets a per-lane byte ceiling. Exceeding it is a |
| @@ -450,8 +462,11 @@ it. |
| - **Accounts without a subject** *(M6)*. "Accept the first subject seen" |
| would disarm the guard for every account that exists today. Instead, |
| the first launch of a build that carries the kit marks every subject-less |
| - account session-ended. That happens before any outbox exists, so nothing |
| - is at risk, and the one re-sign-in records the subject. Apps hold no real |
| + account session-ended. When K5 ships in the same build as K3, that |
| + happens before any outbox exists. If it doesn't, subject-less accounts |
| + are still marked session-ended, and the outbox survives that state, so |
| + nothing is at risk either way. The one re-sign-in records the subject. |
| + Apps hold no real |
| data and Paul is the only user, so one sign-in per app is the whole cost. |
| (A `/native/whoami` endpoint read on the first online request would avoid |
| that sign-in. It is not proposed, because it is another endpoint for a |
| @@ -621,7 +636,9 @@ there. `RastrilloTestSupport` (§3.1) ships four primitives: |
| **The Docs property test (K3).** |
| - **Event alphabet:** edit; writer tick, *including between `command` and |
| - `enqueue`*; ack; lose-response; crash at any store operation; reopen and |
| + `enqueue`*; ack; lose-response; **compact**, sometimes while a batch |
| + overlapping the candidates is in flight, which must throw; crash at any |
| + store operation, including between `replace` steps 1 and 2; reopen and |
| apply the lane; reconnect. |
| - **Assertions, after every event and at the end:** |
| - I1 (§4.3); |