External/buzz
1
0
Fork 0
mirror of https://github.com/block/buzz.git synced 2026-08-18 06:50:31 +02:00
Code Issues Packages Projects Releases Wiki Activity
Files
codex/security-postgres-timeouts
buzz/docs/formal/nip-rs-unread/NOTE.md
T
Will PflegerGitHubnpub1mn7jgtj4w2pd0g0zeuhxsa6jy6p0rewxz4kujt98my82ahfmp72sxjexk7
 209536ade6 docs(nips): add single-coordinate manual-unread override layer and verification model to NIP-RS (#2864) 
## Summary

Amends `docs/nips/NIP-RS.md` with the manual mark-as-unread override
layer and includes `docs/formal/nip-rs-unread/`, the bounded exhaustive
verification model that preceded and informed the spec.

All `ov_*` override state lives in exactly one coordinate per
installation. That single constraint is what makes the rest of the
amendment small: override state never moves between coordinates, so
there is no slot lifecycle to make crash-safe, and the only durability
obligation is carry-forward on `client_id` rotation.

## Spec changes (`docs/nips/NIP-RS.md`)

- **Non-Goals:** drop the stale line stating mark-as-unread is out of
scope; state the `ov_*` durability exception to the
best-effort/time-horizon model.
- **Reserved Namespace:** `ov_` stem and `esc:` escape marker reserved.
Escape on publish (prepend `esc:` to raw IDs beginning with `ov_` or
`esc:`), unescape on receive (strip exactly one `esc:`). Bijection, with
the pre-amendment backward-compat residual documented as a stated
limitation.
- **Content Validation:** override entries are collected and validated
as a complete logical group *before* any decoding, zero-filling,
merging, or canonicalizing. Only two wire shapes are accepted — a
complete live three-key group, or an `ov_c:`-only tombstone floor. Any
other shape rejects the whole group while retaining the frontier entry;
applying the generic per-entry discard rule first is prohibited.
- **`d` Tag:** `<slot-id>` is exactly 32 lowercase hexadecimal
characters, replacing "a random opaque string" of 1–64 ASCII characters.
The fixed shape lets a relay recognize a read-state coordinate
structurally from the `d` tag alone, without decrypting anything, and
apply per-coordinate protections to it — under the old wording a
conforming client could pick a shape that silently forfeits them.
Recognizable coordinates are also what let a relay replace superseded
versions outright rather than accumulating one retained row per publish,
which keeps the coordinate count a full-state load must enumerate near
one per installation. Every client designates one **primary** coordinate
with a stable `<slot-id>` for the installation's lifetime. All `ov_*`
entries, and the frontier entries of the contexts they belong to, MUST
live in the primary. Additional coordinates remain legal for frontier
volume but MUST NOT carry `ov_*`, which keeps them freely rewritable and
freely deletable.
- **`t` Tag:** described as a discoverability marker rather than 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, MUST NOT infer completeness from a short result, and MUST omit
the tag entirely when performing a full-state load.
- **Fetching / Full-State Load:** clients implementing the override
layer MUST NOT apply a finite `since` filter — an encrypted payload
means a relay filter cannot select for override-bearing events, so any
event-level window can exclude the only coordinate holding a tombstone
floor. Removing `since` is not sufficient: relays MAY cap historical
results, MAY cap below the requested `limit`, and emit
end-of-stored-events after the capped query, so neither EOSE nor a short
page proves completeness. No test against the client's requested `limit`
can detect truncation either: the effective cap belongs to the relay, a
relay MAY cap below what was requested, and an advertised maximum limit
is not necessarily the limit enforced.

A full-state load is therefore enumerated on `{"kinds": [30078],
"authors": [<pubkey>], "limit": <n>}` with **no tag constraint**. A
relay MAY apply tag constraints only after its result cap and withhold
the events that fail them, so under a tag-constrained filter the
delivered count is not the count the cap selected — a delivered page can
be empty while older coordinates still exist below it, and `kind:30078`
is arbitrary application data whose `d` tag namespace is open to every
application that has written under the user's key. Omitting the tag
makes delivery observable; read-state selection moves client-side, where
the validation rules already place it.

Completeness is then established by enumeration on a strictly decreasing
cursor: collect a page, descend on the lowest `created_at` across all
delivered events, exhaust that second with a window pinned to it,
continue below it, and treat only an empty delivery as complete. Every
query carries the same explicit `limit` `n` with `n >= L`. Per-second
exhaustion is discharged by comparing the pinned window's delivery
against the largest delivery the relay has already demonstrated in the
same load, floored at `L = 2` so that the ordinary single-coordinate
installation can reach *complete* at all. The comparison fails safe: an
inconclusive window reports *cannot prove complete* rather than
*complete*, and that verdict is terminal for the load.

Because these are addressable events, a coordinate republished mid-load
moves *above* the descending cursor while its previous version stops
existing, so neither is reachable by any later query. A full-state load
is therefore fenced by a live subscription on the same tag-free filter,
established — defined as receipt of end-of-stored-events — before the
first enumeration query and held unbroken on the same connection for the
load's duration. Fence deliveries are collected like enumerated events
but do not contribute to the cursor or to the demonstrated-delivery
bound. Collection deduplicates coordinates on the full NIP-01
addressable ordering — greatest `created_at`, lowest event id on ties —
because an equal-timestamp replacement is legal and is the version the
relay retains. A lapsed or reconnected fence makes the load potentially
incomplete, and a client MUST NOT publish to its own coordinates during
its own load.

Five relay behaviours the *complete* verdict rests on are stated as
normative conformance preconditions rather than assumptions, because
none is verifiable from the responses a client receives: newest-first
prefix delivery with lowest-id tie-breaking (what NIP-01 already
specifies for `limit`), a non-decreasing effective cap within a load,
the floor `L`, push delivery on an open subscription, and a delivery
barrier ordering accepted matching events ahead of a query's
end-of-stored-events on the same connection. Conditioning *complete* on
positive proof of these instead would withdraw the override layer from
every client rather than from the non-conforming relays. A client MUST
NOT load against a relay it has evidence violates them, and MUST treat
any such load as potentially incomplete.

A load that is potentially incomplete, or that failed on any relay the
client publishes to, MUST NOT authorize canonical compaction, publishing
a canonicalized override blob, deleting or abandoning a coordinate, or
reporting a mark-read as successful; the client falls back to local
state.
- **Client-ID Rotation / Orphaned Blob Deletion:** rotation is the only
event that changes an override-bearing coordinate. Before deleting or
abandoning its previous primary, a client MUST republish the
componentwise `max()` of every register that 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. Acceptance on one relay does not authorize deletion
on another. Frontier-only orphans are deletable unconditionally; an
unknown same-`client_id` coordinate is treated as a live carrier until
merged.
- **Live Subscription and Convergence:** the re-publish trigger and its
suppression are evaluated on canonicalized state, so a retained live
peer blob the client has already tombstoned cannot trigger an identical
write on every replay.
- **Manual-Unread Override Layer** (new section):
- **Wire encoding:** `ov_s:<ctx>`, `ov_c:<ctx>`, `ov_b:<ctx>` as uint32
siblings in the existing `contexts` map.
- **Merge rule:** componentwise `max()` per counter — no new wire merge
logic.
- **Liveness predicate:** `S > 0 AND F <= B AND S > C`, transcribed from
`model.py::override_set_b`.
- **Actions:** mark-unread bumps S and captures the effective frontier
as B; mark-read bumps C; a natural frontier advance past B deactivates a
stale set with no counter update. Every action requires a complete
full-state load. At the uint32 ceiling, wrapping and resetting are
prohibited: mark-unread is refused, and mark-read completes only if the
resulting state has `override_active == false` — otherwise it fails
visibly rather than reporting success over a still-live override.
- **Tombstone floor:** a dead ever-active register compacts to `RegB(0,
max(S,C), 0)` — a single `ov_c:` key. A virgin register is omitted
entirely. This blocks counter reuse and the resulting resurrection.
- **Mandatory canonical publication:** a protocol requirement, not an
optimization. Publishing raw dead registers lets two independently-dead
registers from different devices produce a live join.
- **Override group co-location rule:** a context's frontier entry and
all its `ov_*` siblings MUST travel in the same event, and that event
MUST be the primary coordinate. An override-bearing context therefore
has exactly one legal destination for its whole group; only
frontier-only groups may be distributed across additional coordinates.
Grouping is per logical context, never per key.
- **Unescape-before-group rule:** the frontier wire key MUST be
unescaped to its raw logical context ID before use as group identity.
Equal normative weight to atomic grouping.
- **Tie policy:** clear-wins is MUST. The tie verdict is not encoded on
the wire, so a selectable policy makes two conforming clients diverge
permanently on both the unread verdict and the canonical wire form.
- **Override State Durability:** `ov_*` entries are exempt from age
pruning and budget eviction permanently, and durability is defined over
retrievable logical state — the containing event must stay reachable and
the load must establish completeness, not merely retain keys. There is
no safe finite GC horizon.
- **Bounds and budget:** byte/key analysis at both small-counter and
uint32-maximum values. Confining `ov_*` to one blob makes its plaintext
budget a hard lifetime ceiling on ever-overridden contexts — roughly 600
tombstones at the worst-case ~54 bytes against 32 KiB, ~730 at the
common ~45 bytes, ~199 simultaneously live overrides at ~164 bytes. At
the ceiling a client MUST refuse mark-unread and MUST NOT split override
state, drop floors, or publish a truncated override set. Same policy
shape as counter exhaustion: visible failure, never silent degradation.
- **Verification artifact:** `docs/formal/nip-rs-unread/`. The model is
a broader predecessor of this NIP: its `split_blob_into_slots` permits
override groups in any slot, so verified atomicity covers every
arrangement this NIP allows, but the converse does not follow. The model
does not verify the single-primary rule, the completeness procedure, the
relay conformance requirements or the mutation fence, or carry-forward;
malformed-group wire validation is likewise normative but outside
verified scope.

- **Abstract / Non-Goals / Backwards Compatibility:** the absolute "no
relay-side logic" and "no relay behavior changes" claims are narrowed to
what remains true — no new event kind, no new wire message, no
relay-stored read-state logic — with the override layer's relay
conformance contract named as the exception. Frontier sync and clients
that skip the override layer are unaffected on any relay.

## Verification model (`docs/formal/nip-rs-unread/`)

Four Python files constituting a bounded exhaustive verification model
for the override layer's register algebra.

**What it does:** constructs a toy universe — 2–3 devices, 2 channels,
every action that can happen (mark-unread, mark-read, late/duplicate
syncs, app reinstall, storage compaction) — and brute-forces every
reachable ordering (14,258 BFS states; 672-point deep-history parameter
cube; 9-mutant harness over ~45,000 merge pairs). After each world-state
it asks: did all devices converge? Did any unread flag get resurrected
after being cleared, or vanish while live?

**What it found and fixed:**

1. **Killed candidate A.** The model produced a concrete kill sequence:
an old client that doesn't know about the new field rewrites its
read-state blob and silently erases unread flags. That witness is why
the spec uses candidate B (two counters that only count up, plus a
snapshot) instead.
2. **Candidate B passes everything.** All delivery orders converge; the
frontier high-water mark never regresses; duplicated/replayed syncs are
harmless; old clients can't destroy it; compaction never resurrects a
dead unread or drops a live one, including
cleanup-followed-by-weeks-late-stale-sync and
tombstone-landing-on-unrelated-live-state corner cases.
3. **Caught a second real bug late.** Two devices each publishing "this
unread is cleared" could, on merge, reactivate it. The fix (canonicalize
before publishing) is a mandatory rule in the spec; the model re-checks
it across ~45,000 merge pairs.

**Scope and caveats:** bounded to 2–3 devices and 2 channels. Can't
prove the infinite case. `NOTE.md` documents the exact verification
scope and the gap between the model's `split_blob_into_slots` generality
and the single-primary rule the spec adds on top.

**Why it's in the repo:** the spec asserts "verified by bounded
exhaustive model checking." Keeping the artifact in-repo means anyone
who later amends the merge/compaction rules can `python3 exhaustive.py
&& python3 mutation.py` (deterministic, exit 0) and confirm the
guarantees hold. Without it the spec claims a proof nobody can check.

## Diff scope

`docs/nips/NIP-RS.md` — spec amendment, zero product code.

`docs/formal/nip-rs-unread/{NOTE.md,model.py,exhaustive.py,mutation.py}`
— bounded exhaustive verification model, zero product code.
`.gitignore` — `__pycache__/` and `*.pyc` entries for the model
directory.

---------

Signed-off-by: Will Pfleger <pfleger.will@gmail.com>
Co-authored-by: npub1mn7jgtj4w2pd0g0zeuhxsa6jy6p0rewxz4kujt98my82ahfmp72sxjexk7 <dcfd242e557282d7a1e2cf2e6877522682f1e5c6156dc92ca7d90eaedd3b0f95@buzz.block.builderlab.xyz>
2026-07-31 13:06:21 -04:00

39 KiB
Raw Permalink Blame History

title, tags, status, created
title tags status created
NIP-RS manual-unread: bounded exhaustive model — candidates A vs B
nostr
nip-rs
read-state
formal-model
buzz
active 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

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.
Reference in New Issue View Git Blame Copy Permalink