From 2bea189c6743c3ad04a1f7448160498d4b357998 Mon Sep 17 00:00:00 2001 From: "Claude (adr9-steward)" Date: Fri, 9 Oct 2026 21:28:49 -0700 Subject: [PATCH] docs(adr): ADR 009 states correction as the Z-set difference target minus held (improvise-felo.4) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VdfEGXA7aJ6ftMsCc9PJze --- context/adr/009-incremental-evaluation.md | 27 +++++++++++++++-------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/context/adr/009-incremental-evaluation.md b/context/adr/009-incremental-evaluation.md index 4de8bf20..0687f53e 100644 --- a/context/adr/009-incremental-evaluation.md +++ b/context/adr/009-incremental-evaluation.md @@ -227,13 +227,21 @@ an **edge adapter**. So every edge has the same semantics: treats the hop as dropped. The downstream side then asks for a correction from its last stamp. -- **Correction is an engine operation.** The engine offers, per shape key, a - **correction** computed from a client's last stamp. Where the shared log still covers - that stamp, it is the net delta since then. Otherwise it is a replacing delta: the - current state for the client's window, with whatever the client held retracted. A - full refetch is the case with an empty basis. A correction is idempotent, resumable - by stamp, and written in the same lossless delta form as a notice, so a client, a - gateway or a worker applies it with the same code. +- **Correction is Z-set arithmetic.** A correction is `target − held`, where `target` + is the current state for the client's window and `held` is what the client holds. + Applying it with ordinary Z-set addition gives `held + (target − held) = target`, so + the group structure of `ZSet` provides it, with no separate machinery. The client + sends its last stamp: + - where the shared log covers that stamp, the host sends the sum of the logged deltas + since then; + - otherwise the host sends `target`, and the client, which knows `held`, applies + `target − held`; + - a full refetch is `target − ∅`. + + A correction is labelled with the publication range it covers, so it is applied only + at the stamp it starts from, which makes it idempotent and resumable. It uses the same + lossless delta form as a notice, so a client, a gateway or a worker applies it with the + same code. Aggregation stays on the model side (ADR 008), so the operators that aggregate run on the model side, which may itself span a hop. Which other edges cross a wire is a @@ -348,8 +356,9 @@ Step 8's required tests: - `[AddItem, SetCell]` publishes one notice, and no client asks for a correction; - a dropped notice is detected; - a reconnect after a host restart asks for a correction; -- a corrected state equals the state of a client that was never stale (a property - test over random edit sequences and losses); +- a corrected state equals the target, `held + (target − held) = target`, and + correcting a state that is already correct is the zero Z-set (property tests over + random edit sequences and losses); - a refused frame consumes no publication number; - a dropped hop triggers a correction.