docs(framing): generated-buffer immutability, revision 3
Answers review round 2 on #188 @516bd35-- three P1, two P2 -- integrated to main @7586905(#189, COHERENCE.md only; clean merge). P1-1, the route cannot write to a locked buffer. Confirmed, and the review's first repair option cannot work: reordering begin_edit's two checks leaves ensure_writable running one line later, so a locked buffer is still refused and only the reported error changes. Any admitting path must not reach ensure_writable at all. Q#GB3 is reversed -- generated writes get their own run_buffer_edit arm and never touch begin_edit -- and new section 3.4 specifies the transaction: one &mut Buffer method, eight named exits with the post-state of each, relock and editing_in_progress clear unconditional, bounds pre-validated so an invalid range costs no history, and history cleared iff the revision advanced (exact, because revision bumps after the undo push and before the on_edit broadcast). Proved along the way that no Lua runs inside a generated write: LuaInterceptView implements only intercept_edit and inherits View::on_edit's no-op default, so the only re-entrancy direction that needs a gate is outward. P1-2, disambiguation. New section 2.10 is the census: 19 units across 14 grep lines, five classes, arithmetic shown, each classified by reading its enclosing function. Two sites break; between them six downstream consumers, not three. The fourth listview consumer is listview.open's own never-capture-a-panel guard, which fails inverted and silently -- it captures the panel as its own q target, the exact loop its comment says it prevents. compile's slots table is NOT affected (keyed by a module constant, slot_for_buffer is id-based). New Q#GB18 routes both by owned BufferId, and notes listview registers no on_removed so its new list must compact on scan like dired's live_handles. P1-3, unlock_generated. Withdrawn as written; both halves of the finding hold. Sweep C found the mirror-image hole the review did not: the SHIPPED set_generated_contents lifts a lock it did not install, so it can already overwrite a live terminal identity buffer. Provenance (new Q#GB15, generated_lock beside read_only) therefore earns its cost in both directions rather than existing to make the unlock safe. Q#GB7 moves to Stage 2, its claim narrows from "brick escape" to "the closure of the capability { generated = true } adds", and the asymmetry with the standing no-Lua-set_read_only policy is addressed directly: a provenance-bounded unlock adds no reachable state that { generated = true } did not. P2-4, criterion 6. Confirmed, and the framing cited the wrong precedent: terminal_copy_mode_acceptance has zero dispatch_idle_for references. The model is dired_acceptance.rs:969. dispatch_idle_for has six ways to return false and the review named one, so the criterion now carries three halves -- document-window premise, the gate, and acc16's positive control, which rules out the other five clauses in one assertion. P2-5, the path-backed refusal. Now exercised on all four surfaces with guard misplacement as the explicit bite. Sweep C (obligation 3) also found that read_only is one boolean serving three policies: the generated lock, terminal identity, and -- as a reader -- fold.rs:313's "is this a document buffer" test, pinned by folding_acceptance.rs:570. Locking five families silently disables pmacs.fold.fold on all five, which contradicts Q#GB3's own stated rationale for preserving the unfold seam. New Q#GB16 names it and recommends accepting it with a criterion rather than accepting it silently. Two further corrections the review did not name. COHERENCE.md section 14's listview list was corrected by #189 while revision 2 was open, so section 1.5 goes from owed to landed -- a merged correction is removed, not restated. And *help* has two independent writers, src/help.rs:354 (Rust, apply_edit, mark_clean) and default.lua:1239 (Lua, no mark_clean), each with its own find-by-name and its own copy of the name constant, so the inventory's headline is five mechanisms, not four. Section 2.9's is_modified sweep is corrected a second time: seven production consumers, two load-bearing. Revision 1 said two, revision 2 said four. The conclusion is unchanged but was reached twice from an incomplete count. New section 9b records the cross-lane boundaries verbatim and confirms Q#DR25 against #171 revision 7 atfd7ae37. Revisions 1 and 2 never mentioned Q#DR25 at all despite owning it; revision 3 claims it, and carries #171's trap that dired_acceptance.rs:969's read-only status assertion passes both before and after adoption. Twelve acceptance criteria added or rewritten, each stating what it asserts about content produced and the mutation that falsifies it. Stage 2 gains criteria for the transaction's error paths specifically -- a leaked editing_in_progress asserted through the NEXT edit, not the failing one, because the failing call reports the same error either way. Why revision 2 shipped these: it audited criteria against pre-images (sweep A) and capabilities against who may use them (sweep B), but never read the guards its own mechanisms had to pass through. begin_edit, document_bytes and terminal/session.rs:305 were all cited elsewhere in the tree and none was opened. The process fact for revision 4: for every seam the design routes through, read the callee, not the caller's description of it. Status stays PROPOSED. No runtime code, no protocol change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Lv428Fth9LRtffwJSsqH7T
This commit is contained in:
parent
ef56e55f00
commit
8e032d75d8
|
|
@ -463,10 +463,11 @@ has **no branch and no framing yet**.
|
||||||
|
|
||||||
- Portable branch: `githubsucks/generated-buffer-immutability`; worktree
|
- Portable branch: `githubsucks/generated-buffer-immutability`; worktree
|
||||||
`../pmacs-generated-immutability`. **PR #188**, base `main`, forked from
|
`../pmacs-generated-immutability`. **PR #188**, base `main`, forked from
|
||||||
`githubsucks/main` @ `ad41cf1`. Framing only —
|
`githubsucks/main` @ `ad41cf1`, **integrated to `7586905`** (#189,
|
||||||
`docs/generated-buffer-immutability-framing.md`, revision 2, plus this
|
`COHERENCE.md` only; clean merge, no conflict). Framing only —
|
||||||
|
`docs/generated-buffer-immutability-framing.md`, revision 3, plus this
|
||||||
lane. **No runtime code, no protocol change.**
|
lane. **No runtime code, no protocol change.**
|
||||||
- **PROPOSED — one review round closed (five findings, three P1, two P2).
|
- **PROPOSED — two review rounds closed (ten findings, six P1, four P2).
|
||||||
Not approved. Do not implement, do not merge.**
|
Not approved. Do not implement, do not merge.**
|
||||||
- **What it frames.** The class-wide half of the `set_generated_contents`
|
- **What it frames.** The class-wide half of the `set_generated_contents`
|
||||||
invariant that `docs/agent-handoff.md` §4 and `COHERENCE.md` §14 both
|
invariant that `docs/agent-handoff.md` §4 and `COHERENCE.md` §14 both
|
||||||
|
|
@ -480,22 +481,32 @@ has **no branch and no framing yet**.
|
||||||
as a `{ generated = true }` option on the existing Lua mutators, with
|
as a `{ generated = true }` option on the existing Lua mutators, with
|
||||||
`set_generated_contents` reimplemented as its whole-buffer wrapper. It
|
`set_generated_contents` reimplemented as its whole-buffer wrapper. It
|
||||||
is the only candidate in which the buffer is never observably unlocked.
|
is the only candidate in which the buffer is never observably unlocked.
|
||||||
- **Two stages, two PRs.** Stage 1 — listview ownership fix, a one-way
|
**Revision 3 pins the transaction** (framing §3.4): its **own**
|
||||||
`unlock_generated` binding, dired and listview adopting the shipped
|
`run_buffer_edit` arm — **not** the bypass arm, which calls
|
||||||
primitive, and the window-coordinate clamp. Stage 2 — the new
|
`begin_edit`, which calls `ensure_writable` first (`src/buffer.rs:725`)
|
||||||
primitive, compile's nine write sites, the search panel's four,
|
and would refuse every generated write to a locked buffer — one
|
||||||
compile/search ownership, and the path-backed refusal plus
|
`&mut Buffer` method, eight named exits, relock and flag-clear
|
||||||
`mark_clean`.
|
unconditional, and history cleared **iff the revision advanced**.
|
||||||
- **Three facts from this lane that other lanes need before it merges:**
|
- **Two stages, two PRs.** Stage 1 — listview ownership fix **plus its
|
||||||
|
identity-routing fix in the same PR**, dired and listview adopting the
|
||||||
|
shipped primitive, the window-coordinate clamp, and the fold decision.
|
||||||
|
Stage 2 — the new primitive, compile's nine write sites, the search
|
||||||
|
panel's four, compile/search ownership + routing, the path-backed
|
||||||
|
refusal plus `mark_clean`, the `generated_lock` provenance field, and
|
||||||
|
the bounded `unlock_generated`.
|
||||||
|
- **Six facts from this lane that other lanes need before it merges:**
|
||||||
- **`bypass_intercept` is the wrong inventory key.** It misses
|
- **`bypass_intercept` is the wrong inventory key.** It misses
|
||||||
`*buffer-list*`, `*help*` and `*workers*`, which are generated with
|
`*buffer-list*`, `*help*` and `*workers*`, which are generated with
|
||||||
plain writes and no intercept at all. `docs/agent-handoff.md` §4's
|
plain writes and no intercept at all. `docs/agent-handoff.md` §4's
|
||||||
four-row table inherits that blind spot.
|
four-row table inherits that blind spot — **and undercounts by one**:
|
||||||
- **`COHERENCE.md` §14's listview consumer list is wrong.**
|
`src/help.rs:354` `replace_help_buffer` is a fifth writer mechanism
|
||||||
`pmacs.listview.open` has three production callers, all in
|
(own find-or-create, `Buffer::apply_edit`, own `mark_clean`) writing
|
||||||
`lsp.lua` — `*references*` (`:2056`), `*outline*` (`:2102`),
|
the **same** `*help*` buffer as `default.lua:1239`, which does not
|
||||||
`*lsp-help*` (`:2513`). `*buffer-list*` is hand-rolled
|
mark clean. Two owners, one buffer, two copies of the name constant
|
||||||
(`default.lua:387`) and `*search-results*` is independent.
|
across the FFI boundary.
|
||||||
|
- **`COHERENCE.md` §14's listview consumer list was wrong and is now
|
||||||
|
FIXED** — PR #189 (`main` @ `7586905`) landed exactly the correction
|
||||||
|
this lane measured. Nothing owed. Recorded so it is not re-asserted.
|
||||||
- **Three writers adopt any buffer sharing their name** —
|
- **Three writers adopt any buffer sharing their name** —
|
||||||
`listview.lua:95`, `compile.lua:263`, `default.lua:861-868` — against
|
`listview.lua:95`, `compile.lua:263`, `default.lua:861-868` — against
|
||||||
a rule the tree already states at `terminal.lua:300-305` and
|
a rule the tree already states at `terminal.lua:300-305` and
|
||||||
|
|
@ -505,11 +516,44 @@ has **no branch and no framing yet**.
|
||||||
foreign `*compilation*` un-editable. Today `M-x buffer.undo` — this
|
foreign `*compilation*` un-editable. Today `M-x buffer.undo` — this
|
||||||
arc's bug — is the only recovery, so the arc must not lock these
|
arc's bug — is the only recovery, so the arc must not lock these
|
||||||
buffers before fixing ownership.
|
buffers before fixing ownership.
|
||||||
|
- **Disambiguating a name breaks the sites that read one.** Census in
|
||||||
|
framing §2.10: 19 units across 14 grep lines, two genuinely broken.
|
||||||
|
`listview.lua:44`'s `panels[d.name]` (written under the *requested*
|
||||||
|
name at `:97`, read under the *actual* name) has **four** consumers,
|
||||||
|
and the fourth — `listview.open:118-123`'s never-capture-a-panel
|
||||||
|
guard — fails **inverted and silently**, capturing a panel as its own
|
||||||
|
`q` target. `compile.lua:216`'s `is_generated_buffer` has two.
|
||||||
|
`compile.lua`'s `slots` is **not** affected: keyed by a module
|
||||||
|
constant at both ends, with `slot_for_buffer` id-based.
|
||||||
|
- **`read_only` is one boolean serving THREE policies** (framing
|
||||||
|
§2.11): the generated lock; terminal identity
|
||||||
|
(`src/terminal/session.rs:305`); and, as a *reader*,
|
||||||
|
`src/lua_bindings/fold.rs:313`'s "is this a document buffer" test,
|
||||||
|
pinned by `tests/folding_acceptance.rs:570`. Consequence for any
|
||||||
|
lane: **locking a buffer silently disables `pmacs.fold.fold` on it**,
|
||||||
|
with the status `fold rejected: not a document buffer`.
|
||||||
|
- **The SHIPPED `set_generated_contents` can overwrite a live terminal
|
||||||
|
identity buffer.** It does `self.read_only = false` unconditionally
|
||||||
|
(`src/buffer.rs:546`), so it lifts a lock it did not install, writes,
|
||||||
|
and re-locks. Present on `main`, untested, unframed anywhere before
|
||||||
|
this revision. Bounded in Stage 2 by the `generated_lock` field.
|
||||||
- **Overlap warning.** Stage 2 touches `src/lua_bindings/mod.rs`'s buffer
|
- **Overlap warning.** Stage 2 touches `src/lua_bindings/mod.rs`'s buffer
|
||||||
mutator bindings and `src/buffer.rs`. Do not run it concurrently with
|
mutator bindings and `src/buffer.rs`. Do not run it concurrently with
|
||||||
the `apply_resource_op` lane or the bottom-panel 2B work without
|
the `apply_resource_op` lane or the bottom-panel 2B work without
|
||||||
assigning those files to one lane first. The framing itself touches
|
assigning those files to one lane first. The framing itself touches
|
||||||
neither.
|
neither.
|
||||||
|
- **Cross-lane, settled, not re-decided here.** #186 owns the urgent
|
||||||
|
pre-filesystem refusal for synchronous `apply_resource_op`; #171 later
|
||||||
|
owns full post-delete lifecycle reconciliation, including the async
|
||||||
|
race where a buffer becomes modified after dired dispatch. **#171's
|
||||||
|
Q#DR25 is deferred INTO this lane** — confirmed against #171 revision 7
|
||||||
|
(`fd7ae37`), which states that dired's listing becoming immutable is
|
||||||
|
"owned by the `generated-buffer-immutability` lane" and that "Stage 2
|
||||||
|
does not implement it, does not gate on it, and carries no acceptance
|
||||||
|
for it." This lane's Stage 1 claims that work. **Neither ordering
|
||||||
|
conflicts**: #171 Stage 2b changes `paint`'s callers, this lane changes
|
||||||
|
`paint` itself. Revisions 1 and 2 of this framing never mentioned
|
||||||
|
Q#DR25 at all; revision 3 §9b records it.
|
||||||
- **Re-measured at `ad41cf1` while scouting: 276 CRDT-dark tests**
|
- **Re-measured at `ad41cf1` while scouting: 276 CRDT-dark tests**
|
||||||
(3,251 vs 3,527), by
|
(3,251 vs 3,527), by
|
||||||
`cargo test --all-targets --no-default-features --features lua54[,crdt] -- --list | grep -c ': test$'`.
|
`cargo test --all-targets --no-default-features --features lua54[,crdt] -- --list | grep -c ': test$'`.
|
||||||
|
|
|
||||||
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue