docs: narrow R7's causal claim, and record U6's first reproduction
R7's eighth-occurrence write-up said the gate's ambient root, TMPDIR and cross-stage process state were "now the only place the difference can be". That is wrong. The paired runs exclude the SOURCE TREE and nothing else: scheduler load, kernel and socket timing, page cache pressure and whatever else the machine was doing also varied between them, and a BrokenPipe on a socket handshake is exactly what those can drive. The three remain the candidates worth varying one at a time --- because they are the ones this project can vary --- not an exhaustive causal set. U6 gained a second occurrence, and for the first time it REPRODUCED: both selectors, both fragments, two consecutive runs. Margins recorded per U11's lesson --- 1.343883ms against 1ms, and 1.182x against 1.10x. Its asymmetry runs the opposite way to R7's: both failures were out of gate, while the same command as `04-lib-crdt` was green in all four of this lane's gate runs. Whatever the two rows share, it is not a direction. Framing revision 5 and the lane block are updated to match, including the stale "AWAITING APPROVAL. Nothing implemented." header and the gate line that named a commit the branch had already moved past.
This commit is contained in:
parent
b3c90a7949
commit
099b5a7383
|
|
@ -303,19 +303,45 @@ waits for a signal that is not coming.
|
|||
|
||||
## CRDT identity-replace undo — LANE TAKEN, PR #246 OPEN
|
||||
|
||||
**Branch `crdt-identity-undo`, based on `aae5b35`; implemented at
|
||||
`db24ae3`.** Framing `docs/crdt-identity-undo-framing.md`, **APPROVED at
|
||||
revision 4** after four review rounds. Gate green **head-exact**, all 8
|
||||
stages, log `20260830T154827Z-2907414`; `HEAD` and
|
||||
`git status --porcelain` identical before and after.
|
||||
**Branch `crdt-identity-undo`, PR #246, based on `aae5b35`.** Framing
|
||||
`docs/crdt-identity-undo-framing.md`, **APPROVED at revision 4** after
|
||||
four review rounds, then **revision 5** as a correction pass answering
|
||||
implementation review. Gate green **head-exact at the current head**,
|
||||
all 8 stages; the `db24ae3` run recorded here earlier was head-exact for
|
||||
that commit only and the branch has moved since.
|
||||
|
||||
**The decision, ruled:** a visible TEXT delta and a CRDT-VERSION delta
|
||||
are **independent dimensions** of `Edit`. The invariant is narrowed to
|
||||
key on **provenance**, not shape — a forward version-only edit must
|
||||
still carry no op (and still cannot produce one, because the three
|
||||
syntactically empty `EditOp` forms short-circuit at `is_no_op_edit`); a
|
||||
history version-only edit may carry one, and must, or the version
|
||||
advance the replicas need is lost.
|
||||
are **independent dimensions** of `Edit`. The invariant is keyed on
|
||||
**provenance**, and enumerated over three axes rather than defaulted:
|
||||
an **empty text delta** is a shape both paths reach, and `crdt_op` is
|
||||
what separates them — `None` forward (the three syntactically empty
|
||||
`EditOp` forms short-circuit at `is_no_op_edit`), `Some` from
|
||||
`undo`/`redo`, **required** there, because the op is the whole content
|
||||
of such an edit.
|
||||
|
||||
**Revision 5 fixed three things review caught in the implementation:**
|
||||
|
||||
- the predicate **conflated the empty text delta with a version delta**,
|
||||
calling every empty-range/zero-insertion edit `version_only` and then
|
||||
accepting `(History, empty, None)` through a wildcard — contradicting
|
||||
the lane's own "the op must survive". It is now a full enumeration,
|
||||
and C5 asserts all four empty-delta quadrants instead of two. **Both
|
||||
new quadrants were mutation-checked, and neither is caught by the
|
||||
proptest** — no generated input reaches either;
|
||||
- the **public `Edit` doc was factually false**: it said forward
|
||||
`apply_edit` never produces the empty-delta shape, while C2b proves
|
||||
all three forward empty forms do;
|
||||
- **R7's write-up overstated what the paired gate runs exclude.** They
|
||||
exclude the source tree. They do not narrow the cause to three
|
||||
candidates — scheduler load, kernel and socket timing, and unrelated
|
||||
machine state all varied too, and a `BrokenPipe` on a socket handshake
|
||||
is exactly what those can drive.
|
||||
|
||||
**Two registry rows gained occurrences on this lane**: R7's eighth (the
|
||||
green/red pair whose heads differ by one markdown file) and **U6's
|
||||
second — the first time U6 has ever reproduced**, twice in a row, and
|
||||
running the OPPOSITE way to R7: out of gate, while `04-lib-crdt` was
|
||||
green in all four of this lane's gate runs.
|
||||
|
||||
**Two claims THIS BLOCK made are corrected by measurement:**
|
||||
|
||||
|
|
|
|||
|
|
@ -593,13 +593,23 @@ and nothing else: `283 passed; 1 failed` in each.
|
|||
the rerun rule a green run establishes intermittence only, and the
|
||||
seventh occurrence already falsified "in-gate always fails".
|
||||
|
||||
**What this changes about the method.** The seventh occurrence's
|
||||
narrowing said the remaining candidates must be varied INSIDE the gate,
|
||||
one per run. This pair says something stronger about which candidates
|
||||
are live: the gate's own per-run state — its ambient root, its fresh
|
||||
`TMPDIR`, and process state carried across stage boundaries — is now the
|
||||
only place the difference can be, because the tree was held fixed to
|
||||
within a markdown file across a green/red boundary.
|
||||
**What this changes about the method, stated at the strength it
|
||||
carries.** The seventh occurrence's narrowing said the remaining
|
||||
candidates must be varied INSIDE the gate, one per run. This pair
|
||||
sharpens **one** exclusion and nothing else: **the Rust source tree is
|
||||
not the variable.**
|
||||
|
||||
It does **not** narrow the cause to three things. The gate's per-run
|
||||
state — its ambient root, its fresh `TMPDIR`, and process state carried
|
||||
across stage boundaries — remains the set of candidates this project can
|
||||
actually vary one at a time, which is why they are the ones to try. But
|
||||
**they are not an exhaustive causal set**, and an earlier version of
|
||||
this paragraph said they were. Everything unrelated to the repository
|
||||
also differed between the two runs: scheduler load and CPU contention,
|
||||
kernel and socket timing, page cache and memory pressure, and whatever
|
||||
else the machine was doing at 15:48 versus 15:56. A socket handshake
|
||||
racing a `BrokenPipe` is exactly the kind of failure those can drive,
|
||||
and holding the tree fixed says nothing about any of them.
|
||||
|
||||
**Sixth occurrence — the parse-budget diagnosability lane, 2026-08-29,
|
||||
local (Linux), `gpu` step.** All three required fragments present in the
|
||||
|
|
@ -915,11 +925,45 @@ was lost.
|
|||
| **selector** | `--lib --features crdt optimistic::tests::criterion_1_end_of_line_typing_completes_sub_frame_per_keystroke` **and** `editor::tests::composition_overhead_under_ten_percent`, failing in the same run |
|
||||
| **job / flavor** | local (Linux), `scripts/gate` step `04-lib-crdt`, with sibling worktrees building concurrently |
|
||||
| **required fragments** | `criterion 1: per-keystroke orchestrator time` + `exceeds 1ms`; and `composition machinery added more than 10% overhead` |
|
||||
| **status** | **new incident, one occurrence, not reproduced** |
|
||||
| **status** | **SECOND OCCURRENCE 2026-08-30, and the first time it REPRODUCED — twice in a row.** Still no mechanism; see the block below |
|
||||
| **what IS established** | both are **wall-clock budget assertions** — 1.264ms against a 1ms budget, and 1.297× against a 1.10× budget — so both are load-sensitive by construction. Both green in an isolated rerun of exactly those two selectors, and both green in the next full gate run of the same command (2105 passed) |
|
||||
| **what is NOT** | whether the machine's concurrent load caused it. The confound is real (this machine runs one shared `CARGO_TARGET_DIR` and several worktrees) but **was not measured**, so it is a rival explanation, not a finding |
|
||||
| **rival explanation not excluded** | a genuine regression in either path. Nothing in the observing diff touches the optimistic-echo orchestrator or the composition pipeline, but "my diff looks unrelated" is not evidence, and this row does not treat it as such |
|
||||
|
||||
**Second occurrence — the CRDT identity-undo lane, 2026-08-30, local
|
||||
(Linux).** Both required fragments captured, both selectors, one run:
|
||||
|
||||
```
|
||||
criterion 1: per-keystroke orchestrator time 1.343883ms exceeds 1ms
|
||||
composition machinery added more than 10% overhead: 1.182
|
||||
```
|
||||
|
||||
**It reproduced on the immediately following run**, which is new for
|
||||
this row — the first occurrence explicitly recorded "not reproduced".
|
||||
|
||||
Margins are recorded because U11 taught this registry what their absence
|
||||
costs. Here: **1.343883ms against a 1ms budget** (1.34×) and **1.182×
|
||||
against a 1.10× budget**; at the first occurrence, 1.264ms and 1.297×.
|
||||
So the composition margin grew and the keystroke margin grew, but
|
||||
neither by an order that separates load from regression. Both selectors
|
||||
were green in isolated single-selector reruns.
|
||||
|
||||
**The asymmetry runs the OPPOSITE way to R7, and that is the useful
|
||||
part.** Both failures were **out of gate** — a bare
|
||||
`cargo test --lib --features crdt` in the worktree — while the same
|
||||
command as `scripts/gate`'s `04-lib-crdt` step was **green in all four
|
||||
of this lane's gate runs** (`20260830T154827Z`, `T155621Z`, `T160242Z`,
|
||||
`T160824Z`). R7 fails in-gate and has never reproduced outside it; U6
|
||||
here did the reverse. Whatever the two rows share, it is not a
|
||||
direction.
|
||||
|
||||
**No mechanism is claimed, and the load confound is again unmeasured.**
|
||||
The machine was running the agent session's own build and test traffic;
|
||||
that is a rival explanation, not a finding, exactly as the first
|
||||
occurrence recorded. What is worth having is that **this row is now
|
||||
reproducible under some condition**, which the first occurrence could
|
||||
not say.
|
||||
|
||||
**Two budget tests failing in one run and neither in the next is the
|
||||
signature worth matching**, more than either name alone: a real
|
||||
regression in two unrelated subsystems at once is far less likely than
|
||||
|
|
|
|||
|
|
@ -1,8 +1,29 @@
|
|||
# Identity-replace undo — a CRDT-version delta is not a text delta
|
||||
|
||||
**Status: revision 4 — AWAITING APPROVAL. Nothing implemented.**
|
||||
**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 4 answers review of 3, which found one substantive gap: **C9
|
||||
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
|
||||
|
|
@ -22,13 +43,35 @@ 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.**
|
||||
> **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`
|
||||
|
|
@ -38,11 +81,13 @@ testable at all.
|
|||
`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.
|
||||
- **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.
|
||||
|
|
@ -215,9 +260,9 @@ one of the four already classified.
|
|||
| 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 |
|
||||
| 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 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 |
|
||||
| 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 |
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue