feat(check): harden the ownership analysis for universal activation (0063)

The strict linearity check (use-after-consume / consume-while-borrowed,
linearity.rs) runs today only on the ~45 of 258 all-explicit-mode fns;
its activation gate skips any fn with a bare/Implicit param. Deleting
ParamMode::Implicit (#55) would turn it on universally and surface ~21%
false positives in two classes. This closes both, making the core
ownership analysis sharp across the whole codebase for the first time —
the precondition for #55. Diagnostic-only: no schema, no hash, no
codegen change; the two existing diagnostic codes simply fire on a
smaller, more correct set.

Fix 1 — value-type exemption. A new is_value_type predicate
(ailang-core::primitives) names the unboxed set {Int,Bool,Float,Unit};
BinderState gains an is_value flag seeded from the binder's locally
available type (param signatures, ctor field types for pattern binders,
lam typed-params), and use_var short-circuits the Consume arm for it. A
value type has no refcount and is never consumed, so multi-read is
always legal.

  Str is deliberately NOT in the value set, though is_primitive_name
  includes it: 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. is_value_type is the Str-excluding
  subset of is_primitive_name, pinned by a unit test. is_heap_type and
  the over-strict-mode lint are left untouched (separate concern).

Fix 2 — application is a borrow. Term::App walks its callee in
Position::Borrow (was Consume). Applying a function value reads it; it
stays live for further applications. Global fn-refs are untracked
(no-op); a tracked function-typed binder (a HOF param) is no longer
consumed by application. This fixes both the own-f-param
use-after-consume and the borrow-f-param consume-while-borrowed in the
recursion-passing HOF shape (map_int f t). Passing a function value as
an arg is unchanged — it follows the callee param_modes.

Scope decision: value-typed let-binders stay conservatively tracked as
heap (their type is inferred, not annotated, and the linearity walk
does not re-run inference). This is soundness-safe — over-strict, never
unsound — and not a measured corpus shape; lifting it would need a full
binder->type table out of the type-checker.

Verification: all three false-positive classes reproduced today against
explicit-mode fns and shipped as RED->GREEN fixtures
(examples/fp_{value,hof,map}.ail); examples/real_consume.ail stays RED
(heap double-consume still fires) to prove the exemption is type-gated.
715 workspace tests green; bench/check.py 0/34 and bench/compile_check.py
0/24 regressed. merge_states carries is_value so the flag survives
branch merges. RED-first verified per task.

closes #56
This commit is contained in:
2026-06-01 15:38:32 +02:00
parent 47fb328aca
commit aaa70d4c35
7 changed files with 360 additions and 11 deletions
+33
View File
@@ -719,6 +719,39 @@ fn borrow_own_demo_is_linearity_clean() {
);
}
/// #56 Fix 1+2: under universal activation the linearity analysis must
/// not false-fire on value-type params or on applied function params.
/// These three fixtures use explicit-mode signatures (so the analysis
/// is active today) and were RED before the hardening (docs/specs/0063).
#[test]
fn harden_ownership_false_positives_are_clean() {
for name in ["fp_value", "fp_hof", "fp_map"] {
let entry = examples_dir().join(format!("{name}.ail"));
let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}"));
let diags = check_workspace(&ws);
let lin: Vec<&ailang_check::Diagnostic> = diags
.iter()
.filter(|d| d.code == "use-after-consume" || d.code == "consume-while-borrowed")
.collect();
assert!(lin.is_empty(), "{name} must be linearity-clean; got: {lin:#?}");
}
}
/// #56 type-gating: the exemption is value-type-only. A heap param
/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST
/// still fire use-after-consume — proving the fix did not blanket-silence
/// genuine multi-consume.
#[test]
fn harden_ownership_heap_double_consume_still_errors() {
let entry = examples_dir().join("real_consume.ail");
let ws = load_workspace(&entry).expect("load real_consume");
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "use-after-consume"),
"real_consume.dup must still fire use-after-consume; got: {diags:#?}"
);
}
/// RED for fieldtest finding B1 (docs/specs/0058): reading a
/// `borrow (RawBuf a)` *parameter* through a borrow-receiver op
/// (`RawBuf.get` / `RawBuf.size`) must check clean. Both ops are