diff --git a/.gitignore b/.gitignore index 65ddcaf1c4..f26e74136c 100644 --- a/.gitignore +++ b/.gitignore @@ -3,6 +3,10 @@ /dist/ /admin-web/dist/ +# Python cache +__pycache__/ +*.pyc + # lefthook-generated hook scripts (machine-specific) .hooks/ diff --git a/docs/formal/nip-rs-unread/NOTE.md b/docs/formal/nip-rs-unread/NOTE.md new file mode 100644 index 0000000000..7472c3dca3 --- /dev/null +++ b/docs/formal/nip-rs-unread/NOTE.md @@ -0,0 +1,698 @@ +--- +title: "NIP-RS manual-unread: bounded exhaustive model — candidates A vs B" +tags: [nostr, nip-rs, read-state, formal-model, buzz] +status: active +created: 2026-07-16 +--- + +# NIP-RS manual-unread encoding model + +Bounded exhaustive model comparing two candidate CRDT encodings for a +manual mark-as-unread override layer within NIP-RS read state. + +## Run + +```bash +python3 exhaustive.py +python3 mutation.py +``` + +Both scripts are deterministic and exit 0 on success. + +## Context + +NIP-RS v1 encodes read state as grow-only `max(timestamp)` frontiers per +context. Manual mark-as-unread requires a second source of truth (an +override layer) because the frontier cannot be lowered — a lower value is +indistinguishable from a stale replica under `max()` merge. + +The override layer must converge across devices, survive legacy client +rewrite cycles, and remain bounded within the existing 32 KiB plaintext +budget. Two candidate encodings are modeled: + +- **A — lexicographic operation register:** per context, one register + `{counter, client_tiebreak, op, baseline}` in a NEW top-level field. +- **B — two grow-only counters + baseline:** per context, `S` (set + counter), `C` (clear counter), `B` (frontier-at-set-time) encoded as + sibling keys under `contexts`. + +## Model universe + +- 2 upgraded devices + 1 legacy device +- 2 contexts (`c0`, `c1`) +- Actions: mark-unread, mark-read (with frontier advance), + advance-frontier, compact, reinstall (client_id loss), + deliver (including duplicate/replay) +- BFS over canonical global states with interleaved actions and deliveries + (not phased), depth-bounded +- All delivery permutations of published blobs at terminal states +- Multi-slot union (split blob across 2 slots, deliver separately) +- Directed deep-history check: compact → new local actions (counter + reuse) → delayed stale delivery, over a 672-point parameter cube + (stale `(S,C,B)` × post-compaction frontier × 7 action sequences × + 2 tie policies × 1 delivery shape). The prior 2,016-point count + included two duplicate split-delivery shapes (`split_fwd`/`split_rev`) + that became semantically identical to `single` once the atomic-grouping + rule made a single-context compliant split always whole-register+empty; + collapsed to one meaningful shape without loss of register-level + coverage. +- Cross-device compaction transparency check: same tombstone, delivered + to an unrelated device with its own live concurrent state, over a + 312-point parameter cube (stale `(S,C,B)` × post-compaction frontier × + 4 fresh-frontier values × 2 tie policies), plus a monotonicity lemma + over 1,728 points (2 tie policies × 4×4×3×3 receiving-register/frontier + combinations × 6 ceiling values) proving the ceiling can never + *strengthen* a receiving register's set-counter standing +- States explored: 7,129 per tie policy (14,258 total) +- Published-state merge closure: every override is canonicalized against + the device's own effective frontier at serialization time before + hitting the wire (mandatory, not optional) — live unchanged, dead + folded to the tombstone floor, virgin omitted. Checked over a directed + witness (Thufir's exact dead+dead pair) plus a general search: every + pairwise join of a bounded cube of 300 independently-dead published + states (156 clear-wins + 144 set-wins = 300 total across both tie + policies), including a one-hop relay republication to cover + delayed/multi-hop delivery — 45,074 pairs checked total (156² + 144² + + 2 directed witnesses) + +## Invariants checked + +| # | Invariant | A | B (clear-wins) | B (set-wins) | +|---|-----------|---|-----------------|--------------| +| I1 | Join associative/commutative/idempotent | PASS | PASS | PASS | +| I2 | Convergence (all delivery orders) | not exercised | PASS | PASS | +| I3 | No frontier regression | not exercised | PASS | PASS | +| I4 | Concurrent set/clear winner stable | not exercised | PASS | PASS | +| I5 | Compaction: no loss, no resurrection (immediate merge-back) | n/a | PASS | PASS | +| I5c | Deep-history: compact → reuse → delayed stale delivery (same-device replay) | n/a | PASS | PASS | +| I5d | Cross-device compaction transparency (suppress-only, not zero-divergence) | n/a | PASS | PASS | +| I5e | Published-state merge closure: dead+dead join stays inactive | n/a | PASS | PASS | +| I6 | Replay harmless | not exercised | PASS | PASS | +| I7 | Legacy rewrite safety | **FAIL** (witness) | PASS | PASS | +| I8 | Bounded key growth (3 keys/ctx live, 1 key/ctx tombstone) | n/a | PASS | PASS | +| I9 | DeviceA counter absorption | PASS | n/a | n/a | + +Note: Candidate A is exercised only for I1, I7, and I9. BFS/convergence, +frontier-regression, concurrent-winner, and replay tests (I2–I4, I6) are +Candidate B-only; adding A variants would fail minimalism since A is already +dead on I7 (legacy-rewrite erasure). + +I5 covers the immediate compacted-vs-pre-compaction merge shape (both +merge orders). I5c is the same-device deep-history property this round +was originally opened to close: it directly targets the ~9-transition +history a depth-4 BFS cannot structurally reach (compact → new local +set/clear → delayed stale delivery, including from a second slot), +asserting that compaction never resurrects a dead override or drops a +live one **when the delayed delivery is the compacting device's own +pre-compaction ancestor** (or an exact copy of it, e.g. a peer that +never advanced past the original snapshot). + +**I5c does not cover, and NOTE.md previously overstated, the +cross-device case.** Compaction is a storage optimization from the +compacting device's own point of view — its dead register's baseline +`B` was frontier-relative to *that device's* history, and dropping `S` +in favor of the `C` ceiling is safe against replays of *its own* past. +But once published, the tombstone's `C` ceiling is globally comparable +via componentwise `max()`, while the baseline-relative death that +produced it is not. I5d proves the resulting property precisely: +merging in a tombstone can **suppress** — never resurrect, per the +`test_tombstone_merge_monotonic` structural lemma — a different +device's concurrent fresh set whose own counters happen to be at or +below the tombstone's ceiling, and the suppression always recovers with +one more local mark-unread (verified replay-stable against the same +tombstone). This is a one-shot false-negative risk, not a correctness +violation of the CRDT join (idempotent/commutative/associative still +hold per I1) and not new: an *uncompacted* stale explicit clear already +suppresses a fresh concurrent set under clear-wins with no compaction +anywhere (verified directly — see "Tie policy evidence" below); the +tombstone extends the same false-negative-preferring shape to +baseline-dominated dead sets that were never explicitly cleared. + +**I5e — published-state merge closure — is a protocol requirement, not +an optimization.** I5d's suppress-only guarantee assumes the tombstone +was actually on the wire before the merge. Nothing forces that: +`compact_b()`/`do_compact` are a local storage-GC transition a device +may or may not have called before it serializes. Without a mandatory +canonicalization step, `publish_blob()` can emit a register's *raw* +`(S, C, B)` — dead by construction (baseline-dominated, clear-dominated, +or a clear-wins tie) but not yet folded into the tombstone's +globally-comparable `C` ceiling. Two such raw-dead registers, published +by two different devices for unrelated reasons, can componentwise-max +into a **live** join: each register's `S` and `B` came from a different +device history, and the merge recombines them independent of either +history's own death cause. This is a distinct hazard from I5d's +suppression (I5d is a live register losing to a stale dead one; I5e's +witness is two dead registers producing a live one) but the same root +cause — components taken from independent histories can be +recombined in ways neither history's own frontier ever permitted. + +**Fix: canonical publication is mandatory, not advisory.** +`DeviceB.publish_blob()` now canonicalizes every override against the +device's own effective frontier at serialization time, unconditionally +— live unchanged (3 keys), dead folded to the tombstone floor `RegB(0, +max(S,C), 0)` (1 key), virgin omitted (0 keys) — regardless of whether +`do_compact` was ever called locally first. This is a **spec-amendment +requirement for any production client implementing this override +layer**: publication MUST canonicalize before serialization, the same +way it MUST advance the frontier monotonically. It is load-bearing +correctness, not a storage optimization a client can opt out of. +`do_compact` remains available separately to mutate a device's own +`self.overrides` for local storage-GC purposes; it is no longer a +prerequisite for correct publication, because publication no longer +depends on prior local state having been compacted. + +**Proof obligation closed:** `exhaustive.py::test_published_merge_closure` +checks two ways — Thufir's exact witness pair +(`RegB(3,2,0)`@baseline-dead-50 join `RegB(1,2,100)`@clear-dead-100, +raw join is live `RegB(3,2,100)`) as a directed case under both tie +policies, and a general search over every pairwise join of a bounded +cube of 300 independently-dead published states (156 clear-wins + 144 +set-wins = 300 total across both tie policies), including a one-hop +relay republication step to cover delayed/multi-hop delivery (a relay +that receives one operand alone and republishes — re-canonicalizing — +before forwarding). The 45,074 ordered pairs checked comes from +156² + 144² + 2 directed witnesses. `mutation.py::mutant_m7` reverts +`publish_blob` to the pre-fix raw-serialization behavior and reproduces +Thufir's exact resurrection witness directly, confirming the new +invariant has teeth. + +## Candidate comparison + +### Convergence + +Both candidates converge under all tested delivery permutations (algebraic +property). +Candidate B achieves this with componentwise `max()` merge (a standard +state-based CRDT join). Candidate A uses a register with lexicographic +tuple comparison — also convergent, but the register requires a +client-identity tiebreak field. (Convergence for Candidate B is verified +by exhaustive BFS over all reachable states; I2–I4 and I6 are exercised +for Candidate B only — see invariant table.) + +### Legacy compatibility matrix + +| Scenario | A | B | +|----------|---|---| +| Upgraded publishes, legacy reads blob | Legacy drops `overrides` field | Legacy preserves `ov_*` sibling keys | +| Legacy rewrites same slot | **Overrides erased** (expected-witness confirmed) | Sibling keys survive sanitization | +| Upgraded reads legacy-rewritten blob | Override state lost | Override state intact | +| Legacy reads its own frontier | Inert (correct) | Inert (correct) | +| Legacy frontier advance past baseline | Cannot clear override (erased) | Stale set dominated (correct) | + +**Candidate A's legacy erasure is the decisive defect.** The desktop and +mobile parsers (`readStateFormat.ts:82-108`, `read_state_format.dart:100-141`) +reconstruct only `{v, client_id, contexts}`. A same-slot legacy rewrite +drops the top-level `overrides` field entirely and republishes without it. +There is no safe migration path: any user with a single legacy device +loses all manual-unread state on the next rewrite cycle. + +Candidate B's sibling keys (`ov_s:`, `ov_c:`, `ov_b:`) pass all legacy +validation gates — keys are <= 256 UTF-8 bytes, values are uint32 — +and round-trip through legacy rewrite unmodified. + +**Legacy carry-through simplification (documented divergence).** Row +"Legacy preserves `ov_*` sibling keys" is proven two different ways in +this model, and they are not the same claim: + +- `legacy_sanitize_blob` — the byte-sanitization function alone (drop + keys >256 UTF-8 bytes or non-uint32 values) — genuinely preserves + unknown keys as opaque pass-through, matching production + `sanitizeContexts`. `test_legacy_rewrite_b` (I7) exercises exactly + this: an upgraded device's blob is sanitized and received by a + *second upgraded* device; the sibling keys survive because + sanitization never touches keys it doesn't recognize. +- `DeviceB(is_legacy=True)` — the explorer's legacy *device* object used + in the multi-device BFS (`exhaustive.py`) — does **not** carry + through `ov_*` keys it receives. `receive_merge` parses them into a + local dict but the store step is gated on `not self.is_legacy` + (`model.py:268`), so a legacy device's own `publish_blob` only ever + republishes its own frontier keys, never sibling keys it received + from an upgraded peer. This is a deliberate model simplification, not + a claim about production: production's legacy client is a single + `sanitizeContexts` pass with no in-memory override model to gate on, + so it forwards unknown keys unchanged; the model's `DeviceB` needed an + explicit legacy/upgraded split to represent "does not understand or + act on overrides" for the BFS explorer's mark-unread/mark-read action + space, and that split was implemented as drop-on-receive rather than + store-opaque-and-forward. +- **Why this doesn't hide a defect:** every invariant that asserts + sibling-key survival through a legacy hop (I7) is checked via the + sanitize function directly, never via a `DeviceB(is_legacy=True)` + relay round-trip — the two paths are never conflated in a single + assertion. The BFS explorer's own legacy-device transitions are also + gated: `enabled_transitions` only enqueues `mark_unread`/`mark_read`/ + `compact` for a device `if not d.is_legacy` (`exhaustive.py:118-124`), + so a legacy device in the BFS never even attempts to act on overrides; + `do_mark_unread`/`do_mark_read` (`model.py:210-222`) additionally + carry an explicit `if self.is_legacy: return` no-op guard as + defense-in-depth for the same property. `do_compact` + (`model.py:227-236`) carries no such explicit guard — it is a no-op + for a legacy device only *transitively*, because `self.overrides` + is never populated for one (every write path into `self.overrides` + is already gated on `not self.is_legacy`), so `do_compact` finds + `self.overrides.get(ctx)` is always `None` and returns immediately. + Either way, the drop-on-receive simplification never + changes the BFS's own convergence or compaction verdicts (I2, I3, I5, + I5c, I5d) — those are computed only over upgraded devices' + `override_is_set`. The one place a real production legacy client + *does* matter for override survival — sanitizing an upgraded device's + own re-published blob — is I7's scope, and I7 uses the accurate + function. +- **Implication for implementation:** production's `sanitizeContexts` + pass-through behavior is correct and required; this note exists so a + future reader of `DeviceB.receive_merge` doesn't mistake the model's + drop-on-receive simplification for a claim that legacy relaying loses + override state in production — it doesn't, per the function-level + proof above. + +### Identity dependence + +- **A requires client_id** for the tiebreak field. After reinstall + (new `client_id`), the tiebreak changes. Convergence is preserved only + because the counter is strictly higher; a same-counter reinstall would + create an ambiguous merge. +- **B needs no client identity** — componentwise `max()` is + identity-free. Confirmed: reinstall with new `client_id` preserves + convergence. + +### Bytes per manually-unread context + +Sizes computed with realistic context IDs. Envelope cost +(`{"v":1,"client_id":"...","contexts":{}}`) is ~60 bytes and shared +across all contexts — amortized to near zero per context. + +| Context type | Context ID example | ID length | Live override keys (3) | Tombstone key (1) | +|--------------|-------------------|-----------|------------------------|--------------------| +| Channel | `b68cd7cb-6f8d-4641-b743-a7349eb4114b` | 36 | 138 bytes | 45 bytes | +| Message | `msg:` + 64-hex event ID | 68 | 234 bytes | 77 bytes | +| Thread | `thread:` + 64-hex event ID | 71 | 243 bytes | 80 bytes | + +Live-override bytes are unchanged by the reserved-namespace escaping +(below): every context ID Buzz actually generates (channel UUID, +`msg:hex64`, `thread:hex64`) is a no-op under `escape_context_key` — none +begin with `ov_` or `esc:` — so the escape marker costs 0 bytes in the +common case. Tombstone bytes are new in this revision: canonical +publication no longer serializes a dead register at 3 keys (see +"Compaction behavior" below and "Published-state merge closure" above) +but a single `ov_c:` key with the counter ceiling — this is now the +literal output of `publish_blob()` for any dead override, not merely +the output of the optional `do_compact` storage-GC step. + +Breakdown for channel context (worst real-world common case, live): +``` +"ov_s:b68cd7cb-6f8d-4641-b743-a7349eb4114b":1 → 44 chars +"ov_c:b68cd7cb-6f8d-4641-b743-a7349eb4114b":0 → 44 chars +"ov_b:b68cd7cb-6f8d-4641-b743-a7349eb4114b":10 → 45 chars + total ≈ 138 bytes (+ 2 commas) +``` + +Tombstone floor for channel context (dead override after compaction): +``` +"ov_c:b68cd7cb-6f8d-4641-b743-a7349eb4114b":3 → 45 chars ≈ 45 bytes +``` + +Candidate A for comparison: `{"counter":1,"tiebreak":"dev0","op":"SET","baseline":10}` +≈ 56 bytes per context as a JSON object, plus the top-level `overrides` +field overhead. However, this is moot since A's top-level field is erased +by legacy clients. + +### Reserved key namespace + +NIP-RS v1 context IDs are arbitrary UTF-8 (spec `:89`, `:113-114`), so a +pre-existing opaque context could legitimately begin with `ov_s:`, +`ov_c:`, or `ov_b:` and, once flattened into the same `contexts` map, +be misparsed as a control key for a *different* context. + +**Reservation:** the 3-byte stem `ov_` and the escape marker `esc:` are +reserved at the spec-amendment level. A raw context ID that begins with +either is escaped on publish by prepending `esc:`, and unescaped on +receive by stripping exactly one leading `esc:` (`model.py: +escape_context_key`, `unescape_context_key`). This is a bijection, not +an idempotent no-op: a context literally named `esc:foo` escapes to +`esc:esc:foo` on the wire and unescapes back to exactly `esc:foo` on +receipt — the two operations are inverses, so no collision or data +loss occurs even for context IDs that already contain the marker. + +**Cost:** zero bytes for every context ID Buzz generates today (channel +UUID, `msg:hex64`, `thread:hex64` — none start with `ov_` or `esc:`). +Only a context ID that happens to start with the reserved stem pays the +4-byte `esc:` prefix. + +**Backward-compatibility limitation (Thufir's qualification — not a +collision-safe migration of existing data):** a context published +*unescaped* by a client that predates this amendment, and that happens +to start with `ov_` (e.g. an already-published, pre-existing +`ov_s:evil`-style context), is **not safely migrated** by this scheme. +Retroactive escaping cannot rewrite a blob the original publisher never +knew needed escaping — the codec protects contexts generated by +amendment-aware clients going forward, not history that predates the +amendment. This is a theoretical concern for the reasons in the +">256-byte key drop hazard" section: Buzz's own key shapes cannot +trigger it, and no legacy client is known to generate `ov_`-prefixed +context IDs. Documented as a residual, unsolved, backward-compatibility +gap — not modeled further — per the same practical-risk reasoning +already applied to the 256-byte hazard below. + +**Verified:** `exhaustive.py::test_reserved_namespace_collision` — a +context literally named `ov_s:evil` round-trips through publish/receive +as frontier state (not misparsed as an override), and a real override on +a *different* context in the same blob is unaffected. + +### Counter headroom (uint32) + +Each counter (S, C) is a uint32: 2^32 - 1 = 4,294,967,295. At one +toggle per second, ~136 years. No practical concern for manual +right-click actions. + +### >256-byte key drop hazard + +Legacy `sanitizeContexts` drops any key with `len(key.encode('utf-8')) > 256`. +Adding the `ov_s:` prefix (5 bytes) to a context key creates a key of +`len(context_id) + 5` bytes. If the original context key is at or near +the 256-byte limit, the prefixed override key exceeds it and is silently +dropped by legacy sanitization. + +In practice, context keys are UUIDs (36 bytes), hex event IDs (64-68 bytes), +or thread IDs (71 bytes) — all well under 256 bytes. The longest common +override key (`ov_b:thread:` + 64-hex = 76 bytes) has 180 bytes of +headroom. This hazard is theoretical but should be documented in the spec. + +### 10,000-key validation limit + +Legacy `isValidBlob` rejects blobs with >10,000 context keys. Live +override keys consume 3 entries per overridden context; a compacted +(tombstoned) override consumes 1: + +| Overridden contexts | Live override keys | Typical frontier keys | Total | Headroom | +|--------------------|---------------------|-----------------------|-------|----------| +| 50 | 150 | ~500 | 650 | 93.5% | +| 100 | 300 | ~1,000 | 1,300 | 87% | +| 500 | 1,500 | ~2,000 | 3,500 | 65% | +| 3,000 | 9,000 | ~1,000 | 10,000 | 0% (limit) | + +The 32 KiB byte budget is the binding constraint long before key count. + +### Compaction behavior (tombstone-floor, policy-dependent) + +**Revision note:** the prior "compacts to zero" design (delete-on- +dominance: a dead register was dropped entirely, 0 keys) is retracted. +Thufir's pass-3 review found a stale-replay resurrection: dropping all +`(S,C)` state made counters reusable, so a new local set/clear pair +restarting from `S=0,C=0` could be dominated by a delayed stale peer +snapshot on replay (`RegB(3,0,10)` → compact → `None` → local +set+clear → `RegB(1,2,20)` → stale replay merges in → `RegB(3,2,20)`, +`S>C`, resurrected). Fixed by a tombstone floor: any register with +recorded activity (S>0 or C>0) is *never* fully deleted — dead state +compacts to `RegB(0, max(S,C), 0)` instead of `None`. Only a virgin +register (never set, S==0 and C==0) has no ceiling to protect and +compacts to `None`. + +**The compaction rule is now uniform across the dead cases — the +per-branch table collapses to a single test:** + +| Condition | Clear-wins | Set-wins | +|-----------|-----------|----------| +| `override_set_b(reg)` is True (live) | Do not compact | Do not compact | +| `override_set_b(reg)` is False and `S>0 or C>0` (dead, ever-active) | Compact to tombstone floor `RegB(0, max(S,C), 0)` | Compact to tombstone floor (same) | +| `S == 0, C == 0` (virgin, never set) | Drop entirely (`None`) | Drop entirely (same) | + +Because `override_set_b` is already policy-aware, "live" vs. "dead" +differs by policy exactly where it did before (`S == C, S > 0` is dead +under clear-wins, live under set-wins) — the tombstone floor rule itself +does not need to branch on policy; `compact_b` calls `override_set_b` +once and only tombstones the false branch. + +Under clear-wins, a dead override compacts to the ~45-byte tombstone +(one `ov_c:` key, channel context) — **not** to zero, because `C` must +persist as the reuse-blocking ceiling. Under set-wins, `S == C` overrides +remain live and are never compacted (3 keys, ~138 bytes for channel +contexts) — unchanged from the prior revision. + +**Proof obligation closed (same-device replay):** +`exhaustive.py::test_deep_history_compaction` (672-point parameter +cube) and `test_tombstone_stale_merge_direct` verify no resurrection +and no loss of a genuinely-live override across the compact → +new-action → delayed-stale-delivery shape, for both tie policies. +`mutation.py::mutant_m4` +reverts to the old delete-on-dominance rule and reproduces the exact +resurrection witness (`final_reg=RegB(s=3, c=2, b=20)`, +`override_is_set=True`) — confirming the suite would have caught the +defect this round was opened to fix. + +**Proof obligation closed (cross-device transparency, requalified — +suppress-only, not zero-divergence):** +`exhaustive.py::test_cross_device_compaction_suppression` (312-point +cube: stale ancestor `(S,C,B)` × post-compaction frontier × 4 +fresh-frontier values on the receiving device × 2 tie policies) proves +every divergence between "receive the tombstone" and "receive the +uncompacted ancestor" is a suppression of an unrelated device's live +set — never a resurrection — and that every suppression recovers with +one more local mark-unread and stays recovered after re-receiving the +same tombstone. `test_tombstone_merge_monotonic` proves the direction +structurally (not just over the bounded cube): merging in a tombstone +`RegB(0, k, 0)` for any ceiling `k` can only raise the receiving +register's `C`, never its `S` or `B`, so it can only weaken — never +strengthen — the receiving register's live/dead standing under +`override_set_b`. Together these close the compaction-safety proof +obligation to exactly what it can honestly claim: no resurrection ever, +one-shot suppression is a known and recoverable false-negative risk +inherent to the clear-wins/tombstone design, not an unbounded +correctness gap. + +### GC/tombstone behavior + +**Override keys with `ov_` prefix (legacy prune):** Legacy +`pruneStaleContexts` only drops `msg:`/`thread:`-prefixed keys past the +7-day horizon. Unknown-prefix keys (including `ov_*`) are kept forever: + +- **Permanent tombstones:** every override that is ever compacted while + dead leaves a permanent `ov_c:` key (~45 bytes, channel context) — this + is no longer a "harmless, can shrink to zero" cost; it is a durable + floor kept forever to block stale-replay resurrection. This is the + direct storage consequence of fixing the CRITICAL above and must be + budgeted, not treated as free. +- **Live overrides:** an override still live (per `override_set_b`) + keeps all 3 keys (~138 bytes, channel context) until it becomes dead + and is compacted down to the tombstone. + +**Alternative: nesting under `msg:`/`thread:` prefixes** — confirmed +**state-loss hazard**. Legacy prune would delete overrides at the 7-day +horizon, silently losing active unread markers. Rejected. + +### Legacy trim interaction + +Legacy `trimContextsToBudget` evicts only `msg:`/`thread:` keys. +Override `ov_*` keys (including tombstones) are never evicted. Budget +analysis by context type, worst case (all overrides still live, 3 keys +each — the tombstone floor only ever *reduces* this cost): + +| Overridden contexts | Context type | Live override bytes | With ~10 KiB frontiers | Fits 32 KiB? | +|--------------------|-------------|----------------|----------------------|-------------| +| 50 | Channel (UUID) | ~6.9 KiB | ~16.9 KiB | Yes | +| 100 | Channel (UUID) | ~13.8 KiB | ~23.8 KiB | Yes | +| 150 | Channel (UUID) | ~20.7 KiB | ~30.7 KiB | Marginal | +| 50 | Message (hex64) | ~11.9 KiB | ~21.9 KiB | Yes | +| 100 | Message (hex64) | ~23.7 KiB | ~33.7 KiB | **No** | + +At the 100-override cap with every override compacted to its tombstone +floor instead: ~4.5 KiB (channel contexts, 100 × 45 bytes) — well +within budget alongside a full frontier set. The permanent-tombstone +floor from the CRITICAL fix costs storage but is bounded and small; it +does not change the 32 KiB conclusion below. + +**Mitigation:** Upgraded clients should compact aggressively (any dead +override, not just baseline-dominated ones) and enforce a cap on active +override count. A cap of 100 channel-context overrides keeps *live* +override budget under ~14 KiB and *tombstoned* budget under ~4.5 KiB, +both within the 32 KiB limit alongside a full frontier set. + +### Tie policy evidence: clear-wins vs set-wins + +Both tie policies pass all invariants. The choice is a product-semantics +decision: + +- **Clear-wins (S == C → read):** If two devices concurrently set and + clear the same context, the result is "read." Conservative — no + spurious unread badges. Matches the "I already read this" signal being + more definitive than the "remind me" signal. Compaction advantage: + `S == C` states are compactable. +- **Set-wins (S == C → unread):** Concurrent set and clear results in + "unread." Preserves the reminder intent. Risk: a user who reads on one + device while another has a stale mark-unread gets a persistent badge + they can't clear without an explicit action. Compaction disadvantage: + `S == C` states are live and cannot be compacted. + +**Recommendation:** Clear-wins. A false negative (missing badge) is +recovered by re-marking unread. A false positive (badge that won't clear) +is more frustrating. This matches Slack's behavior: reading anywhere +clears everywhere. The compaction advantage further favors clear-wins. + +**Pre-existing false-negative risk (independent of compaction).** Under +clear-wins, a stale explicit clear (`RegB(0,1,0)`, no compaction +involved) merging into a device with a fresh concurrent set +(`RegB(1,0,30)`) already produces `RegB(1,1,30)`, tied, suppressed — +verified directly by evaluating `merge_reg_b`/`override_set_b` on those +two registers with no `compact_b` call anywhere in the path. The +cross-device tombstone-suppression finding (I5d, "Compaction behavior" +above) is the same tie shape reached via a different route: a +baseline-dominated *dead set* (never explicitly cleared) that gets +compacted to a `C`-ceiling tombstone, which is then globally comparable +in a way its pre-compaction, frontier-relative death was not. Compaction +widens the set of histories that can reach the tie, but clear-wins +already accepted this one-shot, re-mark-recoverable false-negative shape +as its stated tradeoff. + +### Multi-slot union + +Production splits blobs across up to 8 slots (`READ_STATE_MAX_SLOTS`). +`mergeReadStateEvents` merges all slots with per-context `max()`. Override +sibling keys are individual context entries and follow the same merge path. + +**Atomic slot-grouping rule (spec-amendment requirement):** a context's +frontier entry and ALL of its `ov_*` sibling entries MUST travel in the +same slot, including during slot growth/rebalancing. This is the transport +half of the same closure property as mandatory canonical publication: + +- Without it, an observer holding only a slot containing `ov_s:ctx` (but + not `ov_b:ctx`) reconstructs `RegB(s=1, c=0, b=0)` — baseline-dead at + any nonzero frontier — and canonically publishes tombstone `RegB(0,1,0)`. + After full eventual delivery of all original slots plus that transient + tombstone, the merged result is `RegB(s=1, c=1, b=10)` — dead under + clear-wins — permanently suppressing a live override. +- With the rule, a receiver always sees either the complete register group + or none of it; partial reconstruction is structurally impossible from a + compliant publisher's output. + +Implementation: amend `splitContextsIntoBudgetedSlots` to round-robin +per-context groups (frontier key + all `ov_*` sibling keys for that context) +rather than per-entry. `DeviceB.split_blob_into_slots` in `model.py` models +this correctly. + +**Unescape-before-group rule (corollary — spec-amendment requirement):** +When grouping context entries, a frontier wire key MUST be unescaped to its +raw logical context ID before being used as the group key. A raw context ID +starting with a reserved prefix (e.g. `ov_s:evil`) escapes to +`esc:ov_s:evil` as its frontier wire key, while its `ov_*` siblings are +keyed by the raw suffix (`ov_s:evil`). Without unescaping the frontier key +before grouping, these resolve to different groups and the register splits +across slots — reproducing the same partial-reconstruction poison across +publication cycles via old/new slot-coordinate mixtures. Fix: derive group +identity via `unescape_context_key(wire_key)` for frontier keys. +`mutation.py::mutant_m9` reverts to escaped-key grouping and confirms +`test_escaped_context_slot_grouping` catches the witness. + +`mutation.py::mutant_m8` reverts to per-entry splitting (M8's split puts +frontier+`ov_s:` in slot 0 and `ov_b:`+`ov_c:` in slot 1) and confirms +`test_interleaved_delivery_grouping` catches Thufir's exact witness. + +This rule carries the same normative weight as mandatory canonical publication: +both are protocol requirements for any client implementing this override layer, +not optional optimizations. + +Confirmed: splitting a published blob across 2 grouped slots and delivering +each separately produces the same final override and frontier state as +delivering the full blob, regardless of delivery order. Interleaved-delivery +test (`test_interleaved_delivery_grouping`) additionally verifies that +receive-one-slot → re-publish → receive-rest permutations, including delayed +transient delivery to a third observer, preserve the live override verdict. + +## Mutation harness + +9 mutants, all caught with recorded counterexamples: + +| Mutant | Rule dropped | Counterexample | +|--------|-------------|----------------| +| M1 | Baseline dominance check | `RegB(1,0,10)` at frontier=100: correct=inactive, mutant=active (stale set persists) | +| M2 | `max(S,C)+1` counter bump | After set→set→clear: correct `RegB(2,3,10)` (clear wins), mutant `RegB(2,1,10)` (set persists) | +| M3 | Tie policy | `RegB(1,1,10)` at frontier=10: clear-wins=False, set-wins=True | +| M4 | Tombstone-floor compaction (delete-on-dominance revert) | `RegB(3,0,10)` at frontier=20 compacts to `None` (vs. tombstone `RegB(0,3,0)`); local set+clear reuses counters from zero; delayed stale replay resurrects — `final_reg=RegB(s=3,c=2,b=20)`, `override_is_set=True` (reproduces Thufir's pass-3 CRITICAL) | +| M5 | uint32 value range | Value 4,294,967,296 rejected by legacy sanitization | +| M6 | Componentwise-max merge | LWW delivery-order-dependent: convergence breaks under permutation | +| M7 | Canonical publication (raw register serialization) | `RegB(3,2,0)`@frontier-50 join `RegB(1,2,100)`@frontier-100 = live `RegB(3,2,100)` (reproduces Thufir's pass-1/2 CRITICAL dead+dead resurrection) | +| M8 | Atomic slot-grouping rule (per-entry split) | Live `RegB(1,0,10)` at frontier=10 split as `{frontier+ov_s:}` / `{ov_b:+ov_c:}`; partial observer reconstructs `RegB(1,0,0)`, publishes tombstone `RegB(0,1,0)`; final merge = `RegB(1,1,10)` → inactive (reproduces Thufir's pass-2/2 CRITICAL transport witness) | +| M9 | Unescape-before-group rule (escaped-key grouping) | Live override on raw ctx `ov_s:evil` (frontier wire key `esc:ov_s:evil`); escaped-key grouping splits frontier from `ov_*` siblings; old/new slot-coordinate mixture → `RegB(1,0,0)` → tombstone `RegB(0,1,0)` → final merge = `RegB(1,1,10)` → inactive (reproduces Thufir's round-2 CRITICAL) | + +Each mutant is injected into the model via DeviceB subclass (M1, M2, M4, +M6, M7, M8, M9) or direct function evaluation (M3, M5), then the applicable +invariant suite is rerun. M4 reverts to the pre-fix delete-on-dominance +compaction rule and directly reproduces Thufir's pass-3 CRITICAL resurrection +witness — the exact `RegB(3,0,10)` → `None` → counter-reuse → stale +replay → `RegB(3,2,20)`,`override_is_set=True` sequence — with a +fallback to the directed deep-history cube (`test_deep_history_compaction`) +if the hand-built scenario doesn't trigger under a given tie policy. M7 +reverts `publish_blob` to raw serialization and reproduces Thufir's pass-1/2 +CRITICAL dead+dead resurrection. M8 reverts `split_blob_into_slots` to +per-entry assignment (frontier+`ov_s:` / `ov_b:`+`ov_c:`) and reproduces +Thufir's pass-2/2 CRITICAL transport witness via `test_interleaved_delivery_grouping`. +M9 reverts `split_blob_into_slots` to escaped-key grouping (groups frontier by +its wire key instead of its unescaped logical ID) and reproduces Thufir's +round-2 CRITICAL for escaped contexts via `test_escaped_context_slot_grouping`. + +## Recommendation + +**Candidate B (two grow-only counters + baseline) with clear-wins tie +policy.** + +Evidence: + +1. **Legacy safety:** B's sibling keys survive legacy rewrite; A's + top-level field is erased. Hard blocker for A — no migration path + tolerates a single legacy device. +2. **Identity-free:** B needs no client_id for correctness; A's + tiebreak creates a reinstall fragility. +3. **CRDT properties:** Candidate B passes all merge invariants (I2–I8) in + the exhaustive model. Candidate A's join is also correct algebraically + (I1, I9), but I2–I4 and I6 are not exercised for A — A is dead on I7 + regardless. B's componentwise max is simpler and more standard. +4. **Bytes:** B at 3 live keys costs 138 bytes/context (channel UUID) to + 243 bytes/context (thread hex64); a dead override compacts to a single + ~45-80 byte tombstone key instead. Cap of 100 overrides stays within + 32 KiB budget for both live and tombstoned cases. +5. **Compaction:** B supports safe policy-aware compaction — no + resurrection, ever (proved structurally, not just over a bounded + cube). Clear-wins allows compacting `S == C` states (set-wins does + not). Cross-device delivery of a tombstone can one-shot suppress an + unrelated device's concurrent fresh set whose counters are at or + below the tombstone's ceiling; this is recoverable by re-marking and + is the same false-negative shape clear-wins already accepts for a + stale explicit clear with no compaction involved (see "Tie policy + evidence"). +6. **Tie policy:** Clear-wins avoids persistent false-positive badges + and enables more aggressive compaction. + +## Honest limits + +- The model enumerates bounded abstract operations, not real encrypted + NIP-59 payloads or relay replacement semantics. +- Counter values in the general BFS explorer are bounded by its exploration + depth (max ~4 via BFS depth 4); the directed deep-history cube + (`test_deep_history_compaction`) reaches counter values up to the stale + parameter range (0-3) plus post-compaction action sequences, covering the + ~9-transition witness the BFS explorer cannot structurally reach. Real + uint32 overflow/wrap is tested only via the legacy sanitization mutant (M5). +- The BFS explorer (I5/I5c) checks compaction safety over reachable + multi-device histories up to depth 4, but its own terminal-state + compaction check (`check_compaction_safety`) only merges a device's + compacted register with its *own* pre-compaction snapshot — it does + not, by construction, exercise an unrelated device's independently- + live concurrent register. `test_cross_device_compaction_suppression` + (I5d) covers that shape directly but over a hand-parameterized cube, + not the full BFS state space; the accompanying + `test_tombstone_merge_monotonic` lemma is what extends the + no-resurrection guarantee beyond the cube's specific points. +- Two contexts are modeled. Production users may have hundreds of contexts, + but the CRDT properties are per-context — cross-context interactions are + limited to the shared byte budget (tested via trim/prune interaction). +- Multi-slot behavior is confirmed via split+merge convergence test, and + the atomic slot-grouping rule is modeled by `DeviceB.split_blob_into_slots` + (including the escaped-context identity fix — `split_blob_into_slots` + unescapes frontier keys before grouping). The production TypeScript + implementation (`splitContextsIntoBudgetedSlots`) is NOT modeled — only + the abstract grouping property is verified here. Implementation-level + testing is still needed for slot placement, slot rebalancing, and the + production d-tag coordinate assignment. +- The model assumes eventual delivery (all blobs eventually reach all + devices). Permanent message loss is not modeled. +- Byte sizes are computed from JSON serialization of realistic key names. + Actual encrypted blob overhead (NIP-59 envelope, relay metadata) adds + to the total but does not affect the 32 KiB plaintext budget. diff --git a/docs/formal/nip-rs-unread/exhaustive.py b/docs/formal/nip-rs-unread/exhaustive.py new file mode 100644 index 0000000000..82d54c6b43 --- /dev/null +++ b/docs/formal/nip-rs-unread/exhaustive.py @@ -0,0 +1,1486 @@ +"""Bounded transition-system explorer for NIP-RS manual-unread candidates. + +BFS over canonical global states. At each depth, enabled transitions are +local actions and message deliveries, interleaved — not phased. + +Universe: 2 upgraded devices + 1 legacy device, 2 contexts. +Transitions: mark_unread, mark_read (with frontier advance), + advance_frontier, compact, reinstall, deliver (including + duplicate/replay). Legacy rewrite semantics are exercised through the + deliver path (legacy_sanitize_and_publish), not as a separate + transition — a legacy device never mutates its own state outside + delivery, so a dedicated no-op transition added nothing (see NOTE.md). + +Invariants: + I1 merge_reg_b associative/commutative/idempotent + I2 convergence: all delivery orders -> identical override verdict + I3 no frontier regression + I4 concurrent set/clear winner stable (order-independent, ancestor-independent) + I5 compaction: no loss of live set, no resurrection of dead clear, + survives merge with stale pre-compaction state + I5c directed deep-history: compact -> new local actions (counter reuse) + -> delayed stale delivery does not resurrect a dead override or + lose a genuinely-live one. Scope: the compacting device's own + pre-compaction ancestor (or an exact copy of it) replayed back to + that same device. + I5d cross-device compaction transparency (requalified, NOT + zero-divergence): a tombstone's counter ceiling can one-shot + suppress an unrelated device's concurrent fresh set with no + resurrection, and the suppression is always recoverable by one + more local action. Proven suppress-only direction via a bounded + witness cube plus a structural monotonicity argument. + I6 replay harmless + I7 legacy rewrite: B sibling keys survive / A overrides erased (witness) + I8 bounded key growth per context + I9 DeviceA post-receive counter absorption +""" +from itertools import permutations +from copy import deepcopy +from model import ( + RegB, merge_reg_b, override_set_b, compact_b, + RegA, merge_reg_a, + DeviceB, DeviceA, + SET, CLEAR, + legacy_prune, legacy_trim, legacy_sanitize_blob, + escape_context_key, unescape_context_key, ESCAPE_PREFIX, +) + +CONTEXTS = ("c0", "c1") +FRONTIER_VALS = (10, 20) + + +# --------------------------------------------------------------------------- +# I1: algebraic properties +# --------------------------------------------------------------------------- + +def test_merge_algebra_b(): + vals = [0, 1, 2, 3] + regs = [RegB(s, c, b) for s in vals for c in vals for b in vals] + violations = [] + for a in regs: + if merge_reg_b(a, a) != a: + violations.append(("idempotent", a)) + for a in regs: + for b in regs: + if merge_reg_b(a, b) != merge_reg_b(b, a): + violations.append(("commutative", a, b)) + for a in regs: + for b in regs: + for c in regs: + if merge_reg_b(merge_reg_b(a, b), c) != merge_reg_b(a, merge_reg_b(b, c)): + violations.append(("associative", a, b, c)) + return violations + + +def test_merge_algebra_a(): + vals = [0, 1, 2] + tiebreaks = ["a", "b"] + ops = [SET, CLEAR] + baselines = [0, 10] + regs = [RegA(ct, t, o, bl) + for ct in vals for t in tiebreaks for o in ops for bl in baselines] + violations = [] + for tie_op in [CLEAR, SET]: + for a in regs: + if merge_reg_a(a, a, tie_op) != a: + violations.append(("idempotent", tie_op, a)) + for a in regs: + for b in regs: + if merge_reg_a(a, b, tie_op) != merge_reg_a(b, a, tie_op): + violations.append(("commutative", tie_op, a, b)) + for a in regs: + for b in regs: + for c in regs: + ab_c = merge_reg_a(merge_reg_a(a, b, tie_op), c, tie_op) + a_bc = merge_reg_a(a, merge_reg_a(b, c, tie_op), tie_op) + if ab_c != a_bc: + violations.append(("associative", tie_op, a, b, c)) + return violations + + +# --------------------------------------------------------------------------- +# BFS state explorer — Candidate B +# --------------------------------------------------------------------------- + +def next_frontier(device, ctx): + cur = device.effective_frontier(ctx) + for fv in FRONTIER_VALS: + if fv > cur: + return fv + return None + + +def enabled_transitions(devices, tie_policy): + """Generate (kind, args) tuples for all enabled transitions.""" + trans = [] + for di, d in enumerate(devices): + for ctx in CONTEXTS: + if not d.is_legacy: + trans.append(("mark_unread", di, ctx)) + fv = next_frontier(d, ctx) + if fv is not None: + trans.append(("mark_read", di, ctx, fv)) + if ctx in d.overrides: + trans.append(("compact", di, ctx)) + fv = next_frontier(d, ctx) + if fv is not None: + trans.append(("advance", di, ctx, fv)) + if not d.is_legacy: + trans.append(("reinstall", di)) + for si in range(len(devices)): + for di in range(len(devices)): + if si != di: + trans.append(("deliver", si, di)) + return trans + + +def apply_transition(devices, t, tie_policy): + kind = t[0] + if kind == "mark_unread": + devices[t[1]].do_mark_unread(t[2]) + elif kind == "mark_read": + devices[t[1]].do_mark_read(t[2], t[3]) + elif kind == "advance": + devices[t[1]].do_advance_frontier(t[2], t[3]) + elif kind == "compact": + devices[t[1]].do_compact(t[2], tie_policy) + elif kind == "reinstall": + devices[t[1]].do_reinstall() + elif kind == "deliver": + src = devices[t[1]] + dst = devices[t[2]] + if src.is_legacy: + blob = src.legacy_sanitize_and_publish(tie_policy) + else: + blob = src.publish_blob(tie_policy) + dst.receive_merge(blob) + + +def state_sig(devices, tie_policy): + return tuple(d.state_key(CONTEXTS, tie_policy) for d in devices) + + +def check_convergence(devices, tie_policy, trace, violations): + """Publish all blobs, deliver in every order, check upgraded devices + converge on override_is_set for each context. + + Tests with latest_ts=5 (below all frontiers) so the override is the + sole unread source — no masking by natural unread. + """ + blobs = [] + for d in devices: + if d.is_legacy: + blobs.append(d.legacy_sanitize_and_publish(tie_policy)) + else: + blobs.append(d.publish_blob(tie_policy)) + + verdicts_per_order = [] + for perm in permutations(range(len(blobs))): + receivers = deepcopy(devices) + for idx in perm: + for r in receivers: + r.receive_merge(blobs[idx]) + per_device = [] + for r in receivers: + if not r.is_legacy: + per_device.append( + tuple(r.override_is_set(ctx, tie_policy) for ctx in CONTEXTS) + ) + verdicts_per_order.append(tuple(per_device)) + + if len(set(verdicts_per_order)) > 1: + violations.append(("I2-convergence", trace, set(verdicts_per_order))) + + +def check_compaction_safety(devices, tie_policy, trace, violations): + """For each upgraded device with overrides: + 1. Check override_is_set directly (not via verdict/latest_ts). + 2. Compact and verify override_is_set unchanged. + 3. Merge compacted state with stale pre-compaction state in both orders. + Verify no resurrection and no loss. + """ + for di, d in enumerate(devices): + if d.is_legacy: + continue + for ctx in CONTEXTS: + reg = d.overrides.get(ctx) + if reg is None: + continue + front = d.effective_frontier(ctx) + ov_before = d._override_set(reg, front, tie_policy) + compacted = d._compact(reg, front, tie_policy) + ov_after = d._override_set(compacted, front, tie_policy) if compacted else False + + if ov_before and not ov_after: + violations.append(( + "I5-compaction-lost-set", trace, di, ctx, + reg, compacted, front, tie_policy + )) + if not ov_before and ov_after: + violations.append(( + "I5-compaction-resurrection", trace, di, ctx, + reg, compacted, front, tie_policy + )) + + if compacted is not None: + for merged in [merge_reg_b(compacted, reg), merge_reg_b(reg, compacted)]: + ov_merged = d._override_set(merged, front, tie_policy) + if not ov_before and ov_merged: + violations.append(( + "I5-compaction-merge-resurrection", trace, di, ctx, + reg, compacted, merged + )) + + +def explore_b(max_depth=4, tie_policy=CLEAR, device_cls=DeviceB): + """BFS over all reachable global states up to max_depth. + + Returns (states_explored, violations). + Accepts device_cls for mutation testing via subclassing. + """ + def make_devices(): + return [ + device_cls("d0", is_legacy=False), + device_cls("d1", is_legacy=False), + device_cls("d2", is_legacy=True), + ] + + violations = [] + seen = set() + states_explored = 0 + queue = [(make_devices(), [])] + + while queue: + devices, trace = queue.pop(0) + sig = state_sig(devices, tie_policy) + if sig in seen: + continue + seen.add(sig) + states_explored += 1 + + for di, d in enumerate(devices): + for ctx in CONTEXTS: + prev_front = d.effective_frontier(ctx) + if prev_front < 0: + violations.append(("I3-frontier-negative", trace, di, ctx)) + + if len(trace) >= max_depth: + check_convergence(devices, tie_policy, trace, violations) + check_compaction_safety(devices, tie_policy, trace, violations) + continue + + for t in enabled_transitions(devices, tie_policy): + new_devs = deepcopy(devices) + fronts_before = { + (di, ctx): d.effective_frontier(ctx) + for di, d in enumerate(new_devs) for ctx in CONTEXTS + } + apply_transition(new_devs, t, tie_policy) + + # Reinstall intentionally wipes local state; frontier regression + # is only invalid during merge/delivery/compaction/advance. + if t[0] != "reinstall": + for (di, ctx), fb in fronts_before.items(): + fa = new_devs[di].effective_frontier(ctx) + if fa < fb: + violations.append(("I3-frontier-regression", trace + [t], di, ctx, fb, fa)) + + queue.append((new_devs, trace + [t])) + + return states_explored, violations + + +# --------------------------------------------------------------------------- +# I4: concurrent set/clear winner stable +# --------------------------------------------------------------------------- + +def test_concurrent_stability(device_cls=DeviceB): + """Two devices concurrently set and clear from every possible ancestor state. + The winner must be the same regardless of delivery order AND ancestor state.""" + violations = [] + for tie_policy in [CLEAR, SET]: + for pre_s, pre_c in [(0, 0), (1, 0), (0, 1), (2, 1), (1, 2), (1, 1)]: + for front in [0, 10]: + for ctx in CONTEXTS: + ancestor = RegB(s=pre_s, c=pre_c, b=front) + + d0 = device_cls("d0") + d0.frontier[ctx] = front + d0.overrides[ctx] = deepcopy(ancestor) + d1 = device_cls("d1") + d1.frontier[ctx] = front + d1.overrides[ctx] = deepcopy(ancestor) + + d0.do_mark_unread(ctx) + d1.do_mark_read(ctx, front + 10) + + blob0 = d0.publish_blob(tie_policy) + blob1 = d1.publish_blob(tie_policy) + + verdicts = set() + for first, second in [(blob0, blob1), (blob1, blob0)]: + r = device_cls("recv") + r.frontier[ctx] = front + r.overrides[ctx] = deepcopy(ancestor) + r.receive_merge(first) + r.receive_merge(second) + verdicts.add(r.override_is_set(ctx, tie_policy)) + + if len(verdicts) > 1: + violations.append(( + "I4-unstable", tie_policy, ctx, + pre_s, pre_c, front + )) + return violations + + +# --------------------------------------------------------------------------- +# I5: direct compaction register-level check (all register values x policies) +# --------------------------------------------------------------------------- + +def test_compaction_register_exhaustive(): + """Exhaustive check over bounded register cube and frontier values. + Tests override_is_set directly — no latest_ts masking.""" + violations = [] + vals = [0, 1, 2, 3] + frontiers = [0, 10, 20] + for tie_policy in [CLEAR, SET]: + for s in vals: + for c in vals: + for b in frontiers: + for fv in frontiers: + reg = RegB(s=s, c=c, b=b) + ov_before = override_set_b(reg, fv, tie_policy) + compacted = compact_b(reg, fv, tie_policy) + ov_after = (override_set_b(compacted, fv, tie_policy) + if compacted else False) + + if ov_before and not ov_after: + violations.append(( + "loss", tie_policy, reg, fv, compacted + )) + if not ov_before and ov_after: + violations.append(( + "resurrection", tie_policy, reg, fv, compacted + )) + + if compacted is not None: + merged_fwd = merge_reg_b(compacted, reg) + merged_rev = merge_reg_b(reg, compacted) + for label, merged in [("fwd", merged_fwd), ("rev", merged_rev)]: + ov_merged = override_set_b(merged, fv, tie_policy) + if not ov_before and ov_merged: + violations.append(( + f"merge-resurrection-{label}", + tie_policy, reg, fv, compacted, merged + )) + return violations + + +# --------------------------------------------------------------------------- +# I5c: directed deep-history — compact -> new actions (counter reuse) -> +# delayed stale delivery (including split across two slots) +# --------------------------------------------------------------------------- + +def _apply_action_seq(dev, ctx, seq, ts): + for a in seq: + if a == "set": + dev.do_mark_unread(ctx) + else: + dev.do_mark_read(ctx, ts) + + +def _ancestor_ctx_dict(ctx, reg): + return {f"ov_s:{ctx}": reg.s, f"ov_c:{ctx}": reg.c, f"ov_b:{ctx}": reg.b} + + +_DEEP_HISTORY_ACTION_SEQS = [ + (), ("set",), ("clear",), ("set", "clear"), ("clear", "set"), + ("set", "set"), ("clear", "clear"), +] +# One delivery shape: single unsplit blob. The prior "split_fwd"/"split_rev" +# shapes are no longer distinct — with the atomic-grouping rule a single- +# context blob's compliant split puts the whole group in one slot and the +# other empty, making split_fwd and split_rev semantically identical to +# single. Keeping only one shape avoids 2/3 duplicate executions (2,016 → +# 672 meaningful points) while losing zero register-level coverage. +_DEEP_HISTORY_DELIVERY_SHAPES = ("single",) + + +def test_deep_history_compaction(device_cls=DeviceB): + """Directed check over the exact shape a depth-4 BFS structurally + cannot reach (~9 transitions): compact -> new local set/clear actions + (counter reuse against the tombstone floor) -> delayed delivery of + the pre-compaction stale ancestor, including split across 2 slots. + + Oracle: compaction is a storage optimization and must never change + the semantic outcome. A reference device that never compacts, given + the identical ancestor / frontier advance / action sequence / late + ancestor delivery, must reach the same override_is_set verdict as + the compacting device. This directly targets Thufir's counterexample + (RegB(3,0,10) -> None under delete-on-dominance -> counter reuse -> + RegB(3,2,20) resurrection) and requires the tombstone floor from + compact_b to hold under it. + + Returns (cube_size, violations). + """ + violations = [] + cube_size = 0 + ctx = "c0" + stale_vals = (0, 1, 2, 3) + baselines = (0, 10) + post_frontiers = (10, 20) + + for s0 in stale_vals: + for c0 in stale_vals: + for b0 in baselines: + for f1 in post_frontiers: + if f1 <= b0: + continue # not a dominance/compaction scenario + ancestor = RegB(s=s0, c=c0, b=b0) + ancestor_blob = _ancestor_ctx_dict(ctx, ancestor) + for seq in _DEEP_HISTORY_ACTION_SEQS: + for tie_policy in (CLEAR, SET): + for shape in _DEEP_HISTORY_DELIVERY_SHAPES: + cube_size += 1 + + dev = device_cls("d0") + dev.frontier[ctx] = b0 + dev.overrides[ctx] = ancestor + dev.do_advance_frontier(ctx, f1) + dev.do_compact(ctx, tie_policy) + _apply_action_seq(dev, ctx, seq, f1) + + if shape == "single": + dev.receive_merge({"contexts": dict(ancestor_blob)}) + ov_after = dev.override_is_set(ctx, tie_policy) + + ref = device_cls("ref") + ref.frontier[ctx] = b0 + ref.overrides[ctx] = ancestor + ref.do_advance_frontier(ctx, f1) + _apply_action_seq(ref, ctx, seq, f1) + ref.receive_merge({"contexts": dict(ancestor_blob)}) + ov_ref = ref.override_is_set(ctx, tie_policy) + + if ov_after != ov_ref: + violations.append(( + "I5c-deep-history-divergence", tie_policy, shape, + ancestor, f1, seq, + f"compacted_path={ov_after}", f"reference={ov_ref}", + )) + return cube_size, violations + + +def test_tombstone_stale_merge_direct(): + """Tombstone floor merged directly with its own pre-compaction stale + ancestor (no intervening local actions) must not resurrect and must + not exceed the ancestor's own verdict.""" + violations = [] + vals = (0, 1, 2, 3) + frontiers = (0, 10, 20) + for tie_policy in (CLEAR, SET): + for s in vals: + for c in vals: + for b in frontiers: + for fv in frontiers: + if fv <= b: + continue + reg = RegB(s=s, c=c, b=b) + compacted = compact_b(reg, fv, tie_policy) + if compacted is None: + continue # virgin register: nothing to tombstone + ov_before = override_set_b(reg, fv, tie_policy) + for merged in (merge_reg_b(compacted, reg), merge_reg_b(reg, compacted)): + ov_merged = override_set_b(merged, fv, tie_policy) + if not ov_before and ov_merged: + violations.append(( + "tombstone-stale-merge-resurrection", + tie_policy, reg, fv, compacted, merged, + )) + return violations + + +# --------------------------------------------------------------------------- +# I5d: cross-device compaction transparency (requalified — suppress-only, +# NOT zero-divergence) + re-mark recovery +# --------------------------------------------------------------------------- + +def test_tombstone_merge_monotonic(): + """Structural lemma: merging in ANY tombstone RegB(0, k, 0) is a + monotonically non-increasing function of the ceiling k in + override_set_b's boolean output, for a fixed receiving register and + frontier. A tombstone only ever adds to C (its S and B are both 0, + so max() with any receiving register leaves that register's own S + and B untouched) — raising C can only weaken S's relative standing, + never strengthen it. This is what makes resurrection structurally + impossible and suppression the only possible direction, independent + of any bounded cube. + """ + violations = [] + vals = (0, 1, 2, 3) + baselines = (0, 10, 20) + ceilings = (0, 1, 2, 3, 4, 5) + for tie_policy in (CLEAR, SET): + for s in vals: + for c in vals: + for b in baselines: + for fv in baselines: + x_reg = RegB(s=s, c=c, b=b) + prev = None + for k in ceilings: + merged = merge_reg_b(x_reg, RegB(s=0, c=k, b=0)) + cur = override_set_b(merged, fv, tie_policy) + if prev is not None and cur and not prev: + violations.append(( + "I5d-non-monotonic-ceiling", tie_policy, + x_reg, fv, k, merged, + )) + prev = cur + return violations + + +def test_cross_device_compaction_suppression(device_cls=DeviceB): + """Compaction is NOT semantically transparent cross-device (I5c only + covers the same-device replay shape). A tombstone re-encodes + baseline-dominated death — frontier-relative, doesn't transfer + across devices — as a clear-counter ceiling — globally comparable — + so it can one-shot suppress an unrelated device's concurrent fresh + set whose own counters don't exceed that ceiling. + + Witness (Paul's report, illustrative — the cube below tests nearby + parameter values `f_x` in `(5, 15, 25, 35)`, not the literal + `f_x=30` used in the original report; the shape is the same): + Y: mark_unread -> RegB(1,0,0); frontier->10 (dead) -> compact -> + tombstone RegB(0,1,0) + X: offline, fresh mark_unread at frontier 30 -> RegB(1,0,30), LIVE + X merges Y's tombstone -> RegB(1,1,30) -> suppressed (clear-wins) + Control (Y publishes the uncompacted RegB(1,0,0) instead): X stays + RegB(1,0,30), LIVE — the divergence is caused by compaction, not + by the merge itself. + + Proves over a bounded cube, both tie policies: every divergence + between "X merges Y's tombstone" and "X merges Y's uncompacted + ancestor" is a suppression (never a resurrection — that would + contradict test_tombstone_merge_monotonic), and every suppression + recovers with one more local mark-unread, stable under tombstone + replay. + + Returns (cube_size, suppress_count, violations). + """ + violations = [] + cube_size = 0 + suppress_count = 0 + dead_vals = (0, 1, 2, 3) + dead_baselines = (0, 10) + dead_post_frontiers = (10, 20) + fresh_frontiers = (5, 15, 25, 35) + + for tie_policy in (CLEAR, SET): + for s_y in dead_vals: + for c_y in dead_vals: + for b_y in dead_baselines: + for f_y in dead_post_frontiers: + if f_y <= b_y: + continue + ancestor = RegB(s=s_y, c=c_y, b=b_y) + tomb = compact_b(ancestor, f_y, tie_policy) + if tomb is None or tomb == ancestor: + continue # virgin, or was live (not compacted) + + for f_x in fresh_frontiers: + cube_size += 1 + x_reg = RegB(s=1, c=0, b=f_x) + x_before = override_set_b(x_reg, f_x, tie_policy) + if not x_before: + violations.append(( + "I5d-setup-not-live", tie_policy, x_reg, f_x, + )) + continue + + ov_tomb = override_set_b( + merge_reg_b(x_reg, tomb), f_x, tie_policy + ) + ov_ancestor = override_set_b( + merge_reg_b(x_reg, ancestor), f_x, tie_policy + ) + + if ov_tomb == ov_ancestor: + continue + if ov_tomb and not ov_ancestor: + violations.append(( + "I5d-resurrection-vs-ancestor", tie_policy, + ancestor, tomb, x_reg, f_x, + )) + continue + + suppress_count += 1 + dev = device_cls("x") + dev.frontier["c0"] = f_x + dev.overrides["c0"] = merge_reg_b(x_reg, tomb) + dev.do_mark_unread("c0") + if not dev.override_is_set("c0", tie_policy): + violations.append(( + "I5d-recovery-failed", tie_policy, + ancestor, tomb, x_reg, f_x, dev.overrides["c0"], + )) + continue + dev.receive_merge({"contexts": { + "ov_s:c0": tomb.s, "ov_c:c0": tomb.c, "ov_b:c0": tomb.b, + }}) + if not dev.override_is_set("c0", tie_policy): + violations.append(( + "I5d-recovery-not-replay-stable", tie_policy, + ancestor, tomb, x_reg, f_x, dev.overrides["c0"], + )) + + return cube_size, suppress_count, violations + + +# --------------------------------------------------------------------------- +# New invariant: published-state merge closure (Paul's fix-scope item 2, +# generalizing Thufir's pass-1/2 CRITICAL — dead+dead merge resurrection) +# --------------------------------------------------------------------------- + +def _dead_register_points(tie_policy): + """Bounded cube of (label, reg, frontier) points independently + verified DEAD (inactive) under `tie_policy` by the real + `override_set_b` predicate — the death cause (baseline dominance, + clear-count dominance, or clear-wins tie) is whatever the predicate + actually computes for that point, not asserted by construction. + """ + vals = (0, 1, 2, 3) + baselines = (0, 10, 50) + frontiers = (0, 20, 60, 100) + points = [] + for s in vals: + for c in vals: + if s == 0 and c == 0: + continue # virgin: not a "dead override" case + for b in baselines: + for fv in frontiers: + reg = RegB(s=s, c=c, b=b) + if override_set_b(reg, fv, tie_policy): + continue # live: out of scope for this invariant + points.append((f"s={s}c={c}b={b}fv={fv}", reg, fv)) + return points + + +def test_published_merge_closure(device_cls=DeviceB): + """Over reachable *published* states: joining any two individually- + inactive published states must remain inactive. + + This targets Thufir's pass-1/2 CRITICAL directly: a dead register's + death cause is frontier-relative (baseline dominance) or + device-local-history-relative (clear-count dominance), but the + componentwise-max join recombines each register's `S`/`C`/`B` + independent of the history that produced them, so two individually- + dead registers could — before canonical publication — recombine + into a live join. Canonicalizing every override to `RegB(0, + max(S,C), 0)` before serialization (this round's CRITICAL fix) + folds every dead cause into a single globally-comparable `C` + ceiling with `S=0`, which per `test_tombstone_merge_monotonic` can + only ever raise a receiver's `C` — never resurrect. + + Checked two ways: + - Directed case: Thufir's exact witness pair — `RegB(3,2,0)` + inactive via baseline dominance at frontier 50, `RegB(1,2,100)` + inactive via clear dominance at frontier 100 — whose raw + componentwise join is `RegB(3,2,100)`, live (`S=3>C=2`, + `frontier(100) not> B(100)`). Both tie policies. + - General search: every pairwise join of a bounded cube of + independently-dead `(reg, frontier)` points (see + `_dead_register_points`), delivered to a fresh receiver in both + direct orders and via a one-hop relay that itself republishes + (re-canonicalizes) what it received before forwarding — covering + delayed/multi-hop delivery, not just direct pairwise merge. + + Returns (cube_size, violations). + """ + violations = [] + cube_size = 0 + + def _check_pair(tie_policy, label_a, blob_a, label_b, blob_b, tag): + nonlocal cube_size + cube_size += 1 + for first, second in [(blob_a, blob_b), (blob_b, blob_a)]: + recv = device_cls("recv") + recv.receive_merge(first) + recv.receive_merge(second) + if recv.override_is_set("c0", tie_policy): + violations.append(( + tag, tie_policy, label_a, label_b, recv.overrides.get("c0"), + )) + # Multi-hop: a relay receives blob_a alone, republishes + # (re-canonicalizes) before forwarding, then the receiver gets + # the relayed form plus blob_b directly, in both orders. + relay = device_cls("relay") + relay.receive_merge(blob_a) + relayed = relay.publish_blob(tie_policy) + for first, second in [(relayed, blob_b), (blob_b, relayed)]: + recv = device_cls("recv_hop") + recv.receive_merge(first) + recv.receive_merge(second) + if recv.override_is_set("c0", tie_policy): + violations.append(( + tag + "-multihop", tie_policy, label_a, label_b, + recv.overrides.get("c0"), + )) + + # --- Directed case: Thufir's exact witness pair. --- + for tie_policy in (CLEAR, SET): + reg_a, front_a = RegB(s=3, c=2, b=0), 50 + reg_b, front_b = RegB(s=1, c=2, b=100), 100 + assert not override_set_b(reg_a, front_a, tie_policy) + assert not override_set_b(reg_b, front_b, tie_policy) + + dev_a = device_cls("a") + dev_a.frontier["c0"] = front_a + dev_a.overrides["c0"] = reg_a + dev_b = device_cls("b") + dev_b.frontier["c0"] = front_b + dev_b.overrides["c0"] = reg_b + + _check_pair( + tie_policy, f"thufir-witness-A={reg_a}@{front_a}", + dev_a.publish_blob(tie_policy), + f"thufir-witness-B={reg_b}@{front_b}", + dev_b.publish_blob(tie_policy), + "merge-closure-thufir-witness", + ) + + # --- General search over a bounded cube of dead published states. --- + for tie_policy in (CLEAR, SET): + points = _dead_register_points(tie_policy) + for label_a, reg_a, front_a in points: + dev_a = device_cls("a") + dev_a.frontier["c0"] = front_a + dev_a.overrides["c0"] = reg_a + blob_a = dev_a.publish_blob(tie_policy) + for label_b, reg_b, front_b in points: + dev_b = device_cls("b") + dev_b.frontier["c0"] = front_b + dev_b.overrides["c0"] = reg_b + blob_b = dev_b.publish_blob(tie_policy) + _check_pair( + tie_policy, label_a, blob_a, label_b, blob_b, + "merge-closure-cube", + ) + + return cube_size, violations + + +# --------------------------------------------------------------------------- +# I6: replay harmless +# --------------------------------------------------------------------------- + +def test_replay_harmless(device_cls=DeviceB): + violations = [] + for tie_policy in [CLEAR, SET]: + for ctx in CONTEXTS: + d = device_cls("d0") + d.frontier[ctx] = 10 + d.do_mark_unread(ctx) + blob = d.publish_blob(tie_policy) + state_before = ( + dict(d.frontier), + {k: v for k, v in d.overrides.items()}, + ) + d.receive_merge(blob) + d.receive_merge(blob) + d.receive_merge(blob) + state_after = ( + dict(d.frontier), + {k: v for k, v in d.overrides.items()}, + ) + if state_before != state_after: + violations.append(("I6-replay", tie_policy, ctx)) + return violations + + +# --------------------------------------------------------------------------- +# I7: legacy rewrite +# --------------------------------------------------------------------------- + +def test_legacy_rewrite_b(): + """B's sibling keys survive legacy sanitization (round-trip).""" + violations = [] + for ctx in CONTEXTS: + d = DeviceB("d0") + d.frontier[ctx] = 10 + d.do_mark_unread(ctx) + blob = d.publish_blob() + sanitized = legacy_sanitize_blob(blob) + + recv_orig = DeviceB("recv1") + recv_orig.receive_merge(blob) + recv_san = DeviceB("recv2") + recv_san.receive_merge(sanitized) + + for c in CONTEXTS: + if recv_orig.overrides.get(c) != recv_san.overrides.get(c): + violations.append(("I7-B-sanitize-mutated", c, + recv_orig.overrides.get(c), + recv_san.overrides.get(c))) + return violations + + +def test_legacy_erasure_a(): + """A's top-level overrides field is erased by legacy rewrite. Expected witness.""" + d = DeviceA("d0") + d.frontier["c0"] = 10 + d.do_mark_unread("c0") + blob = d.publish_blob() + assert "overrides" in blob + legacy_blob = {"v": 1, "client_id": "legacy", "contexts": dict(blob["contexts"])} + return "overrides" not in legacy_blob + + +# --------------------------------------------------------------------------- +# I8: bounded key growth +# --------------------------------------------------------------------------- + +def test_bounded_growth(): + """I8: bounded key growth, canonical wire shape. A live override + (last action = mark_unread, still within baseline) publishes + exactly 3 keys/ctx; a dead override (mark_read past baseline, or + C > S under clear-wins) canonicalizes to exactly 1 key/ctx + (`ov_c:` tombstone) at publish time — never 0 (virgin-only) or 3 + (dead-but-uncompacted, which the pre-fix serializer allowed). + """ + violations = [] + for ctx in CONTEXTS: + # Live: 100 set/clear round-trips, ending on a fresh mark_unread + # so S > C (live under both tie policies) at publish time. + d = DeviceB("d0") + d.frontier[ctx] = 10 + for _ in range(100): + d.do_mark_unread(ctx) + d.do_mark_read(ctx, d.effective_frontier(ctx) + 1) + d.do_mark_unread(ctx) + blob = d.publish_blob(CLEAR) + ov_keys = [k for k in blob["contexts"] if k.startswith("ov_")] + if ov_keys != [f"ov_s:{ctx}", f"ov_c:{ctx}", f"ov_b:{ctx}"]: + violations.append(("I8-growth-live", ctx, ov_keys)) + + # Dead: advance the frontier past baseline B — override_set_b's + # baseline-dominance clause forces S dead regardless of S vs C. + d.do_advance_frontier(ctx, d.effective_frontier(ctx) + 100) + tomb_blob = d.publish_blob(CLEAR) + tomb_keys = [k for k in tomb_blob["contexts"] if k.startswith("ov_")] + if tomb_keys != [f"ov_c:{ctx}"]: + violations.append(("I8-growth-tombstone", ctx, tomb_keys)) + return violations + + +def test_wire_shape_exact(): + """Exact wire-shape regression (Paul's fix-scope item 4): a live + override serializes to exactly 3 `ov_*` keys, a dead override to + exactly 1 (`ov_c:` only, zero-valued `ov_s`/`ov_b` omitted), and a + virgin override to exactly 0. Checked directly against + `publish_blob`'s output, independent of `do_compact`. + """ + violations = [] + for tie_policy in (CLEAR, SET): + # Live. + d_live = DeviceB("d0") + d_live.frontier["c0"] = 10 + d_live.do_mark_unread("c0") + live_blob = d_live.publish_blob(tie_policy) + live_keys = sorted(k for k in live_blob["contexts"] if k.startswith("ov_")) + if live_keys != ["ov_b:c0", "ov_c:c0", "ov_s:c0"]: + violations.append(("wire-shape-live", tie_policy, live_keys)) + + # Dead (clear-wins only: S==C>0 is dead under CLEAR, live under + # SET — use baseline dominance instead so it's dead under both). + d_dead = DeviceB("d0") + d_dead.frontier["c0"] = 10 + d_dead.do_mark_unread("c0") + d_dead.do_advance_frontier("c0", 100) + dead_blob = d_dead.publish_blob(tie_policy) + dead_keys = sorted(k for k in dead_blob["contexts"] if k.startswith("ov_")) + if dead_keys != ["ov_c:c0"]: + violations.append(("wire-shape-tombstone", tie_policy, dead_keys)) + if dead_blob["contexts"]["ov_c:c0"] != 1: + violations.append(( + "wire-shape-tombstone-ceiling", tie_policy, + dead_blob["contexts"]["ov_c:c0"], + )) + + # Virgin: no override ever set for this context. + d_virgin = DeviceB("d0") + d_virgin.frontier["c0"] = 10 + d_virgin.overrides["c0"] = RegB(s=0, c=0, b=0) + virgin_blob = d_virgin.publish_blob(tie_policy) + virgin_keys = [k for k in virgin_blob["contexts"] if k.startswith("ov_")] + if virgin_keys: + violations.append(("wire-shape-virgin", tie_policy, virgin_keys)) + + return violations + + +# --------------------------------------------------------------------------- +# I9: DeviceA counter absorption +# --------------------------------------------------------------------------- + +def test_a_counter_absorption(): + """After receiving a blob with counter=10, a local action must use counter>10.""" + d0 = DeviceA("d0") + d0.frontier["c0"] = 10 + d0.counter = 10 + d0.do_mark_unread("c0") + blob0 = d0.publish_blob() + + d1 = DeviceA("d1") + d1.frontier["c0"] = 10 + d1.receive_merge(blob0) + assert d1.counter >= 10, f"counter not absorbed: {d1.counter}" + + d1.do_mark_read("c0", 20) + reg = d1.overrides.get("c0") + assert reg is not None and reg.counter > 10, \ + f"post-receive clear at counter {reg.counter} would lose to set at 10" + return True + + +# --------------------------------------------------------------------------- +# Identity-free (B): reinstall convergence +# --------------------------------------------------------------------------- + +def test_b_identity_free(device_cls=DeviceB): + violations = [] + for tie_policy in [CLEAR, SET]: + for ctx in CONTEXTS: + d = device_cls("d0") + d.frontier[ctx] = 10 + d.do_mark_unread(ctx) + blob1 = d.publish_blob(tie_policy) + + d_re = device_cls("d0_reinstalled") + d_re.receive_merge(blob1) + d_re.do_mark_read(ctx, 20) + blob2 = d_re.publish_blob(tie_policy) + + verdicts = set() + for first, second in [(blob1, blob2), (blob2, blob1)]: + recv = device_cls("recv") + recv.receive_merge(first) + recv.receive_merge(second) + verdicts.add(recv.override_is_set(ctx, tie_policy)) + if len(verdicts) > 1: + violations.append(("identity-free", tie_policy, ctx)) + return violations + + +# --------------------------------------------------------------------------- +# Legacy prune/trim interaction +# --------------------------------------------------------------------------- + +def test_legacy_prune_interaction(): + """ov_ keys survive prune; msg:ov_ nested keys would be pruned (state loss).""" + base = {"c0": 50, "msg:m1": 30, "thread:t1": 40} + ov = {"ov_s:c0": 1, "ov_c:c0": 0, "ov_b:c0": 10} + all_keys = {**base, **ov} + pruned = legacy_prune(all_keys, horizon=35) + ov_survived = all(k in pruned for k in ov) + msg_pruned = "msg:m1" not in pruned + + nested = {"msg:ov_s:c0": 1, "msg:ov_c:c0": 0, "msg:ov_b:c0": 10} + pruned_nested = legacy_prune({**base, **nested}, horizon=35) + nested_lost = any(k not in pruned_nested for k in nested) + return ov_survived, msg_pruned, nested_lost + + +def test_legacy_trim_interaction(): + """Excess override keys block legacy publish when budget exceeded.""" + contexts = {"c0": 50} + for i in range(1000): + contexts[f"ov_s:c{i}"] = 1 + contexts[f"ov_c:c{i}"] = 0 + contexts[f"ov_b:c{i}"] = 10 + _, fits = legacy_trim(contexts, "client1", max_bytes=32768) + return not fits + + +# --------------------------------------------------------------------------- +# Multi-slot union +# --------------------------------------------------------------------------- + +def test_multi_slot_union(device_cls=DeviceB): + """Split a published blob across 2 slots using the atomic-grouping rule, + deliver each slot separately, verify convergence with delivering the full blob. + + Production: mergeReadStateEvents merges per-slot blobs with per-context + max(). Override sibling keys are individual context entries, so they + follow the same merge path. The atomic-grouping rule requires that all + `ov_*` sibling keys for a context travel with that context's frontier + key in the same slot — `split_blob_into_slots` enforces this. + """ + violations = [] + for tie_policy in [CLEAR, SET]: + dev = device_cls("d0") + dev.frontier["c0"] = 10 + dev.frontier["c1"] = 20 + dev.do_mark_unread("c0") + dev.do_mark_read("c1", 30) + + full_blob = dev.publish_blob(tie_policy) + slots = dev.split_blob_into_slots(tie_policy, n_slots=2) + slot0, slot1 = slots[0], slots[1] + + recv_full = device_cls("recv_full") + recv_full.receive_merge(full_blob) + + for first, second in [(slot0, slot1), (slot1, slot0)]: + recv_split = device_cls("recv_split") + recv_split.receive_merge(first) + recv_split.receive_merge(second) + + for ctx in CONTEXTS: + ov_full = recv_full.override_is_set(ctx, tie_policy) + ov_split = recv_split.override_is_set(ctx, tie_policy) + f_full = recv_full.effective_frontier(ctx) + f_split = recv_split.effective_frontier(ctx) + if ov_full != ov_split: + violations.append(("multi-slot-override", tie_policy, ctx)) + if f_full != f_split: + violations.append(("multi-slot-frontier", tie_policy, ctx)) + return violations + + +# --------------------------------------------------------------------------- +# Interleaved-delivery grouping: Thufir's CRITICAL transport counterexample +# +# Without the atomic-grouping rule a compliant publisher would still split +# ov_s:/ov_c:/ov_b: across slots as independent entries. M8's per-entry +# split places frontier+ov_s: in slot 0 and ov_b:+ov_c: in slot 1. An +# observer holding only slot 0 reconstructs RegB(1,0,0), judges it +# baseline-dead (B=0 ≤ frontier=10), and canonically publishes tombstone +# RegB(0,1,0). After all slots and that transient tombstone are eventually +# merged the result is RegB(1,1,10) — dead under clear-wins — +# permanently suppressing a live override. +# +# The atomic-grouping rule closes this: every ov_* entry for a context +# travels with the context's frontier entry, so a receiver always sees +# either the complete register or nothing. This test exercises both: +# - The PASS path: grouped slots → no false tombstone possible. +# - The FAIL path (M8): per-entry split → Thufir's exact witness reproduced. +# --------------------------------------------------------------------------- + +def test_interleaved_delivery_grouping(device_cls=DeviceB): + """Exercise receive-one-slot → canonical re-publish → receive-rest → + re-publish permutations, both slot orders, including delayed delivery + of both transient re-publications to a third observer. + + Protocol sequence (exact, per Paul's brief): + 1. partial_obs receives first_slot → publishes transient_1. + 2. partial_obs receives second_slot → publishes transient_2. + 3. Third-party finals receive BOTH source slots AND both transient + publications in relevant interleaving orders. + Oracle: after eventual delivery of ALL blobs (both source slots + + both transients), every observer's override matches source liveness. + + With the atomic-grouping rule (default DeviceB): + - The compliant split puts the full register in one slot, the other + is empty. partial_obs after step 1 holds either the complete + register (live → transient_1 is live) or nothing (transient_1 is + empty/virgin). Either way, step 2 delivers the remaining (possibly + empty) slot. Final merge of all blobs = source liveness. PASS. + With per-entry splitting (M8): + - slot 0 carries frontier + ov_s: (partial → RegB(1,0,0), dead). + transient_1 is tombstone RegB(0,1,0). After step 2 partial_obs + holds full register but transient_1 tombstone is already in + circulation. Finals that receive transient_1 get + RegB(1,1,10) — dead under clear-wins. FAIL (Thufir's witness). + """ + violations = [] + + # Source: live override RegB(1,0,10) at frontier=10 — Thufir's witness. + src_s, src_c, src_b, src_front = 1, 0, 10, 10 + + for tie_policy in (CLEAR, SET): + src = device_cls("src") + src.frontier["c0"] = src_front + src.overrides["c0"] = RegB(s=src_s, c=src_c, b=src_b) + + # Confirm source is actually live. + assert src.override_is_set("c0", tie_policy), ( + f"test precondition: source must be live under {tie_policy}" + ) + + # Produce the source's two slots via the (possibly mutated) split. + slots = src.split_blob_into_slots(tie_policy, n_slots=2) + slot0, slot1 = slots[0], slots[1] + src_live = src.override_is_set("c0", tie_policy) + + for first_slot, second_slot in [(slot0, slot1), (slot1, slot0)]: + # Step 1: partial_obs receives first slot, canonically re-publishes. + partial_obs = device_cls("partial_obs") + partial_obs.receive_merge(first_slot) + transient_1 = partial_obs.publish_blob(tie_policy) + + # Step 2: partial_obs receives second slot, publishes again. + partial_obs.receive_merge(second_slot) + transient_2 = partial_obs.publish_blob(tie_policy) + + # Step 3: third-party finals receive BOTH source slots AND both + # transient publications, in several representative interleaving + # orders. All must agree with source liveness. + # Representative orders: transient_1 before both slots (most + # dangerous under M8), transient_1 after both slots, and + # interleaved. We check 3 explicit orders rather than all 4! + # permutations (24) for speed; M8's canonical false-clear path + # (transient_1 first, then second_slot only) is order 1. + check_orders = [ + # Most dangerous: transient_1 arrives first, before any source + [transient_1, slot0, slot1, transient_2], + # Normal: both source slots first, then both transients + [slot0, slot1, transient_1, transient_2], + # Interleaved: first source, transient_1, second source, transient_2 + [first_slot, transient_1, second_slot, transient_2], + ] + + for order in check_orders: + final = device_cls("final") + for blob in order: + final.receive_merge(blob) + final_live = final.override_is_set("c0", tie_policy) + if final_live != src_live: + t1_reg = partial_obs.overrides.get("c0") + violations.append(( + "interleaved-delivery-false-clear", + tie_policy, + f"slot_order=(first={list(first_slot['contexts'].keys())[:2]}...)", + f"delivery_order={[list(b['contexts'].keys())[:2] for b in order]}", + f"transient_1_reg={t1_reg}", + f"final_reg={final.overrides.get('c0')}", + f"expected_live={src_live} got_live={final_live}", + )) + + return violations + + +# --------------------------------------------------------------------------- +# Escaped-context slot-grouping regression +# +# Thufir's CRITICAL (round 2): a raw context ID that starts with a +# reserved prefix (e.g. "ov_s:evil") escapes to "esc:ov_s:evil" as its +# frontier wire key. Before the fix, split_blob_into_slots grouped the +# frontier by its wire key ("esc:ov_s:evil") but the ov_* siblings by +# the raw suffix ("ov_s:evil") — two identities for one logical context. +# The frontier and its siblings landed in different slots. +# +# Across publication cycles the replaceable slot d-tag coordinates +# update slot-by-slot. A relay can therefore serve: new frontier slot +# (just published, carries esc:ov_s:evil=10) + stale override slot +# (old coordinate, carries ov_s/ov_c/ov_b at b=0 from the old pub). +# The reconstructed register is RegB(s=1, c=0, b=0) at frontier=10 — +# baseline-dead. Canonical re-publication emits tombstone RegB(0,1,0). +# Eventually both current slots + the transient merge to RegB(1,1,10) — +# dead under clear-wins — permanently suppressing a live override. +# +# The fix: derive the frontier's group identity via unescape_context_key +# so it joins the same group as its ov_* siblings. This test exercises +# both directions: M9 (reverts to escaped-key grouping) must reproduce +# the witness, and the correct model must pass. +# --------------------------------------------------------------------------- + +def test_escaped_context_slot_grouping(device_cls=DeviceB): + """Regression for escaped-context identity mismatch in split_blob_into_slots. + + Scenario: + 1. Source has a live override on raw context "ov_s:evil" (escapes to + "esc:ov_s:evil" as frontier wire key) — Thufir's exact escaped witness. + 2. Source publishes twice: first at frontier=0/b=0, then after advancing + frontier to 10 and re-marking unread (b=10). Each publication produces + 2 slots. Simulates a relay retaining a stale old-cycle slot under its + old replaceable coordinate while only the new-cycle slot for the OTHER + half has been updated — the old/new slot-coordinate mixture. + 3. An observer receives: new-cycle frontier-bearing slot (frontier=10, + esc:ov_s:evil=10) + stale old-cycle override slot (ov_s/ov_c/ov_b from + first pub where b=0). + 4. Observer canonically re-publishes (mandatory, per NIP-RS spec). + 5. A third-party final observer receives both current-cycle source slots + plus the transient re-publication. + 6. Oracle: final observer must see the override as live. + + With the unescape-before-group fix: frontier + ov_* siblings always land + in the same slot → no partial register → no false tombstone. PASS. + With M9 (escaped-key grouping): frontier in one slot, siblings in another + → partial reconstruction → false tombstone → final merge dead. FAIL. + """ + violations = [] + raw_ctx = "ov_s:evil" + + for tie_policy in (CLEAR, SET): + # --- Publication cycle 1: initial state, frontier=0 --- + src_old = device_cls("src") + src_old.frontier[raw_ctx] = 0 + src_old.do_mark_unread(raw_ctx) # RegB(s=1, c=0, b=0) + old_slots = src_old.split_blob_into_slots(tie_policy, n_slots=2) + # old_slots[0] is the "stale old-coordinate slot" a relay may retain. + + # --- Publication cycle 2: frontier advances, re-mark-unread --- + src_new = device_cls("src") + src_new.frontier[raw_ctx] = 10 + src_new.do_mark_unread(raw_ctx) # RegB(s=1, c=0, b=10) — live at frontier=10 + + assert src_new.override_is_set(raw_ctx, tie_policy), ( + f"test precondition: source must be live under {tie_policy}" + ) + + new_slots = src_new.split_blob_into_slots(tie_policy, n_slots=2) + + # --- Full delivery: both new slots → both current-cycle slot arrive --- + recv_full = device_cls("recv_full") + recv_full.receive_merge(new_slots[0]) + recv_full.receive_merge(new_slots[1]) + if not recv_full.override_is_set(raw_ctx, tie_policy): + violations.append(( + "escaped-ctx-full-delivery-dead", tie_policy, + f"full={recv_full.overrides.get(raw_ctx)}", + )) + + # --- Mixture: new frontier-bearing slot + stale old override slot --- + # Identify which new slot carries the frontier and which carries ov_*, + # then pair the frontier slot with the old-cycle override slot. + wire_frontier = escape_context_key(raw_ctx) + + new_frontier_slot_idx = 0 if wire_frontier in new_slots[0]["contexts"] else 1 + new_frontier_slot = new_slots[new_frontier_slot_idx] + old_override_slot = old_slots[1 - new_frontier_slot_idx] # opposite slot + + # Check whether the frontier and ov_* siblings are co-located in new_slots. + ov_s_key = f"ov_s:{raw_ctx}" + frontier_and_ov_same_slot = ( + wire_frontier in new_slots[new_frontier_slot_idx]["contexts"] and + ov_s_key in new_slots[new_frontier_slot_idx]["contexts"] + ) + + if frontier_and_ov_same_slot: + # Correct grouping: old override slot has nothing relevant, mixture + # is safe by construction — the stale slot is just an empty dict. + # Verify anyway for defense-in-depth. + obs = device_cls("obs") + obs.receive_merge(new_frontier_slot) + obs.receive_merge(old_override_slot) + transient = obs.publish_blob(tie_policy) + + final = device_cls("final") + final.receive_merge(new_slots[0]) + final.receive_merge(new_slots[1]) + final.receive_merge(transient) + if not final.override_is_set(raw_ctx, tie_policy): + violations.append(( + "escaped-ctx-grouped-mixture-dead", tie_policy, + f"transient={obs.overrides.get(raw_ctx)}", + f"final={final.overrides.get(raw_ctx)}", + )) + else: + # Mismatched grouping (M9 path): frontier and siblings split. + # The mixture produces a partial register → false tombstone. + obs = device_cls("obs") + obs.receive_merge(new_frontier_slot) # gets frontier=10, no ov_* + obs.receive_merge(old_override_slot) # gets ov_s/ov_c/ov_b at b=0 + transient = obs.publish_blob(tie_policy) + + # Final observer gets everything: both new slots + transient. + for order in [(new_slots[0], new_slots[1]), (new_slots[1], new_slots[0])]: + final = device_cls("final") + final.receive_merge(order[0]) + final.receive_merge(order[1]) + final.receive_merge(transient) + if not final.override_is_set(raw_ctx, tie_policy): + violations.append(( + "escaped-ctx-mixture-false-clear", tie_policy, + f"obs_reg={obs.overrides.get(raw_ctx)}", + f"transient_reg={transient['contexts']}", + f"final_reg={final.overrides.get(raw_ctx)}", + )) + + return violations + + +# --------------------------------------------------------------------------- +# Reserved key namespace: adversarial prefix collision +# --------------------------------------------------------------------------- + +def test_reserved_namespace_collision(): + """A genuine user context whose raw ID begins with the reserved `ov_` + stem (e.g. a pre-existing legacy context literally named `ov_s:evil`) + must round-trip as frontier state, not be misparsed as a control key + for a different context, and must not collide with a real override's + sibling keys in the same flattened contexts map. + + Exercises: escape on publish, unescape on receive, and a live + override on a DIFFERENT context in the same blob to prove no + control-key collision occurs. + """ + violations = [] + adversarial_raw = "ov_s:evil" # would misparse as ov_s: control for ctx "evil" + real_ctx = "c0" + + # Escaping must be a no-op for every context ID Buzz actually + # generates, and must trigger for the adversarial one. + for benign in ("b68cd7cb-6f8d-4641-b743-a7349eb4114b", + "msg:" + "a" * 64, "thread:" + "b" * 64): + if escape_context_key(benign) != benign: + violations.append(("namespace-benign-escaped", benign)) + if escape_context_key(adversarial_raw) == adversarial_raw: + violations.append(("namespace-adversarial-not-escaped", adversarial_raw)) + if not escape_context_key(adversarial_raw).startswith(ESCAPE_PREFIX): + violations.append(("namespace-adversarial-missing-marker", adversarial_raw)) + + dev = DeviceB("d0") + dev.frontier[adversarial_raw] = 42 + dev.frontier[real_ctx] = 5 + dev.do_mark_unread(real_ctx) + blob = dev.publish_blob() + + wire_key = escape_context_key(adversarial_raw) + if wire_key not in blob["contexts"]: + violations.append(("namespace-wire-key-missing", wire_key, blob["contexts"])) + if blob["contexts"].get(wire_key) != 42: + violations.append(("namespace-value-corrupted", wire_key, blob["contexts"].get(wire_key))) + + recv = DeviceB("recv") + recv.receive_merge(blob) + if recv.effective_frontier(adversarial_raw) != 42: + violations.append(( + "namespace-roundtrip-failed", adversarial_raw, + recv.effective_frontier(adversarial_raw), + )) + if adversarial_raw in recv.overrides: + violations.append(("namespace-misparsed-as-override", adversarial_raw)) + if recv.overrides.get(real_ctx) is None or recv.overrides[real_ctx].s == 0: + violations.append(("namespace-real-override-corrupted", real_ctx, recv.overrides.get(real_ctx))) + + return violations + + +# --------------------------------------------------------------------------- +# Run all +# --------------------------------------------------------------------------- + +def run_all(): + print("=" * 60) + print("NIP-RS manual-unread exhaustive model") + print("=" * 60) + total_violations = 0 + + def report(name, violations): + nonlocal total_violations + n = len(violations) if isinstance(violations, list) else 0 + total_violations += n + status = "PASS" if n == 0 else f"FAIL ({n})" + print(f" {name}: {status}") + if n > 0: + for v in violations[:3]: + print(f" {v}") + + print("\n--- I1: merge algebra (B) ---") + report("assoc/commut/idempot", test_merge_algebra_b()) + + print("\n--- I1: merge algebra (A) ---") + report("assoc/commut/idempot", test_merge_algebra_a()) + + print("\n--- I2+I3+I5: BFS explorer (B, clear-wins) ---") + n, v = explore_b(max_depth=4, tie_policy=CLEAR) + print(f" states explored: {n}") + report("convergence+frontier+compaction", v) + + print("\n--- I2+I3+I5: BFS explorer (B, set-wins) ---") + n, v = explore_b(max_depth=4, tie_policy=SET) + print(f" states explored: {n}") + report("convergence+frontier+compaction", v) + + print("\n--- I4: concurrent set/clear stability ---") + report("stable winner", test_concurrent_stability()) + + print("\n--- I5: compaction register-level exhaustive ---") + report("all register values x policies", test_compaction_register_exhaustive()) + + print("\n--- I5c: directed deep-history (compact -> reuse -> stale delivery) ---") + cube_size, deep_v = test_deep_history_compaction() + print(f" parameter cube size: {cube_size}") + report("no divergence from never-compact reference", deep_v) + + print("\n--- I5c: tombstone + stale-ancestor merge (direct) ---") + report("no resurrection", test_tombstone_stale_merge_direct()) + + print("\n--- I5d: tombstone-merge monotonicity (structural lemma) ---") + report("ceiling never strengthens S", test_tombstone_merge_monotonic()) + + print("\n--- I5d: cross-device compaction transparency (suppress-only) ---") + cd_cube, cd_suppress, cd_v = test_cross_device_compaction_suppression() + print(f" parameter cube size: {cd_cube} suppressions observed: {cd_suppress}") + report("suppress-only + recoverable", cd_v) + + print("\n--- Published-state merge closure (canonical publication guarantee) ---") + mc_cube, mc_v = test_published_merge_closure() + print(f" pairs checked: {mc_cube}") + report("no dead+dead resurrection", mc_v) + + print("\n--- I6: replay harmless ---") + report("replay", test_replay_harmless()) + + print("\n--- I7: legacy rewrite (B) ---") + report("sibling keys survive", test_legacy_rewrite_b()) + + print("\n--- I7: legacy erasure (A) — expected witness ---") + erased = test_legacy_erasure_a() + print(f" overrides erased by legacy: {'CONFIRMED' if erased else 'NOT FOUND'}") + if not erased: + total_violations += 1 + + print("\n--- I8: bounded growth ---") + report("canonical wire shape (3 live / 1 tombstone)", test_bounded_growth()) + + print("\n--- I8: exact wire-shape regression ---") + report("live=3 keys, tombstone=1 key, virgin=0 keys", test_wire_shape_exact()) + + print("\n--- I9: DeviceA counter absorption ---") + absorbed = test_a_counter_absorption() + print(f" post-receive counter > received: {'CONFIRMED' if absorbed else 'FAIL'}") + if not absorbed: + total_violations += 1 + + print("\n--- Identity-free (B) ---") + report("reinstall convergence", test_b_identity_free()) + + print("\n--- Legacy prune interaction ---") + ov_ok, msg_ok, nested_lost = test_legacy_prune_interaction() + print(f" ov_ keys survive: {'PASS' if ov_ok else 'FAIL'}") + print(f" msg: pruned at horizon: {'PASS' if msg_ok else 'FAIL'}") + print(f" nested msg:ov_ lost: {'CONFIRMED (hazard)' if nested_lost else 'NOT FOUND'}") + if not ov_ok: + total_violations += 1 + + print("\n--- Legacy trim interaction ---") + blocked = test_legacy_trim_interaction() + print(f" excess overrides block publish: {'CONFIRMED (hazard)' if blocked else 'NOT FOUND'}") + + print("\n--- Multi-slot union ---") + report("split+merge convergence", test_multi_slot_union()) + + print("\n--- Interleaved delivery + atomic grouping rule ---") + report("no false clear under slot interleaving", test_interleaved_delivery_grouping()) + + print("\n--- Escaped-context slot-grouping regression ---") + report("escaped ctx: frontier + ov_* siblings same slot", test_escaped_context_slot_grouping()) + + print("\n--- Reserved key namespace: adversarial prefix collision ---") + report("escape/unescape + no misparse", test_reserved_namespace_collision()) + + print("\n" + "=" * 60) + if total_violations == 0: + print("ALL INVARIANTS HOLD — 0 violations") + else: + print(f"VIOLATIONS: {total_violations}") + print("=" * 60) + return total_violations + + +if __name__ == "__main__": + import sys + sys.exit(0 if run_all() == 0 else 1) diff --git a/docs/formal/nip-rs-unread/model.py b/docs/formal/nip-rs-unread/model.py new file mode 100644 index 0000000000..4400280571 --- /dev/null +++ b/docs/formal/nip-rs-unread/model.py @@ -0,0 +1,492 @@ +"""Bounded exhaustive model comparing two NIP-RS manual-unread encodings. + +Candidate A: lexicographic operation register + Per context: {counter, client_tiebreak, op in {SET,CLEAR}, baseline} + in a NEW top-level field beside `contexts`. + Merge = max tuple (counter, tiebreak, op-rule on full tie). + +Candidate B: two grow-only counters + baseline + Per context: S (set counter), C (clear counter), B (frontier-at-set-time) + as sibling keys under `contexts` (ov_s:, ov_c:, ov_b: prefixes). + Action: own counter := max(S,C)+1; set also writes B := effective frontier. + Merge = componentwise max. Tie policy on S == C is a parameter. + +Both share: + - Frontier: grow-only max() per NIP-RS v1 (unchanged). + - Verdict: unread(ctx) = latest > effective_frontier(ctx) OR override_set(ctx). + - Mark-read = advance frontier + clear override. + - Mark-unread = set override with baseline B = current effective frontier. + - Natural frontier advance strictly past B dominates a stale set. + +Device simulators use overridable methods (_override_set, _compact, _merge_reg, +_bump, _sanitize_value) so the mutation harness can inject weakened rules via +subclassing without monkeypatching. +""" +from dataclasses import dataclass +from typing import Optional + + +SET = "SET" +CLEAR = "CLEAR" + + +# --------------------------------------------------------------------------- +# Reserved key namespace + escaping +# +# NIP-RS v1 context IDs are arbitrary UTF-8 (spec :89, :113-114), so a +# pre-existing opaque context could legitimately begin with `ov_s:`, +# `ov_c:`, or `ov_b:` and collide with a control key for a DIFFERENT +# context in the same flattened `contexts` map. `ov_` (the shared +# 3-byte stem) and the escape marker itself are reserved; any raw +# context ID that would collide is escaped before being used as a +# plain frontier key. Escaping is a no-op for every context ID Buzz +# actually generates (channel UUID, `msg:`, `thread:` +# — none start with `ov_` or `esc:`), so the common case pays zero +# bytes. Only a pathological ID pays the 4-byte `esc:` cost. +# +# This protects context IDs generated by amendment-aware clients. +# It does NOT retroactively protect a context that a PRE-EXISTING +# legacy client already published unescaped before the amendment +# shipped — that residual hazard is documented, not solved (see +# NOTE.md "Reserved key namespace"). +# --------------------------------------------------------------------------- + +ESCAPE_PREFIX = "esc:" +_RESERVED_STEM = "ov_" + + +def _needs_escape(raw_key: str) -> bool: + return raw_key.startswith(_RESERVED_STEM) or raw_key.startswith(ESCAPE_PREFIX) + + +def escape_context_key(raw_key: str) -> str: + return ESCAPE_PREFIX + raw_key if _needs_escape(raw_key) else raw_key + + +def unescape_context_key(wire_key: str) -> str: + if wire_key.startswith(ESCAPE_PREFIX): + return wire_key[len(ESCAPE_PREFIX):] + return wire_key + + +# --------------------------------------------------------------------------- +# Candidate B — two grow-only counters + baseline +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class RegB: + s: int = 0 + c: int = 0 + b: int = 0 + + +def merge_reg_b(a: Optional[RegB], b: Optional[RegB]) -> Optional[RegB]: + if a is None: + return b + if b is None: + return a + return RegB(s=max(a.s, b.s), c=max(a.c, b.c), b=max(a.b, b.b)) + + +def override_set_b(reg: Optional[RegB], frontier_val: int, tie_policy=CLEAR) -> bool: + if reg is None: + return False + if frontier_val > reg.b and reg.s > 0: + return False + if reg.s > reg.c: + return True + if reg.s == reg.c and reg.s > 0: + return tie_policy == SET + return False + + +def compact_b(reg: RegB, frontier_val: int, tie_policy=CLEAR) -> Optional[RegB]: + """Compact override state. + + Tombstone-floor design: a register with any recorded counter + activity (S>0 or C>0) is never fully deleted. Its counter + high-water-mark is exactly what prevents a stale replica — + any (S,C) pair below that ceiling — from dominating a freshly + created register after compaction (delete-on-dominance made + counters reusable: a dead register dropped entirely, then a new + local set/clear pair restarted from S=0/C=0, so a delayed stale + peer snapshot with S>0 could out-rank the new state on replay). + Only a virgin register (S==0, C==0, no activity ever recorded) + has no ceiling to protect and compacts to None. + + A live override (per `override_set_b`, which is already + policy-aware) is returned unchanged — compaction only touches dead + state. Dead overrides — whether dominated by C>S, tied under + clear-wins, or baseline-dominated by frontier advance — compact to + the clear-tombstone floor `RegB(s=0, c=max(S,C), b=0)`: S is + zeroed (no longer overriding), but C retains the ceiling so both a + future local bump (`max(S,C)+1`) and a componentwise-max merge with + any pre-compaction stale snapshot start strictly above the + historical maximum, never below it. + """ + if reg.s == 0 and reg.c == 0: + return None + if override_set_b(reg, frontier_val, tie_policy): + return reg + return RegB(s=0, c=max(reg.s, reg.c), b=0) + + +# --------------------------------------------------------------------------- +# Candidate A — lexicographic operation register +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class RegA: + counter: int = 0 + tiebreak: str = "" + op: str = CLEAR + baseline: int = 0 + + def as_tuple(self, op_wins): + op_val = 1 if self.op == op_wins else 0 + return (self.counter, self.tiebreak, op_val) + + +def merge_reg_a(a: Optional[RegA], b: Optional[RegA], tie_op=CLEAR) -> Optional[RegA]: + if a is None: + return b + if b is None: + return a + at = a.as_tuple(tie_op) + bt = b.as_tuple(tie_op) + if at == bt: + return RegA( + counter=a.counter, tiebreak=a.tiebreak, op=a.op, + baseline=max(a.baseline, b.baseline), + ) + return a if at > bt else b + + +# --------------------------------------------------------------------------- +# Device simulation — Candidate B +# --------------------------------------------------------------------------- + +class DeviceB: + """Simulates one device's NIP-RS read-state blob with manual-unread + override layer (candidate B encoding). + + All model operations go through overridable _methods so the mutation + harness can inject weakened rules via subclassing. + """ + + def __init__(self, client_id, is_legacy=False): + self.client_id = client_id + self.is_legacy = is_legacy + self.frontier = {} + self.overrides = {} + + def effective_frontier(self, ctx): + return self.frontier.get(ctx, 0) + + def _override_set(self, reg, frontier_val, tie_policy): + return override_set_b(reg, frontier_val, tie_policy) + + def _compact(self, reg, frontier_val, tie_policy): + return compact_b(reg, frontier_val, tie_policy) + + def _merge_reg(self, a, b): + return merge_reg_b(a, b) + + def _bump(self, s, c): + return max(s, c) + 1 + + def _sanitize_value(self, v): + return isinstance(v, int) and 0 <= v <= 4294967295 + + def override_is_set(self, ctx, tie_policy=CLEAR): + return self._override_set( + self.overrides.get(ctx), self.effective_frontier(ctx), tie_policy + ) + + def verdict(self, ctx, latest_ts, tie_policy=CLEAR): + return (latest_ts > self.effective_frontier(ctx) + or self.override_is_set(ctx, tie_policy)) + + def do_mark_unread(self, ctx): + if self.is_legacy: + return + cur = self.overrides.get(ctx, RegB()) + new_s = self._bump(cur.s, cur.c) + self.overrides[ctx] = RegB(s=new_s, c=cur.c, b=self.effective_frontier(ctx)) + + def do_mark_read(self, ctx, frontier_ts): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), frontier_ts) + if not self.is_legacy: + cur = self.overrides.get(ctx, RegB()) + new_c = self._bump(cur.s, cur.c) + self.overrides[ctx] = RegB(s=cur.s, c=new_c, b=cur.b) + + def do_advance_frontier(self, ctx, ts): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), ts) + + def do_compact(self, ctx, tie_policy=CLEAR): + reg = self.overrides.get(ctx) + if reg is None: + return + result = self._compact(reg, self.effective_frontier(ctx), tie_policy) + if result is None: + if ctx in self.overrides: + del self.overrides[ctx] + else: + self.overrides[ctx] = result + + def do_reinstall(self): + self.client_id = self.client_id + "_r" + self.frontier = {} + self.overrides = {} + + def _canonicalize_for_publish(self, ctx, tie_policy): + """Canonical published form of `ctx`'s override register, + computed fresh against the current effective frontier — + independent of whether `do_compact` was ever called locally. + Returns `(is_live, canonical_reg)`; `canonical_reg is None` + means virgin (omit from the wire entirely). Reuses the same + overridable `_compact`/`_override_set` hooks `do_compact` uses, + so a mutation-harness subclass that weakens one weakens both + the storage-GC path and the publish path identically. + """ + reg = self.overrides.get(ctx) + if reg is None: + return False, None + front = self.effective_frontier(ctx) + canonical = self._compact(reg, front, tie_policy) + if canonical is None: + return False, None + return self._override_set(canonical, front, tie_policy), canonical + + def publish_blob(self, tie_policy=CLEAR): + """Serialize this device's read-state blob. + + Every override is canonicalized at serialization time: live -> + unchanged (3 keys), dead -> tombstone floor (1 key, `ov_c:` + only), virgin -> omitted (0 keys). Canonical publication is a + protocol requirement, not an optimization — noncanonical wire + output is structurally impossible here, not merely avoided by + convention. `do_compact` remains a separate storage-GC + transition that mutates `self.overrides`; publication no + longer depends on it having been called first. + + **Atomic slot-grouping rule (spec-amendment requirement):** + A context's frontier entry and ALL of its `ov_*` sibling entries + MUST travel in the same slot. `split_blob_into_slots` below + enforces this by round-robining per-context groups, never + per-entry. A receiving client that only holds part of a context + group and attempts to reconstruct a `RegB` from it would see + partial zeroes and might canonically re-publish a false + tombstone. Group atomicity makes partial reconstruction + structurally impossible from a compliant publisher's output. + """ + blob_ctx = {escape_context_key(k): v for k, v in self.frontier.items()} + if not self.is_legacy: + for k in self.overrides: + is_live, canonical = self._canonicalize_for_publish(k, tie_policy) + if canonical is None: + continue # virgin: omitted from the wire entirely + if is_live: + blob_ctx[f"ov_s:{k}"] = canonical.s + blob_ctx[f"ov_c:{k}"] = canonical.c + blob_ctx[f"ov_b:{k}"] = canonical.b + else: + blob_ctx[f"ov_c:{k}"] = canonical.c # tombstone: ceiling only + return {"v": 1, "client_id": self.client_id, "contexts": blob_ctx} + + def split_blob_into_slots(self, tie_policy=CLEAR, n_slots=2): + """Split this device's blob into `n_slots` compliant slots. + + **Atomic grouping rule:** a context's frontier entry and ALL of + its `ov_*` sibling entries travel together in the same slot. + Round-robin assignment is per-context group, never per-entry. + This matches production `splitContextsIntoBudgetedSlots` when + it is amended to group by context instead of by individual entry. + + Returns a list of `n_slots` blobs, each with the same `v` and + `client_id` but a disjoint subset of context groups. + """ + blob = self.publish_blob(tie_policy) + contexts = blob["contexts"] + + # Gather per-context groups: each group is a list of (key, value) pairs. + # A "group" is: the frontier key (escaped ctx) + any ov_* siblings. + # Contexts that appear only as ov_* keys (no frontier entry) are + # also grouped together. + groups = {} # logical_ctx -> list of (wire_key, value) + for wire_key, value in contexts.items(): + if wire_key.startswith("ov_s:"): + ctx = wire_key[5:] + elif wire_key.startswith("ov_c:"): + ctx = wire_key[5:] + elif wire_key.startswith("ov_b:"): + ctx = wire_key[5:] + else: + # Frontier key: may be escaped (e.g. "esc:ov_s:evil"). + # Derive the logical context ID by unescaping so this + # entry joins the same group as its ov_* siblings, which + # are keyed by the RAW context ID (e.g. "ov_s:evil" -> + # ctx = "evil", but "esc:ov_s:evil" frontier -> ctx = + # "ov_s:evil" after unescape). Without this step an + # escaped frontier key and its ov_* siblings would be + # treated as two different groups, splitting the register + # across slots — reproducing the round-1 partial- + # reconstruction poison for escaped context IDs. + ctx = unescape_context_key(wire_key) + groups.setdefault(ctx, []).append((wire_key, value)) + + slots = [{"v": blob["v"], "client_id": blob["client_id"], "contexts": {}} + for _ in range(n_slots)] + for i, (_ctx, pairs) in enumerate(sorted(groups.items())): + slot = slots[i % n_slots] + for wire_key, value in pairs: + slot["contexts"][wire_key] = value + return slots + + def receive_merge(self, blob): + incoming_overrides = {} + for k, v in blob.get("contexts", {}).items(): + if k.startswith("ov_s:"): + ctx = k[5:] + incoming_overrides.setdefault(ctx, [0, 0, 0])[0] = v + elif k.startswith("ov_c:"): + ctx = k[5:] + incoming_overrides.setdefault(ctx, [0, 0, 0])[1] = v + elif k.startswith("ov_b:"): + ctx = k[5:] + incoming_overrides.setdefault(ctx, [0, 0, 0])[2] = v + else: + ctx = unescape_context_key(k) + self.frontier[ctx] = max(self.frontier.get(ctx, 0), v) + + if not self.is_legacy: + for ctx, (s, c, b) in incoming_overrides.items(): + incoming_reg = RegB(s=s, c=c, b=b) + self.overrides[ctx] = self._merge_reg( + self.overrides.get(ctx), incoming_reg + ) + + def legacy_sanitize_and_publish(self, tie_policy=CLEAR): + blob = self.publish_blob(tie_policy) + sanitized = {} + for k, v in blob["contexts"].items(): + if len(k.encode("utf-8")) <= 256 and self._sanitize_value(v): + sanitized[k] = v + return {"v": 1, "client_id": self.client_id, "contexts": sanitized} + + def state_key(self, contexts, tie_policy=CLEAR): + parts = [] + for ctx in sorted(contexts): + f = self.effective_frontier(ctx) + reg = self.overrides.get(ctx, RegB()) + ov = self.override_is_set(ctx, tie_policy) + parts.append((ctx, f, reg.s, reg.c, reg.b, ov)) + return (self.client_id, self.is_legacy, tuple(parts)) + + +# --------------------------------------------------------------------------- +# Device simulation — Candidate A +# --------------------------------------------------------------------------- + +class DeviceA: + def __init__(self, client_id, is_legacy=False): + self.client_id = client_id + self.is_legacy = is_legacy + self.frontier = {} + self.overrides = {} + self.counter = 0 + + def effective_frontier(self, ctx): + return self.frontier.get(ctx, 0) + + def override_is_set(self, ctx): + reg = self.overrides.get(ctx) + if reg is None or reg.op == CLEAR: + return False + if self.effective_frontier(ctx) > reg.baseline: + return False + return True + + def verdict(self, ctx, latest_ts): + return latest_ts > self.effective_frontier(ctx) or self.override_is_set(ctx) + + def do_mark_unread(self, ctx): + if self.is_legacy: + return + self.counter += 1 + self.overrides[ctx] = RegA( + counter=self.counter, tiebreak=self.client_id, + op=SET, baseline=self.effective_frontier(ctx), + ) + + def do_mark_read(self, ctx, frontier_ts): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), frontier_ts) + if not self.is_legacy: + self.counter += 1 + self.overrides[ctx] = RegA( + counter=self.counter, tiebreak=self.client_id, + op=CLEAR, baseline=0, + ) + + def do_advance_frontier(self, ctx, ts): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), ts) + + def receive_merge(self, blob, tie_op=CLEAR): + for ctx, ts in blob.get("contexts", {}).items(): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), ts) + if not self.is_legacy: + for ctx, reg in blob.get("overrides", {}).items(): + self.overrides[ctx] = merge_reg_a( + self.overrides.get(ctx), reg, tie_op + ) + if reg.counter > self.counter: + self.counter = reg.counter + + def publish_blob(self): + blob = {"v": 1, "client_id": self.client_id, "contexts": dict(self.frontier)} + if not self.is_legacy: + blob["overrides"] = dict(self.overrides) + return blob + + def legacy_rewrite_and_publish(self): + return {"v": 1, "client_id": self.client_id, "contexts": dict(self.frontier)} + + +# --------------------------------------------------------------------------- +# Legacy pruning/trim model +# --------------------------------------------------------------------------- + +def legacy_prune(contexts, horizon): + return {k: v for k, v in contexts.items() + if not (k.startswith("msg:") or k.startswith("thread:")) or v >= horizon} + + +def legacy_trim(contexts, client_id, max_bytes=32768): + import json + + def size(ctx): + return len(json.dumps({"v": 1, "client_id": client_id, "contexts": ctx}).encode()) + + if size(contexts) <= max_bytes: + return contexts, True + evictable = sorted( + ((k, v) for k, v in contexts.items() + if k.startswith("msg:") or k.startswith("thread:")), + key=lambda kv: kv[1], + ) + out = dict(contexts) + for k, _ in evictable: + del out[k] + if size(out) <= max_bytes: + return out, True + return out, size(out) <= max_bytes + + +def legacy_sanitize_blob(blob): + sanitized = {} + for k, v in blob.get("contexts", {}).items(): + if (len(k.encode("utf-8")) <= 256 + and isinstance(v, int) and 0 <= v <= 4294967295): + sanitized[k] = v + return {"v": 1, "client_id": blob.get("client_id", ""), "contexts": sanitized} diff --git a/docs/formal/nip-rs-unread/mutation.py b/docs/formal/nip-rs-unread/mutation.py new file mode 100644 index 0000000000..4450a99c8f --- /dev/null +++ b/docs/formal/nip-rs-unread/mutation.py @@ -0,0 +1,519 @@ +"""Mutation harness for candidate B (two-counter) model. + +Each mutant: subclass DeviceB with a weakened rule, run the BFS explorer, +require a recorded counterexample. A model that stays green under a real +weakening is worthless. + +Mutants: + M1: drop baseline dominance (frontier > B no longer clears stale set) + M2: drop max(S,C)+1 bump (use S+1 or C+1 — counter can regress) + M3: flip tie policy (verify the model distinguishes them) + M4: revert to delete-on-dominance compaction (drops the tombstone floor + entirely instead of zeroing S and keeping max(S,C) as C) — reproduces + Thufir's pass-3 CRITICAL: stale-replay resurrection after counter reuse + M5: uint32 overflow bypass (legacy sanitization disabled) + M6: componentwise-max -> last-write-wins merge (convergence breaks) + M7: publish without canonicalization (serialize raw registers instead + of the compact-at-publish canonical form) — reproduces Thufir's + pass-1/2 CRITICAL: dead+dead merge resurrection + M8: revert split_blob_into_slots to per-entry splitting (violates the + atomic-grouping rule) — reproduces Thufir's pass-2/2 CRITICAL: + partial-slot reconstruction of a live RegB creates a false tombstone + that permanently suppresses the override after eventual full delivery + M9: revert split_blob_into_slots to escaped-key grouping (groups frontier + by wire key instead of unescaped logical ID) — reproduces Thufir's + round-2 CRITICAL: for a context whose raw ID starts with a reserved + prefix (e.g. "ov_s:evil"), the frontier's escaped wire key + ("esc:ov_s:evil") and the ov_* siblings (keyed by raw suffix "ov_s:evil") + resolve to different groups → register split across slots → + old/new slot-coordinate mixture produces partial reconstruction → + false tombstone → permanent false clear across publication cycles + +Each mutant is injected into the model via DeviceB subclass, then the +explorer or invariant suite is rerun. The counterexample (first violation) +is recorded and printed. +""" +from copy import deepcopy +from model import ( + RegB, merge_reg_b, override_set_b, compact_b, + DeviceB, legacy_sanitize_blob, + escape_context_key, + SET, CLEAR, +) +from exhaustive import ( + explore_b, test_concurrent_stability, + test_compaction_register_exhaustive, test_deep_history_compaction, + test_published_merge_closure, test_interleaved_delivery_grouping, + test_escaped_context_slot_grouping, + CONTEXTS, +) + + +# --------------------------------------------------------------------------- +# M1: drop baseline dominance +# --------------------------------------------------------------------------- + +class M1_NoBaselineDominance(DeviceB): + def _override_set(self, reg, frontier_val, tie_policy): + if reg is None: + return False + if reg.s > reg.c: + return True + if reg.s == reg.c and reg.s > 0: + return tie_policy == SET + return False + + def _compact(self, reg, frontier_val, tie_policy): + if reg.s == 0 and reg.c == 0: + return None + if self._override_set(reg, frontier_val, tie_policy): + return reg + if reg.c > reg.s: + return RegB(s=0, c=reg.c, b=0) + if reg.c == reg.s and tie_policy == CLEAR: + return RegB(s=0, c=reg.c, b=0) + return reg + + +def mutant_m1(): + """M1: without baseline dominance, a stale set persists after frontier + advance past baseline. Verify by constructing the scenario directly: + mark-unread at frontier=10, then advance frontier to 100. The correct + model clears the override; the mutant keeps it live.""" + violations = [] + for ctx in CONTEXTS: + dev = M1_NoBaselineDominance("d0") + dev.frontier[ctx] = 10 + dev.do_mark_unread(ctx) + dev.do_advance_frontier(ctx, 100) + + correct = override_set_b(dev.overrides[ctx], 100, CLEAR) + mutant_result = dev.override_is_set(ctx, CLEAR) + + if correct != mutant_result: + violations.append(( + "baseline-dominance-missing", ctx, + dev.overrides[ctx], 100, + f"correct={correct}", f"mutant={mutant_result}", + )) + + if not violations: + _, violations = explore_b(max_depth=3, tie_policy=CLEAR, + device_cls=M1_NoBaselineDominance) + return violations + + +# --------------------------------------------------------------------------- +# M2: drop max(S,C)+1 bump +# --------------------------------------------------------------------------- + +class M2_NoBump(DeviceB): + """Each counter bumps only itself: mark_unread does S := S+1, + mark_read does C := C+1. When S > C from a prior set, a clear + at C+1 can produce C < S even though the clear is causally later.""" + def do_mark_unread(self, ctx): + if self.is_legacy: + return + cur = self.overrides.get(ctx, RegB()) + self.overrides[ctx] = RegB(s=cur.s + 1, c=cur.c, + b=self.effective_frontier(ctx)) + + def do_mark_read(self, ctx, frontier_ts): + self.frontier[ctx] = max(self.frontier.get(ctx, 0), frontier_ts) + if not self.is_legacy: + cur = self.overrides.get(ctx, RegB()) + self.overrides[ctx] = RegB(s=cur.s, c=cur.c + 1, b=cur.b) + + +def mutant_m2(): + """M2: each counter bumps independently. After set→set→clear at + the SAME frontier (no advance past baseline): correct clear has + C=3 > S=2, mutant clear has C=1 < S=2 — a causally later clear + fails to dominate. + + Use mark_read at the current frontier (not advancing past baseline) + so baseline dominance doesn't mask the counter discrepancy. + """ + violations = [] + for ctx in CONTEXTS: + front = 10 + dev_correct = DeviceB("d0") + dev_correct.frontier[ctx] = front + dev_correct.do_mark_unread(ctx) + dev_correct.do_mark_unread(ctx) + dev_correct.do_mark_read(ctx, front) + + dev_mutant = M2_NoBump("d0") + dev_mutant.frontier[ctx] = front + dev_mutant.do_mark_unread(ctx) + dev_mutant.do_mark_unread(ctx) + dev_mutant.do_mark_read(ctx, front) + + correct_set = dev_correct.override_is_set(ctx, CLEAR) + mutant_set = dev_mutant.override_is_set(ctx, CLEAR) + + if correct_set != mutant_set: + violations.append(( + "bump-independent", ctx, + f"correct={dev_correct.overrides[ctx]}", + f"mutant={dev_mutant.overrides[ctx]}", + f"correct_set={correct_set}", f"mutant_set={mutant_set}", + )) + + if not violations: + _, violations = explore_b(max_depth=4, tie_policy=CLEAR, + device_cls=M2_NoBump) + return violations + + +# --------------------------------------------------------------------------- +# M3: tie policy distinguishable +# --------------------------------------------------------------------------- + +def mutant_m3(): + """M3: tie policy is load-bearing — S==C must produce different verdicts. + Not a DeviceB mutation; tests the model function directly.""" + reg = RegB(s=1, c=1, b=10) + frontier = 10 + v_clear = override_set_b(reg, frontier, CLEAR) + v_set = override_set_b(reg, frontier, SET) + if v_clear == v_set: + return [] + return [("tie-distinguishable", v_clear, v_set, reg, frontier)] + + +# --------------------------------------------------------------------------- +# M4: revert to delete-on-dominance compaction (drops the tombstone floor) +# --------------------------------------------------------------------------- + +class M4_DeleteOnDominance(DeviceB): + """The pre-fix compaction rule: any dead/dominated register is deleted + entirely rather than reduced to the tombstone floor RegB(0, max(S,C), 0). + This makes counters reusable — a later local set/clear pair restarts + from S=0/C=0, so a delayed stale peer snapshot can dominate it on + replay. This is exactly the rule Thufir's pass-3 CRITICAL found live + at e453b3945.""" + def _compact(self, reg, frontier_val, tie_policy): + if reg.s == 0 and reg.c == 0: + return None + if self._override_set(reg, frontier_val, tie_policy): + return reg + if frontier_val > reg.b: + return None + if reg.c > reg.s: + return RegB(s=0, c=reg.c, b=0) + if reg.c == reg.s and tie_policy == CLEAR: + return RegB(s=0, c=reg.c, b=0) + return reg + + +def mutant_m4(): + """M4: without the tombstone floor, compaction deletes the counter + ceiling instead of preserving it. Reproduce Thufir's exact witness + directly: RegB(3,0,10) at frontier=20 compacts to None under the old + rule (vs. RegB(0,3,0) under the fix); a subsequent local set+clear + reuses counters from zero; the stale ancestor then replays and + resurrects (S>C) under both tie policies. + + Then confirm the explorer/deep-history suite also catches it (defense + in depth — a mutant that only fails a hand-built scenario would still + be a real bug, but the directed check is what's supposed to catch this + class per T2/T3).""" + violations = [] + stale = RegB(s=3, c=0, b=10) + frontier_after = 20 + + for tie_policy in (CLEAR, SET): + dev = M4_DeleteOnDominance("d0") + dev.frontier["c0"] = 10 + dev.overrides["c0"] = stale + dev.do_advance_frontier("c0", frontier_after) + dev.do_compact("c0", tie_policy) + if "c0" in dev.overrides: + continue # old rule didn't drop it here; not the witness shape + + dev.do_mark_unread("c0") # S := 1, B := 20 + dev.do_mark_read("c0", frontier_after) # C := 2 + + stale_blob = {"contexts": {"ov_s:c0": stale.s, "ov_c:c0": stale.c, "ov_b:c0": stale.b}} + dev.receive_merge(stale_blob) + resurrected = dev.override_is_set("c0", tie_policy) + + if resurrected: + violations.append(( + "M4-delete-on-dominance-resurrection", tie_policy, + f"stale_ancestor={stale}", f"post_compact_reuse=(set,clear)", + f"final_reg={dev.overrides['c0']}", f"override_is_set={resurrected}", + )) + + if not violations: + _, violations = test_deep_history_compaction(device_cls=M4_DeleteOnDominance) + return violations + + +# --------------------------------------------------------------------------- +# M5: uint32 overflow bypass +# --------------------------------------------------------------------------- + +def mutant_m5(): + """M5: values outside uint32 range must fail legacy sanitization.""" + blob = {"v": 1, "client_id": "x", "contexts": { + "ov_s:c0": 4294967296, + "ov_c:c0": 0, + "ov_b:c0": 10, + }} + sanitized = legacy_sanitize_blob(blob) + if "ov_s:c0" in sanitized["contexts"]: + return [] + return [("overflow-rejected", blob["contexts"]["ov_s:c0"], + sanitized["contexts"])] + + +# --------------------------------------------------------------------------- +# M6: last-write-wins merge (breaks convergence) +# --------------------------------------------------------------------------- + +class M6_LastWriteWins(DeviceB): + def _merge_reg(self, a, b): + if a is None: + return b + if b is None: + return a + return b + + +def mutant_m6(): + """M6: replace componentwise max with last-write-wins. Convergence must + break — different delivery orders produce different final states.""" + _, violations = explore_b(max_depth=3, tie_policy=CLEAR, + device_cls=M6_LastWriteWins) + return violations + + +# --------------------------------------------------------------------------- +# M7: publish without canonicalization (reproduces Thufir's pass-1/2 +# CRITICAL — dead+dead merge resurrection) +# --------------------------------------------------------------------------- + +class M7_PublishWithoutCanonicalization(DeviceB): + """Reverts `publish_blob` to serialize raw, uncompacted registers — + the exact pre-fix behavior Thufir's pass-1/2 CRITICAL exploited: + a dead register's baseline-relative death (or clear-count-relative + death) never gets folded into a globally-comparable ceiling before + hitting the wire, so two individually-dead registers can + componentwise-max-merge into a live join.""" + def publish_blob(self, tie_policy=CLEAR): + blob_ctx = {escape_context_key(k): v for k, v in self.frontier.items()} + if not self.is_legacy: + for k, reg in self.overrides.items(): + blob_ctx[f"ov_s:{k}"] = reg.s + blob_ctx[f"ov_c:{k}"] = reg.c + blob_ctx[f"ov_b:{k}"] = reg.b + return {"v": 1, "client_id": self.client_id, "contexts": blob_ctx} + + +def mutant_m7(): + """M7: publish-without-canonicalization must be caught by the + published-state merge-closure invariant — proving that invariant + has teeth. Reproduce Thufir's exact witness directly first (fast, + deterministic); fall back to the full search if the hand-built + scenario doesn't trigger under a given tie policy.""" + violations = [] + for tie_policy in (CLEAR, SET): + dev_a = M7_PublishWithoutCanonicalization("a") + dev_a.frontier["c0"] = 50 + dev_a.overrides["c0"] = RegB(s=3, c=2, b=0) + dev_b = M7_PublishWithoutCanonicalization("b") + dev_b.frontier["c0"] = 100 + dev_b.overrides["c0"] = RegB(s=1, c=2, b=100) + + blob_a = dev_a.publish_blob(tie_policy) + blob_b = dev_b.publish_blob(tie_policy) + + for first, second in [(blob_a, blob_b), (blob_b, blob_a)]: + recv = M7_PublishWithoutCanonicalization("recv") + recv.receive_merge(first) + recv.receive_merge(second) + if recv.override_is_set("c0", tie_policy): + violations.append(( + "M7-publish-without-canonicalization-resurrection", + tie_policy, blob_a, blob_b, recv.overrides["c0"], + )) + + if not violations: + _, violations = test_published_merge_closure( + device_cls=M7_PublishWithoutCanonicalization + ) + return violations + + +# --------------------------------------------------------------------------- +# M8: revert split_blob_into_slots to per-entry splitting +# (violates the atomic-grouping rule — reproduces Thufir's pass-2/2 CRITICAL) +# --------------------------------------------------------------------------- + +class M8_PerEntrySplit(DeviceB): + """Reverts `split_blob_into_slots` to a per-entry split that violates the + atomic-grouping rule by separating `ov_s:` + frontier from `ov_b:` + `ov_c:`. + + This reproduces Thufir's exact transport witness: + - Slot 0: frontier key + `ov_s:` entry (the "partial set" slot) + - Slot 1: `ov_c:` + `ov_b:` entries + + An observer receiving only slot 0 reconstructs `RegB(s=1, c=0, b=0)` at + `frontier=10`. Because `frontier(10) > b(0)`, the override is baseline-dead. + Canonical re-publication emits tombstone `RegB(0, 1, 0)`. After full + eventual delivery (both original slots + transient tombstone), the merged + result is `RegB(s=1, c=1, b=10)` — dead under clear-wins — permanently + suppressing a live override. + """ + + def split_blob_into_slots(self, tie_policy=CLEAR, n_slots=2): + """Split by key type: frontier + ov_s: in slot 0, ov_b: + ov_c: in slot 1. + Violates the atomic-grouping rule by separating ov_s: from ov_b:.""" + blob = self.publish_blob(tie_policy) + slots = [{"v": blob["v"], "client_id": blob["client_id"], "contexts": {}} + for _ in range(n_slots)] + for wire_key, value in blob["contexts"].items(): + if wire_key.startswith("ov_b:") or wire_key.startswith("ov_c:"): + # ov_b and ov_c go to slot 1 — separated from their ov_s: sibling + slots[1]["contexts"][wire_key] = value + else: + # frontier keys and ov_s: go to slot 0 + slots[0]["contexts"][wire_key] = value + return slots + + +def mutant_m8(): + """M8: per-entry splitting must be caught by test_interleaved_delivery_grouping — + proving that the new interleaved-delivery test has teeth. + + Reproduce Thufir's exact transport witness directly: source live + `RegB(1,0,10)` at frontier=10. Per-entry split puts frontier+`ov_s:c0` + in slot 0 and `ov_c:c0`+`ov_b:c0` in slot 1. An observer receiving only + slot 0 reconstructs `RegB(1,0,0)`, re-publishes tombstone `RegB(0,1,0)`. + Full merge including the transient: `RegB(1,1,10)` → inactive. + + Confirmed by running test_interleaved_delivery_grouping with M8_PerEntrySplit; + the witness must be caught before resorting to the full suite.""" + return test_interleaved_delivery_grouping(device_cls=M8_PerEntrySplit) + + +# --------------------------------------------------------------------------- +# M9: revert split_blob_into_slots to escaped-key grouping +# (groups frontier by wire key instead of unescaped logical ID — +# reproduces Thufir's round-2 CRITICAL) +# --------------------------------------------------------------------------- + +class M9_EscapedKeyGrouping(DeviceB): + """Reverts `split_blob_into_slots` to group the frontier key by its + ESCAPED wire key rather than the unescaped logical context ID. + + For a normal context like "c0", this is a no-op (escape_context_key("c0") + == "c0"), so M9 is identical to the correct model on normal contexts. + The defect only manifests when the raw context ID starts with a reserved + prefix — e.g. raw "ov_s:evil" escapes to frontier wire key "esc:ov_s:evil". + The ov_* sibling keys are keyed by the RAW suffix ("ov_s:evil"), while + the frontier is keyed by the escaped wire key ("esc:ov_s:evil") — two + identities for one logical context, so they land in different slots. + + This reproduces Thufir's round-2 CRITICAL: across publication cycles an + observer can receive the new frontier slot (esc:ov_s:evil=10) plus the + stale old-cycle override slot (ov_s/ov_c/ov_b at b=0), reconstructing + RegB(s=1,c=0,b=0) at frontier=10 — baseline-dead — and emitting tombstone + RegB(0,1,0). Full eventual delivery merges to RegB(1,1,10) — dead under + clear-wins — permanently suppressing a live override. + """ + + def split_blob_into_slots(self, tie_policy=CLEAR, n_slots=2): + """Split by original (escaped) wire key identity — does not unescape + frontier keys before grouping, so escaped contexts split incorrectly.""" + blob = self.publish_blob(tie_policy) + contexts = blob["contexts"] + + groups = {} # wire_key -> list of (wire_key, value) + for wire_key, value in contexts.items(): + if wire_key.startswith("ov_s:"): + ctx = wire_key[5:] + elif wire_key.startswith("ov_c:"): + ctx = wire_key[5:] + elif wire_key.startswith("ov_b:"): + ctx = wire_key[5:] + else: + ctx = wire_key # frontier: use escaped wire key as group ID (BUG) + groups.setdefault(ctx, []).append((wire_key, value)) + + slots = [{"v": blob["v"], "client_id": blob["client_id"], "contexts": {}} + for _ in range(n_slots)] + for i, (_ctx, pairs) in enumerate(sorted(groups.items())): + slot = slots[i % n_slots] + for wire_key, value in pairs: + slot["contexts"][wire_key] = value + return slots + + +def mutant_m9(): + """M9: escaped-key grouping must be caught by test_escaped_context_slot_grouping — + proving that the escaped-context regression test has teeth. + + For a context whose raw ID starts with a reserved prefix ("ov_s:evil"), + the frontier wire key is "esc:ov_s:evil" and the ov_* sibling keys are + "ov_s:ov_s:evil", "ov_c:ov_s:evil", "ov_b:ov_s:evil". The escaped-key + grouping treats "esc:ov_s:evil" (frontier) and "ov_s:evil" (ov_* suffix) + as different groups, splitting the register across slots. + + Old/new slot-coordinate mixture across publication cycles then reproduces + the round-1 transport poison: partial reconstruction → false tombstone → + permanent false clear of a live override. + + The test is parameterized to route through the "mismatched grouping" path + (else branch) when the M9 split puts frontier and siblings in different slots, + and the witness must be caught.""" + return test_escaped_context_slot_grouping(device_cls=M9_EscapedKeyGrouping) + + +# --------------------------------------------------------------------------- +# Runner +# --------------------------------------------------------------------------- + +def run_mutations(): + mutants = [ + ("M1: drop baseline dominance", mutant_m1), + ("M2: drop max(S,C)+1 bump", mutant_m2), + ("M3: tie policy distinguishable", mutant_m3), + ("M4: revert to delete-on-dominance compaction (reproduces pass-3 CRITICAL)", mutant_m4), + ("M5: uint32 overflow bypass", mutant_m5), + ("M6: last-write-wins merge", mutant_m6), + ("M7: publish without canonicalization (reproduces pass-1/2 CRITICAL)", mutant_m7), + ("M8: per-entry split violates atomic-grouping rule (reproduces pass-2/2 CRITICAL)", mutant_m8), + ("M9: escaped-key grouping splits escaped-ctx register across slots (reproduces round-2 CRITICAL)", mutant_m9), + ] + + print("=" * 60) + print("Mutation harness — candidate B") + print("=" * 60) + + caught = [] + missed = [] + for name, fn in mutants: + violations = fn() + if violations: + caught.append(name) + v = violations[0] + detail = str(v)[:200] + print(f" CAUGHT: {name}") + print(f" counterexample: {detail}") + else: + missed.append(name) + print(f" MISSED: {name}") + + print(f"\nCaught {len(caught)}/{len(mutants)} mutants") + if missed: + print(f"MISSED: {missed}") + print("=" * 60) + return len(missed) == 0 + + +if __name__ == "__main__": + import sys + sys.exit(0 if run_mutations() else 1) diff --git a/docs/nips/NIP-RS.md b/docs/nips/NIP-RS.md index 1ca30ea08f..6a095df60a 100644 --- a/docs/nips/NIP-RS.md +++ b/docs/nips/NIP-RS.md @@ -20,15 +20,14 @@ read. A user running Nostr clients on multiple devices (phone, desktop, web) has no way to share read position across those clients. Each instance independently tracks what has been read, causing already-read content to appear unread on other devices. -This NIP defines a minimal, privacy-preserving protocol for propagating read state across client instances without requiring relay-side logic or coordination between different client implementations. +This NIP defines a minimal, privacy-preserving protocol for propagating read state across client instances without requiring a new event kind, a new wire message, relay-stored read-state logic, or coordination between different client implementations. It is not free of relay obligations: a relay serving the manual-unread override layer's full-state load must satisfy the ordering, capacity, floor, push, and barrier contract that section enumerates. ## Non-Goals -This NIP does not define a durable log of all read messages — blobs are best-effort recent activity hints bounded by a time horizon. +This NIP does not define a durable log of all read messages — frontier blobs are best-effort recent activity hints bounded by a time horizon. Exception: `ov_*` override entries, including tombstone floors, are durable state — they are exempt from age pruning, budget eviction, and horizon-bounded fetching, they live in a single coordinate per installation, and they MUST be carried forward before that coordinate is deleted or abandoned (see Manual-Unread Override Layer — Override State Durability). This NIP does not define cross-client interoperability on context ID format — context identifiers are opaque by default and meaningful only within a single client family, except for OPTIONAL well-known schemes defined in this NIP (`thread:` and `msg:`, defined under Read Context Schemes), which are provided for cross-client thread/message-read interoperability. -This NIP does not define mark-as-unread — the merge rule is monotonic by design. This NIP does not guarantee ordering of read events across devices. -This NIP does not require relay-side logic. +This NIP does not require relay-stored read-state logic: no new event kind, no new wire message, and nothing a relay must interpret about read state. Clients implementing the manual-unread override layer do depend on relay behaviour their full-state load cannot verify (see Full-State Load). This NIP does not define read receipts, seen-by lists, or any mechanism for tracking what other users have read. @@ -53,18 +52,26 @@ Clients publish a `kind:30078` addressable event (per [NIP-78](78.md)) with the #### `d` Tag -The `d` tag MUST be `read-state:`, where `` is a random opaque string (e.g., 32 random hex characters) generated by the client on first launch and persisted locally. The `` has no relationship to the `client_id` — it is solely a unique key for NIP-33 addressable event semantics. Each client instance MUST use a stable, unique `` for the lifetime of that installation. +The `d` tag MUST be `read-state:`, where `` is exactly 32 lowercase hexadecimal characters (`[0-9a-f]{32}`), generated randomly by the client on first launch and persisted locally. The `` has no relationship to the `client_id` — it is solely a unique key for NIP-33 addressable event semantics. The shape is fixed rather than opaque so that a relay can recognize a read-state coordinate structurally, from the `d` tag alone and without decrypting anything, and apply per-coordinate protections to it; a client that picks some other shape is not merely stylistically different, it forfeits those protections silently. + +**Primary coordinate:** a client MUST designate one coordinate as its **primary** and MUST use a single stable, unique `` for it for the lifetime of that installation. The primary `` changes only on a `client_id` conflict (below) or rotation (see Client-ID Rotation). + +**Additional frontier-only coordinates:** a client MAY publish additional coordinates under distinct `` values when its primary blob would otherwise exceed the size budget. Additional coordinates MUST NOT contain `ov_*` entries — they carry frontier entries only, and are therefore freely rewritable and freely deletable (see Orphaned Blob Deletion). A client MUST persist the `` values of its additional coordinates locally so that it can rewrite and delete them. + +**All `ov_*` entries, and the frontier entries of the contexts they belong to, MUST live in the primary coordinate.** A client implementing the manual-unread override layer MUST NOT distribute `ov_*` entries across coordinates and MUST NOT move them between coordinates: there is exactly one override-bearing coordinate per installation. If a client fetches its own `d` tag coordinate and the decrypted `client_id` does not match its local `client_id`, the coordinate is conflicted. The client MUST NOT publish to that coordinate and MUST generate a new random `` before the next publish. Events with zero `d` tags MUST be ignored. Events whose `d` tag value does not begin with `read-state:` MUST be ignored. Events with more than one `d` tag MUST be ignored. -The `` MUST be a non-empty ASCII string of 1–64 characters. +Events whose `` is not exactly 32 lowercase hexadecimal characters MUST be ignored. + +Recognizable coordinates also serve the accumulation discipline this NIP depends on: a relay that can identify a read-state coordinate structurally can replace superseded versions outright instead of retaining a tombstone row per publish, which keeps the coordinate count a full-state load must enumerate near one per live installation (see Full-State Load). #### `t` Tag -Events MUST include exactly one `["t", "read-state"]` tag. This enables relay-side filtering without fetching all `kind:30078` events for the user. +Events MUST include exactly one `["t", "read-state"]` tag. The tag is a discoverability marker: it lets a client express "read-state events only" in a single filter. It is not a guarantee of relay-side selectivity — a relay MAY apply tag constraints after its result cap, and `kind:30078` is shared with unrelated application data — so clients MUST apply the tag as a correctness filter locally on everything they receive, and MUST NOT infer from a short result that no further coordinates exist. A client performing a full-state load MUST omit the tag from its filter entirely (see Full-State Load). Events with zero `t` tags with value `read-state`, or more than one `t` tag with value `read-state`, MUST be ignored. @@ -104,6 +111,7 @@ After decryption, clients MUST apply the following validation rules: - Events whose `contexts` field is not a JSON object MUST be discarded. - Individual context entries whose timestamp is not an integer in the range 0–4294967295 MUST be discarded (the entry is dropped; the rest of the blob is still processed). - Individual context entries whose context ID exceeds 256 bytes MUST be discarded. +- Override counter entries (keys beginning with `ov_s:`, `ov_c:`, or `ov_b:`) MUST be validated as a complete logical group BEFORE any decoding, zero-filling, merging, or canonicalizing. Clients MUST collect all `ov_s:`, `ov_c:`, and `ov_b:` entries for the same `` suffix together before processing them. The only accepted wire shapes for an override group are: (a) a complete live group containing exactly the three keys `ov_s:`, `ov_c:`, and `ov_b:` with valid uint32 values, or (b) a tombstone floor containing only `ov_c:` with a valid uint32 value. Any other shape (partial group, extra keys, or invalid value in any sibling) MUST cause the entire override group to be rejected; the corresponding frontier entry for `` MUST be retained. Applying the generic per-entry discard rule before group collection is prohibited for override entries. - Blobs containing more than 10,000 context entries MUST be rejected. - If a blob contains duplicate context keys, clients SHOULD use the last value encountered (consistent with RFC 8259 §4). - Clients SHOULD ensure the total serialized event does not exceed the relay's maximum event size (commonly 64 KB per NIP-01). Clients receiving events that exceed their configured size limit SHOULD discard them. @@ -112,6 +120,15 @@ After decryption, clients MUST apply the following validation rules: Context identifier format is not prescribed by this NIP. Clients choose identifiers appropriate to their context type (e.g., a NIP-28 channel event ID, a NIP-29 group address, a pubkey for DMs). Interoperability between different client implementations on context ID conventions is outside the scope of this NIP. +#### Reserved Namespace + +The key prefix stem `ov_` (3 bytes) and the escape marker `esc:` (4 bytes) are reserved for the manual-unread override layer defined below. Clients MUST escape any raw context ID that begins with `ov_` or `esc:` when using it as a frontier key in the `contexts` map: + +- **On publish:** prepend `esc:` to any raw context ID beginning with `ov_` or `esc:` before writing it as a frontier key (e.g., raw `ov_s:evil` → wire key `esc:ov_s:evil`; raw `esc:foo` → wire key `esc:esc:foo`). +- **On receive:** strip exactly one leading `esc:` from any frontier wire key beginning with `esc:` to recover the raw context ID (e.g., wire key `esc:ov_s:evil` → raw `ov_s:evil`; wire key `esc:esc:foo` → raw `esc:foo`). This is a bijection — applying escape then unescape is the identity function. Clients MUST NOT strip more than one `esc:` prefix per receive. + +**Backward-compatibility limitation:** a context published *unescaped* by a client predating this amendment, whose raw ID happens to start with `ov_` or `esc:`, is not safely migrated. The scheme protects contexts generated by amendment-aware clients going forward; it does not retroactively rewrite history. This residual hazard is documented as a known limitation. Buzz's own context ID shapes (channel UUID, `msg:hex64`, `thread:hex64`) cannot trigger it. + #### Read Context Schemes (Optional) This subsection defines OPTIONAL well-known context schemes for tracking read @@ -281,13 +298,13 @@ Because context timestamps are derived from message `created_at` values — whic ### Fetching -To load read state, a client MUST fetch all `kind:30078` events for the user within the time horizon using the `#t` filter: +To load read state, a client MUST fetch all `kind:30078` events for the user. Unless it is performing a full-state load (below), it SHOULD narrow the fetch with the `#t` filter: ```json -{"kinds": [30078], "authors": [""], "#t": ["read-state"], "since": } +{"kinds": [30078], "authors": [""], "#t": ["read-state"]} ``` -Clients SHOULD limit the fetch to events with `created_at` within a configurable time horizon (default: 7 days). +Clients that neither read nor write `ov_*` override state SHOULD limit the fetch to events with `created_at` within a configurable time horizon (default: 7 days) by adding `"since": `, accepting that frontiers older than the horizon become unknown. Clients that implement the manual-unread override layer MUST NOT filter the fetch by age or by tag, and MUST establish completeness (see Full-State Load below). After fetching, clients MUST: @@ -295,11 +312,71 @@ After fetching, clients MUST: 2. Discard blobs that fail validation (see Content Validation). 3. Identify the blob whose decrypted `client_id` matches the client's own `client_id` — this is the client's own blob. -If multiple blobs decrypt to the same `client_id` (e.g., due to a prior rotation that left an orphaned blob, or a backup/restore that duplicated identifiers), the client MUST treat the blob with the highest `created_at` as its own and merge all others into the read state as if they were from other instances. The client SHOULD delete the stale duplicate(s) via NIP-09 deletion. +If multiple blobs decrypt to the same `client_id` (e.g., due to a prior rotation that left an orphaned blob, or a backup/restore that duplicated identifiers), the client MUST treat the blob at its own primary coordinate as its own and merge all others into the read state as if they were from other instances. If none of them is at the client's own primary coordinate, the blob with the highest `created_at` is its current reference. Deletion of such a stale duplicate is governed by Orphaned Blob Deletion — a duplicate carrying `ov_*` entries MUST NOT be deleted until its override state has been carried forward. 4. Merge all valid blobs (including the client's own) using the merge rule. -Absence of a context in all fetched blobs means the read state for that context is **unknown** — clients SHOULD treat unknown contexts as unread (conservative default). The horizon is a storage and fetch optimization, not a semantic claim about read status. Contexts that were read but have aged out of the time horizon are indistinguishable from never-read contexts. Clients MAY extend the horizon or maintain a local cache to mitigate this. +Absence of a context in all fetched blobs means the read state for that context is **unknown** — clients SHOULD treat unknown contexts as unread (conservative default). For clients using a finite horizon, the horizon is a storage and fetch optimization, not a semantic claim about read status: contexts that were read but have aged out of the time horizon are indistinguishable from never-read contexts. Clients MAY extend the horizon or maintain a local cache to mitigate this. Clients implementing the override layer do not filter the fetch by age at all (see above), so for them this ambiguity arises only from write-time frontier pruning. + +#### Full-State Load + +Clients that implement the manual-unread override layer MUST perform a **full-state load**: they MUST NOT apply a finite `since` filter, and they MUST establish that every one of the user's `read-state` coordinates has been retrieved. Because the payload is encrypted, a relay filter cannot select for override-bearing events: any event-level window can exclude the only coordinate carrying a tombstone floor, which reopens the resurrection witness in Override State Durability regardless of any per-entry exemption. For these clients the time horizon is a *write-time* frontier pruning policy only (see Debounce and Pruning), never a fetch filter. + +Removing `since` does not by itself make the result complete. Relays MAY cap the number of events returned for a historical query, MAY cap below the client's requested `limit`, and emit end-of-stored-events after the capped query — so **a single query proves nothing.** End-of-stored-events marks the end of the capped result, not the end of the matching set, and a short result does not establish that no further coordinates exist. Caps typically retain the newest events and drop the oldest, which are precisely the rotation-predecessor and orphaned coordinates whose tombstone floors this layer depends on. A silently truncated load that omits the sole carrier of a floor merges a stale live register unopposed and reports a manually-unread context as read, permanently. + +A full-state load MUST therefore be enumerated with no tag constraint in the filter: + +```json +{"kinds": [30078], "authors": [""], "limit": } +``` + +A relay MAY deliver fewer events than its result cap selected — for example, by applying tag constraints only after the cap and withholding the events that fail them. Under a tag-constrained filter the number of events the client receives is therefore not the number the cap selected: a delivered page can be short, or empty, while older matching coordinates still exist below it, and no observation the client can make distinguishes the two. `kind:30078` is arbitrary application data whose `d` tag namespace is open to every application that has ever written under the user's key, so this is not a hypothetical — a page can be filled entirely by coordinates unrelated to read state. With the tag constraint omitted, the client asks for exactly what it will accept, and the events the cap selects are the events it receives. Selection moves client-side, which is where the validation rules already place it: collect coordinates only from `d` tags of the form `read-state:` and ignore every other event. The cost is that the client fetches its own application data at that kind rather than a relay-selected subset of it. + +A client MUST NOT test completeness by comparing the number of events returned against the `limit` it requested: the effective cap is the relay's, a relay MAY cap below the requested value, and a relay's advertised maximum limit is not necessarily the limit it enforces — so no comparison against the requested `limit` is a valid truncation test. What the client MAY compare is one delivery against another. Let `C` be the largest number of events the relay delivered for any single **preceding** query in this load. The relay demonstrably delivered `C` events at once, so its cap is at least `C`, and a query that delivers fewer than `C` events was not cut short by that cap. Completeness is established by continuation on a strictly decreasing cursor, with each band discharged by that comparison. + +`C` yields nothing at the start of a load, and yields nothing for the whole of a load whose entire history at this kind is a single event: one delivery of one event bounds the cap below by one, and no delivery can be smaller than that. The procedure therefore also fixes a floor, `L = 2`, required of relays below. A delivery is bounded by the requested `limit` as well as by the relay's cap, so the floor licenses a conclusion about a delivery only together with step 1's requirement that the requested `limit` be at least `L`: what the client may conclude is that a query it issued for at least `L` events, whose matching set holds at least `L`, delivers at least `L`. A threshold above the requested `limit` would be unreachable by construction, and a test that can never be met declares a truncated page exhausted. It is stated at the smallest value that admits a second event, because a larger floor is a stronger claim about relays that buys nothing further: a relay that will deliver only one event per query cannot express `limit` semantics and cannot serve a user who has two coordinates at all, whereas any floor above two would begin excluding relays this procedure does not need to exclude. + +Enumeration descends, so it cannot see a coordinate that moves *up* while it runs. Because these are addressable events, a republish replaces the previous version rather than appending: a coordinate the client already collected at a low `created_at` can be replaced, during the load, by a version above the cursor the client has already passed — and the old version stops existing, so no continuation and no pinned window will ever return either one. If that new version carries a tombstone floor the old one lacked, a load that reported *complete* merged without it. + +A full-state load therefore MUST be fenced by a live subscription on the same tag-free filter, established **before** the first enumeration query and held unbroken for the duration of the load. The fence is *established* when the client has received end-of-stored-events for that subscription, not when it sent the request: sending a request is not an observation, and the relay's answer to it is the first point at which the client knows the subscription is registered and that what the relay accepts from then on will be pushed to it. The fence and every enumeration query MUST be issued on the same connection. + +Every event the fence delivers is collected exactly as an enumerated event is (step 2), which is what repairs the moved coordinate: the replacing event is itself what the relay pushes. Delivery is necessary but not sufficient — it must be delivery *before the verdict*, and those are different properties. Under push delivery alone, a relay that accepts a replacement, removes the version sitting below the cursor, and pushes the replacement some time later has violated nothing: the enumeration in between finds neither version, the pinned window and the continuation both come back empty, and the load reports *complete* moments before the fence delivers the floor it was missing. Ordering that push ahead of the verdict is what the delivery barrier below requires of the relay. On the client side, the verdict MUST NOT be rendered until end-of-stored-events for the final continuation has been received and every fence delivery received before it has been collected. + +If the client did not hold such a subscription for the whole load, or it lapsed or reconnected at any point during it, the load is potentially incomplete regardless of what the enumeration returned. A client MUST NOT publish to its own coordinates while its own load is in progress; a self-inflicted replacement is the same defect with the client on both ends of it. + +1. Every query MUST carry the same explicit `limit` `n`, `n` MUST be at least `L`, and no query MUST constrain tags. `C` and the floor are only meaningful across queries that differ solely in their time bounds. `n` SHOULD be substantially larger than `L`: `n` bounds how many events a single band can retrieve, so a small `n` costs round trips without making any verdict safer. +2. From each delivered event, collect the read-state coordinates — those whose `d` tag has the form `read-state:` — deduplicating by `d` tag value and retaining, of the entries sharing a `d` tag value, the one with the greatest `created_at`, and on equal `created_at` the one with the lexicographically lowest event id. That is the addressable ordering NIP-01 defines, and both halves of it are load-bearing here: a replacement published in the same second as the version it replaces is legal and is the one the relay retains, so a retention rule that only compares `created_at` may keep the superseded version even when the fence delivered its successor perfectly. Ignore the other events, but count them: they are part of what the cap returned. Events the fence delivers are collected the same way, but MUST NOT contribute to `T` or to `C`: they are not a query result, and an event arriving below the cursor would otherwise move it down and skip the band between. Collection is what recovers a moved coordinate; the cursor descends on query results alone. +3. Let `T` be the lowest `created_at` across **all** events delivered by the queries in this load, not only the read-state ones. The cursor therefore advances on every non-empty page, including one that yielded no coordinate. +4. Before advancing past `T`, the client MUST query the pinned window `{"since": T, "until": T}` and merge the result. A cap can cut mid-second, leaving events at `T` that a continuation at `"until": T - 1` would skip forever; pinning both bounds to one second removes every event outside that second from contention for the cap. +5. Second `T` is exhausted only if that pinned query delivered fewer than `max(C, L)` events. If it delivered `max(C, L)` or more, the cap may have bound inside the second, no finer cursor exists on the standard filter surface, and the load is **potentially incomplete** and MUST be reported as such. This verdict is terminal for the load: the client MUST NOT continue to step 6, and no later observation upgrades it. A continuation past an undischarged second can deliver nothing simply because that second was the oldest, so an empty continuation is not evidence that the second above it was exhausted. +6. Otherwise continue with `"until": T - 1`. Because a bare `until` is inclusive, decrementing guarantees each continuation covers a strictly older band, so the loop makes progress regardless of how the relay caps. +7. The load is **complete** when a continuation delivers no events at all, every preceding second having been discharged by step 5, the fence having been established before the first query and held unbroken since, and every fence delivery received up to that continuation's end-of-stored-events having been collected. Because the filter constrains nothing the relay applies after its cap, an empty delivery is an empty result — a cap that returns nothing is not a cap. +8. A load that failed, or whose fence lapsed, on any relay the client publishes to is potentially incomplete (see Read-Before-Write). + +This layer places five requirements on every relay a client performs a full-state load against. They are stated normatively, not as background assumptions, because a *complete* verdict rests on them and none of them is verifiable from the responses a client receives: + +- **Newest-first prefix delivery.** A capped result MUST consist of the newest events by `created_at` for the filter, ties broken by lowest id — the delivery NIP-01 already specifies for `limit`. A relay that caps by returning some other subset can omit an event lying *above* the cursor the client derives from that same delivery, so the omitted event is never queried at all. Repeating a query cannot recover it, because the same filter with the same bounds is the same request. +- **Non-decreasing effective cap within a load.** A relay MUST NOT reduce, within a single load, the number of events it will deliver for queries that differ solely in their time bounds. A cap that shrinks between the query establishing `C` and a later pinned window makes that window's short delivery indistinguishable from exhaustion, which converts a truncated second into a discharged one. +- **The floor `L`.** A relay MUST deliver at least `L` events for a query whose matching set holds at least `L` and whose requested `limit` is at least `L`. `L = 2`, fixed by this NIP; a client MUST NOT derive it from relay-advertised discovery, because an advertised maximum is not necessarily the limit a relay enforces. +- **Push delivery on an open subscription.** A relay MUST deliver every event it accepts that matches an open subscription's filter to that subscription. The mutation fence in step 2 is exactly this delivery; a relay that accepts a replacement without pushing it gives the client no way to observe a coordinate that moved above the cursor. +- **The delivery barrier.** Before a relay sends end-of-stored-events for a query, every event it accepted before that query read its stored events, and which matches an open subscription on the same connection, MUST already have been delivered to that subscription. Push delivery alone promises only that the replacement arrives eventually; the barrier is what places it before the verdict that depends on it. Without it, a relay whose accept path and query path proceed independently can answer a query from storage the replacement has already changed while the corresponding push is still pending, and the client discharges the load in the interval between the two. + +A client cannot distinguish a relay that violates any of these from one that simply had fewer events to return, so these are conformance preconditions of this layer rather than properties a load establishes. A client MUST NOT perform a full-state load against a relay it knows, or has evidence, to violate them, and MUST treat any load against such a relay as potentially incomplete. Conditioning *complete* on positive proof of these properties instead would be equivalent to never issuing it — no such proof exists on the standard filter surface — which would withdraw the override layer from every client rather than from the non-conforming relays. + +The comparison in step 5 fails safe: a pinned window is reported potentially incomplete unless the relay has already shown it will deliver at least that many at once, so an inconclusive result is never mistaken for an exhaustive one. A plateau of more events at a single `created_at` than the relay will deliver for a window pinned to that second is therefore unenumerable, because this NIP defines no finer cursor, and it resolves to *cannot prove complete* rather than to a false *complete*. The comparison is a lower bound on the cap rather than the cap itself, so it is also conservative in the other direction: a load whose oldest second holds as many events as the largest delivery observed so far resolves to *cannot prove complete* even where the relay would have delivered more. Where more than one coordinate exists this is transient, because any later publish moves that coordinate to a different second and separates the two. + +The floor is the narrowest of the five requirements and the one that makes the ordinary case reachable at all. A coordinate at a replaceable kind contributes exactly one event no matter how many times it is republished, because a republish replaces the previous version rather than appending to it; a client's event count at this kind therefore does not grow over time, and a single-installation client publishing under one coordinate has one event at one second permanently. Without a floor, `C` for such a client is one, its pinned window delivers one, and step 5 can never be discharged — mark-unread would be permanently unavailable to the most common conforming deployment, and no amount of waiting or republishing would change the observation. `L = 2` discharges it: the pinned window delivers one event, `max(C, L)` is two, `1 < 2`, the second is exhausted, and the continuation below it is empty. That same replacement behaviour is what the fence exists for: the one event a coordinate contributes can move, and it moves by being replaced. + +A **potentially incomplete** load MUST NOT be the basis for any of the following, each of which either destroys override state or asserts authority over it: + +- canonical compaction of an override register (see Mandatory Canonical Publication), +- publishing a canonicalized override blob, +- deleting or abandoning any coordinate (see Orphaned Blob Deletion), +- reporting an explicit mark-read as successful (see Actions). + +Until a complete load succeeds, the client MUST evaluate unread state from its own locally persisted state and MUST report override actions as failed rather than acting on a partial view. The honest terminal states are *complete* and *cannot prove complete*; a client MUST NOT treat the second as the first. + +The number of coordinates a full-state load must retrieve is bounded by the number of installations that have ever used the override layer, plus their not-yet-deleted rotation predecessors. It grows with the user's device history, not with elapsed time, and — because a coordinate carrying `ov_*` entries may not be deleted until it has been carried forward (see Client-ID Rotation) — it does not shrink on its own. Clients SHOULD carry forward and delete rotation predecessors promptly so the count stays near one coordinate per live installation. ### Merge Rule @@ -311,6 +388,8 @@ effective[context] = max(timestamp) across all blobs This is a grow-only max-register state-based CvRDT with an associative, commutative, idempotent join. Clients MUST NOT lower a read timestamp — only advance it. +The manual-unread override layer (see Manual-Unread Override Layer below) adds per-context set/clear counters merged by the same componentwise `max()` rule. The frontier merge rule is unchanged. + ### Writing Clients MAY publish read state automatically when read-position sync is part of @@ -320,28 +399,32 @@ to other users MUST require explicit user consent. Clients SHOULD publish read state blobs to the same relays they use for general event storage. Clients that implement NIP-65 (relay list metadata) SHOULD publish to their write relays and fetch from their read relays. -Each client instance maintains its own blob (one `kind:30078` event per ``). Writing replaces the previous blob via parameterized replaceable event semantics ([NIP-33](33.md)). +Each client instance maintains its own primary blob (one `kind:30078` event at its primary coordinate), plus one event per additional frontier-only coordinate if it uses any. Writing replaces the previous blob at each coordinate via parameterized replaceable event semantics ([NIP-33](33.md)). -Clients MUST only update the blob whose decrypted `client_id` matches their own `client_id`. Clients MUST NOT overwrite another instance's blob. +Clients MUST only update blobs whose decrypted `client_id` matches their own `client_id`. Clients MUST NOT overwrite another instance's blob. -If the client discovers multiple blobs with its own `client_id` during a fetch, it MUST select the one with the highest `created_at` as its active blob and SHOULD delete the others. +If the client discovers same-`client_id` blobs at coordinates that are neither its primary nor one of its known additional coordinates (e.g., rotation orphans or backup/restore duplicates), it MUST merge them into its own state and MUST NOT delete them until their override state has been carried forward (see Orphaned Blob Deletion). It MUST NOT publish to them: its own writes go to its primary and its known additional coordinates only. #### Read-Before-Write Before publishing, a client MUST: -1. Fetch its own current blob from each relay it intends to publish to, and merge all fetched versions. +1. Fetch its own current blob(s) from each relay it intends to publish to, and merge all fetched versions. -The client fetches its own blob using its known `d` tag value: +A client fetches its own coordinates using their known `d` tag values — its primary, plus its additional frontier-only coordinates if any — and unions them componentwise: ```json -{"kinds": [30078], "authors": [""], "#d": ["read-state:"]} +{"kinds": [30078], "authors": [""], "#d": ["read-state:", "read-state:", ...]} ``` -2. Decrypt and merge the fetched blob with local state using `max()` per context. +A read-before-write fetch of the client's own coordinates is not a full-state load: it cannot discover rotation orphans or duplicates. Before canonicalizing override state or publishing a canonicalized override blob, the client MUST have a complete full-state load (see Full-State Load). + +2. Decrypt and merge the fetched blob(s) with local state using `max()` per context. 3. Publish the merged result. -If a relay is unreachable during the fetch step, the client SHOULD proceed with the data available from reachable relays. The merge rule ensures that data from the unreachable relay will be incorporated on the next successful fetch, provided the relay retains the event. Permanent relay loss or event expiry may result in state loss — this is an accepted property of the best-effort model (see Non-Goals). +If a relay is unreachable during the fetch step, the client SHOULD proceed with the data available from reachable relays. The merge rule ensures that data from the unreachable relay will be incorporated on the next successful fetch, provided the relay retains the event. Permanent relay loss or event expiry may result in loss of frontier state — this is an accepted property of the best-effort model (see Non-Goals). + +That accepted loss does not extend to override state. A client MUST NOT treat a fetch that failed on any relay it publishes to as a complete view of its own override state, and MUST NOT canonicalize, publish canonicalized override state, or delete or abandon any of its own coordinates on the basis of such a partial fetch (see Full-State Load). Clients implementing the override layer SHOULD publish override state to more than one relay so that the loss of a single relay does not erase a tombstone floor. This read-before-write requirement also applies to re-publishes triggered by incoming blobs from other instances (see Live Subscription and Convergence). @@ -358,12 +441,14 @@ Clients SHOULD subscribe to `kind:30078` events for their own pubkey with `#t: [ When a blob from another client instance arrives (i.e., its decrypted `client_id` does not match the client's own `client_id`): 1. Merge it into local state using `max()` per context. -2. If any context timestamp in the incoming blob is greater than the corresponding timestamp in the client's last-published blob (or the context is absent from the last-published blob), perform a read-before-write and re-publish the client's own blob after a debounce delay. -3. Clients MUST suppress the re-publish if the merged result is identical to the client's last-published blob. A client that has never published treats its last-published blob as empty. +2. Canonicalize the merged override state against the client's own effective frontier (applying the tombstone floor and live/dead/virgin rules from Mandatory Canonical Publication). If any context entry in the canonical merged result differs from the corresponding entry in the client's last-published canonical blob (or the context is absent from the last-published blob), perform a read-before-write and re-publish the client's own blob after a debounce delay. +3. Clients MUST suppress the re-publish if the canonical merged result is identical to the canonical form of the client's last-published blob. Comparing canonical-to-canonical prevents a retained live peer blob (which the client has already tombstoned) from triggering an identical write on every replay. A client that has never published treats its last-published blob as empty. 4. Clients SHOULD limit re-publishes triggered by incoming blobs to at most one per debounce window, regardless of how many blobs arrive during that window. This drives convergence without a coordination round-trip, assuming eventual relay reachability and event retention. +A live subscription is not a full-state load. A relay MAY return a capped set of stored events before end-of-stored-events on this filter, so a client implementing the override layer MUST NOT treat what the subscription delivers as a complete view of its coordinates (see Full-State Load). Merging an incoming blob into local state (step 1) is always safe, because merge is componentwise `max()`; the canonicalize-and-re-publish in steps 2–3 is a canonical publication and therefore requires a complete full-state load. A client that does not have one MUST defer the re-publish rather than publish a canonical blob derived from a partial view. A subscription is nonetheless a required *component* of a full-state load, serving as its mutation fence, and the fence MUST use the tag-free filter rather than the `#t`-narrowed one above — a replacement it fails to deliver is a replacement the descending enumeration cannot recover. + #### Clock Skew When publishing, if the client's local clock produces a `created_at` value less than or equal to the maximum `created_at` seen across all fetched blobs for the same `d` tag, the client MUST use `max_fetched_created_at + 1` instead. @@ -372,17 +457,158 @@ When publishing, if the client's local clock produces a `created_at` value less Clients SHOULD debounce writes to avoid excessive relay traffic (e.g., flush 5–10 seconds after the last local read-state change, or on app close/background transition). Clients MUST NOT write on every individual read action. -The blob SHOULD contain only contexts the client has explicitly interacted with. Clients SHOULD prune aggressively, prioritizing recently-active contexts, and MAY drop entries older than the time horizon before writing. Clients MUST ensure the published event does not exceed relay event size limits (typically 64 KB content). +The blob SHOULD contain only contexts the client has explicitly interacted with. Clients SHOULD prune aggressively, prioritizing recently-active contexts, and MAY drop frontier entries older than the time horizon before writing. Clients MUST NOT drop `ov_*` override entries (including tombstone floors) based on age or budget pressure; see Override State Durability in the Manual-Unread Override Layer section. Clients MUST ensure the published event does not exceed relay event size limits (typically 64 KB content). #### Client-ID Rotation -Clients MAY rotate their `client_id` by generating a new one, generating a new random ``, and publishing a new blob. The old blob becomes orphaned and ages out of the time horizon naturally. Rotation adds one extra blob temporarily. Clients SHOULD keep their `client_id` stable for as long as possible to minimize blob proliferation. +Clients MAY rotate their `client_id` by generating a new one, generating a new random `` for the primary coordinate, and publishing a new blob. Rotation adds one extra blob temporarily. Clients SHOULD keep their `client_id` stable for as long as possible to minimize blob proliferation. + +Rotation is the only event that changes a client's override-bearing coordinate, and it carries the layer's single durability obligation: + +**Carry-forward rule.** Before deleting or abandoning its previous primary, a rotating client MUST publish the componentwise `max()` of every override register the old primary holds — every tombstone ceiling included — under its new primary, and MUST confirm acceptance **on every relay from which the old primary will be deleted or allowed to lapse**. If any such relay rejects the publish or is unreachable, the client MUST retain the old primary on that relay and MUST NOT delete it there. Acceptance on one relay does not authorize deletion on another: a relay that never received the replacement would otherwise be left with no local carrier of the floor. The old primary MUST NOT be left to age out while it is the only carrier of an override floor on any relay. -If a device backup or clone results in two installations sharing the same `client_id` and `slot-id`, both will write to the same blob. This is operationally equivalent to a single client and does not corrupt state, but the two installations will overwrite each other's context entries. Clients that detect this condition (e.g., by observing unexpected context changes in their own blob) SHOULD generate a new `client_id` and `slot-id`. +Additional frontier-only coordinates carry no override state, so rotation may abandon or delete them freely. + +If a device backup or clone results in two installations sharing the same `client_id` and primary ``, both will write to the same coordinate. This is operationally equivalent to a single client and does not corrupt state, but the two installations will overwrite each other's context entries. Clients that detect this condition (e.g., by observing unexpected context changes in their own blob) SHOULD generate a new `client_id` and a fresh primary ``, again carrying override state forward per the carry-forward rule. #### Orphaned Blob Deletion -Clients MAY delete blobs from decommissioned client instances by publishing a `kind:5` deletion event per [NIP-09](09.md) targeting the orphaned event's `a` tag coordinate (`30078::`). This is optional — orphaned blobs are harmless and age out naturally. +Clients MAY delete blobs from decommissioned client instances by publishing a `kind:5` deletion event per [NIP-09](09.md) targeting the orphaned event's `a` tag coordinate (`30078::`). For blobs carrying no `ov_*` entries — including a client's own additional frontier-only coordinates — this is optional and unconditional: such blobs are harmless and age out naturally. + +A blob carrying `ov_*` entries MUST NOT be deleted or abandoned until its override state has been carried forward per the carry-forward rule in Client-ID Rotation. This applies to the client's own previous primary and to same-`client_id` orphans discovered from a prior rotation or a backup/restore. A client's record of its own coordinates MAY be stale — for example restored from a backup taken before a rotation — so an unknown same-`client_id` coordinate MUST be treated as a live carrier of override state, not as a deletable duplicate, until it has been merged and carried forward. + +### Manual-Unread Override Layer + +This section defines a manual mark-as-unread mechanism as a CRDT override layer within the existing `contexts` map. It does not change the frontier merge rule, event structure, or encryption scheme. Fetching follows the override-specific full-state procedure (see Full-State Load) rather than the horizon-bounded fetch used by clients that do not implement this section. Clients that do not implement this section remain fully interoperable (see Backwards Compatibility). + +#### Wire Encoding + +For each manually-unread context ``, a client publishes up to three sibling keys alongside the existing frontier entry in the `contexts` map: + +| Key | Type | Description | +|-----|------|-------------| +| `ov_s:` | uint32 | Set counter S — incremented on each mark-unread | +| `ov_c:` | uint32 | Clear counter C — incremented on each mark-read | +| `ov_b:` | uint32 | Baseline B — the effective frontier value at the time of the most recent mark-unread | + +Values MUST be integers in the range 0–4294967295 (same validation range as context timestamps). The `` suffix is the raw context ID without any escaping (escaping applies only to the frontier wire key; see Reserved Namespace). + +#### Merge Rule (Override Registers) + +Override counters are merged by componentwise `max()`, identical to the frontier merge rule: + +``` +merged_S[ctx] = max(S) across all blobs +merged_C[ctx] = max(C) across all blobs +merged_B[ctx] = max(B) across all blobs +``` + +No new wire-level merge logic is required. The same `mergeReadStateEvents` path that joins frontier timestamps joins the counter entries as integer max. + +#### Liveness Predicate + +A context `ctx` has an active manual-unread override if and only if ALL of the following hold, evaluated against the merged register `(S, C, B)` and the merged effective frontier `F`: + +1. `S > 0` — at least one mark-unread action has been recorded. +2. `F <= B` — the effective frontier has not advanced past the baseline captured at mark-unread time. (A natural frontier advance strictly past `B` dominates a stale set, clearing the override without any explicit clear action.) +3. `S > C` — set counter exceeds clear counter. (`S == C` is treated as inactive: clear wins on ties — see Tie Policy.) + +Formally (clear-wins is the only conforming tie policy — see Tie Policy): + +``` +override_active(S, C, B, F) = + S > 0 + AND F <= B + AND S > C +``` + +The **unread verdict** for a context is: + +``` +unread(ctx) = (latest_message_ts > F) OR override_active(S, C, B, F) +``` + +where `latest_message_ts` is the `created_at` of the newest message in the context. + +#### Actions + +Every action below requires a complete full-state load (see Full-State Load); on a potentially incomplete load the client MUST report the action as failed rather than act on a partial view of its own override state. + +**Mark-unread:** increment S to `max(S, C) + 1`; set B to the current effective frontier value for the context. C is unchanged. If `max(S, C) == 4294967295` (uint32 maximum), the client MUST refuse the mark-unread action and leave the register unchanged; wrapping or resetting to zero is prohibited. + +**Mark-read (explicit):** advance the frontier to cover the context as normal; increment C to `max(S, C) + 1`. S and B are unchanged. If `max(S, C) == 4294967295`, no representable counter increment exists; wrapping or resetting to zero is prohibited. The client MUST then complete the action only if the resulting state satisfies `override_active == false` — i.e. the frontier advance alone deactivates the override, or the override was already inactive. Otherwise the counters MUST be left unchanged and the client MUST report the mark-read as failed; the monotone frontier advance itself is still permitted, but a client MUST NOT report an explicit mark-read as successful while `override_active` remains true. + +**Natural read (frontier advance):** advance the frontier past B. No counter update is needed — the liveness predicate's `F <= B` condition automatically deactivates the override when the frontier dominates the baseline. + +#### Tombstone Floor + +A register where `S > 0` or `C > 0` (ever-active) that evaluates as inactive MUST be compacted to the tombstone floor before publication: + +``` +tombstone = RegB(S=0, C=max(S, C), B=0) +``` + +This preserves the counter ceiling as a reuse-blocking floor. A register where `S == 0` and `C == 0` (virgin, never activated) MUST be omitted from the wire entirely (0 keys). + +#### Mandatory Canonical Publication + +Publishers MUST canonicalize every override against their own effective frontier at serialization time before writing to the wire: + +- **Live override** (`override_active` is true): publish all three keys (`ov_s:`, `ov_c:`, `ov_b:`) with their current values unchanged. +- **Dead override** (`override_active` is false, `S > 0` or `C > 0`): publish only the tombstone floor — a single `ov_c:` key with value `max(S, C)`. +- **Virgin register** (`S == 0` and `C == 0`): omit all three keys from the wire. + +This is a protocol requirement, not an optimization. A client that publishes raw (non-canonical) dead registers can cause two independently-dead registers from different devices to produce a live join on merge. See `docs/formal/nip-rs-unread/` for the exhaustive proof and mutation harness. + +#### Override Group Co-Location Rule + +A context's frontier entry and ALL of its `ov_*` sibling entries MUST travel in the same event, and that event MUST be the primary coordinate. Because all `ov_*` entries live in the primary (see `d` Tag), an override-bearing context has exactly one legal destination for its whole group: a client that splits frontier entries into additional coordinates MUST NOT move the frontier entry of an override-bearing context out of the primary, and MUST NOT place `ov_*` entries anywhere else. Only frontier-only groups — contexts with no `ov_*` entries — may be distributed across additional coordinates. + +Implementations that split blobs across coordinates MUST group context entries per logical context — not per individual key — and assign the entire group atomically to one coordinate. Round-robin or other assignment strategies MUST operate on groups, not on individual entries. + +**Unescape-before-group rule (corollary):** when grouping, a frontier wire key MUST be unescaped to its raw logical context ID (stripping one leading `esc:` if present) before being used as the group identity. Without this step, a frontier key `esc:ov_s:evil` and its `ov_*` siblings (keyed by the raw suffix `ov_s:evil`) resolve to different groups and the register splits across coordinates, reproducing the partial-reconstruction poison across publication cycles. + +**Rationale:** a receiver holding only a partial group (e.g., `ov_s:ctx` without `ov_b:ctx`) reconstructs a register with incorrect baseline and may canonically publish a false tombstone. With atomic grouping, a compliant publisher's output never permits partial reconstruction. + +#### Tie Policy + +**Clients MUST use clear-wins.** When `S == C` and `S > 0`, the override MUST be treated as inactive, and the register MUST be compacted to the tombstone floor on publication (see Tombstone Floor). + +Clear-wins is normative rather than a local implementation choice because the tie verdict is not encoded on the wire. Two conforming clients holding the same merged register `(S, C, B, F) = (1, 1, 10, 10)` would otherwise disagree permanently: a clear-wins client reports read and publishes the single-key tombstone floor, a set-wins client reports unread and publishes all three keys. Further deliveries converge the counters but can never converge either the verdict or the canonical wire form, which defeats cross-device synchronization. Supporting a selectable tie policy would require encoding the policy in the blob plus a separate interoperability design; neither is in scope here. + +Clear-wins also matches the product semantics this layer is designed for: a false negative (a missed badge) is recoverable by re-marking unread, while a false positive (a badge that will not clear) is more disruptive. See `docs/formal/nip-rs-unread/NOTE.md` for the policy comparison — both policies satisfy the merge-correctness invariants in isolation, so this is an interoperability requirement, not a merge-safety one. + +#### Override State Durability + +`ov_*` override entries — especially tombstone floors (`ov_c:` keys) — carry a reuse-blocking counter ceiling that prevents stale override components from resurrecting a dead register. Specifically, if a tombstone floor `(S=0, C=k, B=0)` is dropped and a stale snapshot `(S=k, C=0, B=b)` is later replayed, the merged result `(S=k, C=0, B=b)` would evaluate as live — a resurrection. + +Because legacy clients can carry and republish old `ov_*` keys indefinitely (they pass through `sanitizeContexts` as unknown opaque entries), there is no finite time after which all stale override components are guaranteed absent. Therefore: + +**Clients MUST NOT drop `ov_*` override entries (including tombstone floors) based on age pruning or budget eviction.** This exemption applies permanently. Age-based pruning applies to frontier entries only. Eviction strategies that respect byte/key budgets MUST apply to frontier and `msg:`/`thread:` entries first and MUST NOT touch `ov_*` entries. + +**Durability is a property of retrievable logical state, not of keys within one blob.** An override register survives only if a client that loads its full state can still reach every component. Therefore, in addition to the per-entry rule above: + +- Full-state loads by clients implementing this layer MUST NOT be restricted by a finite event-level `since` window, and MUST establish completeness rather than assume it; the containing event must remain reachable, not merely retain its keys (see Full-State Load). +- No coordinate carrying `ov_*` entries may be deleted or abandoned until the componentwise `max()` of every override register it holds — especially every tombstone ceiling — has been republished under the client's current primary coordinate and accepted on every relay from which the old coordinate will be deleted or allowed to lapse (see Client-ID Rotation, Orphaned Blob Deletion). + +**There is no safe finite GC horizon for override state.** Any protocol that proposes to delete tombstone floors after a bounded period requires a separately proved guarantee that no stale override component can re-enter the merge — this amendment does not provide such a guarantee. + +#### Bounds and Budget + +- **Key growth:** a live override adds 3 entries per context; a tombstoned override adds 1 entry per context. At 100 overridden channel contexts: ~300 live entries or ~100 tombstone entries. +- **Byte cost (small-counter example, common case):** channel UUID context (36 chars), counters S=1/C=0/B=10 — live override ~138 bytes; tombstone ~45 bytes. **Byte cost at uint32 maximum** (S=4294967295, worst case): live override ~164 bytes; tombstone ~54 bytes. +- **Hard ceiling on ever-overridden contexts.** Because all `ov_*` entries live in one coordinate (see `d` Tag) and tombstones can never be pruned (see Override State Durability — there is no safe finite GC horizon), the primary blob's plaintext budget is a hard ceiling on the number of contexts a single installation can ever have manually marked unread. Against a 32 KiB plaintext budget: roughly **600** tombstoned contexts at the worst-case ~54 bytes, ~730 at the common ~45 bytes, or ~199 simultaneously live overrides at ~164 bytes — and that is before frontier entries get any room at all. +- **Terminal behaviour at the ceiling.** When the primary blob cannot accommodate a new override group after all prunable frontier entries have been evicted, the client MUST refuse the mark-unread action and report it as failed. It MUST NOT split override state across coordinates and MUST NOT drop tombstone floors to make room. Likewise, a client whose merged override state — including tombstones merged in from peer installations — no longer fits in its primary blob MUST leave its last-published primary in place, MUST NOT publish a primary that omits merged `ov_*` entries, and MUST report override actions as failed; publishing a truncated override set is budget-driven override loss under another name. No floor is lost in this state, because the installations that originated those floors still carry them; the constrained installation simply stops acting as a replica until it has room. This is the same policy shape as counter exhaustion (see Actions): visible failure, never silent degradation. +- **10,000-key limit:** override entries count toward the existing per-blob validation limit. Tombstones accumulate permanently with every distinct ever-overridden context; they cannot be pruned. Clients SHOULD compact dead overrides aggressively and MAY enforce an active-live-override cap. Note that a cap on live overrides does not bound the total `ov_*` entry count over an unbounded context lifetime — tombstones from all historical overrides remain. The 32 KiB and 10,000-entry limits are expressed per blob at write time; a client that has overridden many distinct contexts over its lifetime must account for all accumulated tombstones when evaluating budget headroom. +- **256-byte key limit:** override keys (`ov_s:`, `ov_c:`, `ov_b:` + context ID) count toward the per-entry 256-byte validation limit. Context IDs up to 251 bytes are safe. Buzz's own context ID shapes (UUID 36 bytes, `msg:hex64` 68 bytes, `thread:hex64` 71 bytes) are well within this limit. + +#### Verification Artifact + +The design was verified by bounded exhaustive model checking prior to this amendment. See `docs/formal/nip-rs-unread/` for the full model (`model.py`, `exhaustive.py`), 9-mutant harness (`mutation.py`), and design notes (`NOTE.md`). + +The harness verifies the three load-bearing safety requirements — tombstone floor, mandatory canonical publication, and atomic per-context grouping with unescape-before-group — are necessary: each mutant that drops one of these rules produces a detectable witness of permanent false-clear or resurrection. M3 validates that the clear-wins tie policy produces the intended product-semantics behavior; M5 and M6 witness value-range and convergence failures respectively. Clear-wins is normative for interoperability (see Tie Policy), not because set-wins violates merge safety — the model confirms both tie policies satisfy the merge-correctness invariants when applied uniformly. + +**Scope of formal verification:** the bounded model covers the CRDT register algebra, merge/compaction rules, per-context grouping atomicity, and escape/unescape bijection. The model is a broader predecessor of this NIP: its `split_blob_into_slots` permits override groups in any slot, whereas this NIP confines them to one primary coordinate, so the verified atomicity property holds for every arrangement this NIP permits but the converse does not follow. The model does **not** verify the single-primary rule, the full-state-load completeness procedure, the relay conformance requirements or the mutation fence it depends on, or the carry-forward rule; those are normative here and argued, not proved. The model also does NOT cover malformed-group wire validation (the accepted-shape rules in Content Validation). That rule is sound by the partial-group argument (rejecting a partial group leaves a virgin register — a merge no-op — which is strictly safer than zero-filling missing components), but its correctness under parser-level implementation is outside the model's verified scope. Implementation-level tests MUST cover the accepted wire shapes and rejection behavior. ## Example @@ -504,9 +730,9 @@ The conversation key is `nip44_conversation_key(private_key, public_key)` — EC ### Conflict Detection Vector -Device A has `slot-id` = `aaa111` and `client_id` = `client-A`. It fetches its own `d` tag coordinate `read-state:aaa111` and decrypts the blob. The decrypted `client_id` is `client-B` (not `client-A`). This is a slot-id conflict — another device has claimed this coordinate. +Device A has `slot-id` = `aaa111aaa111aaa111aaa111aaa111aa` and `client_id` = `client-A`. It fetches its own `d` tag coordinate `read-state:aaa111aaa111aaa111aaa111aaa111aa` and decrypts the blob. The decrypted `client_id` is `client-B` (not `client-A`). This is a slot-id conflict — another device has claimed this coordinate. -Device A MUST NOT publish to `read-state:aaa111`. Device A MUST generate a new random `slot-id` (e.g., `ccc333`) and publish its blob under `read-state:ccc333`. +Device A MUST NOT publish to `read-state:aaa111aaa111aaa111aaa111aaa111aa`. Device A MUST generate a new random `slot-id` (e.g., `ccc333ccc333ccc333ccc333ccc333cc`) and publish its blob under `read-state:ccc333ccc333ccc333ccc333ccc333cc`. ### Clock Skew Vector @@ -541,7 +767,7 @@ Ciphertext length reveals the approximate number of tracked contexts and may cor Because slot IDs are random and independent of `client_id` values, relay operators cannot directly link blobs to specific devices or client implementations. Timing correlation and write patterns may still allow probabilistic linkage. -Because the merge rule is monotonic, replaying an old event to a relay is harmless — it cannot lower a read timestamp. However, replaying many old events simultaneously could trigger convergence re-publishes from active clients. The debounce window (see Debounce and Pruning) limits this to at most one re-publish per window. +Because the frontier merge rule is monotonic, replaying an old frontier event to a relay is harmless — it cannot lower a read timestamp. The override layer's counter merge is also monotonic (componentwise max), so replaying an old override event cannot lower a counter; however, a stale override component replayed after a tombstone floor was published could suppress a fresh set for one reconciliation cycle (see Override State Durability). The debounce window (see Debounce and Pruning) limits convergence re-publishes to at most one per window. Clients supporting multiple Nostr identities SHOULD use distinct `client_id` values and distinct slot IDs per identity. Reusing identifiers across pubkeys allows relay operators to link those identities. @@ -557,10 +783,13 @@ that expose read activity to other users MUST require explicit user consent. ## Backwards Compatibility -This NIP introduces no changes to existing event kinds or relay behavior. It uses only standard NIP-01 event storage, NIP-33 addressable event semantics, NIP-44 encryption, and NIP-78 application data conventions. Clients that do not implement this NIP are unaffected. +This NIP introduces no changes to existing event kinds and adds no new kind, wire message, or relay-stored read-state logic. It uses only standard NIP-01 event storage, NIP-33 addressable event semantics, NIP-44 encryption, and NIP-78 application data conventions. Clients that do not implement this NIP are unaffected, as are clients that implement everything but the manual-unread override layer. + +The override layer is the exception, and it is a relay-compatibility one rather than a client one. Its full-state load carries the completeness guarantee only against a relay that satisfies the ordering, capacity, floor, push, and barrier requirements enumerated in Full-State Load. Against a relay known or evidenced not to conform, every load resolves to *cannot prove complete* and the actions that depend on a complete load report as failed; against an undetectably nonconforming relay, a load may still return *complete*, and the completeness guarantee does not apply to that verdict. In either case the layer still runs and still merges, and frontier sync is unaffected. ## References +- [NIP-01](01.md) — Basic Protocol Flow Description (defines filter `limit`, `since`, and `until`) - [NIP-09](09.md) — Event Deletion Request - [NIP-33](33.md) — Parameterized Replaceable Events - [NIP-44](44.md) — Versioned Encryption