# 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).