From 10a0595b473c2bfcb2983b6c4a1051712d44372f Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 15 May 2026 15:44:15 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20correct=20it.3=20=C2=A7Remove=20+=20?= =?UTF-8?q?=C2=A7Codegen-rework=20(it.3-recon-surfaced=20defects)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two HEAD-vs-spec defects the it.3 recon found, fixed at the spec: (1) "remove is_false" was wrong — is_false is shared with WorkspaceDef.drop_iterative; it survives, doc re-scoped only. (2) "remove the Decision-3 Diverge line" struck — it.2 already rewrote Decision 3 to make Diverge the real effect (the milestone's payload); it.3 touches Decision 8 only. (3) The codegen-rework bullet under-described the real risk: the 18g.1 pre-tail-call husk-dec (match_lower.rs:658-736) reads Term::App{tail:true} directly, protects the 18f.2 RC-RSS pin, and its field-forced deletion is RC-safe ONLY if it.1 loop codegen drops superseded owned binders across recur — unverified. Spec now names this as the load-bearing it.3 risk with a RED-gated verification + a named remediation (owned-loop-binder-drop-on-recur in scope for it.3). Only 3 (not 7) setters are tail-driven. No design decision (D1-D4) changes; design validated by shipped it.1/it.2. Not relitigating shipped work (spec_over_plan_patches). --- docs/specs/2026-05-15-iteration-discipline.md | 73 ++++++++++++++++--- 1 file changed, 61 insertions(+), 12 deletions(-) diff --git a/docs/specs/2026-05-15-iteration-discipline.md b/docs/specs/2026-05-15-iteration-discipline.md index df1e57e..e039d17 100644 --- a/docs/specs/2026-05-15-iteration-discipline.md +++ b/docs/specs/2026-05-15-iteration-discipline.md @@ -217,25 +217,74 @@ lower + escape → e2e example. ### it.3 — retire `tail-app` / `tail-do` -- **Remove.** `Term::App.tail`, `Term::Do.tail`, `is_false`; +- **Remove.** `Term::App.tail`, `Term::Do.tail` (the two `tail` + fields only — **not** the `is_false` serde helper: it.1/it.2-era + recon found `is_false` is shared with `WorkspaceDef.drop_iterative`; + it survives, only its doc-comment is re-scoped); `tail-app` / `tail-do` dispatch + `parse_tail_app` / `parse_tail_do` + the keyword-list entries + the `print.rs` - `(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection; + `(tail-app …)`/`(tail-do …)` arms + the prose `"tail "` projection + (render + subst arms; the free-var counter arms are already + `tail`-agnostic); `verify_tail_positions`'s tail-app role (the pass keeps only the - `recur`-in-tail-position role from it.1); `CheckError:: - TailCallNotInTailPosition`; the `musttail` lowering in `emit_call` + `recur`-in-tail-position role from it.1 — note `verify_tail_positions` + and `verify_loop_body` are entangled mutual recursion: the tail-app + arms are deleted in place, the functions are not removed); + `CheckError::TailCallNotInTailPosition` (+ its `code()` arm; it has + no dedicated `ctx()` arm — it falls into the catch-all, so no + `ctx()` edit); the `musttail` lowering in `emit_call` / `emit_indirect_call` and the `tail call` hint in `lower_effect_op`. DESIGN.md Decision 8 rewritten as *superseded* (kept as a tombstone explaining why explicit tail calls were retired — the schema-drift anchors and EBNF/jsonc blocks updated in - lockstep); the Decision-3 `Diverge` line and the EBNF - `tail-app-term` production removed. -- **Codegen block-termination rework.** The `block_terminated = true` - seam, currently set by `tail: true` and consumed by - `match_lower.rs:658–913` + `lib.rs:1238–1577`, becomes solely - `recur`'s (and the ordinary fall-through `ret`). This is the only - non-mechanical part of it.3 and the reason it.1 ships the new seam - first. + lockstep); the EBNF `tail-app-term`/`tail-do-term` productions + removed. + + > **Correction (it.3-recon-surfaced).** The original draft also + > said "the Decision-3 `Diverge` line removed". That clause is + > **struck**: it.2 already rewrote Decision 3 to make `Diverge` + > the *real* effect of `loop`-bearing code — that rewrite is the + > milestone's central payload and stays verbatim. it.3 touches + > Decision **8** only (tombstone), never Decision 3. + +- **Codegen block-termination rework + the 18g.1 husk-dec deletion + (the real non-mechanical part).** Two coupled things, only one of + which the original draft named: + 1. *`block_terminated` seam.* Only **three** setters are + tail-driven (`emit_call`, `emit_indirect_call`, + `lower_effect_op`) — not "seven"; the it.1 journal's "seven" + was stale. They are removed with the `musttail` lowering. Every + other `block_terminated` consumer (`lib.rs` fn-body + fall-through `ret`, Let-scope binder dec, if-branch join + bookkeeping; `match_lower.rs` arm-close/phi gates; + `lambda.rs` save/restore) is `block_terminated`-mediated and + `recur`'s it.1 setter feeds the identical signal — these + re-verify clean. + 2. *18g.1 pre-tail-call shallow husk-dec + (`match_lower.rs:658–736`).* This is the **one consumer that + reads `Term::App{tail:true}` DIRECTLY**, not via + `block_terminated`. It is an RC-correctness optimisation + written to fix the **18f.2 tail-latency RC-RSS pin** (a + `musttail call … ret` strands the moved-from scrutinee's outer + cons-cell husk; 18g.1 shallow-decs it pre-emptively). Removing + the `tail` field forces this block's deletion (it no longer + compiles). The original spec framed the codegen rework as + "solely the `block_terminated` seam" and **missed this**. + `recur` is a back-edge `br` (no `musttail`, no frame-exit + `ret`) so it strands no husk **iff** it.1's loop codegen drops + superseded *owned* binder values across the back-edge. The + spec's "it.1 ships the seam first" claim is verified for the + `block_terminated` half but is **unverified for the + owned-binder-drop half**. it.3 therefore: (i) deletes 18g.1 + (mechanically forced); (ii) re-runs the 18f.2 / RC-RSS bench + pins post-migration as the **gate**; (iii) if RED, the + remediation is **owned-loop-binder-drop-on-`recur` added to + loop codegen** — this is in scope for it.3 (it is the loop-side + of the seam the spec wrongly claimed it.1 fully shipped), + **not** a reason to keep 18g.1 (which cannot survive the field + removal). This contingency + its named remediation is the + load-bearing risk of the milestone; the it.3 plan carries it as + a RED-gated step, not a footnote. - **Corpus migration (full non-structural set — see the Scope-correction note; ~20 tail-app + ~18 no-ADT-candidate + the 2 RC fixtures, exact set is the it.3 plan's recon job).**