plan: form-a-scalar-param-mode-carveout — M1 fieldtest friction+spec_gap#1 docs-honesty tidy

2026-05-18 15:45:28 +02:00
parent 4bc7eb2e0a
commit 4c266a64b4
1 changed files with 463 additions and 0 deletions
@@ -0,0 +1,463 @@
+# form_a.md scalar-parameter mode carve-out — Implementation Plan
+
+> **Parent spec:** `docs/specs/2026-05-18-fieldtest-embedding-abi-m1.md`
+> (findings **[friction]** "The published authoring rule steers an LLM
+> away from the only spelling that works for scalar export params" +
+> **[spec_gap]#1** "form_a.md mandates a mode on every fn param;
+> scalar params accept (and require) no mode"). Orchestrator design
+> decision recorded in `docs/roadmap.md` P1 entry "[todo] form_a.md
+> scalar-parameter mode carve-out". This is a **docs-honesty tidy** in
+> the `docs-honesty-lint` class, NOT a milestone — there is no
+> `docs/specs/<milestone>.md`; the fieldtest spec + roadmap entry are
+> the design carrier.
+>
+> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
+> to run this plan. Steps use `- [ ]` checkboxes for tracking.
+
+**Goal:** Reconcile `crates/ailang-core/specs/form_a.md` and
+`docs/DESIGN.md` §"Embedding ABI (M1)" with the *actual* checker
+behaviour — scalar (`Int`/`Bool`/`Unit`/`Str`) `(fn …)` parameters
+take **no** mode and are written bare, mirroring the existing
+return-type carve-out — and pin the corrected state against
+regrowth.
+
+**Architecture:** Pure documentation + a regression pin. **Zero**
+language / checker / codegen change: the iteration only edits two
+docs and adds one `#[test]`. The checker behaviour being documented
+is already shipped and unchanged (recon Section D: the linearity
+pass in `crates/ailang-check/src/linearity.rs:324-329` skips entirely
+unless *all* params carry an explicit mode; a mode on a scalar makes
+the checker hold the primitive to linear discipline, so an ordinary
+reuse trips `use-after-consume` / `consume-while-borrowed` pointed at
+the body — `crates/ailang-check/src/linearity.rs:757` / `:1074`). The
+fix is RED-first: the pin is written first asserting the post-edit
+state, fails (new carve-out absent + old unconditional phrasing still
+present), then the doc edits turn it green.
+
+**Tech Stack:** `crates/ailang-core/specs/form_a.md`,
+`docs/DESIGN.md`, `crates/ailang-core/tests/docs_honesty_pin.rs`
+(uses `ailang_core::FORM_A_SPEC` — the `include_str!`'d constant at
+`crates/ailang-core/src/lib.rs:120`, the single canonical in-code
+handle for that spec, also used by `tests/spec_drift.rs`; the
+DESIGN.md half reuses the file's existing `read("docs/DESIGN.md")`
+helper). `spec_drift.rs` is **not** a lockstep partner — recon
+confirmed all its `FORM_A_SPEC` anchors are short keyword tokens
+(`(own` / `(borrow` survive because the carve-out *adds*, never
+removes, the mode wrappers); no `spec_drift.rs` assertion pins any
+altered text.
+
+**Scope: four form_a.md sites + one DESIGN.md insertion + one pin.**
+Recon found the unconditional rule restated in four places inside
+`form_a.md`; all four are in scope because a docs-honesty tidy whose
+thesis is "the doc mirrors only the true current state, consistently"
+cannot fix some and leave others contradicting them (that ships the
+exact internal inconsistency the pin class forbids). Site 5
+(`form_a.md:521-524`, a few-shot annotation) already states the
+correct rule using the canonical "heap-shaped / primitive value
+type" vocabulary — it is left **verbatim** (no churn), and the new
+carve-out text deliberately reuses its framing so the document is
+internally consistent end to end.
+
+---
+
+## Files this plan creates or modifies
+
+- Modify: `crates/ailang-core/specs/form_a.md:96-98` — site 1, the
+  `### Function` prose mode sentence.
+- Modify: `crates/ailang-core/specs/form_a.md:230` — site 2, the
+  grammar-block `implicit mode` comment.
+- Modify: `crates/ailang-core/specs/form_a.md:347-352` — site 3,
+  "Schema invariants" item 1.
+- Modify: `crates/ailang-core/specs/form_a.md:381-383` — site 4, the
+  "Forgetting mode annotations" Pitfalls bullet.
+- Modify: `docs/DESIGN.md:2285` — insert the canonical bare-scalar
+  export-param Form-A example after the §"Embedding ABI (M1)"
+  scalar-constraint paragraph, before `## Data model` (2287).
+- Test: `crates/ailang-core/tests/docs_honesty_pin.rs:12` /
+  `:26` — add `use ailang_core::FORM_A_SPEC;` and a new `#[test] fn
+  form_a_scalar_param_carveout_present_and_old_rule_absent`.
+
+Files that do NOT change (verified by recon, recorded so the
+implementer does not "tidy" them): `crates/ailang-core/specs/form_a.md:521-524`
+(already-correct few-shot annotation, left verbatim);
+`crates/ailang-core/tests/spec_drift.rs` (not a lockstep partner);
+`crates/ailang-core/src/lib.rs` (only defines the const);
+any `crates/ailang-check/**` source (zero behaviour change).
+
+---
+
+## Task 1: RED — write the regression pin asserting the post-edit state
+
+**Files:**
+- Test: `crates/ailang-core/tests/docs_honesty_pin.rs`
+
+- [ ] **Step 1: Add the `FORM_A_SPEC` import**
+
+In `crates/ailang-core/tests/docs_honesty_pin.rs`, the current line 12 is:
+
+```rust
+use std::fs;
+```
+
+Replace it with:
+
+```rust
+use ailang_core::FORM_A_SPEC;
+use std::fs;
+```
+
+(`FORM_A_SPEC` is `pub const FORM_A_SPEC: &str` at
+`crates/ailang-core/src/lib.rs:120`; this integration test is in the
+`ailang-core` crate's `tests/` dir and may use the crate's public
+API, exactly as `tests/spec_drift.rs:17` does.)
+
+- [ ] **Step 2: Append the new pin test**
+
+Append this `#[test]` fn to the END of
+`crates/ailang-core/tests/docs_honesty_pin.rs` (after the closing
+`}` of `prose_roundtrip_md_has_no_wunschdenken`, which is the last
+item, currently line 100):
+
+```rust
+
+#[test]
+fn form_a_scalar_param_carveout_present_and_old_rule_absent() {
+    // form_a.md is read via the canonical include_str! const, not a
+    // re-derived path: single source of truth, compile-checked, no
+    // stale-path bug. norm() collapses the docs' hard line-wrap so
+    // every asserted substring below is the single-spaced form
+    // (planner Step-5 item 6: line-wrap is structurally discharged,
+    // the substrings need not be contiguous in the .md source).
+    let f = norm(FORM_A_SPEC);
+    let d = norm(&read("docs/DESIGN.md"));
+
+    // --- ABSENT: the four old unconditional phrasings must be gone ---
+    assert!(!f.contains("Mode annotations on every `(fn ...)` parameter."),
+        "form_a.md item 1 must no longer head with the unconditional 'every (fn ...) parameter' rule (site 3)");
+    assert!(!f.contains("All parameters of a `(fn ...)` MUST carry a mode annotation"),
+        "form_a.md ### Function prose must no longer state the unconditional all-params rule (site 1)");
+    assert!(!f.contains("(DO NOT USE in new (fn ...) defs)"),
+        "form_a.md grammar block must no longer blanket-forbid the bare (implicit-mode) form (site 2)");
+    assert!(!f.contains("Wrap every `(fn ...)` parameter in `(own ...)` or `(borrow ...)`."),
+        "form_a.md Pitfalls bullet must no longer state the unconditional 'wrap every parameter' imperative (site 4)");
+
+    // --- PRESENT: the scalar-parameter carve-out, the four sites ---
+    assert!(f.contains("A scalar (non-heap-shaped) parameter or return takes **no** mode: write it bare, e.g. `(con Int)`."),
+        "form_a.md item 1 must state the scalar-parameter carve-out symmetrically with the return-type carve-out (site 3)");
+    assert!(f.contains("a scalar (non-heap-shaped: `(con Int)`, `(con Bool)`, `(con Unit)`, `(con Str)`) takes **no** mode and is written bare"),
+        "form_a.md ### Function prose must carry the scalar carve-out (site 1)");
+    assert!(f.contains("; no mode — REQUIRED for scalars (Int/Bool/Unit/Str), rejected for heap-shaped"),
+        "form_a.md grammar block comment must state the bare form is required for scalars (site 2)");
+    assert!(f.contains("Putting a mode on a scalar parameter."),
+        "form_a.md Pitfalls must carry the inverse pitfall — over-wrapping a scalar (site 4)");
+
+    // --- PRESENT: the DESIGN.md §\"Embedding ABI (M1)\" mirror ---
+    assert!(d.contains("Export parameters are written **bare**: a scalar type carries no `own`/`borrow` mode"),
+        "DESIGN.md §Embedding ABI (M1) must mirror the canonical bare-scalar export-param rule");
+}
+```
+
+- [ ] **Step 3: Run the pin — it MUST FAIL (this is the RED)**
+
+Run: `cargo test -p ailang-core --test docs_honesty_pin form_a_scalar_param_carveout_present_and_old_rule_absent`
+
+Expected: **FAIL**. The first failing assertion is the first ABSENT
+check — `form_a.md item 1 must no longer head with the unconditional
+'every (fn ...) parameter' rule (site 3)` — because the old phrasing
+`Mode annotations on every \`(fn ...)\` parameter.` is still present
+in `form_a.md` (the doc edits are Tasks 2–3). This proves the pin
+discriminates the pre-edit state.
+
+- [ ] **Step 4: Confirm the rest of the file's pins are unaffected**
+
+Run: `cargo test -p ailang-core --test docs_honesty_pin`
+
+Expected: the four pre-existing tests
+(`design_md_has_no_wunschdenken`, `design_md_has_no_doc_archaeology`,
+`design_md_present_tense_anchors_present`,
+`prose_roundtrip_md_has_no_wunschdenken`) **PASS**; only
+`form_a_scalar_param_carveout_present_and_old_rule_absent` **FAILS**.
+("test result: FAILED. 4 passed; 1 failed".)
+
+---
+
+## Task 2: form_a.md — the four carve-out sites
+
+**Files:**
+- Modify: `crates/ailang-core/specs/form_a.md`
+
+Each step Reads nothing extra — the verbatim current text is given
+as `old` and the replacement as `new`. The implementer applies each
+as an exact string replacement.
+
+- [ ] **Step 1: Site 1 — `### Function` prose (lines 96-98)**
+
+Replace, verbatim:
+
+old:
+```
+`type` is a `(fn-type ...)` (possibly wrapped in `(forall ...)` for
+polymorphic defs). All parameters of a `(fn ...)` MUST carry a mode
+annotation — see *Modes* below.
+```
+
+new:
+```
+`type` is a `(fn-type ...)` (possibly wrapped in `(forall ...)` for
+polymorphic defs). A *heap-shaped* parameter or return of a
+`(fn ...)` MUST carry a mode annotation; a scalar (non-heap-shaped:
+`(con Int)`, `(con Bool)`, `(con Unit)`, `(con Str)`) takes **no**
+mode and is written bare — see *Modes* below.
+```
+
+- [ ] **Step 2: Site 2 — grammar-block comment (line 230)**
+
+Replace, verbatim (single line):
+
+old:
+```
+TYPE                ; implicit mode (DO NOT USE in new (fn ...) defs)
+```
+
+new:
+```
+TYPE                ; no mode — REQUIRED for scalars (Int/Bool/Unit/Str), rejected for heap-shaped
+```
+
+- [ ] **Step 3: Site 3 — "Schema invariants" item 1 (lines 347-352)**
+
+Replace, verbatim:
+
+old:
+```
+1. **Mode annotations on every `(fn ...)` parameter.** Every type in
+   the `(params ...)` clause of a `(fn ...)` definition's
+   `(fn-type ...)` MUST be wrapped in `(own T)` or `(borrow T)`. The
+   return type MUST also carry a mode whenever the type is heap-shaped
+   (i.e. anything other than `(con Int)`, `(con Bool)`, `(con Unit)`,
+   `(con Str)`). Implicit mode on a `(fn ...)` def is rejected.
+```
+
+new:
+```
+1. **Mode annotations on every heap-shaped `(fn ...)` parameter.** A
+   parameter type in the `(params ...)` clause of a `(fn ...)`
+   definition's `(fn-type ...)`, and the return type, MUST be wrapped
+   in `(own T)` or `(borrow T)` whenever the type is heap-shaped
+   (i.e. anything other than `(con Int)`, `(con Bool)`, `(con Unit)`,
+   `(con Str)`). A scalar (non-heap-shaped) parameter or return takes
+   **no** mode: write it bare, e.g. `(con Int)`. Scalars are
+   primitive value types, not linear resources; putting a mode on a
+   scalar makes the checker hold the primitive to linear discipline
+   (single use under `own`, no use while a `borrow` is live), so an
+   ordinary scalar reused in the body (`sample * sample`) trips a
+   body-pointing `use-after-consume` / `consume-while-borrowed`
+   rather than a mode error. Implicit (omitted) mode on a
+   *heap-shaped* `(fn ...)` parameter or return is rejected.
+```
+
+- [ ] **Step 4: Site 4 — Pitfalls bullet (lines 381-383)**
+
+Replace, verbatim:
+
+old:
+```
+- **Forgetting mode annotations.** `(fn-type (params (con List)) ...)`
+  is accepted by the parser but rejected by the checker. Wrap every
+  `(fn ...)` parameter in `(own ...)` or `(borrow ...)`.
+```
+
+new:
+```
+- **Forgetting mode annotations on a heap-shaped parameter.**
+  `(fn-type (params (con List)) ...)` is accepted by the parser but
+  rejected by the checker. Wrap every *heap-shaped* `(fn ...)`
+  parameter in `(own ...)` or `(borrow ...)`.
+- **Putting a mode on a scalar parameter.** The inverse trap:
+  `(fn-type (params (own (con Int))) ...)` is wrong — scalars
+  (`Int`/`Bool`/`Unit`/`Str`) take no mode, write them bare
+  `(con Int)`. A mode on a scalar makes the checker treat the
+  primitive as a linear resource, so an ordinary reuse trips a
+  body-pointing `use-after-consume` / `consume-while-borrowed`
+  instead of pointing at the signature.
+```
+
+- [ ] **Step 5: Run the pin — form_a.md half now GREEN, DESIGN half still RED**
+
+Run: `cargo test -p ailang-core --test docs_honesty_pin form_a_scalar_param_carveout_present_and_old_rule_absent`
+
+Expected: still **FAIL**, but now the *only* failing assertion is the
+last one — `DESIGN.md §Embedding ABI (M1) must mirror the canonical
+bare-scalar export-param rule` (the four form_a.md ABSENT + four
+form_a.md PRESENT assertions now all pass; DESIGN.md is edited in
+Task 3). If any form_a.md assertion still fails, an exact-string
+replacement above did not match — re-read the named line range and
+fix the replacement, do not weaken the assertion.
+
+- [ ] **Step 6: Confirm spec_drift.rs is unaffected (it is not a lockstep partner)**
+
+Run: `cargo test -p ailang-core --test spec_drift`
+
+Expected: **PASS**, all 8 tests
+(`spec_mentions_every_term_variant`,
+`spec_mentions_every_pattern_variant`,
+`spec_mentions_every_type_variant`,
+`spec_mentions_every_literal_variant`,
+`spec_mentions_every_def_kind`, `spec_mentions_mode_keywords`,
+`spec_mentions_tail_variants`, `spec_mentions_suppress_clause`).
+`spec_mentions_mode_keywords` pins only the bare `(own` / `(borrow`
+tokens, which the carve-out keeps; this run confirms the recon
+finding that no `spec_drift.rs` assertion couples to the altered
+text.
+
+---
+
+## Task 3: DESIGN.md §"Embedding ABI (M1)" mirror
+
+**Files:**
+- Modify: `docs/DESIGN.md:2285`
+
+- [ ] **Step 1: Insert the canonical bare-scalar export-param example**
+
+In `docs/DESIGN.md`, the §"Embedding ABI (M1)" scalar-constraint
+paragraph ends at line 2285 (`The value/record layout freeze is
+M3.`), followed by a blank line (2286) and `## Data model` (2287).
+
+Replace, verbatim:
+
+old:
+```
+change this C signature; do not treat the M1 signature as frozen.
+The value/record layout freeze is M3.
+
+## Data model
+```
+
+new:
+```
+change this C signature; do not treat the M1 signature as frozen.
+The value/record layout freeze is M3.
+
+Export parameters are written **bare**: a scalar type carries no
+`own`/`borrow` mode (modes apply only to heap-shaped types, which the
+scalar-only rule above forbids at an export boundary anyway). The
+canonical M1 export shape:
+
+```
+(fn step
+  (export "backtest_step")
+  (type
+    (fn-type
+      (params (con Int) (con Int))
+      (ret (con Int))))
+  (params state sample)
+  (body
+    (app + state (app * sample sample))))
+```
+
+## Data model
+```
+
+(This Form-A snippet is the `step` fn of the public
+`examples/embed_backtest_step.ail` corpus fixture — recon confirmed
+lines 3-11 — so the example is corpus-grounded, not minted.)
+
+- [ ] **Step 2: Run the pin — now fully GREEN**
+
+Run: `cargo test -p ailang-core --test docs_honesty_pin form_a_scalar_param_carveout_present_and_old_rule_absent`
+
+Expected: **PASS**. All ABSENT + PRESENT assertions hold.
+
+- [ ] **Step 3: Full docs_honesty_pin suite GREEN**
+
+Run: `cargo test -p ailang-core --test docs_honesty_pin`
+
+Expected: **PASS**, "test result: ok. 5 passed; 0 failed" (the four
+pre-existing tests + the new carve-out pin).
+
+---
+
+## Task 4: Regression gate — zero behavioural drift
+
+**Files:** (none — verification only)
+
+- [ ] **Step 1: Full `ailang-core` test suite**
+
+Run: `cargo test -p ailang-core`
+
+Expected: **PASS**, no test regressed. In particular `spec_drift`
+(8) and `docs_honesty_pin` (5) green; all pre-existing `ailang-core`
+tests green. Record the total ("N passed; 0 failed").
+
+- [ ] **Step 2: Workspace-wide no-behavioural-drift assertion**
+
+This iteration changes only two docs and adds one test — no
+language / checker / codegen byte changes. The full workspace suite
+must therefore not lose any passing test.
+
+Run: `cargo test --workspace 2>&1 | grep -E "test result:" | awk '{p+=$4} END {print "TOTAL_PASSED="p}'`
+
+Expected: `TOTAL_PASSED=` a number **≥ the count on `main` HEAD before
+this iteration** (the only delta is **+1**, the new
+`form_a_scalar_param_carveout_present_and_old_rule_absent`). If the
+total is lower than the pre-iteration baseline, a pre-existing test
+broke — STOP and investigate; a docs+pin iteration cannot regress a
+behavioural test, so any drop is a real problem, not an expected
+cost. (Unfiltered suite + explicit pass-count per planner Step-5
+item 8 — "nothing ran" cannot masquerade as "nothing regressed".)
+
+- [ ] **Step 3: Confirm zero source-code change**
+
+Run: `git diff --stat -- crates/ailang-check crates/ailang-codegen crates/ailang-core/src crates/ailang-surface`
+
+Expected: **empty output** (no diff). The only modified paths are
+`crates/ailang-core/specs/form_a.md`, `docs/DESIGN.md`, and
+`crates/ailang-core/tests/docs_honesty_pin.rs`. Any source-code diff
+under those crate `src/` trees is out of scope for this tidy and a
+defect — STOP.
+
+---
+
+## Self-review (planner Step 5)
+
+1. **Spec coverage:** [friction] + [spec_gap]#1 both resolved —
+   form_a.md carve-out (Task 2, four sites) + DESIGN.md mirror
+   (Task 3) + anti-regression pin (Task 1). Roadmap entry's
+   "symmetrically with the existing return-type carve-out" satisfied
+   (item 1 new text scopes params to heap-shaped exactly as the
+   pre-existing return-type clause does). ✔
+2. **Placeholder scan:** no "TBD/TODO/implement later/similar to/add
+   appropriate". The literal string `; no mode — REQUIRED for
+   scalars …` and the test phrases are content, not placeholders. ✔
+3. **Type/name consistency:** test fn
+   `form_a_scalar_param_carveout_present_and_old_rule_absent` named
+   identically in Task 1 Step 2/3, Task 2 Step 5, Task 3 Step 2.
+   `FORM_A_SPEC`, `norm`, `read` match the actual file. ✔
+4. **Step granularity:** every step is one exact replacement or one
+   command, 2-5 min. ✔
+5. **No commit steps:** none. ✔
+6. **Pin/replacement substring contiguity:** the pin `norm()`s both
+   docs and every asserted substring is written single-spaced; the
+   `norm()` whitespace-collapse **structurally discharges** the
+   line-wrap family (the docs-honesty-lint precedent's `norm()` is
+   reused verbatim, not a fresh keep-on-one-line constraint). Every
+   PRESENT substring appears single-spaced-contiguously inside the
+   exact `new` replacement bodies in Tasks 2–3 (verified: e.g. "A
+   scalar (non-heap-shaped) parameter or return takes **no** mode:
+   write it bare, e.g. `(con Int)`." is one clause in the Task 2
+   Step 3 `new` block; line-wrap between "takes" and "**no**" is
+   collapsed by `norm()`). Every ABSENT substring is verbatim
+   contiguous in the corresponding `old` block and verbatim **gone**
+   from the `new` block. ✔
+7. **Compile-gate vs. deferred-caller ordering:** N/A — no signature
+   change, no crate-wide compile break; the only Rust change is one
+   additive `#[test]` + one `use`. Task ordering is RED-pin → doc
+   edits → green, the docs-honesty-lint pattern. ✔
+8. **Verification-command filter strings resolve:** `--test
+   docs_honesty_pin` and `--test spec_drift` are real test-target
+   files (recon-confirmed); the filter
+   `form_a_scalar_param_carveout_present_and_old_rule_absent` is the
+   exact name of the test added in Task 1 (not guessed from a
+   feature word). Task 4 Step 2 uses the **unfiltered** workspace
+   suite + an explicit `TOTAL_PASSED` count assertion so "0 ran"
+   cannot read as "0 regressed". ✔