neuwirth
/
pmacs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

fix(crdt): enumerate the invariant over three axes, not two 

Review found the predicate conflating the two things this lane exists to
separate. It called every empty-range/zero-insertion edit `version_only`
and then accepted `(History, empty, None)` through a wildcard arm ---
which contradicts the lane's own ruling that the op must survive, and
contradicts the public contract's "carries Some, and must".

The rule is now a full enumeration over provenance x text delta x
crdt_op. An EMPTY TEXT DELTA is a shape, not a verdict: both paths reach
it, and `crdt_op` is what separates them.

  forward + empty + None   valid, a syntactic no-op
  forward + empty + Some   invalid, the original bug
  history + empty + Some   valid, a version-only edit
  history + empty + None   invalid, the version advance is gone

C5 asserts all four rather than two. Both new quadrants were
mutation-checked and both fire; neither is caught by the proptest,
because no generated input reaches either --- which is the same reason
C5 was a directed injection to begin with.

The public `Edit` doc was also factually false. It said forward
`apply_edit` never produces the empty-delta shape while C2b proves all
three forward empty forms do. It now names the shape and says which path
yields which `crdt_op`.
This commit is contained in:
Levi Neuwirth 2026-08-30 19:19:35 +02:00
parent c597f9c3e4
commit b3c90a7949
No known key found for this signature in database
2 changed files with 114 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
src/buffer.rs
View File

@ -2986,28 +2986,45 @@ mod tests {
} }
} }
/// The `crdt_op` shape invariant, as a function of provenance. /// The `crdt_op` shape invariant, over three independent axes.
/// ///
/// Four rules, checked in order: /// The axes are **provenance** (forward vs. history), the
/// **text delta** (empty vs. real), and whether a **CRDT op** is
/// carried. They are independent, which is the whole point of
/// this lane, so the rule is a full enumeration rather than a
/// default with exceptions:
/// ///
/// 1. a present `crdt_op` carries the buffer's peer id and /// | provenance | text delta | `crdt_op` | verdict |
/// non-empty wire bytes; /// |---|---|---|---|
/// 2. an edit that changed text must carry an op; /// | forward | empty | `None` | **valid** — a syntactic no-op |
/// 3. a **forward** version-only edit (empty range, zero /// | forward | empty | `Some` | **invalid** |
/// insertion) must NOT carry one — the three syntactically /// | forward | real | `Some` | **valid** |
/// empty `EditOp` forms short-circuit at `is_no_op_edit` /// | forward | real | `None` | **invalid** |
/// before the CRDT path exists; /// | history | empty | `Some` | **valid** — a version-only edit |
/// 4. a **history** version-only edit MAY carry one. Undo and /// | history | empty | `None` | **invalid** |
/// redo diff two ropes; an identity replace makes those /// | history | real | `Some` | **valid** |
/// ropes equal, so the empty range describes a real version /// | history | real | `None` | **invalid** |
/// advance rather than the absence of one. ///
/// An **empty text delta** — `range.is_empty() && inserted_len
/// == 0` — is a SHAPE, and forward edits reach it routinely:
/// each of the three syntactically empty `EditOp` forms produces
/// exactly this shape. What separates the two empty-delta cases
/// is the op. Forward, `is_no_op_edit` short-circuits before the
/// CRDT path exists, so there is nothing to carry. History
/// diffs two ropes; an identity replace makes them equal, so the
/// op IS the content of the edit and **dropping it loses the
/// version advance**. That is why the history row demands
/// `Some` rather than merely tolerating it.
///
/// A present op is separately required to carry the buffer's
/// peer id and non-empty wire bytes.
/// ///
/// Returns `Err(reason)` rather than asserting, so the same /// Returns `Err(reason)` rather than asserting, so the same
/// predicate serves the proptest (over generated sequences) and /// predicate serves the proptest (over generated sequences) and
/// a directed injection. The injection is not optional: rule 3 /// a directed injection. The injection is not optional: the
/// is **unreachable from any generated forward input**, because /// `(forward, empty, Some)` row is **unreachable from any
/// a forward empty form short-circuits and a forward non-empty /// generated forward input**, because a forward empty form
/// form has a non-empty range or a non-zero `inserted_len`. /// short-circuits and a forward real-delta form is not empty.
fn check_crdt_op_shape( fn check_crdt_op_shape(
class: OperationClass, class: OperationClass,
edit: &Edit, edit: &Edit,
@ -3024,22 +3041,25 @@ mod tests {
return Err("wire bytes must be non-empty".to_owned()); return Err("wire bytes must be non-empty".to_owned());
} }
} }
let version_only = edit.range.is_empty() && edit.inserted_len == 0; let empty_text_delta = edit.range.is_empty() && edit.inserted_len == 0;
if !version_only { match (class, empty_text_delta, edit.crdt_op.is_some()) {
if edit.crdt_op.is_none() { (OperationClass::Forward, true, false) => Ok(()),
return Err( (OperationClass::Forward, true, true) => Err(
"a text-changing CRDT-mode edit must have crdt_op = Some".to_owned() "a FORWARD edit with an empty text delta must have crdt_op = None: the \
); three syntactically empty EditOp forms short-circuit at is_no_op_edit"
} .to_owned(),
return Ok(()); ),
} (OperationClass::History, true, true) => Ok(()),
match class { (OperationClass::History, true, false) => Err(
OperationClass::Forward if edit.crdt_op.is_some() => { "a HISTORY edit with an empty text delta must have crdt_op = Some: the \
Err("a FORWARD version-only edit must have crdt_op = None (see \ op is the version advance, and without it the edit carries nothing"
is_no_op_edit)" .to_owned(),
.to_owned()) ),
} (_, false, true) => Ok(()),
_ => Ok(()), (_, false, false) => Err(
"an edit with a real text delta must have crdt_op = Some in CRDT mode"
.to_owned(),
),
} }
} }
@ -3283,34 +3303,53 @@ mod tests {
} }
} }
/// C5: the invariant is keyed on PROVENANCE, and still rejects a /// C5: the invariant is keyed on PROVENANCE, and covers all
/// version-only `Edit` on the forward path. /// four empty-text-delta quadrants.
/// ///
/// This must be a directed injection rather than a property. /// Two of these must be a directed injection rather than a
/// `check_crdt_op_shape`'s forward rule is **unreachable from /// property. `(forward, empty, Some)` is **unreachable from any
/// any generated forward input** — an empty form short-circuits /// generated forward input** — an empty form short-circuits
/// before the CRDT path, and a non-empty form has a non-empty /// before the CRDT path, and a real-delta form is not empty — so
/// range or a non-zero `inserted_len` — so the proptest alone /// the proptest alone cannot tell a narrowed rule from a deleted
/// cannot tell a narrowed rule from a deleted one. /// one. `(history, empty, None)` is equally unreachable, because
/// `undo_crdt_mode` and `redo_crdt_mode` always attach the op;
/// it is asserted so that a future change which stops attaching
/// it fails here rather than silently losing version advances.
#[test] #[test]
fn the_shape_invariant_rejects_a_version_only_edit_on_the_forward_path() { fn the_shape_invariant_covers_all_four_empty_text_delta_quadrants() {
let version_only = Edit { let with_op = |op: Option<Box<crate::rope::CrdtOp>>| Edit {
new_rope: crate::rope::Rope::from_bytes(b"hello"), new_rope: crate::rope::Rope::from_bytes(b"hello"),
range: Range::new(5, 5), range: Range::new(5, 5),
inserted_len: 0, inserted_len: 0,
crdt_op: Some(Box::new(crate::rope::CrdtOp { crdt_op: op,
};
let carrying = || {
Some(Box::new(crate::rope::CrdtOp {
peer_id: 1, peer_id: 1,
bytes: vec![0xAB], bytes: vec![0xAB],
})), }))
}; };
// Forward + empty delta + None: a syntactic no-op. Valid.
assert!( assert!(
check_crdt_op_shape(OperationClass::Forward, &version_only, 1).is_err(), check_crdt_op_shape(OperationClass::Forward, &with_op(None), 1).is_ok(),
"C5: a forward version-only edit carrying an op is still a bug" "C5: a forward syntactic no-op carries no op, and that is correct"
); );
// Forward + empty delta + Some: the original bug.
assert!( assert!(
check_crdt_op_shape(OperationClass::History, &version_only, 1).is_ok(), check_crdt_op_shape(OperationClass::Forward, &with_op(carrying()), 1).is_err(),
"C5: a forward edit with an empty text delta must not carry an op"
);
// History + empty delta + Some: a version-only edit. Valid.
assert!(
check_crdt_op_shape(OperationClass::History, &with_op(carrying()), 1).is_ok(),
"C5: the same shape from undo/redo is a legitimate version advance" "C5: the same shape from undo/redo is a legitimate version advance"
); );
// History + empty delta + None: the version advance is gone.
assert!(
check_crdt_op_shape(OperationClass::History, &with_op(None), 1).is_err(),
"C5: a history edit with an empty text delta and no op carries nothing at all"
);
} }
/// The two history operations every history witness must cover. /// The two history operations every history witness must cover.

42
src/rope.rs
View File

@ -301,17 +301,27 @@ impl<'a> Iterator for Chunks<'a> {
/// A pure insert has `range.start == range.end` and `inserted_len > 0`. /// A pure insert has `range.start == range.end` and `inserted_len > 0`.
/// A pure delete has `range.start < range.end` and `inserted_len == 0`. /// A pure delete has `range.start < range.end` and `inserted_len == 0`.
/// A replace has both nonzero. /// A replace has both nonzero.
/// A **version-only** edit has `range.start == range.end` and /// An **empty text delta** has `range.start == range.end` and
/// `inserted_len == 0` — no bytes changed at all. CRDT-mode `undo` and /// `inserted_len == 0` — no bytes changed at all.
/// `redo` produce this shape when the operation being inverted was ///
/// itself a textual no-op (replacing bytes with identical bytes), and /// That last shape is produced on BOTH paths, and `crdt_op` is what
/// it still carries a [`CrdtOp`]: a CRDT VERSION delta is a separate /// tells them apart:
/// dimension from a TEXT delta. Forward `apply_edit` never produces it, ///
/// because the three syntactically empty `EditOp` forms short-circuit /// * **forward** `apply_edit` reaches it whenever the `EditOp` is one of
/// before the CRDT path exists. Its `range` sits at the buffer end, /// the three syntactically empty forms (an empty insert, an
/// which is where `derive_replacement_edit` reports a no-difference /// empty-range delete, an empty-range/empty-bytes replace). Those
/// diff; see `docs/crdt-identity-undo-framing.md` for the consumer /// short-circuit before the CRDT path exists, so `crdt_op` is `None`
/// census that ruled that location harmless. /// — nothing happened;
/// * **CRDT-mode `undo`/`redo`** reach it when the operation being
/// inverted was itself a textual no-op (replacing bytes with
/// identical bytes). Here `crdt_op` is `Some`, and **must be**: a CRDT
/// VERSION delta is a separate dimension from a TEXT delta, and the
/// op is the whole content of such an edit.
///
/// The history case's `range` sits at the buffer end, which is where
/// `derive_replacement_edit` reports a no-difference diff; see
/// `docs/crdt-identity-undo-framing.md` for the consumer census that
/// ruled that location harmless.
#[derive(Clone, Debug)] #[derive(Clone, Debug)]
pub struct Edit { pub struct Edit {
/// The rope after the edit. `Send + Sync`; safe to hand to a worker. /// The rope after the edit. `Send + Sync`; safe to hand to a worker.
@ -328,10 +338,12 @@ pub struct Edit {
/// syntactically empty `EditOp` forms, which `is_no_op_edit` /// syntactically empty `EditOp` forms, which `is_no_op_edit`
/// short-circuits before the CRDT path runs. /// short-circuits before the CRDT path runs.
/// ///
/// A **version-only** edit is NOT one of those: an empty range with /// An empty text delta is therefore NOT by itself a `None` signal:
/// zero insertion coming out of `undo`/`redo` carries `Some`, and /// forward, it means the edit short-circuited and `crdt_op` is
/// must, or the version advance the replicas need is lost. See the /// `None`; from `undo`/`redo` it means an identity operation was
/// shape list on [`Edit`] above. /// inverted, and `crdt_op` is `Some` — and must be, or the version
/// advance the replicas need is lost. See the shape list on
/// [`Edit`] above.
/// ///
/// `Box` indirection: keeps Edit's None-case cost to 8 bytes /// `Box` indirection: keeps Edit's None-case cost to 8 bytes
/// (Box has a niche-optimized None) rather than the ~32 bytes /// (Box has a niche-optimized None) rather than the ~32 bytes