diff --git a/docs/specs/0063-harden-ownership-analysis.md b/docs/specs/0063-harden-ownership-analysis.md new file mode 100644 index 0000000..b663e97 --- /dev/null +++ b/docs/specs/0063-harden-ownership-analysis.md @@ -0,0 +1,382 @@ +# Harden the ownership analysis for universal activation — Design Spec + +**Date:** 2026-06-01 +**Status:** Draft — awaiting user spec review +**Authors:** orchestrator + Claude + +## Goal + +Make the strict linearity analysis (`use-after-consume` / +`consume-while-borrowed`, `crates/ailang-check/src/linearity.rs`) +correct when it runs on **every** fn, not just the ~45 of 258 +fn-bearing modules that today carry an all-explicit signature. The +analysis is the core ownership-safety feature, yet its activation gate +(`linearity.rs:339`) skips any fn with a bare/`Implicit` param — so it +almost never runs. Deleting `ParamMode::Implicit` (#55, spec 0062) +turns it on universally, and two blind spots then surface as ~21% +false positives (38 of ~182 functional fixtures, measured 2026-06-01): + +1. **Value-type params** — an `Int`/`Bool`/`Float`/`Unit` param read + multiple times trips `use-after-consume`. Value types have no + refcount and are never consumed; multi-read is always legal. +2. **Function params applied in HOFs** — applying a function param + (`apply_thrice`, `map_int`, `fold_left`) trips `use-after-consume` + (own f-param) or `consume-while-borrowed` (borrow f-param). + Applying a function value reads it; it is a borrow, not a consume. + +This is the **precondition for #55**: spec 0062 §8 derives each +migrated parameter's mode from the consume analysis and asserts "the +corpus contains none [of the rejected shapes]". That assertion only +holds once these two blind spots are closed — otherwise the cutover +turns ~21% of the corpus red. Closing them is also independently +valuable: it makes the core ownership analysis sharp across the whole +codebase for the first time. + +The rationale anchors are `design/models/0008-ownership-totality.md` +§3.2 (value types are trivial-`own`; a value type "has nothing to +lend") and §4 (HOF mode slots — each canonical HOF applies its +function param, which is a read), plus the RC/uniqueness contract +`design/contracts/0008-memory-model.md`. The model is `status: Design +exploration`; its claims are validated against the live tool below +(Testing strategy), not assumed. + +### Scope decisions ratified here + +1. **`Str` is heap, not a value type, for consume-tracking.** The + model §1 calls `Str` "an RC-heap value"; codegen confirms it: + `drop.rs:490–492` lowers only `Int`/`Bool`/`Float`/`Unit` to + non-`ptr`, and `Str` lowers to `ptr` and is RC-`dec`'d. A `Str` + binder **can** be consumed (its slab freed) and a multi-consume + without `clone` is a genuine use-after-free. So the value-type + exemption covers exactly the **unboxed** set `{Int, Bool, Float, + Unit}` — narrower than `primitives::is_primitive_name`, which + includes `Str`. This divergence is deliberate and named: "primitive + zero-arity type constructor" (`is_primitive_name`, includes `Str`) + is a different predicate from "unboxed value type, no RC" + (`is_value_type`, excludes `Str`). + +2. **Applying a function value is a borrow.** A function value + (closure or fn-ref) applied at a call site is read, not moved; it + stays live for further applications and is dropped at scope close + like any other binder. Passing a function value **as an argument** + is unchanged — it follows the callee's `param_modes` (borrow-param + → borrow, own-param → consume), which `callee_arg_modes` already + resolves. The recursion-passing pattern (`map_int f t`) is then + consistent: `f` is borrowed for the application *and* borrowed for + the recursive hand-off when `map_int`'s f-param is `borrow`. + +### Out of scope + +- **#55 itself** — deleting `ParamMode::Implicit`, the schema/hash + reset, the parser/return changes. This spec only hardens the + analysis; it changes no schema, resets no hash, and is testable + today against explicit-mode fns (Testing strategy). +- **Value-typed `let`-binders.** The exemption is driven from the + binder's type where it is locally available: parameter signatures, + ctor field types (pattern binders), and `lam` typed-params. A + `let`-binder's type is inferred, not annotated, and the linearity + walk is a post-typecheck pass that does not re-run inference, so a + value-typed `let`-binder stays conservatively tracked as heap. This + is soundness-safe (it can only keep the analysis *over-strict* — a + potential false positive — never miss a real consume) and is not a + measured corpus shape. Lifting it would mean threading a full + binder→type table out of the type-checker; deferred until a corpus + shape demands it. +- **The `over-strict-mode` lint's `Str` treatment.** That lint uses + `is_heap_type` (which routes through `is_primitive_name`, so it + treats `Str` as non-heap). Whether that is correct for the lint is a + separate question; this spec does not touch `is_heap_type` or the + lint. + +## Architecture + +Two orthogonal, additive changes inside `linearity.rs`, plus one new +shared predicate. No schema change, no new `Type` variant, no hash +shift, no codegen change. The analysis stays a pure diagnostic pass. + +**New shared predicate (`crates/ailang-core/src/primitives.rs`):** + +`is_value_type(name) -> bool` returns `true` for exactly `Int` / +`Bool` / `Float` / `Unit`. It is the "unboxed, no-RC" predicate, as +distinct from `is_primitive_name` (which also returns `true` for +`Str`). Both live in the same module so the divergence is visible in +one place, and a unit test pins that `is_value_type` ⊊ +`is_primitive_name`, the sole difference being `Str`. + +**Fix 1 — value-type exemption (`linearity.rs`):** + +A binder of a value type is never consumed. `BinderState` gains an +`is_value: bool` flag; `use_var` skips all consume bookkeeping (no +`consumed = true`, no `consume-while-borrowed`) when it is set. The +flag is set from the binder's locally-available type at three +introduction sites: + +- **parameters** — `check_fn` already has `param_tys`; a param whose + type is a value type starts with `is_value = true`; +- **pattern binders** — `walk_arm` looks the binder's type up in the + ctor field types (the `ctors` map, now threaded into the `Checker`) + and sets `is_value` accordingly; +- **`lam` typed-params** — `Term::Lam` carries each param's declared + type; a value-typed lam param starts with `is_value = true`. + +Because the flag rides on `BinderState`, it follows the existing +save/restore scoping (`with_binder`) automatically and survives the +branch/match `merge_states` (a binder's value-ness is invariant across +branches, so the merge keeps it). + +**Fix 2 — application is a borrow (`linearity.rs`):** + +`Term::App` walks its callee in `Position::Borrow` instead of +`Position::Consume` (`linearity.rs:433`). For a global fn-ref callee +this is a no-op (globals are not tracked binders, so `use_var` returns +early either way); for a tracked function-typed binder (a HOF param, +or a `let`/`lam`-bound function value) it stops the application from +consuming the binder. The callee's `consumed` flag is still checked, +so applying an already-consumed function value still fires +`use-after-consume`. + +## Concrete code shapes + +### RED fixtures (check-error today, clean post-fix) + +These are the feature-acceptance evidence: the post-#55 authoring +surface forces every value-type and function-type slot to carry a mode +(`(own …)` / `(borrow …)`), and an LLM author writing the natural form +below trips a false positive **today** — exactly the friction this +cycle removes. All three are testable now against explicit-mode fns, +without #55, because an all-explicit signature already activates the +analysis. Live `ail check` traces (`target/debug/ail`, run +2026-06-01) are in the Testing section. + +**Class 1 — value-type param read multiple times** (`(borrow (con +Int))` is an error per model §3.2, so a multi-read `Int` param *must* +be `own`): + +```ail +(module fp_value + (fn sum_explicit + (doc "value-type param read multiple times") + (type (fn-type (params (own (con Int))) (ret (own (con Int))))) + (params n) + (body (if (app eq n 0) 0 (app + n (app sum_explicit (app - n 1)))))) + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body (app print (app sum_explicit 10))))) +``` + +**Class 2a — own function param applied multiple times:** + +```ail +(module fp_hof + (fn apply_thrice + (doc "apply a function param three times") + (type (fn-type + (params (own (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con Int))) + (ret (own (con Int))))) + (params f x) + (body (app f (app f (app f x))))) + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body (app print (app apply_thrice (lam (params (typed y (con Int))) (ret (con Int)) (body (app + y 1))) 0))))) +``` + +**Class 2b — recursive HOF, borrow function param applied + passed:** + +```ail +(module fp_map + (data IntList + (doc "boxed list") + (ctor Nil) + (ctor Cons (con Int) (con IntList))) + (fn map_int + (doc "recursive HOF: f applied AND passed to the recursive call") + (type (fn-type + (params (borrow (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con IntList))) + (ret (own (con IntList))))) + (params f xs) + (body (match xs + (case (pat-ctor Nil) (term-ctor IntList Nil)) + (case (pat-ctor Cons h t) (term-ctor IntList Cons (app f h) (app map_int f t))))))) +``` + +### Must-stay-RED fixture (a genuine consume, not exempted) + +The exemption must not silence a real heap multi-consume. This +boxed-ADT param is consumed twice with no `clone`; it is a real +`use-after-consume` and **stays** an error after the fix (proves the +exemption is type-gated to value types, not blanket): + +```ail +(module real_consume + (data Box + (doc "heap cell") + (ctor Box (con Int))) + (data Pair + (doc "two boxes") + (ctor Pair (con Box) (con Box))) + (fn dup + (doc "MUST STAY an error: a heap param consumed twice without clone") + (type (fn-type (params (own (con Box))) (ret (own (con Pair))))) + (params b) + (body (term-ctor Pair Pair b b)))) +``` + +### Secondary: implementation shapes (before → after) + +*Supporting detail, not the headline.* + +**`crates/ailang-core/src/primitives.rs` — new predicate:** + +```text +after (added alongside is_primitive_name): + /// Unboxed value type — no RC, no heap slab. Narrower than + /// `is_primitive_name`: `Str` is a primitive zero-arity ctor but is + /// heap-allocated (`ptr`, RC'd), so it is NOT a value type. + pub fn is_value_type(name: &str) -> bool { + matches!(name, "Int" | "Bool" | "Float" | "Unit") + } +``` + +**`crates/ailang-check/src/linearity.rs` — `BinderState`:** + +```text +before: struct BinderState { consumed: bool, borrow_count: u32 } +after: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool } + // is_value: a value-typed binder is never consumed. +``` + +**`linearity.rs` — `use_var` consume arm:** + +```text +before (Position::Consume): + if state.borrow_count > 0 { ...consume-while-borrowed...; return; } + state.consumed = true; +after: + if state.is_value { return; } // value types are never consumed + if state.borrow_count > 0 { ...consume-while-borrowed...; return; } + state.consumed = true; +``` + +**`linearity.rs` — `Term::App` callee walk (`:433`):** + +```text +before: self.walk(callee, Position::Consume); // "the function value is consumed" +after: self.walk(callee, Position::Borrow); // applying a function value reads it + // global fn-refs are untracked → no-op; a tracked function-typed + // binder (HOF param) is no longer consumed by application. +``` + +**`linearity.rs` — param/pattern/lam `is_value` seeding:** `check_fn` +sets `is_value` from `param_tys[i]` (a `Type::Con` whose name +satisfies `is_value_type`); `walk_arm` threads the `ctors` map to type +each pattern binder; `Term::Lam` reads its typed-param types. All three +default `is_value = false` (heap, conservative) when the type is not a +value `Type::Con`. + +## Components + +- **`ailang-core::primitives`** — gains `is_value_type`; a unit test + pins it as the `Str`-excluding subset of `is_primitive_name`. +- **`ailang-check::linearity`** — `BinderState.is_value`; the `use_var` + consume short-circuit; the `App` callee borrow walk; `is_value` + seeding at param / pattern / lam introduction; `Checker` gains an + immutable `ctors` reference for pattern-binder typing. +- **`.ail` fixtures** — the three RED fixtures plus the must-stay-RED + heap-consume fixture, under `examples/`. + +No change to: the schema (`ParamMode`, `Type::Fn`), the parser, the +printer, codegen, the runtime, the `over-strict-mode` lint, or +`is_heap_type`. + +## Data flow + +**Value exemption.** The linearity walk does not infer types; it reads +them where the source already pins them. A parameter's type is on the +signature (`param_tys`); a pattern binder's type is the corresponding +ctor field type (`ctors[ctor].fields[i]`); a `lam` param's type is its +`(typed x T)` annotation. Each of these is a `Type::Con { name }` for a +value type, and `is_value_type(name)` decides the flag. The flag is +immutable per binder and rides `BinderState`, so lexical scoping +(`with_binder`) and branch merging (`merge_states`) carry it without +special handling. A binder whose type is *not* a locally-pinned value +`Type::Con` (a heap ADT, `Str`, a type variable, a `let`-binder) +defaults to `is_value = false` and is tracked exactly as today. + +**Application borrow.** `Term::App` already distinguishes callee from +args: args go through `callee_arg_modes` to pick up per-position +modes, while the callee was walked as `Consume`. Switching the callee +to `Borrow` aligns it with the semantics — a function value is read by +application — and leaves the arg path untouched, so passing a function +value to an `own` param still consumes it and to a `borrow` param +still borrows it. The `consumed`-check in `use_var` still runs in +`Borrow` position, so applying an already-consumed function value is +still caught. + +## Error handling + +No new diagnostic codes. The two existing codes +(`use-after-consume`, `consume-while-borrowed`) fire on a strictly +*smaller, more correct* set: they no longer fire on value-type +multi-reads or on function-param applications, and they continue to +fire on genuine heap multi-consume (the must-stay-RED fixture) and on +applying an already-consumed function value. The change is a precision +improvement to existing diagnostics, not a new check surface. + +## Testing strategy + +Live `ail check` traces (run 2026-06-01, `target/debug/ail`) — the +state **today**, before the fix: + +```text +fp_value.ail : exit 1 error: [use-after-consume] sum_explicit: `n` ... +fp_hof.ail : exit 1 error: [use-after-consume] apply_thrice: `f` ... (x2) +fp_map.ail : exit 1 error: [consume-while-borrowed] map_int: `f` ... +real_consume.ail : exit 1 error: [use-after-consume] dup: `b` ... +``` + +- **RED→GREEN fixtures.** `fp_value`, `fp_hof`, `fp_map` land under + `examples/`; each asserts the named diagnostic fires **today** and + is **clean** after the fix (exit 0). These are the RED side of the + two blind-spot fixes. +- **Stays-RED fixture.** `real_consume` asserts the heap + `use-after-consume` still fires after the fix — the exemption is + type-gated, not blanket. +- **Unit test on the predicate.** `is_value_type` agrees with + `is_primitive_name` on every name except `Str`, where + `is_value_type` is `false` and `is_primitive_name` is `true`. +- **Linearity unit tests.** The in-source `#[cfg(test)] mod tests` in + `linearity.rs` gains cases: a value-typed param multi-read produces + no diagnostic; an own/borrow function-param application produces no + diagnostic; a heap-typed param multi-consume still produces + `use-after-consume`. +- **Full corpus regression.** `cargo test --workspace` stays green, + and the existing `examples/` typecheck/codegen suite is the net for + "the exemption silenced nothing it should not have". Per the + typed-MIR re-synth strictness memory, run the whole workspace suite, + not just e2e. +- **Regression scripts.** `bench/check.py` and + `bench/compile_check.py` stay green (the analysis is diagnostic-only; + no compile-baseline shift is expected). + +## Acceptance criteria + +1. `is_value_type` exists in `ailang-core::primitives`, returns `true` + for exactly `{Int, Bool, Float, Unit}`, and a unit test pins it as + the `Str`-excluding subset of `is_primitive_name`. +2. `fp_value`, `fp_hof`, `fp_map` check **clean** (exit 0) after the + fix; each shipped as an `examples/` fixture asserting its today→post + transition. +3. `real_consume` still fails with `use-after-consume` after the fix. +4. `apply_thrice`-style own-function-param application and + `map_int`-style borrow-function-param application+recursion both + check clean. +5. The value exemption is type-gated: an in-source unit test shows a + heap param multi-consume still produces `use-after-consume` while a + value param multi-read produces none. +6. `cargo test --workspace` green; `bench/check.py` and + `bench/compile_check.py` green. +7. No change to `ParamMode`, `Type::Fn`, the parser/printer, codegen, + the runtime, `is_heap_type`, or the `over-strict-mode` lint (grep / + diff clean).