docs(nips): add single-coordinate manual-unread override layer and verification model to NIP-RS

[wpfleger96]

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.

[wesbillman]

Reviewed at d2f6b22. The revised register algebra, validation, canonicalization, clear-wins rule, and publish-before-retire transition are coherent, but one lifecycle/bounds contradiction remains.

docs/nips/NIP-RS.md:305 says the mandatory no-since full-state fetch is bounded by client instances x active slots per instance. That is not the set the same paragraph requires clients to fetch: lines 313 and 426-428 explicitly recognize orphaned/retired coordinates outside every persisted active-slot set, and deletion is optional after their override state has been carried forward. Such parameterized replaceable coordinates can therefore remain queryable indefinitely. A history of rotations/rebalances/backups can make the returned set grow with historical coordinates, not current active slots, so “This is cheap” and the stated bound are not guaranteed by this protocol.

Please state the actual bound (all extant read-state coordinates, including historical/orphan coordinates), or add a lifecycle requirement that makes the active-slot bound true. If cleanup is intended to establish the bound, specify what a client MUST delete and when, and account for relays where NIP-09 deletion is unavailable or not honored. The permanent tombstone/key growth is otherwise acknowledged and can be handled by additional slots; this finding is specifically about the mandatory fetch set and its claimed operational bound.

Current applicable CI is fully green; this is a protocol-completeness issue rather than a CI failure.