diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 2bbe70b..1b7a38b 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -6141,3 +6141,166 @@ informative — design discipline corrupts faster than I notice when I let "implementer-friendly" creep into the slot reserved for "language-honest". The CLAUDE.md rule exists so the next session catches this earlier. + +## Iter 18c.2 — linearity check + suggested_rewrites + +Pure diagnostic addition. New module `ailang-check::linearity` +walks every fn whose `param_modes` are all explicit (`Borrow` +or `Own`, no `Implicit`); tracks per-binder consume/borrow state +through the AST; emits `use-after-consume` and +`consume-while-borrowed` diagnostics with form-A +`suggested_rewrites`. No IR change, no codegen change, no runtime +change. Existing fixtures (all `Implicit`) untouched; the +all-explicit `borrow_own_demo` fixture passes the check +unchanged. + +### Activation gate + +The check is opt-in *by signature*: a fn has to have spelled +every param mode explicitly (none `Implicit`) and have at least +one param. Any `Implicit` in the signature skips the fn's body +entirely. This is the back-compat lane Decision 10 promised — +LLMs that want linearity guarantees opt in by writing modes; +hand-written or transitional code keeps the old behaviour. + +### Diagnostics + +Two codes, both at `Severity::Error`, both with +`ctx = {"binder": ""}`: + +- `use-after-consume` — a binder is referenced after a previous + reference already consumed it. Replacement: `(clone )` at + the *earlier* site, so the later site stays the unique + consume. + +- `consume-while-borrowed` — a binder is consumed while a borrow + of it is still live (a sibling subterm in the same call passed + it to a `Borrow` param earlier; or, for a `Borrow` parameter + of the enclosing fn, the caller's outer borrow is always live + for the body's whole duration). Replacement: `(clone )` at + the offending consume site. + +### Position model + +Each `Term::Var` occurrence is in either `Consume` or `Borrow` +position, computed from its parent term: + +- `App.callee` → Consume. +- `App.args[i]` → Borrow if the resolved callee type's + `param_modes[i] == Borrow`; otherwise Consume (Own / Implicit + / unknown all default to Consume). +- `Clone.value` → Borrow (clone reads + bumps RC, doesn't move). +- `Match.scrutinee` → Borrow. +- Everything else (`Let.value`, `If.cond`, `Ctor.args[*]`, + `Do.args[*]`, `Lam`-captures, …) → Consume. + +For `App` whose callee is a fn-typed `Var`: when an arg slot +takes a *bare* `Term::Var { name }` in Borrow position, we bump +`borrow_count[name]` *before* evaluating subsequent args, and +release after the call. So a sibling Consume of the same binder +within the same call triggers `consume-while-borrowed`. + +### `suggested_rewrites` + +New `Diagnostic` field, always serialised (`[]` when empty — +stable JSON shape for `ail check --json` consumers). Currently +populated only by the linearity codes; everything else emits +`[]`. Each `SuggestedRewrite` carries a free-form `description` +and a `replacement` string. The replacement is form-A AILang — +parseable by `ailang_surface::parse_term`, the new +single-term entrypoint added in this iter alongside the dual +`term_to_form_a`. The round-trip is a contract guarded by tests: +the workspace integration tests parse every emitted replacement +and panic if any fail. + +### Why a new `parse_term` / `term_to_form_a` pair + +Parser and printer previously only had whole-`Module` +entrypoints. The linearity check produces snippet-sized +suggestions, which forced either (a) ad-hoc string formatting +inside the check, or (b) a fully-fledged single-term +parser/printer pair. Choice (b) is right because the +`replacement` field is part of the diagnostic's *contract* — if +any future code path produces a string that the surface refuses +to parse, the round-trip test catches it before it ships. + +The pair is now public surface API of `ailang-surface` and is +the canonical way for any tool to produce form-A snippets that +round-trip cleanly. + +### Why gate on clean-typecheck before running + +`check_workspace` skips the linearity pass on any module that +already produced a typecheck diagnostic. Running on a partly- +defined IR (unresolved `Var` lookups, mismatched ctor arities) +would produce noise that competes with the upstream errors the +author actually has to fix first. Cleanly-typechecked modules +with at least one all-explicit fn are the surface this check is +designed to inspect. + +### Known false negatives (deferred to 18c.3) + +- **Missing-consume-of-Own.** An `Own` param matched by + `Term::Match` but never moved out of the body is not flagged. + Matching is a Borrow-position read by the position model; + catching "you declared `own`, you have to consume" requires a + must-consume analysis that the assignment kept out of scope. + 18c.3 will see it because uniqueness inference computes a + per-binder must-be-consumed bit anyway. + +- **Lam captures conservatively in Consume.** A `Term::Lam` body + is walked with each capture in Consume position; we don't + model "the closure borrows its capture for the closure's + lifetime". For 18c.2 this means closures over an explicit-mode + param effectively consume the param at the lam site, which + matches the conservative thing to flag if anyone tries to use + the param after closing over it. Full closure-borrow + discipline is 18c.3. + +- **Pattern bindings start fresh.** `Match` arm patterns bind + fresh names with default state; we don't propagate ownership + from the scrutinee into the pattern bindings. False positives + could only arise if a pattern re-binds a name already in scope + in the enclosing all-explicit fn — none in shipping fixtures. + +These three are deliberate scope cuts, not bugs. 18c.3's +uniqueness inference subsumes the first two by construction; the +third is rare enough that an explicit shadow-warning isn't worth +the schema cost. + +### Tests + +- `crates/ailang-check/src/linearity.rs` — 3 unit tests + (`explicit_fn_with_no_uses_is_clean`, `implicit_fn_is_exempt`, + `mixed_implicit_explicit_is_exempt`). +- `crates/ailang-check/tests/workspace.rs` — 3 integration tests + (`use_after_consume_on_own_param_is_reported`, + `consume_while_borrowed_in_sibling_arg_is_reported`, + `borrow_own_demo_is_linearity_clean`). Each negative test + asserts diagnostic kind, def, `ctx.binder`, AND that every + emitted `replacement` parses via `parse_term` (the contract + test). +- 1 unit test for `suggested_rewrites` JSON serialisation in + `diagnostic.rs`. + +`cargo build --workspace` clean, `cargo test --workspace` green. +E2E unchanged (52 → 52); ailang-check unit 34 → 38; ailang-check +integration 5 → 8. + +### Next + +Iter 18c.3: uniqueness inference + codegen `inc`/`dec` +emission. A dataflow over the AST computes, per binder, the +"unique" / "shared" status; codegen under `--alloc=rc` emits +`ailang_rc_inc` / `ailang_rc_dec` calls at the appropriate +seams (most notably: a single `inc` for every `Term::Clone` +inserted by 18c.2's suggested rewrites, and a `dec` at the last +use of each binder leaving scope). This is the iter where RC +actually starts collecting memory; 18b's leak-everything +behaviour ends here. + +The check from 18c.2 stays as the *user-visible* enforcement +surface; 18c.3's inference is internal codegen-side bookkeeping. +The two layers communicate only through the explicit +`Term::Clone` markers in the source — the linearity check +demands them, the codegen pass honours them.