fix(lean4): tie the deferred expansion to the fan-out that queued it

`buffer.after-edit` fan-outs NEST — the typed-edit contract supports a
consumer calling `pmacs.hook.run`, and typed_edit.lua's header says so
in its second paragraph. A nested run re-enters every subscriber,
including the deferred expansion's, while the OUTER chain is still
walking its consumer list and pairing has not yet seen the terminator.

So a consumer registered at priority 75 — between the expander at 50
and pairing at 100 — that runs one nested fan-out made `\alp(` yield
`α(` again: the nested pass consumed the queued expansion and edited,
and outer pairing then resumed holding a record the replace had
invalidated. That is round 10's failure reached through the chain's
documented re-entrancy seam rather than through claiming, which is why
deferring alone did not close it.

Deferring work past a fan-out means owning WHICH fan-out it belongs to.
The chain's subscriber and this module's each run exactly once per
fan-out, in that order, so counting invocations of the first and
matching them off in the second identifies the nesting level. Only the
outermost pass expands; a nested one leaves the expansion queued. No
new seam in typed_edit.lua, which is merged Stage 4a substrate.

Both halves bite: removing the level check and never counting
invocations each fail the new acceptance 45n.

Also fixes a test comment that still described the span design round 10
discarded — it claimed the expansion replaces the span "INCLUDING the
terminator". The behaviour asserted was right; the explanation was
stale. Framing rev 11.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_011LFvC4FQtux4y32KuevZ7B

builtin/runtime/lean_input.lua

@@ -229,7 +229,26 @@ end
 -- The consumer
 -- ---------------------------------------------------------------------
 
+-- Chain-consumer invocations not yet matched by a `run_deferred`.
+--
+-- `buffer.after-edit` fan-outs NEST: the typed-edit contract explicitly
+-- supports a consumer calling `pmacs.hook.run("buffer.after-edit")`,
+-- and a nested run re-enters every subscriber — including this module's
+-- deferred-expansion subscriber, while the OUTER chain is still walking
+-- its consumer list and pairing has not yet seen the terminator. A
+-- nested run that performed the expansion would reproduce exactly the
+-- bug deferring exists to fix: pairing resumes afterwards holding a
+-- record the replace has invalidated, declines, and the closer is lost.
+--
+-- The chain's subscriber and this module's subscriber run exactly once
+-- each per fan-out, in that order, so counting invocations of the first
+-- and matching them off in the second identifies the nesting level
+-- without any new seam in typed_edit.lua. Only the outermost pass
+-- performs the expansion; a nested one leaves it queued.
+local depth = 0
+
 local function on_typed_edit(rec)
+  depth = depth + 1
   local fid = frontend_id()
   if fid == nil then return false end
 
@@ -404,6 +423,15 @@ end
 -- A claim by ANY chain consumer stops the chain but not this — which
 -- is the point. Pairing claims the terminator it reacts to.
 local function run_deferred()
+  -- Match off this fan-out's chain invocation. `> 1` means the outer
+  -- chain is still mid-list — pairing has not had the terminator yet —
+  -- so the queued expansion stays queued for the outer pass. The clamp
+  -- keeps this honest if a lower-priority consumer claimed before the
+  -- chain reached ours, in which case there is nothing queued anyway.
+  local level = depth
+  if depth > 0 then depth = depth - 1 end
+  if level > 1 then return end
+
   local fid = frontend_id()
   if fid == nil then return end
   local d = deferred[fid]

docs/active-work.md

@@ -175,8 +175,8 @@ If it does not, stop and repair the remote/fetch configuration.
 
 ### Stage 4b — the Unicode input method (branch `lean4-stage4b-input-method`)
 
-- Framing `docs/lean4-mode-framing.md` **revision 10** (round 10 =
-  review of the implementation). Stage
+- Framing `docs/lean4-mode-framing.md` **revision 11** (rounds 10 and
+  11 = review of the implementation). Stage
   4a (the typed-edit consumer chain) MERGED as #179; this branch is 4b,
   the Lean content that registers on it.
 - Footprint: `scripts/regen-lean-abbrev` (new, the generator),
@@ -184,7 +184,7 @@ If it does not, stop and repair the remote/fetch configuration.
   from `leanprover/vscode-lean4@17d1d08`, Apache-2.0),
   `builtin/runtime/lean_input.lua` (new, the consumer at priority 50),
   `src/editor.rs` (two `include_str!` blocks),
-  `tests/lean_input_acceptance.rs` (new, 29 tests), and one
+  `tests/lean_input_acceptance.rs` (new, 30 tests), and one
   `#[cfg(feature = "crdt")]` `--lib` test in `src/daemon.rs`
   (acceptance 45f). No protocol change (Q#LN14). Entirely Lua apart
   from the load sites and that one test.
@@ -245,6 +245,8 @@ If it does not, stop and repair the remote/fetch configuration.
   | drop the `cursor() == post_cursor` check | 1 |
   | place the point without the context guard | 1 |
   | load lean_input.lua after lsp.lua | 1 |
+  | let a nested fan-out consume the deferred slot | 1 |
+  | stop counting chain invocations | 1 |
 
   Acceptance 45f bit by construction: without a registered window for
   the source frontend it ran six fan-outs with a nil record and proved
@@ -265,6 +267,17 @@ If it does not, stop and repair the remote/fetch configuration.
   relevance check needs `cursor() == post_cursor`, as pairing's has
   since #110), and cursor placement could move a buffer an intercept
   had switched to.
+- **Round 11 found the round-10 fix incomplete in one place:
+  `buffer.after-edit` fan-outs NEST.** A consumer between the expander
+  (50) and pairing (100) that calls `pmacs.hook.run("buffer.after-edit")`
+  re-enters the expander's subscriber while the OUTER chain is still
+  mid-list; the nested pass expanded and outer pairing then resumed with
+  an invalidated record — `α(` again, through the chain's documented
+  re-entrancy seam instead of through claiming. **Deferring work past a
+  fan-out means owning which fan-out it belongs to.** The chain's
+  subscriber and the expander's each run exactly once per fan-out, so
+  counting the first and matching it off in the second identifies the
+  nesting level with no new seam in merged Stage 4a substrate.
 - Undo is cross-peer-degraded on CRDT frontends and that is ACCEPTED,
   named in the module header (Q#LN21): six source-peer optimistic
   inserts replaced by one daemon-peer op. `set_round_trip_input` would

docs/agent-handoff.md

@@ -139,7 +139,11 @@ commands, read `docs/active-work.md` immediately after this file.
     be used. The expansion therefore runs on a SECOND
     `buffer.after-edit` subscriber after the chain — which is how a
     pair character that terminates an abbreviation still pairs
-    (`\alp(` → `α()`). Its other durable facts:
+    (`\alp(` → `α()`). And **deferring work past a fan-out means
+    owning which fan-out it belongs to**: these fan-outs NEST, so a
+    consumer between the expander and pairing that calls
+    `pmacs.hook.run` re-enters the deferred subscriber while the outer
+    chain is still mid-list. Its other durable facts:
     the table must stay an ORDERED SEQUENCE (equal-length ties resolve
     by source declaration order, which a `pairs`-iterated map cannot
     express); a generator round-trip check must re-read the BYTES ON

docs/lean4-mode-framing.md

@@ -46,7 +46,7 @@ during a rebase.
 
 ## 0.1 Revision history
 
-Revision 1 — initial. Current revision: **10**.
+Revision 1 — initial. Current revision: **11**.
 
 ### Round 1 (rev 1 → rev 2)
 
@@ -567,6 +567,26 @@ Acceptance 45m was added with them: the expansion now runs on its own
 `buffer.after-edit` subscriber, which is a new instance of Q#AP7 and
 was unpinned.
 
+### Round 11 (rev 10 → rev 11)
+
+One P1 in the round-10 fix, and one stale comment.
+
+1. **The deferred expansion was not tied to the fan-out that queued
+   it.** `buffer.after-edit` fan-outs nest — the typed-edit contract
+   supports a consumer calling `pmacs.hook.run` — and a nested run
+   re-enters the expander's subscriber while the OUTER chain is still
+   mid-list. A consumer at priority 75 running one nested fan-out made
+   `\alp(` yield `α(` again: the nested pass expanded, and outer
+   pairing then resumed with a record the replace had invalidated.
+   Round 10's own failure mode, reached through re-entrancy instead of
+   claiming. Q#LN22 now specifies matching chain invocations against
+   expander invocations so only the outermost pass expands; acceptance
+   45n pins it.
+2. **A test comment still described the discarded span design** — it
+   said the expansion replaces the span "INCLUDING the terminator",
+   which round 10 deliberately stopped doing. The behaviour it asserts
+   was correct; only the explanation was stale.
+
 ## 1. What ships
 
 Nine stages, after round 4 split Stage 3 and round 5 split Stage 4. The
@@ -1785,6 +1805,22 @@ and the typed text only; whatever pairing did lands after it and
 survives untouched. One undo restores the same text either way, because
 the terminator was always its own insert.
 
+**The deferred expansion must belong to its own fan-out** (round 11).
+`buffer.after-edit` fan-outs NEST — Q#AP9 and typed_edit.lua's header
+both say so explicitly, and a consumer may call `pmacs.hook.run`. A
+nested run re-enters every subscriber, including the deferred
+expansion's, while the OUTER chain is still walking its consumer list
+and pairing has not yet seen the terminator. A nested pass that
+performed the expansion would reproduce the exact bug deferring exists
+to fix, reached through the chain's documented re-entrancy seam instead
+of through claiming.
+
+The chain's subscriber and the expander's subscriber each run exactly
+once per fan-out, in that order, so counting invocations of the first
+and matching them off in the second identifies the nesting level — no
+new seam in typed_edit.lua, which is merged substrate. Only the
+outermost pass expands; a nested one leaves the expansion queued.
+
 Two guards this exposes, both of which pairing already carries:
 
 - The relevance check is **three-part**, not two: buffer, window, **and
@@ -2692,6 +2728,14 @@ criterion 46 requires to stay byte-identical.
     unexpanded text. Pinned with the `sighelp` fake server and `(` as
     the trigger — the flush carrying the terminator carries `α()`.
     Falsified by loading lean_input.lua after lsp.lua.
+45n. **A nested fan-out must not expand early** (round 11). A consumer
+    registered BETWEEN the expander and pairing that calls
+    `pmacs.hook.run("buffer.after-edit")` once still yields `α()` for
+    `\alp(`. Bites against a deferred slot consumed by whichever
+    fan-out happens to reach it: the nested pass would expand, and the
+    outer chain would then hand pairing a record the replace had
+    invalidated — the round-10 failure again, through the chain's
+    documented re-entrancy seam rather than through claiming.
 45h. **Tie-break by source order (§2.11).** `\f` + space yields `‹` —
     `f<` and `f>` are both length 2, and `f<` is declared first. Same
     for `\"` + space → `Ä`, first of eleven equal-length candidates.
@@ -2846,7 +2890,7 @@ uncapped event queue, the dropped `cfg.restart`, and — unchanged from
 languages other than Lean, and §4's rule is what keeps them out of a Lean
 PR.
 
-### 9.1 Coherence impact — stages 4a and 4b (rev 10)
+### 9.1 Coherence impact — stages 4a and 4b (rev 11)
 
 **Sections served.** §6 (interaction islands) primarily, and in the
 *preventing* direction rather than the fixing one — see below. §11

tests/lean_input_acceptance.rs

@@ -98,7 +98,10 @@ fn lean_editor() -> (EditorState, PathBuf) {
 fn the_finish_path_retains_the_terminator_in_one_undo_step() {
     // `alp` is not a key; `alpha` is the shortest key extending it. The
     // space does not extend anything, so it lands first and the
-    // expansion replaces the whole span INCLUDING the terminator.
+    // expansion replaces the leader and the typed text — the span stops
+    // BEFORE the terminator, so whatever auto-pairing did with it
+    // survives. One undo restores the same text either way, because the
+    // terminator was its own insert to begin with.
     let (mut s, _f) = lean_editor();
     type_str(&mut s, "\\alp ");
     assert_eq!(text(&s), "α ", "terminator retained, not consumed");
@@ -209,6 +212,45 @@ fn a_pair_character_that_terminates_an_abbreviation_still_pairs() {
     );
 }
 
+#[test]
+fn a_nested_fan_out_between_the_expander_and_pairing_does_not_expand_early() {
+    // `buffer.after-edit` fan-outs NEST — the typed-edit contract
+    // explicitly supports a consumer calling `pmacs.hook.run`, and a
+    // nested run re-enters every subscriber, including the deferred
+    // expansion's. If the nested pass performed the expansion, the
+    // OUTER chain would then resume and hand pairing a record the
+    // replace had already invalidated: `α(` again, reached through the
+    // chain's documented re-entrancy seam rather than through claiming.
+    let (mut s, _f) = lean_editor();
+    exec(
+        &s,
+        r#"
+        _G.NESTED = 0
+        pmacs.typed_edit.add_consumer {
+          name = "nested-fan-out",
+          priority = 75,   -- between the expander (50) and pairing (100)
+          fn = function()
+            if _G.NESTED == 0 then
+              _G.NESTED = 1
+              pmacs.hook.run("buffer.after-edit")
+            end
+            return false
+          end,
+        }
+        "#,
+    );
+
+    type_str(&mut s, "\\alp(");
+    let nested: i64 = eval(&s, "return _G.NESTED");
+    assert_eq!(nested, 1, "the nested fan-out must actually have run");
+    assert_eq!(
+        text(&s),
+        "α()",
+        "the expansion waited for the OUTERMOST pass, so pairing still \
+         held a valid record when the terminator reached it"
+    );
+}
+
 #[test]
 fn a_pair_character_outside_a_pending_abbreviation_still_pairs() {
     // The other direction: claiming extensions must not disable pairing