mirror of
https://github.com/block/buzz.git
synced 2026-08-18 06:50:31 +02:00
209536ade6
## 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>
699 lines
39 KiB
Markdown
699 lines
39 KiB
Markdown
---
|
||
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.
|