pmacs/docs/crdt-identity-undo-framing.md

# Identity-replace undo — a CRDT-version delta is not a text delta

**Status: revision 5 — APPROVED at revision 4 and IMPLEMENTED**
(PR #246, branch `crdt-identity-undo`). Revision 5 is a correction pass
answering implementation review; it changes the invariant's shape, not
its ruling.

Revision 5 answers three findings against the implementation:

1. **the predicate conflated an empty TEXT delta with a version
   delta.** It called every empty-range/zero-insertion edit
   `version_only` and then accepted `(History, empty, None)` through a
   wildcard arm — which contradicts this framing's own "the op must
   survive". The rule is now a full enumeration over three independent
   axes (§1a), and C5 asserts all four empty-delta quadrants rather
   than two;
2. **the public `Edit` doc was factually false**, saying forward
   `apply_edit` never produces the empty-delta shape while C2b proves
   all three forward empty forms do. The shape is now named an **empty
   text delta**, reachable on both paths, with `crdt_op` as the
   discriminator;
3. **R7's write-up overstated what the paired gate runs exclude** — see
   `docs/ci-red-signatures.md`; the pair excludes the source tree and
   nothing else.

Revision 4 answered 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:

> **An empty TEXT delta carrying a CRDT op is legitimate when the
> `Edit` came from `undo`/`redo`, and REQUIRED there. On the FORWARD
> path the same shape carrying an op is a bug, and stays asserted.**

That is a real narrowing, not a repeal, and it is what makes C5
testable at all.

### 1a. The three axes, enumerated

Revision 4 wrote this as one predicate with a default, and the
implementation inherited the gap: `(History, empty delta, None)` fell
through a wildcard and was accepted. The axes are independent — that is
the lane's whole claim — so the rule is a full enumeration:

| provenance | text delta | `crdt_op` | verdict |
|---|---|---|---|
| forward | empty | `None` | **valid** — a syntactic no-op |
| forward | empty | `Some` | **invalid** — the original bug |
| forward | real | `Some` | valid |
| forward | real | `None` | invalid |
| history | empty | `Some` | **valid** — a version-only edit |
| history | empty | `None` | **invalid** — the version advance is gone |
| history | real | `Some` | valid |
| history | real | `None` | invalid |

**An empty text delta is a SHAPE, not a verdict.** Both paths reach it.
`crdt_op` is what separates them, and each direction of that separation
is asserted.

**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.
- **Forward edits reach the empty-delta shape routinely** — each of
  the three syntactically empty `EditOp` forms produces exactly it, as
  C2b asserts. What is unreachable forward is the shape **carrying an
  op**: an empty form short-circuits to `(None, None)`, and a
  real-delta form is not empty. So forward "empty range and zero
  insertion" implies `crdt_op == None`, still — which is what lets the
  invariant keep its full strength there.
- 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 covers **all four** empty-text-delta quadrants of §1a | preserve the `GenOp` classification (`buffer.rs:3101`, where `op` is moved before it can be classified) as an operation class; extract the shape check to take `(class, &Edit)`; then **inject** all four: `(Forward, empty, None)` accepted, `(Forward, empty, Some)` rejected, `(History, empty, Some)` accepted, `(History, empty, None)` rejected | widen the forward rule → C5 fires; accept `(History, empty, None)` → C5 fires, and **revision 4's two-assertion C5 did not**. **The proptest alone catches neither**, because no generated input reaches either row — 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 names the **empty text delta** and says which path produces which `crdt_op` | the `Edit` doc (from `src/rope.rs:292`) gains the empty-delta shape **as reachable on BOTH paths** — `None` forward, `Some` from history — and the `crdt_op` field doc stops asserting that no-op edits have no op | leave the doc → it contradicts the code the lane just blessed. **An earlier version of this row said forward `apply_edit` never produces the shape; C2b proves all three forward empty forms do**, so the doc it produced was false and is corrected in revision 5 |
| 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.