Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

spec: harden the ownership analysis for universal activation (0063)

Browse Source 
Precondition for #55 (eliminate ParamMode::Implicit, spec 0062). The
strict linearity check (use-after-consume / consume-while-borrowed)
runs today only on the ~45 of 258 all-explicit-mode fns; deleting
Implicit turns it on universally and surfaces ~21% false positives in
two classes — value-type params (Int/Bool/Float/Unit, never consumed)
and applied function params in HOFs (application is a borrow).

Two design questions settled against the live tool, not the model:
- Str is heap, NOT a value type for consume-tracking. drop.rs:490-492
  lowers only Int/Bool/Float/Unit to non-ptr; Str is a ptr, RC-dec'd,
  so a multi-consume of Str without clone is a real use-after-free. The
  value-type set is the unboxed {Int,Bool,Float,Unit}, narrower than
  is_primitive_name (which includes Str).
- Applying a function value is a borrow; passing it as an arg follows
  callee param_modes (unchanged). The recursion-passing HOF pattern is
  then consistent under a borrow f-param.

All three false-positive classes reproduced today against explicit-mode
fns (testable without #55) and recorded as RED fixtures; a heap
double-consume fixture stays RED to prove the exemption is type-gated.
grounding-check PASS. refs #56
This commit is contained in:
Brummel
2026-06-01 15:29:12 +02:00
parent 6c351af169
commit 8cdac7ecef
1 changed files with 382 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/specs/0063-harden-ownership-analysis.md
+382
View File
@@ -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).