From 870209cca9775b9933f6acafd3401aa017e7ba78 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Fri, 24 Jul 2026 21:34:08 -0400 Subject: [PATCH] test(buffer): capture the CRDT undo no-op-with-op case MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Found during #155's sweep and recorded there as one line of prose with an uncommitted proptest seed. This turns it into something that cannot be lost and that states what is actually known. Reproduced on main @ e745068 with PROPTEST_CASES=2000 against rope_matches_crdt_projection_after_arbitrary_edits, then reduced by hand to five lines: replacing a byte range with IDENTICAL bytes is a textual no-op but a real CRDT operation, so undoing it advances the CRDT version while leaving the materialized text unchanged. `undo_crdt_mode` derives an empty replacement edit and still attaches the op `crdt.undo()` produced, which trips the proptest's "a no-op edit must have crdt_op = None" invariant. The test is `#[ignore]`d rather than asserted-as-correct or left as a seed, because the resolution is a judgement call I should not make silently: - the raw proptest seed is NOT committed, since it would fail the suite on every run for a case whose correct outcome is undecided; - the deterministic reduction reproduces without any seed, so nothing is lost by leaving the seed out. What the doc comment records, so the next reader need not redo it: content stays correct (rope and CRDT projection agree either side); both `crdt_op` consumers read the field unconditionally and do not short-circuit on an empty range, so replicas still converge; and `EditorCore::undo` never seeks `edit.range.start`, so no cursor jumps. The open question is whether the invariant is simply mis-scoped — it was written for the forward `apply_edit` short-circuit, which returns before producing an op, and CRDT-mode undo/redo never reach that path. One artifact is arbitrary either way: `derive_replacement_edit` reports the empty range at the buffer END rather than at the edit site. Co-Authored-By: Claude Opus 5 (1M context) --- src/buffer.rs | 82 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 82 insertions(+) diff --git a/src/buffer.rs b/src/buffer.rs index 304918b..7f048d5 100644 --- a/src/buffer.rs +++ b/src/buffer.rs @@ -2790,6 +2790,88 @@ mod tests { } } + /// Deterministic reduction of a `rope_matches_crdt_projection_ + /// after_arbitrary_edits` failure found by raising the case + /// count (`PROPTEST_CASES=2000`) on `main` @ `e745068`. + /// + /// **What happens.** Replacing a byte range with *identical* + /// bytes is a textual no-op but a real CRDT operation (a delete + /// plus an insert). Undoing it therefore advances the CRDT + /// version while leaving the materialized text unchanged, so + /// `undo_crdt_mode` derives an EMPTY replacement edit — and + /// still attaches the `crdt_op` that `crdt.undo()` produced. + /// That trips the proptest's `crdt_op` shape invariant, "a + /// no-op edit must have `crdt_op = None`". + /// + /// **What was verified about the consequences**, so the next + /// reader does not have to redo it: + /// + /// * content stays correct — rope and CRDT projection agree + /// before and after (asserted below); + /// * replicas stay converged — both `crdt_op` consumers + /// (`EditorCore::queue_daemon_origin_crdt_op` and the remote-op + /// path) read `edit.crdt_op` unconditionally and do **not** + /// short-circuit on an empty range, so the op is broadcast; + /// * the cursor does not jump — `EditorCore::undo` only clamps + /// to buffer length and never seeks `edit.range.start`. + /// + /// **The open question** is therefore whether the *invariant* is + /// simply mis-scoped rather than the behavior being wrong. It + /// was written for the FORWARD `apply_edit` short-circuit, which + /// returns before ever producing an op; CRDT-mode undo/redo + /// never reach that path. One artifact is genuinely arbitrary + /// either way: `derive_replacement_edit` reports the empty range + /// at the buffer END rather than at the edit site. + /// + /// Ignored, not deleted: it documents a real, reproducible + /// asymmetry that nothing else on `main` records, and un-ignoring + /// it is the first step of whichever resolution wins. + #[test] + #[ignore = "known pre-existing main behavior; see the doc comment \ + for the verified consequences and the open question"] + fn crdt_undo_of_an_identity_replace_reports_a_no_op_edit_carrying_an_op() { + let mut buffer = + Buffer::new_with_crdt(BufferId::next(), "*identity-undo*", 1).expect("crdt"); + buffer + .apply_edit(EditOp::Insert { + pos: 0, + bytes: b"hello", + }) + .expect("seed insert"); + + // Replace one byte with the SAME byte. + let forward = buffer + .apply_edit(EditOp::Replace { + range: Range::new(1, 2), + bytes: b"e", + }) + .expect("identity replace"); + assert_eq!(forward.range, Range::new(1, 2)); + assert_eq!(forward.inserted_len, 1); + + let undone = buffer.undo().expect("undo"); + assert!( + undone.range.is_empty() && undone.inserted_len == 0, + "the undo produced no textual change: {:?}/{}", + undone.range, + undone.inserted_len + ); + assert!( + undone.crdt_op.is_some(), + "…yet it carries a version-advancing CRDT op — the invariant \ + the proptest trips on" + ); + + // Content is unharmed in both projections. + let mut bytes = vec![0u8; buffer.len() as usize]; + buffer.snapshot_rope().slice(0, buffer.len(), &mut bytes); + assert_eq!(String::from_utf8(bytes).expect("utf8"), "hello"); + assert_eq!( + buffer.crdt_state().expect("crdt").materialize_string(), + "hello" + ); + } + proptest! { // Smaller proptest case count than the default (64) to keep // CI overhead modest; the per-op invariant check is the