From c8b765614d270755107bebc9d90ed06106c3a42b Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 14:21:26 +0200 Subject: [PATCH] spec: eliminate the Implicit ownership default (0062) Design spec for #55, superseding #54. Deletes ParamMode::Implicit in a single cutover -> binary {Own, Borrow}; no defaulted ownership mode survives on any fn-type slot, authored or compiler-synthesised. The grounding pass corrected the central architecture claim. Both #55 and the first draft assumed a new return-provenance check was needed to reject an own-return aliasing a borrowed binder, "silently accepted today". Running the candidate fixtures through the live `ail check` falsified that: consume-while-borrowed already rejects all three provenance paths -- direct passthrough, let-indirection, and borrow escaping into a returned constructor (regime A). Own-return soundness and regime A are already-green properties. The cutover therefore adds exactly one new check (borrow-return rejection) plus one signature-level reject (borrow-over-value), not two new provenance analyses. Scope decisions ratified: keyword stays verbal (own/borrow), ParamMode keeps its name; totality is strict including value-type slots (every slot moded, (own value) trivial, (borrow value) an error, bare slot a parse error) so an LLM author needs no heap/value knowledge. The leak fix (spec 0061 symptom) falls out of Implicit->Own at the synthesis sites: the old typechecker made Implicit and Own indistinguishable (mode_eq), so setting Own changes no typecheck outcome -- it only flips the codegen dec gate from skip to emit. Out of scope: re-enabling borrow-returns (needs the escape/liveness axis), multi-return, mode polymorphism. grounding-check: PASS (7 assumptions ratified against named green tests; all fenced ail blocks validated against the live tool). refs #55 --- docs/specs/0062-eliminate-implicit-mode.md | 490 +++++++++++++++++++++ 1 file changed, 490 insertions(+) create mode 100644 docs/specs/0062-eliminate-implicit-mode.md diff --git a/docs/specs/0062-eliminate-implicit-mode.md b/docs/specs/0062-eliminate-implicit-mode.md new file mode 100644 index 0000000..11d9112 --- /dev/null +++ b/docs/specs/0062-eliminate-implicit-mode.md @@ -0,0 +1,490 @@ +# Eliminate the Implicit ownership default — Design Spec + +**Date:** 2026-06-01 +**Status:** Draft — awaiting user spec review +**Authors:** orchestrator + Claude + +## Goal + +Delete `ParamMode::Implicit` from the language in a single cutover. +`ParamMode` becomes binary `{Own, Borrow}`. After this cycle no +fn-type slot — parameter or return, authored or compiler-synthesised +— carries a defaulted ownership mode. Every authored slot reads +`(own T)` or `(borrow T)`; every compiler-synthesised fn-type carries +a concrete `Own`. + +This closes #55 and supersedes #54. It also fixes the typed-MIR +fieldtest leak (spec 0061): the leak is the observable symptom of the +real defect, which is that `Implicit` is read two ways — the +typechecker treats `Implicit ≡ Own` (`mode_eq`, +`crates/ailang-core/src/ast.rs:894`), while codegen omits the caller +`dec` for it (`crates/ailang-codegen/src/drop.rs:476`), so the same +fn-type means two different things. Removing the variant removes the +fork. + +The design rationale is `design/models/0008-ownership-totality.md` +§§1–3 (the totality principle: a default cannot be half-removed) and +the 2026-06-01 design review (full totality is not atomically +shippable *because of* borrow-returns; this spec carves them out). The +model is `status: Design exploration` — its claims are validated +against the live tool by this spec, not assumed. + +### What the grounding work changed in this spec + +Both #55 and the first draft of this spec assumed a **new +return-provenance check** was needed to reject an `own` return that +aliases a borrowed binder (the `fn f(x: (borrow T)) -> (own T) { x }` +passthrough), and that this passthrough is "silently accepted today". +Running the candidate fixtures through the live `ail check` (traces in +the Testing section) **falsified that assumption**: the existing +`consume-while-borrowed` analysis already rejects all three provenance +paths — + +- direct passthrough `(body b)` → rejected today; +- let-indirection `(body (let y b y))` → rejected today; +- borrow escaping into a returned constructor `(body (term-ctor Wrap Wrap b))` + (regime A, model §5.1) → rejected today. + +A borrow parameter holds a live borrow for the whole function body, so +*any* use of it at a consume position (own-return, ctor arg, own-param +arg) trips `consume-while-borrowed`. **Own-return soundness and regime +A are therefore already-green properties, not new work.** The cutover +adds exactly **one** new check (borrow-return rejection) plus one +signature-level reject (borrow-over-value), not two new provenance +analyses. This is the central correction the grounding pass produced. + +### Scope decisions ratified here + +1. **Keyword form stays verbal** (`own` / `borrow`, today's surface). + No adjectival rename, no keyword churn. The internal type keeps the + name `ParamMode`. *(User decision, 2026-06-01.)* + +2. **Totality is strict, including value-type slots.** Every fn-type + slot carries `(own T)` or `(borrow T)`, value types included. + `(own (con Int))` is trivial-own (no inc/dec ever emitted); + `(borrow (con Int))` is a check error (§3.2 of the model). Bare type + in a fn-type slot is rejected by the parser everywhere. Rationale: + this gives an LLM author a heap/value-agnostic rule — *always write + a mode; `own` is always safe; reach for `borrow` only when you want + a heap view* — so the author never needs to know which types are + boxed. The alternative (bare = trivial-own for value types only) + forces exactly that heap/value classification on every slot and is + rejected. + +### Out of scope + +- **Re-enabling borrow-returns.** `(ret (borrow T))` is a check error + in this cut, with a diagnostic naming the liveness/escape gap. The + escape/liveness axis that would make borrow-returns sound is separate + later work (model §5.2, §8). +- **Multi-return** (model §5.3, §7-Q4). +- **Mode polymorphism** (model §4). A type-variable slot takes a + concrete `own`/`borrow`; the surface already cannot express a mode + variable, so no change is needed. + +## Architecture + +The cutover has four schema/representation edits, one new check, one +new signature-level reject, and one corpus migration. They land +together: a deleted `Implicit` means returns must be `own`/`borrow`, +every checked-in `.ail` source carries `Implicit` slots today, and the +hash shift is one-time for the whole corpus. + +**Schema / representation (`crates/ailang-core`):** + +1. `ParamMode` loses the `Implicit` variant and `#[derive(Default)]` — + ownership has no default, so the type has no default. +2. `Type::Fn::param_modes` / `ret_mode` lose their `skip_serializing_if` + elision. Modes are always serialised. This is the one-time + canonical-JSON hash shift for the whole corpus. +3. `mode_eq` (the `Implicit ≡ Own` interchange) is deleted; mode + equality becomes structural `==`. +4. `Type::fn_implicit` is renamed `Type::fn_owned` and sets `Own` on + every synthesised slot (justified in Data flow). + +**New check (`crates/ailang-check`):** + +5. **Borrow-return rejection.** `(ret (borrow T))` is a check error + with a diagnostic pointing at the out-of-scope liveness axis. This + is the *only* genuinely new ownership analysis in the cycle. + +**New signature-level reject (`crates/ailang-check`):** + +6. **Borrow-over-value.** `(borrow value-type)` in any slot is a check + error, fired on the signature before body analysis so it does not + depend on the body tripping `consume-while-borrowed`. Specified by + model §3.2; this cycle makes it reachable now that every value slot + is moded. + +**Parser (`crates/ailang-surface`):** + +7. A bare type in a fn-type slot is a parse error. The slot grammar + becomes `fn-type-param ::= "(" ("borrow" | "own") type ")"` — the + bare-`type` alternative is removed. + +**Migration:** + +8. Every `.ail` source (prelude, kernel `raw_buf`, the ~208 example + fixtures) gets explicit modes. Param modes are derived from the + existing uniqueness/consume analysis (consumed ⇒ `own`, read-only ⇒ + `borrow`; value types always `own`); return modes are `own` + everywhere (no borrow-return survives). The hash-pin tests reset + their pinned hashes once. + +**Already-green, pinned not built:** own-return provenance and regime A +are enforced by the existing `consume-while-borrowed` check. The cycle +adds regression pins (Testing) proving the schema deletion does not +weaken them, but builds no new analysis for them. + +## Concrete code shapes + +Every block below was run through the configured `ail check`; the +exit-code traces are in the Testing section. + +### User-facing: the post-cutover authoring surface (checks clean today) + +The canonical form an LLM author writes after this cycle. Every slot +carries a mode; value-type slots use trivial-`own`: + +```ail +(module ownership_total + + (data List + (doc "Monomorphic singly-linked Int list — boxed, recursive.") + (ctor Nil) + (ctor Cons (con Int) (con List))) + + (fn list_length + (doc "Borrow the list, count its elements.") + (type + (fn-type + (params (borrow (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) + (app + 1 (app list_length t)))))) + + (fn sum_list + (doc "Consume the list, sum its elements.") + (type + (fn-type + (params (own (con List))) + (ret (own (con Int))))) + (params xs) + (body + (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) + (app + h (app sum_list t)))))) + + (fn main + (doc "Build [1,2,3]; print length (3) then sum (6).") + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body + (let xs + (term-ctor List Cons 1 + (term-ctor List Cons 2 + (term-ctor List Cons 3 + (term-ctor List Nil)))) + (seq + (seq (app print (app list_length xs)) (do io/print_str "\n")) + (seq (app print (app sum_list xs)) (do io/print_str "\n"))))))) +``` + +This is the feature-acceptance evidence: an LLM author writes a mode +on every slot, never a bare type, and never needs to know that `Int` +is unboxed and `List` is boxed — `own` is the always-safe choice, +`borrow` the deliberate heap-view on `list_length`'s parameter. + +### New RED fixture: borrow-return rejection + +The one new check. Wellformed today (no return check exists), a check +error post-cutover; the diagnostic names the liveness gap and the +out-of-scope status: + +```ail +(module borrow_return_reject + + (data Box + (doc "Heap cell holding one Int.") + (ctor Box (con Int))) + + (fn peek + (doc "MUST FAIL post-cutover: borrow-return is refcount-invisible and can outlive its source; re-enabling needs the escape axis.") + (type + (fn-type + (params (own (con Box))) + (ret (borrow (con Box))))) + (params b) + (body b))) +``` + +### New RED fixture: borrow-over-value + +Wellformed today, a signature-level check error post-cutover. The body +ignores the param so the rejection is unambiguously about the +signature, not a body-level consume: + +```ail +(module borrow_value_reject + + (fn ignore + (doc "MUST FAIL post-cutover: borrow over a value type is meaningless.") + (type + (fn-type + (params (borrow (con Int))) + (ret (own (con Int))))) + (params n) + (body 0))) +``` + +### New parser reject: bare type in a fn-type slot + +Wellformed today (bare = `Implicit`), a parse error post-cutover: + +```ail +(module bare_slot_reject + + (fn id + (doc "MUST FAIL post-cutover: bare `(con Int)` slot carries no mode.") + (type + (fn-type + (params (con Int)) + (ret (con Int)))) + (params x) + (body x))) +``` + +### Already-green regression pin: own-return provenance + regime A + +These are **rejected today** by `consume-while-borrowed`. They are +pinned as regressions to prove the schema deletion does not weaken the +existing guard — not as new checks: + +```ail +(module own_return_provenance_reject + + (data Box + (doc "Heap cell holding one Int.") + (ctor Box (con Int))) + + (fn passthrough + (doc "Already rejected today (consume-while-borrowed): own-return aliases a borrowed binder.") + (type + (fn-type + (params (borrow (con Box))) + (ret (own (con Box))))) + (params b) + (body b))) +``` + +### North-star: the fixed leak + +`examples/rc_let_implicit_returning_app.ail` asserts `live=1` today as +an intentional Implicit back-compat lane. Post-cutover its return is +`own`, the caller `dec` is emitted, and the property flips to `live=0`. +The fixture header and its property-3 assertion are rewritten from +"Implicit leaks by design" to "own-return frees correctly". + +### Secondary: implementation shapes (before → after) + +*Supporting detail, not the headline.* + +**`crates/ailang-core/src/ast.rs` — `ParamMode`:** + +```text +before: + #[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)] + #[serde(rename_all = "lowercase")] + pub enum ParamMode { #[default] Implicit, Own, Borrow } + +after: + #[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] + #[serde(rename_all = "lowercase")] + pub enum ParamMode { + Own, // (own T) — caller transfers ownership; callee consumes + Borrow, // (borrow T) — caller retains ownership; callee may not consume + } + // no #[derive(Default)]: ownership has no default. +``` + +**`crates/ailang-core/src/ast.rs` — `Type::Fn` serde:** + +```text +before: + #[serde(default, skip_serializing_if = "all_implicit")] param_modes: Vec, + #[serde(default, skip_serializing_if = "ParamMode::is_implicit")] ret_mode: ParamMode, + +after: + param_modes: Vec, // always present, len == params.len() + ret_mode: ParamMode, // always present + // all_implicit / is_implicit helpers deleted. +``` + +**`crates/ailang-core/src/ast.rs` — `mode_eq` deleted:** + +```text +before: fn mode_eq(a, b) { Implicit and Own interchangeable; Borrow distinct } +after: removed; modes compared with derived PartialEq (a == b) +``` + +**`crates/ailang-core/src/ast.rs` — `fn_implicit` → `fn_owned`:** + +```text +before: pub fn fn_implicit(params, ret, effects) -> Type // sets Implicit +after: pub fn fn_owned(params, ret, effects) -> Type // sets Own + // 16 call sites updated; Own is correct by the Data-flow argument. +``` + +**`crates/ailang-codegen/src/drop.rs` — App ret-mode gate (`:467–478`):** + +```text +before: matches!(m, ParamMode::Own) with Implicit/Borrow → no dec (the leak) +after: matches!(m, ParamMode::Own) unchanged in form; the Implicit case no + longer exists, so every former-Implicit return now matches Own and is + dec'd. Comment updated to drop the Implicit back-compat language. +``` + +**`crates/ailang-surface/src/parse.rs` — slot grammar (`:32`, `parse_param_with_mode`):** + +```text +before: fn-type-param ::= type | "(" "borrow" type ")" | "(" "own" type ")" +after: fn-type-param ::= "(" "borrow" type ")" | "(" "own" type ")" + // bare type → ParseError (no mode on slot) +``` + +## Components + +- **`ailang-core::ast`** — the enum, the `Type::Fn` fields, the + constructor, equality. Blast-radius origin. +- **`ailang-surface::parse` / `print`** — slot grammar gains a reject + arm; printer drops the `Implicit` arm (`print.rs:360`). +- **`ailang-check::uniqueness` / `linearity`** — host the borrow-return + reject and the borrow-over-value reject (both signature inspections). + The migration mode-derivation reuses `consume_count`. No new + provenance analysis — `consume-while-borrowed` (`linearity.rs:1272`) + already covers own-return provenance and regime A. +- **`ailang-codegen::drop` / `lambda` / `match_lower` / `lib`** — every + `ParamMode::Implicit` match arm deleted; gate logic unchanged in form. +- **`.ail` corpus** — prelude, `raw_buf`, examples; mechanically + re-moded then reviewed. + +## Data flow + +**Why `Own` is correct for every synthesised slot (`fn_owned`).** +`Implicit` had two roles: the authoring default (bare type) and the +internal marker for fn-types the compiler builds (lambda types, builtin +signatures, inferred application results). The authoring role is +deleted. The synthesis role resolves to `Own` with no behaviour +change: the old typechecker made `Implicit` and `Own` indistinguishable +(`mode_eq` true for every `Implicit`/`Own` pairing), so every +synthesised fn-type was already semantically `Own` under typechecking — +no check ever depended on a slot being `Implicit` rather than `Own`. +Setting `Own` at synthesis changes no typecheck outcome. It changes +exactly one thing: the codegen gate (`drop.rs:476`) flips from "skip +the caller `dec`" to "emit it" for those former-`Implicit` returns — +precisely the leak fix. The synthesis sites do not need the consume +analysis (that is for *authored* params during migration); `Own` is +correct for them by construction. The corpus typecheck/codegen suite is +the regression net for this claim (Testing). + +**Migration mode-derivation.** For each authored param: run the +uniqueness pass, read `consume_count` — `> 0 ⇒ (own T)`, `== 0 ⇒ +(borrow T)` for heap types, `(own T)` for value types. For each return: +`(own T)` (no borrow-return survives; any borrow-passthrough body is +now rejected and must be restructured — and is already rejected today, +so the corpus contains none). Derived sources are reviewed by the +orchestrator before commit — the author owns the annotations; the +derivation is a drafting aid, not a surviving default. + +**Check flow for the new rejects.** Both the borrow-return reject and +the borrow-over-value reject are signature inspections on the fn-type, +fired before body dataflow — no new tracking. Own-return provenance and +regime A need no flow here: `consume-while-borrowed` already fires +because a borrow parameter's borrow is live across the whole body, so +any consume of it (return-as-own, ctor arg) is caught. Ctor args are +`Position::Consume` (`linearity.rs:527`), which is why regime A holds — +a borrowed value cannot escape into a returned constructor. + +## Error handling + +- **Bare slot (parse error).** `parse_param_with_mode` returns a + `ParseError` when a slot is a bare type, naming the slot and + requiring `(own …)` or `(borrow …)`. Rendered in AILang syntax. +- **Borrow-return (check error, new).** New `CheckError` variant. + States `(ret (borrow …))` is not permitted in this language version + and points at the liveness/escape axis — an honest "not yet". +- **Borrow-over-value (check error, new).** New `CheckError` variant. + Signature-level: borrow is meaningless over an unboxed value type. +- **Own-return provenance.** No new diagnostic — `consume-while-borrowed` + already covers it; its message is unchanged. + +Each new `CheckError` variant gets a stable code via the existing +`CheckError::code()` registry (the diagnostic registry — not a separate +doc list). + +## Testing strategy + +Live `ail check` traces of the spec's fixtures (run 2026-06-01, +`target/debug/ail`): + +```text +ownership_total.ail : exit 0 ok (surface checks + runs) +bare_slot_reject.ail : exit 0 (legal today; parser reject post-cutover) +borrow_return_reject.ail : exit 0 (legal today; new check post-cutover) +borrow_value_reject.ail : exit 0 (legal today; new sig reject post-cutover) +own_return_provenance_reject.ail : exit 1 error: [consume-while-borrowed] passthrough: `b` ... + let-indirection (let y b y) : exit 1 error: [consume-while-borrowed] f: `b` ... + ctor-escape (term-ctor Wrap b) : exit 1 error: [consume-while-borrowed] f: `b` ... (regime A) +``` + +- **New RED fixtures** (`borrow_return_reject`, `borrow_value_reject`, + `bare_slot_reject`) land under `examples/`, each asserting the + specific diagnostic fires post-cutover. These are the RED side of the + one new check, the one new signature reject, and the parser reject. +- **Already-green regression pins** (`own_return_provenance_reject` and + the let-indirection / ctor-escape variants) assert + `consume-while-borrowed` still fires after the schema deletion. They + protect the own-return-soundness and regime-A properties the cycle + relies on but does not build. +- **North-star leak flip.** `rc_let_implicit_returning_app.ail` and its + pin family (`crates/ail/tests/print_no_leak_pin.rs`) flip from + `live=1` to `live=0` under `AILANG_RC_STATS`. +- **Hash-pin reset.** `crates/ailang-core/tests/hash_pin.rs` and + `crates/ailang-surface/tests/prelude_module_hash_pin.rs` get their + pinned hashes regenerated once and re-asserted (memory: hash-pin + blast-radius audit — both sites). +- **Round-trip invariant.** `ailang-surface` round-trip tests stay + green with modes always present; add a case proving a bare-slot input + now fails to parse. +- **Synthesis-site behaviour.** The corpus typecheck/codegen suite is + the regression net for `fn_implicit → fn_owned`: if any synthesised + slot was not semantically `Own`, a test breaks. Green corpus ratifies + the Data-flow argument. +- **Full workspace suite**, not just e2e — typed-MIR re-synth + strictness (memory) means mode changes surface in `lower_to_mir` + re-unification; run `cargo test --workspace`. + +## Acceptance criteria + +1. `ParamMode` has exactly two variants `{Own, Borrow}`, no `Default`, + no `Implicit` anywhere in `crates/` (grep clean). +2. The parser rejects a bare type in any fn-type slot; round-trip tests + prove it. +3. `borrow_return_reject` and `borrow_value_reject` fail their checks + with the specified diagnostics; the post-cutover authoring-surface + module checks and runs clean. +4. The own-return-provenance / regime-A pins stay red + (`consume-while-borrowed` fires) after the deletion. +5. `rc_let_implicit_returning_app.ail` reports `live=0` under + `AILANG_RC_STATS` (leak fixed). +6. `cargo test --workspace` green, with hash-pins regenerated once and + re-asserted. +7. `design/contracts/0008-memory-model.md` sections describing + `Implicit` (`:180-182`, `:288-298`) are updated to the binary model + as part of this cycle (a contract change rides with the feature that + forces it).