From aae5b3514a7b519d583a8badf5e391359855a05f Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Sun, 30 Aug 2026 14:07:31 +0200 Subject: [PATCH] docs: the dispatched red is known #157, not a new defect I recorded the dispatched run's proptest red as "a DETERMINISTIC red", "not like anything else in this registry --- a property violation with a concrete witness, not a load artefact", and proposed committing the proptest seed as the first step. All of that was wrong, and it was wrong for a plain reason: I recorded a finding without checking whether main already documented it. src/buffer.rs:3005 carries an #[ignore]d deterministic fixture, crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op, that reduces this exact case. The shrunken input is a randomly sampled recurrence of it: Replace(5, 1, " ") replaces the trailing space with itself, a textual no-op but a real CRDT delete-plus-insert, so Undo emits a version-advancing operation with no visible text change. Committing the seed was a second error. It duplicates a deterministic fixture that already exists and would only make a disputed assertion fail permanently instead of occasionally. The fixture already verified what I would have re-derived: content stays correct, replicas stay converged because the op IS broadcast and neither crdt_op consumer short-circuits on an empty range, and the cursor does not jump. The entry now frames the actual decision --- whether a visible text delta and a CRDT-version delta are independent dimensions of Edit --- and the evidence a lane owes: that forward textual no-ops still produce no operation, that any permitted empty-text undo operation carries valid bytes and preserves remote replay convergence, and an explicit disposition of derive_replacement_edit reporting the empty range at the buffer end rather than the edit site. The interruption is bounded and does not reorder the roadmap. GUI arc 1b remains the next product lane. Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai --- docs/active-work.md | 84 ++++++++++++++++++++++++++++----------------- 1 file changed, 53 insertions(+), 31 deletions(-) diff --git a/docs/active-work.md b/docs/active-work.md index d2f1ead..6c5aa66 100644 --- a/docs/active-work.md +++ b/docs/active-work.md @@ -301,44 +301,66 @@ waits for a signal that is not coming. - **THE FIRST DISPATCH IMMEDIATELY FOUND A RED ON `main`**, which is what this lane was built for. See the proptest entry below. -## CRDT undo proptest — a DETERMINISTIC red on `main` — NEEDS A LANE +## CRDT identity-replace undo — the proptest invariant may be MIS-SCOPED — NEEDS A LANE -**Found by the first `workflow_dispatch` run**, `33307137965`, job -`99247616970`, at `main` = `7b82e14`. Log preserved at -`/home/jeans/build/pmacs-ci-logs/`. +**CORRECTION.** An earlier version of this entry called the dispatched +run's red "a DETERMINISTIC red" and "not like anything else in this +registry — a property violation with a concrete witness, not a load +artefact", and proposed committing the proptest seed as the first +step. **All of that was wrong**, and it was wrong because I recorded a +finding without checking whether `main` already documented it. -- **Selector:** `--lib --features crdt - buffer::tests::proptests::rope_matches_crdt_projection_after_arbitrary_edits` -- **Assertion:** `src/buffer.rs:3120` — - `no-op edit must have crdt_op = None (Undo)` -- **`2172 passed; 1 failed`**, failing after 17 successes. +**It is a randomly sampled recurrence of known #157 behaviour.** +`src/buffer.rs:3005` carries an `#[ignore]`d deterministic fixture, +`crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op`, +which reduces this exact case and records its mechanism: -**THIS IS NOT LIKE THE OTHER ROWS IN THIS REGISTRY.** Every red this -session has been timing-dependent and green on rerun. This one is a -**proptest failure that SHRANK to a minimal input**, which means it is -a property violation with a concrete witness, not a load artefact: +1. the inserts produce `aaaaa `; +2. `Replace(5, 1, " ")` replaces the trailing space **with itself** — a + textual no-op but a real CRDT delete-plus-insert; +3. `Undo` therefore emits a **version-advancing CRDT operation with no + visible text change**, and `derive_replacement_edit` yields an empty + edit that still carries its `crdt_op`. -``` -ops = [ Insert(0, "aa"), Insert(2, "aaa "), Replace(5, 1, " "), Undo ] -``` +**Committing the seed is NOT the first step**, and proposing it was a +second error: it duplicates a deterministic fixture that already +exists, and its only effect would be to make a disputed assertion fail +permanently instead of occasionally. -proptest also emitted its regression seed: -`cc fbc94ffbf80519d277eb49aa7ee46c726e1adc3a319d44cf32509d122d6ab5be` +**What the fixture already verified**, so the lane does not redo it: +content stays correct (rope and CRDT projection agree), replicas stay +converged (**the op IS broadcast** — both `crdt_op` consumers read it +unconditionally and neither short-circuits on an empty range), and the +cursor does not jump. -- **It did NOT reproduce in one local `--features crdt` run**, which - proves nothing: proptest draws fresh cases each run and **no - `.proptest-regressions` file is committed** for `src/buffer.rs`, so - the failing case is not replayed automatically. -- **The reproduction path is therefore known and cheap**: drive the - shrunken `ops` sequence directly as a unit test, or commit the - regression seed so proptest replays it. -- **Committing that regression file may be the first thing the lane - does**, since without it this exact input is only reachable by luck. +**THE ACTUAL DECISION** is whether a **visible text delta** and a +**CRDT-version delta** are independent dimensions of `Edit`. The +proptest's invariant assumes they are the same dimension. It was +written for the FORWARD `apply_edit` short-circuit, which returns +before producing an op at all — and **CRDT-mode undo/redo never reach +that path**. -**Not investigated here.** This lane's scope was one workflow key, and -a CRDT/undo property violation is nowhere near it. Recorded with -everything needed to start: selector, assertion, minimal input, seed, -and the reason a local pass is not evidence. +**What the lane owes as evidence:** + +- **forward textual no-ops still produce NO operation** — whatever the + resolution, the short-circuit the invariant was actually written for + must keep holding; +- **any permitted empty-text undo operation carries valid bytes and + preserves remote replay convergence** — permitting the shape must not + become permitting a malformed op; +- **an explicit disposition of the arbitrary artifact**: + `derive_replacement_edit` reports the empty range at the **buffer + end** rather than at the edit site. The fixture calls this genuinely + arbitrary either way; the lane must say which it is choosing, not + leave it unexamined. + +**Un-ignoring that fixture is the first step of whichever resolution +wins**, as its own doc comment says. + +**Why it is worth a bounded interruption:** a mis-scoped property can +now randomly redden `main`, and the dispatched run proved it. **It does +NOT reorder the roadmap** — GUI arc 1b remains the next product lane +per `COHERENCE.md` §20's priority order. ### Superseded lane state, kept for the record