GO-7290 Chat read counters: causal-ordinal CORE (Option D, Stage 1) - #3179
Draft
requilence wants to merge 9 commits into
Draft
GO-7290 Chat read counters: causal-ordinal CORE (Option D, Stage 1)#3179requilence wants to merge 9 commits into
requilence wants to merge 9 commits into
Conversation
Convergent, exact read* counters with no graph walk at query time and no mutable per-message read flags. Two layers: CORE (bandSet + tail-range decomposition; O(1) queries incl. cold start; bounded walk only at frontier changes; O(1) incremental maintenance via parent-first attachment) and LABELS (immutable causal-past cardinality labels computed locally at apply; zero-band certificate sound under deletes; walk termination bound). Staged rollout: CORE alone is already exact+convergent. Includes the snapshot contract guard (product decision: no snapshots for chat CRDT trees), proofs (count identity, certificate soundness, O(1) maintenance, fold apply-order invariance), test plan with the cross-device convergence gate, and cost table. Base = develop (old DiffManager): no user-visible semantic change — D keeps develop's exact DAG-ancestor semantics while removing the O(tree) cold-start rebuild and SetReadFlag write storms. Supersedes the hybrid (Option B) design; prototype branches remain reference material.
From go-7290-chat-read-counter-computed (reference prototypes stay there): - computed-theory.md: formal theory + Theorems A/B + the §5.3 cross-device divergence analysis that motivated the convergent redesign. - formal-problem.md: abstract problem statement (external-reasoner handoff). - hybrid-design.md: Option B design; its §5 bounded-walk machinery is reused inside Option D's frontier-change recompute and merge-fold. - cmd/readcounter-bandsize: real-DB band/concurrency measurement (87% of trees band=0, max 439 on wide-collab objects; fork-span p95 ≤ 28) — the numbers Option D's cost model cites. Builds + tests green on this base.
Reactions move onto the same CORE machinery: immutable reaction-event sidecar rows (logged from the existing handleReactionsModify add/remove detection) + a refcounted unread-message map (the bandSet pattern) + a pastReact label for the O(1) zero-certificate. Honest limitation stated: the deduped count is count-distinct over targets, which doesn't fold into label arithmetic — it's an output-bounded cached scan instead. Retires the per-message mutable reaction-unread state, ClearUnreadReactions (over-clear bug), and the GetNewestUnreadReactionOrderId scans. Two semantics pins (S1 event definition content-based vs apply-time, S2 counted predicate) must be resolved against current behavior before Stage 4; it does not block Stages 1-3.
Option D Stage 1 (spec §5): ComputeBand walks the change DAG backward from local heads ∪ frontier in decreasing OrderId with two sticky colors, stopping at the read boundary. Returns the band candidates — unread change ids at or below the frontier cut; the indexed g>maxF range (repo-side) covers the rest (spec Theorem 1 decomposition). Pure function of (DAG, frontier-id-set): no AddSeq, no apply order — the basis of cross-device convergence. Pending (not-yet-local) heads are omitted from the cut: safe over-count. Tests: canonical a1∥b1, merge-closes, multi-head, pending heads, in-past insert, ancient-frontier walk bound, and a 3000-iteration randomized property test against a literal read* closure oracle.
… model
Option D Stage 1, spec §11 test 1 — the dimension no prior harness could
express: each device is a REAL storage-backed objecttree receiving the same
DAG in a DIFFERENT batch order (one AddRawChanges per batch), so AddSeq and
lexid OrderId strings genuinely differ per device.
Gates: (1) the canonical a1∥b1 case — the exact shape on which the
(OrderId,AddSeq) watermark prototype permanently diverged (0 vs 1) — both
devices now report band {a1}; (2) branches + merge + late in-past insert +
multi-head + pending frontiers across three delivery schedules, checked
against a literal read* closure oracle; (3) randomized delivery partitions
(12 device-pairs x 6 frontiers, fixed seed). Also pins the foundation:
OrderId comparison signs converge across devices while the strings differ.
Option D Stage 1 wiring, default off (bool path stays authoritative): - source.ReadCoreSnapshotProvider (off the Store interface; no mock churn): sourceimpl exposes seen heads + tree heads + change-meta resolution to a callback UNDER THE OBJECT-TREE LOCK, mirroring the seen-heads KV subscription's locking (tree storage reads share a parser; the prototype's unlocked-backfill race is designed out). - repository.CountCoreUnread: tail (indexed _o.id > maxF) + band candidates (In-filter), counted = peer + counter filter, no read flags consulted; explicit own-exclusion (the bool path gets it implicitly via insert-read). - chatobject: computeReadCoreCount (snapshot -> ComputeBand -> repo count vs bool count) + shadowReadCoreCount logging divergences, called from markReadMessages behind readCoreShadowEnabled=false. Tests: repo tail/band/mention/own/no-frontier; shadow disabled no-op, non-provider degrade, and agree+diverge on the canonical a1∥b1 shape (the divergence case is exactly the apply-order-dependent mis-flag class the shadow exists to surface).
…ntenance Option D Stage 1, the cached runtime flows (spec §5): the DAG walk now runs ONLY when the frontier changes; between frontier changes the band is maintained incrementally and queries reuse the cache. - readCoreManager: per-counter cached state (maxF, frontier hash, band set), persisted device-locally in crdt.db (<objectId>readcore, one doc per counter). Inert until the first walk: no collection created, hooks are cheap no-ops — zero cost while the shadow flag is off. - Theorem-3 rule wired into ChatHandler.BeforeCreate/BeforeDelete: a newly attached change can never be an ancestor of an already-resolved frontier head (parent-first attachment), so an arriving counted message at/below the cut joins the band with NO ancestry check; deletes drop it. Own messages skipped; mention band additionally gated on hasMention. - computeReadCoreCount: cache hit (same frontier, no pending heads) -> no walk; miss -> walk inside the tree-locked snapshot, then refresh + persist strictly OUTSIDE the tree lock. Pending heads always force a re-walk (they can resolve at any moment and move the cut). Persisted docs are NOT trusted as live state across restarts in the shadow stage (in-past inserts could have arrived while down) — first in-process use re-walks and logs a staleness signal; trusting cold-start state needs the Stage-2 apply-cursor. Tests: Theorem-3 rule matrix (below-cut/tail/own/mention/no-cut/invalid/ delete); cachedCut contract (order-insensitive frontier identity, pending forces walk); persistence round-trip + trust policy; the incremental==fresh- walk equality gate; and the end-to-end cache test observing walk-skips via resolve-call counting (walk -> hit -> incremental arrival without walk -> frontier change re-walks).
Two product decisions, recorded in the spec and applied to the CORE: D4 — one frontier, counters are filters: reading a message reads its attachments (mention, reactions). The mention counter shares THE message frontier; mention-unread = unread AND hasMention at query time, so 'message read but its mention unread' is unrepresentable. readCoreManager collapses to a single cached state serving both counters (one walk, one band, one cache); the independent mention diff manager survives only as the bool path's shadow oracle until cutover, and Stage 4's reaction frontier becomes the same frontier. The shadow soak doubles as the measurement of how far the two legacy frontiers drift in practice. D5 — MarkMessagesAsUnread deprecated (unused by clients), removed at cutover: the frontier is now MONOTONE. This deletes every regression flow, regression event, and regression cache-invalidation from the design — and with them all three known bool-vs-CORE soak-divergence classes the legacy flow produced (own-messages-flipped-unread, the g-prefix frontier swallow, and the reading.go mention/messages diff-manager hardcode bug). New gate: mention counter snapshots the MESSAGE frontier and reuses the shared cache without a second walk.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Context
The existing chat read-counter on
developuses the old DiffManager DAG-ancestor walk (changediffer.goRemoveBefore/dfsPrev) — exact and cross-device convergent, but O(tree) on every cold start (~18.6s on large trees). A watermark replacement (PR #3154) was designed for speed but introduced a permanent cross-device count divergence for late-arriving concurrent messages (AddSeq is device-local for concurrent changes — non-convergent by construction). That PR never merged.This branch introduces Option D — causal-ordinal CORE: a convergent, O(1)-query read model using the causal structure of the any-sync objecttree directly, with no per-message read flags. Since
developstill runs the old DiffManager, Option D introduces zero user-visible semantic change in Stage 1 — it runs as a flag-gated shadow (readCoreShadowEnabled = false) alongside the existing path.Design spec:
docs/superpowers/specs/2026-06-10-read-counter-option-d-causal-ordinals.mdKey design decisions recorded in spec
MarkMessagesAsUnreaddeprecated (unused by clients), removed at cutover. Frontier is monotone — no regression flows, no regression cache-invalidation. Eliminates all three known bool-vs-CORE soak-divergence classes.What's in this PR (Stage 1 — CORE, no labels)
chatmodel.ComputeBand— the core DAG walk: decreasing-OrderId two-color traversal, pure function of (DAG, frontier-id-set), no AddSeq anywhere. Frontier seeds READ, local heads seed UNREAD, stops at the read boundary, emits band candidates. Verified by a 3,000-iteration randomized property test against a literalread*closure oracle (deliberately different algorithm).Cross-device convergence gate — the test the watermark would fail: per-device real storage-backed objecttrees via
objecttree.NewMockChangeCreator+BuildTestableTree, oneAddRawChangesper delivery batch so AddSeq and lexid strings genuinely differ per device. The canonicala1∥b1shape (the permanent 0-vs-1 divergence case) now gates at 1=1. Randomized delivery partitions over 12 pairs × 6 frontiers.Flag-gated shadow wiring (
readCoreShadowEnabled = false):source.ReadCoreSnapshotProvider— type-assert, kept off theStoreinterface (no mock churn). Snapshot delivered under the object-tree lock.repository.CountCoreUnread— tail (indexed_o.id > maxF) + band (In-filter); counted = peer + counter filter; own-exclusion explicit.chatobject.shadowReadCoreCountinmarkReadMessages— logs divergences, non-fatal.Frontier cache + Theorem-3 incremental maintenance (
readCoreManager):ChatHandler.BeforeCreate/BeforeDelete: a newly attached change can never be an ancestor of a resolved frontier head (parent-first attachment), so an arriving message at/below the cut joins the band with no ancestry check.<objectId>readcore). Inert until first walk — zero cost while flag is off.Soak rule (once shadow is enabled)
CORE > bool→ flag residue (missedonRemoveevent etc.); CORE is correct.CORE < bool→ real alarm (no benign class remains after D5).Not in this PR (staged rollout)
readlabelssidecar +pastMsg/pastMentionfold at apply time +PreviousIdsplumbing throughstorestate.ChangeSet+ gated async backfill + apply-cursor trustable cold start.MarkMessagesAsUnread+ its RPC chain deleted.Test plan
go test ./core/block/chats/chatmodel/—ComputeBand+ 3k-iter oracle property testgo test ./core/block/editor/chatobject/ -run TestReadCore— cross-device convergence gate (canonical + branches/merge/late-insert + randomized)go test ./core/block/chats/chatrepository/—CountCoreUnreadtail/band/mention/own/no-frontiergo test ./core/block/editor/chatobject/ -run TestComputeReadCoreCount— shadow disabled no-op, non-provider degrade, agree+diverge on canonical shape, cache+incremental (walk-skip via resolve-call counting), mention-is-filter-over-message-frontier (D4 gate)go test ./core/block/editor/chatobject/— full chatobject suite (no regressions)source,sourceimpl,chats,chatmodel,chatrepository,chatsubscription,chatobject