diff --git a/docs/crdt-identity-undo-framing.md b/docs/crdt-identity-undo-framing.md new file mode 100644 index 0000000..0811fbd --- /dev/null +++ b/docs/crdt-identity-undo-framing.md @@ -0,0 +1,298 @@ +# Identity-replace undo — a CRDT-version delta is not a text delta + +**Status: revision 4 — AWAITING APPROVAL. Nothing implemented.** + +Revision 4 answers review of 3, which found one substantive gap: **C9 +guarded the census by file set and count, which a same-file substitution +walks straight through.** C9 now asserts the exact +`(file, impl target)` pairs, and its claim is scoped to in-tree +implementations. + +Revision 3 answered review of 2 by completing §4's census: it closes by +construction, and two of its results changed the framing's own claims. + +## 1. The decision, ANSWERED — and it is about PROVENANCE, not shape + +**A visible TEXT delta and a CRDT-VERSION delta are INDEPENDENT +dimensions of `Edit`.** An `Edit` may legitimately carry +`crdt_op = Some(_)` with `range.is_empty() && inserted_len == 0`. + +**Revision 2 stated that without qualification, and review 2 showed why +that is too loose:** an `Edit` carries no provenance marker, so if the +shape alone were legitimate the invariant would have nothing left to +assert. The precise answer: + +> **The version-only shape is legitimate when the `Edit` came from +> `undo`/`redo`. On the FORWARD path it remains a bug, and stays +> asserted.** + +That is a real narrowing, not a repeal, and it is what makes C5 +testable at all. + +**Why this answer:** + +- The invariant it contradicts was written for `is_no_op_edit` + (`src/buffer.rs:1836`), a **pre-check on the `EditOp`** reached only + from `run_rope_edit_and_broadcast` (`:1256`). **`undo_crdt_mode` and + `redo_crdt_mode` never reach it** — they diff two ropes via + `derive_replacement_edit` (`:1440`, `:1525`) and attach the op + `crdt.undo()` produced (`:1454`), so identical ropes yield an empty + range describing a real operation. +- **On the forward path the shape is unreachable**, which is what lets + the invariant keep its full strength there. A forward empty form + short-circuits to `(None, None)`; a forward non-empty form has a + non-empty range or `inserted_len > 0`. So forward "empty range and + zero insertion" implies `crdt_op == None`, still. +- The op must survive. Dropping it would lose a version advance the + replicas need — which is what C3 now actually tests, and revision 1's + C3 did not. +- **The codebase already assumes this, in two places written for other + reasons.** `FoldStore::translate` (`src/fold.rs:211`–`:213`) and + `BufferStyleSpanTranslator::on_edit` (`src/overlay.rs:261`–`:263`) + both return early on `old_len == 0 && new_len == 0`, and both say so + in a comment — *"Buffers broadcast no-op edits; nothing moved."* This + lane is not introducing a doctrine; it is naming one that consumers + were already written against. +- The public contract has room for it. `src/rope.rs:301`–`:303` + enumerates pure insert, pure delete and replace, and **has no fourth + case**; the `crdt_op` field doc (`src/rope.rs:316`) goes further and + asserts the conflation outright ("`None` … for no-op edits in CRDT + mode"). Both are updated by this lane. + +**The empty range's LOCATION is settled by §4's census, not deferred.** +It stays at the buffer end. No consumer is harmed there, and for the +one consumer whose cost depends on it, the buffer end is the *cheapest* +choice — see §4. + +## 2. What is already known — and precisely how well + +`src/buffer.rs:3044` carries a deterministic fixture, +`crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op`, +`#[ignore]`d at `:3042` and documented from `:3005`. It reduces this +exact case: replacing bytes with **identical bytes** is a textual no-op +but a real CRDT delete-plus-insert, so undoing it advances the CRDT +version while leaving text unchanged. + +**Its evidence is narrower than revision 1 claimed, and narrower in one +more place than revision 2 admitted:** + +| claim | how it is established | strength | +|---|---|---| +| content stays correct | **asserted** in the fixture — rope and CRDT projection agree | direct | +| the op reaches broadcast consumers | **by INSPECTION of the call sites** | reasoning, not execution | +| the cursor does not jump | **by INSPECTION** — `EditorCore::undo` only clamps to length | reasoning, not execution | + +**The cursor row was marked "direct" in revision 2. It is not.** The +fixture body (`buffer.rs:3044`–`:3093`) contains **no reference to +`EditorCore` and none to a cursor**; it exercises `Buffer` alone. The +cursor claim is inspection of a different function than the one the +fixture runs. + +**Nothing here replays the op on a remote replica or witnesses +convergence.** Revision 1 said "replicas stay converged" as though it +were established. It is not. **That is exactly what C3 must newly +establish**, and it is the main new evidence this lane produces. + +The CI red that prompted the lane is a randomly sampled recurrence of +this fixture, not a new defect. + +## 3. Terminology, because revision 1's contradicted itself + +**An identity replace IS a forward textual no-op**, and it *does* +produce an operation. So "forward textual no-ops produce no operation" +is false, and revision 1 asserted it while §2 said the opposite. + +The correct statement names a **syntactic** category: + +> The three **syntactically empty `EditOp` forms** — `Insert` with +> empty bytes, `Delete` with an empty range, and `Replace` with both +> empty — produce no CRDT operation. + +That is what `is_no_op_edit` tests, and it stays true. + +## 4. The consumer census — COMPLETE + +Revision 2 listed `broadcast_on_edit` as a row reading *"every attached +view — not enumerated, owes."* **That is a dispatcher, not a consumer, +and review 2 was right that it cannot stand.** Here is the enumeration. + +Both `undo_crdt_mode` (`buffer.rs:1456`) and `redo_crdt_mode` +(`:1537`) do broadcast, so this path is real. + +### 4a. How the census closes + +Three measurements bound it, so it is complete by construction rather +than by search effort — **for this tree**; see §4d on why no in-tree +measurement can reach further: + +1. **The `View` trait's `on_edit` default is `Ok(())`** + (`src/view.rs:450`–`:452`). Every impl that does not override it is + **structurally inert** — it never reads the range. +2. **Exactly four non-test impls override `on_edit`**: `ParseView` + (`syntax.rs:1637`), `TextView` (`text_view.rs:521`), + `FoldStoreTranslator` (`fold.rs:274`), `BufferStyleSpanTranslator` + (`overlay.rs:248`). The other twelve inherit the default. +3. **Exactly four production `Buffer::attach_view` call sites exist** + — `fold.rs:341`, `lua_bindings/mod.rs:3963`, `:4008`, `:8137`. + Measured over the 50 occurrences of `attach_view` outside its own + definition: **38 sit inside `#[cfg(test)]`**, and of the 12 + remaining, **8 are doc comments or a different API** (the Lua + `pmacs.diag._attach_view` name, and `SyntaxRegistry::attach_view` at + `lua/mod.rs:8138`, which registers a handle rather than a buffer + view). + +### 4b. Broadcast consumers, classified + +| attached view | site | reads range? | verdict | +|---|---|---|---| +| `FoldStoreTranslator` | `fold.rs:341` | via `FoldStore::translate` | **INERT** — explicit `old_len == 0 && new_len == 0` early return at `fold.rs:211`–`:213` | +| `BufferStyleSpanTranslator` | `lua/mod.rs:4008` | yes | **INERT** — same explicit early return, `overlay.rs:261`–`:263` | +| `ParseView` | `lua/mod.rs:8137` | yes | **PERMITTED, justified below** | +| `LuaInterceptView` | `lua/mod.rs:3963` | — | **INERT** — overrides `intercept_edit` only (`lua/mod.rs:2132`); inherits the `Ok(())` default | + +**`ParseView` is the one permitted effect.** At 0→0 its splice +(`syntax.rs:1656`) is `source.splice(n..n, [])` — the source mirror is +**unchanged** — and it pushes one `InputEdit` with +`start_byte == old_end_byte == new_end_byte` and all three `Point`s +equal (`:1661`–`:1668`). **Why that is acceptable:** a degenerate +`InputEdit` describes no change, so the incremental parse it feeds must +produce an identical tree. **C4 asserts that rather than assuming it**, +and also asserts the pending queue drains, since an effect that +accumulates per undo would not be acceptable. + +### 4c. Direct (non-broadcast) consumers + +**Revision 2 filed `TextView` under broadcast. It is not attached to +any buffer** — it lives on the window (`win.text_view`) and +`EditorCore::undo` calls it directly at `editor_core.rs:2846`. + +| consumer | reads range? | verdict | +|---|---|---| +| `Buffer::adjust_marks_for_edit` (def. `buffer.rs:1609`; called `:1442` undo, `:1527` redo) | yes | **INERT, arithmetically** — with `start == end` and `inserted_len == 0`, every branch is identity: `pos < start` → `pos`; `pos > end` → `pos - 0 + 0`; `pos == start` → `start` under both gravities (`:1617`–`:1629`) | +| `EditorCore::undo` → `TextView::on_edit` (`editor_core.rs:2846`, body `text_view.rs:521`) | yes | **PERMITTED** — `rebuild_lines_from(buf, line_at_offset(range.start))`. Text is unchanged, so the rebuild is **output-identical**; the cost is the tail of the buffer from `range.start`. **The buffer-end location makes this the CHEAPEST possible rebuild** — moving the range to the edit site would rebuild strictly more | +| `search_invalidate_for_edit` → `mark_stale` (`editor_core.rs:1974`) | **no** | **PERMITTED** — unconditional and range-independent. Search matches are marked stale on an edit that changed no text. Acceptable (correctness is preserved; a re-search is redundant, not wrong), and **moving the range would not change it** | +| `search_invalidate_for_edit` → `translate_search_origin` (`editor_core.rs:1984`) | yes | **INERT, arithmetically** — with `start == end` and `inserted_len == 0`: `pos < start` → `pos`; `pos > end` → `pos - 0 + 0`; else `start + 0`, reachable only at `pos == start` (`:1994`–`:2000`) | + +### 4d. The disposition + +**Five inert, three permitted, none harmed. The range does not move,** +and that conclusion now rests on measurement rather than on a deferral. + +| | inert | permitted | +|---|---|---| +| broadcast (§4b) | `FoldStoreTranslator`, `BufferStyleSpanTranslator`, `LuaInterceptView` | `ParseView` | +| direct (§4c) | `adjust_marks_for_edit`, `translate_search_origin` | `TextView`, `mark_stale` | + +*(Revision 3 said four and three. Miscount, corrected.)* + +The two permitted effects with a cost — `TextView`'s rebuild and +`mark_stale` — are both **strictly cheaper or equal at the buffer end** +than at the edit site, so the location the fixture called arbitrary is +not merely harmless but weakly preferable. + +**This census is a point-in-time measurement of THIS TREE**, valid at +the commit the lane branches from. Both `View` (`src/view.rs:419`) and +`Buffer::attach_view` (`src/buffer.rs:674`) are **public**, so a +downstream crate may implement `on_edit` and attach it, and no in-tree +measurement can enumerate that. The census, and C9 with it, are scoped +to in-tree implementations; the public contract §5's C7 updates is what +speaks to anyone outside. Revision 3 claimed C4 would guard it against a new +override or attach site; **it cannot — executing three consumers says +nothing about a fourth, and that claim is withdrawn.** C9 is the guard +that actually holds, and it holds the one condition that matters: if +the set of `on_edit` overrides is unchanged, then every attach site, +new or old, attaches a view that is either the inert trait default or +one of the four already classified. + +## 5. Acceptance + +| # | contract | witness | mutation | +|---|---|---|---| +| C1 | the fixture runs, and is not silently re-ignored | un-ignore it; **plus a structural assertion** that no `#[ignore]` attribute precedes the fixture's `fn` (via `include_str!` on the file), **plus** the run's `1 passed; 0 ignored` line recorded as gate evidence | restore `#[ignore]` → the structural assertion fires **and** the recorded line reads `0 passed; 1 ignored`. Without one of these, re-ignoring is a green suite | +| C2a | `is_no_op_edit` classifies all three **syntactically empty forms** as no-ops | assert `is_no_op_edit` **directly** for `Insert{bytes:[]}`, `Delete{range:empty}`, `Replace{range:empty,bytes:[]}` | flip **any one** arm (`buffer.rs:1838`–`:1840`) → C2a fires. Nothing sits between the assertion and the classifier, so this mutant **cannot be masked** | +| C2b | end-to-end, each empty form still yields `crdt_op == None` | apply each form through `apply_edit` on a CRDT buffer | **compound mutant, and it must be**: flip the arm **and delete that variant's defensive early return** — `buffer.rs:1177`–`:1182` (Insert) or `:1192`–`:1194` (Delete). See below | +| C3 | an empty-text history op **replays convergently on a REMOTE replica**, **for both `undo` and `redo`** | seed replica B with the **forward** ops, apply the history op to B, assert **(a)** identical materialized text **and (b)** identical CRDT version/frontier; then apply a **causally dependent** op and assert both still agree | **drop the history op before replay** → text still matches, so only the version/frontier assertion catches it | +| C4a | the history edit is **broadcast at all**, for both `undo` and `redo` | attach a counting view (the `RecorderView` shape, `buffer.rs:2218`) and assert **exactly one** `on_edit` per history op | **delete `self.broadcast_on_edit(&inverse_edit)?`** at `buffer.rs:1456` (undo) or `:1537` (redo) → the count is 0 → C4a fires | +| C4b | the classified consumers are unchanged by the real history edit | attach `FoldStoreTranslator`, `BufferStyleSpanTranslator` and `ParseView`; run the identity-replace op; assert fold store unchanged, span vector unchanged, **parse tree identical**, and `pending_edit_count()` returns to 0 after the drain (`syntax.rs:712`, `:737`) | see the note below — **C4b claims no guard mutation**, and C4a is what makes it non-vacuous | +| C4c | the style-span guard's own contract, pinned where it can fire | call `BufferStyleSpanTranslator::on_edit` with a **synthetic INTERIOR 0→0 `Edit`** whose position falls strictly inside an existing span, and assert the span vector is **byte-identical** — not merely equal in coverage | delete `overlay.rs:261`–`:263` → the span splits into two adjacent fragments and the vector differs → C4c fires | +| C5 | the invariant is keyed on **provenance**, and still rejects a version-only `Edit` on the FORWARD path | preserve the `GenOp` classification (`buffer.rs:3101`, where `op` is currently moved before it can be classified) as an operation class; extract the shape check to take `(class, &Edit)`; then **inject** `(Forward, version-only Edit)` and assert it is rejected, and `(History, version-only Edit)` and assert it is accepted | widen the `Forward` branch to permit the version-only shape → C5 fires. **The proptest alone cannot catch this**, because no forward input produces that shape — which is why C5 is a directed injection, not a property | +| C6 | the executed history-case set **is** `{Undo, Redo}` | after the parameterized loop, assert the collected set of cases actually run equals the literal `{Undo, Redo}`; a `match` over the case enum keeps a future variant from being added silently | drop `Redo` from the case list → the **set assertion** fires. Without it the suite simply runs one case and stays green, which is why revision 3's C6 was a zero-execution witness | +| C7 | the public contract admits the fourth shape | `src/rope.rs:301`–`:303` (in the `Edit` doc from `:292`) gains the empty-range/zero-inserted case, and the `crdt_op` field doc (`:316`) stops asserting that no-op edits have no op | leave the doc → it contradicts the code the lane just blessed | +| C8 | **the fixture's own doc comment is corrected**, not just its attribute | rewrite `buffer.rs:3005`–`:3040`: convergence is **established by C3**, not "verified" (`:3023`–`:3026`); the buffer-end range is **ruled and weakly preferable** per §4, not "genuinely arbitrary" (`:3034`–`:3036`); "**The open question**" (`:3030`) becomes the ruling; and the `#[ignore]` reason string (`:3042`–`:3043`) goes with the attribute | leave the comment → the repository's most-read record of this defect still says the decision is open and that convergence was already checked, contradicting §1, §2 and C3 | +| C9 | §4's census stays closed **for in-tree implementations** | walk `CARGO_MANIFEST_DIR/src` and assert the set of **`(file, impl target)` pairs** carrying a non-`#[cfg(test)]` `fn on_edit` override is exactly `{(syntax.rs, ParseView), (text_view.rs, TextView), (fold.rs, FoldStoreTranslator), (overlay.rs, BufferStyleSpanTranslator)}` — pairs, not file set and count, and by name rather than line number | **replace `ParseView`'s override with an unclassified type in the SAME file** → file set and count are both unchanged, and only the pair set catches it. Adding a fifth override anywhere under `src/` fires it too, naming the file and the type | + +**Why C4 was rebuilt.** Revision 3's C4 claimed that deleting the fold +or style guard would make an assertion fire. **Both mutants survive**, +and the arithmetic says why: the history edit sits at the buffer end, +so with `old_start == old_end == len` and `old_len == new_len == 0`, +`BufferStyleSpanTranslator` emits a left fragment `[s, min(e, len))` +for every span within the buffer and no right fragment — the vector is +unchanged with or without the guard (`overlay.rs:269`–`:285`). The fold +store's remaining arithmetic is identity for the same reason. **At this +location the fold guard is an optimization, not a behaviour +discriminator, and no mutation is claimed for it.** What discriminates +is whether the broadcast happens at all (C4a) and whether the style +guard holds where the fragmenting is reachable (C4c). + +*(A span of zero width at exactly `len` would be dropped without the +guard and kept with it. That is not used as a witness: whether such a +span is constructible is unestablished, and a witness resting on a +degenerate value is a worse instrument than the interior injection.)* + +**C2b's mutant is compound because two of three variants mask it, and +the asymmetry is measured.** `apply_to_crdt_then_normalize_bytes` +returns `(None, None)` early for an empty `Insert` (`:1177`–`:1182`) +and an empty `Delete` (`:1192`–`:1194`), so flipping those arms alone +still yields `crdt_op == None` and the simple mutant survives. The +empty `Replace` has **no** early return — `:1208` skips the delete, +`:1211` skips the insert, and control falls through to the +unconditional `Some(crdt_op)` at `:1231`–`:1236` — so there, and only +there, the simple mutant dies. C2a exists so this asymmetry cannot hide +a classifier regression. + +**C3's mutation is the point of C3.** Revision 1's version asserted +text equality alone, and an identity-replace history op leaves text +unchanged — so **dropping the op passed it**. Version/frontier equality +is what discriminates; the causally dependent op is corroboration on +top. + +**C5 is the second half of §1's answer.** §1 makes the shape legitimate +*for history ops*; without a provenance-keyed check there is no +remaining assertion for the forward path, and the invariant would have +been repealed rather than narrowed. + +**C1, C6 and C9 exist because a green suite is not evidence that a +suite RAN.** Re-ignoring a fixture, dropping a parameter, and adding an +unclassified consumer are all silent under ordinary assertions. Each +gets a witness that fails on absence rather than reporting it. + +## 6. Coherence impact (`COHERENCE.md` §20) + +Under the resolution the census confirms — invariant narrowed to +provenance, behaviour unchanged: + +- **Journey steps touched: NONE.** No product behaviour changes; the + work is a test contract, a census, and public documentation. +- **Interaction islands: none added.** +- **Config registry: no entry.** +- **Background work: none started.** + +Revision 2 made this section conditional on a census that had not run. +**It has now run, and no consumer is harmed, so the section is +unconditional.** + +## 7. What this does NOT do + +- **It does not commit the proptest regression seed.** That duplicates + a deterministic fixture and would make a disputed assertion fail + permanently rather than occasionally. +- **It does not re-verify content correctness**, which §2 records as + directly asserted. It *does* newly establish remote convergence, + which §2 records as only inspected. +- **It does not move the empty range**, and after §4 that is a measured + result rather than a deferral. +- **It does not audit `intercept_edit`**, a different stage with a + different contract. The census covers `on_edit` and the direct + consumers of the history `Edit`. +- **It does not reorder the roadmap.** GUI arc 1b remains the next + product lane.