Brummel
f6a8607518
The #55 cutover (plan 0121, Task 4) is blocked: deleting
ParamMode::Implicit activates the strict linearity check universally,
but the migrated corpus does not pass cleanly. #56 (spec 0063) closed
two false-positive classes; universal activation surfaces three more
plus one genuine corpus over-consume. This spec is the "#56 part 2"
hardening, sibling to 0063, landing before the irreversible variant
deletion. It does NOT patch a fifth phase onto plan 0121 (project
rule: 2+ blocking classes = spec defect).
Four additive fixes, no schema/hash/codegen change, check stays
diagnostic-only:
- Type table teed from the typecheck pass (synth Let arm at lib.rs:3808
computes the binder type then discards it) into (def,binder)->Type,
threaded to linearity. The "stop discarding known information" fix,
not a re-run of inference in the walk (ruled out by aaa70d4 / 0063).
- Class 3 (value-typed let-binder): is_value seeded from the table,
extending 0063's per-binder flag to the let site it deferred.
- Class 1 (local function-typed binder): BinderState.fn_param_modes;
callee_arg_modes consults local binders (params/lam from signature,
let from the table) before the global table.
- Class 2 (let-alias of a borrowed value): an alias REDIRECT (not a
state clone -- a clone would miss a real double-consume), root-
resolved in use_var. Closes the contract 0008:340 carve-out.
- Class 4 (partition_eithers): genuine double-consume, body rewrite
(destructure rest once); check unchanged, must-stay-RED fixture pins
it.
Design call (user delegated): the binder->type table is the chosen
mechanism over local/shallow derivation -- the type is known and
discarded, and 0063's deferral of exactly this class is what produced
#57; a local-only patch re-creates the latent class. All five fenced
ail fixtures parse and reach the linearity stage with the recorded
exit codes (parse-every-block gate fired). Grounding-check PASS: every
load-bearing assumption ratified by a green in-source test or a live
RED trace.
refs #57
509 lines
22 KiB
Markdown
509 lines
22 KiB
Markdown
# Harden the ownership analysis for universal activation, part 2 — Design Spec
|
||
|
||
**Date:** 2026-06-01
|
||
**Status:** Draft — awaiting user spec review
|
||
**Authors:** orchestrator + Claude
|
||
|
||
## Goal
|
||
|
||
Close the remaining precision gaps in the strict linearity analysis
|
||
(`use-after-consume` / `consume-while-borrowed`,
|
||
`crates/ailang-check/src/linearity.rs`) so that deleting
|
||
`ParamMode::Implicit` (#55, spec 0062) does not turn part of the
|
||
migrated corpus red. This is the **second hardening pass** —
|
||
`#56` (spec 0063, plan 0120) closed two false-positive classes
|
||
(value-type *params*; application-is-a-borrow). Executing the #55
|
||
cutover (plan 0121, Task 4) surfaced **three more** false-positive
|
||
classes plus **one genuine corpus over-consume** that no mode
|
||
annotation can fix:
|
||
|
||
1. **Local function-typed binder modes (false positive).**
|
||
`callee_arg_modes` (`linearity.rs:750`) resolves the param-modes of a
|
||
call's callee only for **global** fns; a local function-typed binder
|
||
(a HOF predicate param such as `std_list.filter`'s `p`) returns an
|
||
empty mode vector, so every arg of `(app p h)` defaults to `Consume`.
|
||
`filter` then reuses `h` in the kept `Cons` after `(app p h)`
|
||
"consumed" it → false `use-after-consume`. Blocks `std_list.filter`
|
||
and its importers.
|
||
2. **`let`-alias of a borrowed value (false positive).** `Term::Let`
|
||
walks its value in `Position::Consume` (`linearity.rs:506`).
|
||
`(let a t (match a …))` over a `borrow`-mode `t` therefore *consumes*
|
||
`t` at the binding, tripping `consume-while-borrowed`.
|
||
`design/contracts/0008-memory-model.md:340` documents this
|
||
propagation as explicitly **not shipped**.
|
||
3. **Inferred value-typed `let`-binders (false positive).** A
|
||
`let`-binder of an unboxed value type (`Float` etc.) is installed as
|
||
a default `BinderState` with `is_value = false` (`linearity.rs:507`),
|
||
so a value-typed `let`-binder used more than once trips
|
||
`use-after-consume`. Spec 0063 deferred exactly this class
|
||
("value-typed `let`-binders … deferred until a corpus shape demands
|
||
it"); `eqord_3_newton_sqrt.iterate`'s `(let xnew (app / …) …)` is
|
||
that shape. No mode annotation applies — the binder's type is
|
||
inferred, not annotated.
|
||
4. **Genuine double-consume (real corpus bug, NOT a false positive).**
|
||
`std_either_list.partition_eithers` projects both `(app Pair.fst
|
||
rest)` and `(app Pair.snd rest)` from one owned `rest`. `Pair.fst` /
|
||
`Pair.snd` are `own`-param projections that move a field out, so each
|
||
consumes `rest` → `rest` is genuinely consumed twice without a
|
||
`clone`. The fix is a body rewrite (destructure `rest` once), out of
|
||
the migration's mechanical scope; the check correctly stays RED on
|
||
the unrewritten shape.
|
||
|
||
Classes 1–3 are precision gaps the gated-off `Implicit` activation was
|
||
hiding; class 4 is a real fixture over-consume. This is the
|
||
**precondition for #55**: spec 0062 §8 asserts the migrated corpus
|
||
"contains none" of the rejected shapes, which only holds once classes
|
||
1–3 are closed and class 4 is rewritten.
|
||
|
||
The rationale anchors are `design/models/0008-ownership-totality.md` §4
|
||
(HOF mode slots — a function param is applied, which is a read) and
|
||
§3.2 (value types are trivial-`own`), plus the RC/uniqueness contract
|
||
`design/contracts/0008-memory-model.md` (whose `:340` let-alias
|
||
carve-out this cycle closes). The model is `status: Design
|
||
exploration`; its claims are validated against the live tool below
|
||
(Testing strategy), not assumed.
|
||
|
||
### Scope decisions ratified here
|
||
|
||
1. **The let-binder type is teed out of the type-checker, not
|
||
re-inferred.** The inferred type of every `Term::Let` binder is
|
||
*already computed* at `synth`'s `Let` arm (`lib.rs:3808`, `let v =
|
||
synth(value, …)`) and then **discarded**. The fix records it into a
|
||
`(def, binder) → Type` table returned alongside the typecheck
|
||
diagnostics; linearity reads the table. This is the "stop discarding
|
||
known information" fix, not the "re-run inference in the linearity
|
||
walk" anti-pattern that aaa70d4 / spec 0063 ruled out. The table is
|
||
the chosen mechanism for classes 1 (function-typed `let`/`lam`
|
||
binders) and 3 (value-typed `let` binders) uniformly. *(User
|
||
decision, 2026-06-01.)*
|
||
|
||
2. **Parameter and `lam`-param modes/types stay signature-local.** A
|
||
parameter's fn-type (with `param_modes`) and a `lam`-param's type are
|
||
already on the signature where the linearity walk installs the binder
|
||
(`check_fn` has `param_tys`; `Term::Lam` carries `param_tys`). These
|
||
continue to be read from the signature — the type table is only
|
||
needed for `let`-binders, whose type is not locally annotated. The
|
||
corpus driver for class 1 (`filter`'s `p`) is a **param**, so its
|
||
mode resolution is signature-local; the table generalises class 1 to
|
||
`let`/`lam`-bound function values for free.
|
||
|
||
3. **The `let`-alias fix is an alias *redirect*, not a state clone.**
|
||
`(let a t body)` where `t` is a bare `Term::Var` resolving to a
|
||
tracked binder records `a → root(t)` in an alias map for the body
|
||
scope and does **not** walk `t` in `Consume`; `use_var`, the `App`
|
||
borrow-count bump, and `callee_arg_modes` resolve a name through the
|
||
map first. A clone of `t`'s state would be **unsound** — `(let a t
|
||
(seq (consume a) (consume t)))` would mark two independent binders
|
||
and miss the double-consume. The redirect keeps consume/borrow
|
||
bookkeeping on the single root, so a real double-consume through an
|
||
alias is still caught.
|
||
|
||
### Out of scope
|
||
|
||
- **#55 itself** — deleting `ParamMode::Implicit`, the schema/hash
|
||
reset, the parser/return changes (spec 0062). This spec only hardens
|
||
the analysis; it changes no schema, resets no hash, and is testable
|
||
**today** against explicit-mode fns (Testing strategy).
|
||
- **Re-running inference in the linearity walk.** Ruled out by aaa70d4
|
||
and reaffirmed here; the type is teed, never recomputed.
|
||
- **`Str` consume semantics.** Unchanged — `Str` stays heap
|
||
(`is_value_type` excludes it, spec 0063 scope decision 1).
|
||
- **The `over-strict-mode` lint.** Untouched. (It emits a benign
|
||
Warning on the `fst`/`snd` projection helpers; that is pre-existing
|
||
and orthogonal.)
|
||
|
||
## Architecture
|
||
|
||
Four additive changes, no schema change, no new `Type` variant, no hash
|
||
shift, no codegen change. The analysis stays a pure diagnostic pass.
|
||
|
||
**New type-checker output (`crates/ailang-check/src/lib.rs`):**
|
||
|
||
A `LetBinderTypes` table, `HashMap<(String, String), Type>` keyed
|
||
`(def_name, binder_name)`, populated at the `synth` `Term::Let` arm
|
||
(`lib.rs:3808`) with the binder's resolved inferred type, and threaded
|
||
out of `check_in_workspace` / `check_workspace` to the linearity
|
||
dispatch. One insert, the value already in hand; the cost is plumbing
|
||
the table through the two pass functions and into the `Checker`.
|
||
|
||
**Fix 1 — local function-typed binder modes (`linearity.rs`):**
|
||
|
||
`BinderState` gains `fn_param_modes: Option<Vec<ParamMode>>`. It is
|
||
seeded at every binder-introduction site whose binder is function-typed:
|
||
params and `lam`-params from the locally-available signature type;
|
||
`let`-binders from the `LetBinderTypes` table. `callee_arg_modes`, for a
|
||
local `Var` callee, reads the callee binder's `fn_param_modes` before
|
||
falling back to the global symbol table. A local HOF predicate's
|
||
declared arg modes then resolve, so its borrow-arg slot is walked
|
||
`Borrow`, not `Consume`.
|
||
|
||
**Fix 2 — value-typed `let`-binder exemption (`linearity.rs`):**
|
||
|
||
`Term::Let` looks the binder's type up in the `LetBinderTypes` table and
|
||
sets `is_value` from `type_is_value` — the same per-binder flag spec
|
||
0063 already seeds at param / pattern / `lam` sites, now extended to the
|
||
`let` site. The walk reads the table where the source's type is
|
||
otherwise unavailable; it never re-infers.
|
||
|
||
**Fix 3 — `let`-alias borrow propagation (`linearity.rs`):**
|
||
|
||
The `Checker` gains `aliases: HashMap<String, String>`. `Term::Let`
|
||
with a bare `Term::Var` value resolving (through the alias map) to a
|
||
tracked binder records the alias and skips the `Consume` walk of the
|
||
value; `use_var` / the `App` borrow bump / `callee_arg_modes` resolve a
|
||
name to its root before touching `binders`. Scoped by the existing
|
||
save/restore discipline.
|
||
|
||
**Fix 4 — class-4 corpus body rewrite (`examples/std_either_list.ail`):**
|
||
|
||
`partition_eithers` is rewritten to destructure `rest` once via `(match
|
||
rest (case (pat-ctor MkPair ls rs) …))` and reuse `ls` / `rs`, instead
|
||
of the double `Pair.fst` / `Pair.snd` projection. No check change; the
|
||
check correctly rejects the old shape (a genuine double-consume) and
|
||
accepts the new one. Any other corpus fn the universal activation
|
||
reveals to have the same genuine-consume shape is rewritten the same
|
||
way (enumerated during the migration, not here).
|
||
|
||
**Contract update (`design/contracts/0008-memory-model.md`):**
|
||
|
||
The `:340` "Does not cover let-aliases of borrowed values" carve-out is
|
||
rewritten to record that the propagation now ships (Fix 3). A contract
|
||
change rides with the feature that forces it.
|
||
|
||
## Concrete code shapes
|
||
|
||
Every `ail` block below was run through `ail check`
|
||
(`target/debug/ail`, 2026-06-01); the exit-code traces are in the
|
||
Testing section. All are **explicit-mode** fns, so the linearity check
|
||
is active **today** without #55 — each is RED now and GREEN after the
|
||
named fix.
|
||
|
||
### RED→GREEN class 1: local function-typed predicate param
|
||
|
||
An LLM author writes the canonical `filter` HOF; the borrow-mode
|
||
predicate `p` is applied to the heap element `h`, which is then reused
|
||
in the kept `Cons`. False `use-after-consume` today:
|
||
|
||
```ail
|
||
(module c1_local_hof
|
||
(data Box
|
||
(doc "heap cell")
|
||
(ctor Box (con Int)))
|
||
(data List
|
||
(doc "boxed list of boxes")
|
||
(ctor Nil)
|
||
(ctor Cons (con Box) (con List)))
|
||
(fn filter_box
|
||
(doc "borrow-mode predicate p applied to h; h reused in the kept Cons")
|
||
(type
|
||
(fn-type
|
||
(params (borrow (fn-type (params (borrow (con Box))) (ret (own (con Bool)))))
|
||
(own (con List)))
|
||
(ret (own (con List)))))
|
||
(params p xs)
|
||
(body
|
||
(match xs
|
||
(case (pat-ctor Nil) (term-ctor List Nil))
|
||
(case (pat-ctor Cons h t)
|
||
(if (app p h)
|
||
(term-ctor List Cons h (app filter_box p t))
|
||
(app filter_box p t)))))))
|
||
```
|
||
|
||
### RED→GREEN class 2: `let`-alias of a borrowed param
|
||
|
||
`(let a t …)` over a `borrow`-mode `t`; false `consume-while-borrowed`
|
||
today:
|
||
|
||
```ail
|
||
(module c2_let_alias
|
||
(data Tree
|
||
(doc "boxed tree")
|
||
(ctor TLeaf)
|
||
(ctor TNode (con Int) (con Tree) (con Tree)))
|
||
(fn count
|
||
(doc "alias a := borrowed t, then match a")
|
||
(type (fn-type (params (borrow (con Tree))) (ret (own (con Int)))))
|
||
(params t)
|
||
(body
|
||
(let a t
|
||
(match a
|
||
(case (pat-ctor TLeaf) 0)
|
||
(case (pat-ctor TNode v l r) 1))))))
|
||
```
|
||
|
||
### RED→GREEN class 3: value-typed `let`-binder used multiple times
|
||
|
||
`xnew` is a `Float` `let`-binder used in the cond and both branches;
|
||
false `use-after-consume` (×2) today:
|
||
|
||
```ail
|
||
(module c3_value_let
|
||
(fn iterate
|
||
(doc "xnew is a Float let-binder used in cond and both branches")
|
||
(type (fn-type (params (own (con Float)) (own (con Float))) (ret (own (con Float)))))
|
||
(params x tol)
|
||
(body
|
||
(let xnew (app / x 2.0)
|
||
(if (app float_lt (app - xnew x) tol)
|
||
xnew
|
||
xnew)))))
|
||
```
|
||
|
||
### Must-stay-RED class 4: genuine double-consume
|
||
|
||
`rest` is projected by both `fst` and `snd` (`own`-param projections) →
|
||
genuinely consumed twice. This is a **real** `use-after-consume` and
|
||
**stays an error** after every fix (the exemptions are type-/alias-gated,
|
||
not blanket). The migration rewrites the body; the check is unchanged:
|
||
|
||
```ail
|
||
(module c4_double_consume
|
||
(data Pair
|
||
(doc "boxed pair of ints")
|
||
(ctor MkPair (con Int) (con Int)))
|
||
(fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
|
||
(body (match p (case (pat-ctor MkPair a b) a))))
|
||
(fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p)
|
||
(body (match p (case (pat-ctor MkPair a b) b))))
|
||
(fn both
|
||
(doc "MUST STAY RED: rest projected by fst AND snd = consumed twice")
|
||
(type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
|
||
(params rest)
|
||
(body (term-ctor Pair MkPair (app fst rest) (app snd rest)))))
|
||
```
|
||
|
||
### Class-4 fix: destructure once (clean today)
|
||
|
||
The body rewrite — the same shape applied to the real
|
||
`partition_eithers`. Clean today, clean after:
|
||
|
||
```ail
|
||
(module c4_rewrite
|
||
(data Pair
|
||
(doc "boxed pair of ints")
|
||
(ctor MkPair (con Int) (con Int)))
|
||
(fn both
|
||
(doc "rewrite: destructure rest once via match")
|
||
(type (fn-type (params (own (con Pair))) (ret (own (con Pair)))))
|
||
(params rest)
|
||
(body (match rest (case (pat-ctor MkPair a b) (term-ctor Pair MkPair a b))))))
|
||
```
|
||
|
||
### Secondary: implementation shapes (before → after)
|
||
|
||
*Supporting detail, not the headline.*
|
||
|
||
**`crates/ailang-check/src/lib.rs` — tee the let-binder type at `synth`'s `Let` arm (`:3808`):**
|
||
|
||
```text
|
||
before:
|
||
Term::Let { name, value, body } => {
|
||
let v = synth(value, env, locals, …, subst, …)?;
|
||
let prev = locals.insert(name.clone(), v);
|
||
let r = synth(body, …)?;
|
||
…restore prev…
|
||
Ok(r)
|
||
}
|
||
after:
|
||
Term::Let { name, value, body } => {
|
||
let v = synth(value, env, locals, …, subst, …)?;
|
||
let_binder_types.insert((in_def.clone(), name.clone()), subst.apply(&v)); // tee the known type
|
||
let prev = locals.insert(name.clone(), v);
|
||
…unchanged…
|
||
}
|
||
// let_binder_types is a new &mut out-param on synth, threaded out of
|
||
// check_fn → check_in_workspace → check_workspace to the linearity dispatch.
|
||
```
|
||
|
||
**`crates/ailang-check/src/linearity.rs` — `BinderState`:**
|
||
|
||
```text
|
||
before: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool }
|
||
after: struct BinderState { consumed: bool, borrow_count: u32, is_value: bool,
|
||
fn_param_modes: Option<Vec<ParamMode>> }
|
||
// Some(modes) for a function-typed binder; None otherwise.
|
||
```
|
||
|
||
**`linearity.rs` — `callee_arg_modes` consults local binders first (`:750`):**
|
||
|
||
```text
|
||
before: only Term::Var resolving to self.globals; locals → vec![]
|
||
after: for a Term::Var callee, resolve through self.aliases, then:
|
||
1. if the binder carries fn_param_modes, return them;
|
||
2. else fall back to self.globals (today's path).
|
||
```
|
||
|
||
**`linearity.rs` — `Term::Let` (`:505`):**
|
||
|
||
```text
|
||
before:
|
||
Term::Let { name, value, body } => {
|
||
self.walk(value, Position::Consume);
|
||
self.with_binder(name, BinderState::default(), |this| { this.walk(body, pos); });
|
||
}
|
||
after:
|
||
Term::Let { name, value, body } => {
|
||
// (a) bare-Var alias of a tracked binder → record alias, skip the consume walk;
|
||
// (b) otherwise walk value in Consume as today;
|
||
// seed the let-binder's is_value / fn_param_modes from LetBinderTypes
|
||
// (keyed (def, name)) for the body scope.
|
||
}
|
||
```
|
||
|
||
**`examples/std_either_list.ail` — `partition_eithers` Cons arm (`:61`):**
|
||
|
||
```text
|
||
before:
|
||
(case (pat-ctor Cons h t)
|
||
(let rest (app partition_eithers t)
|
||
(match h
|
||
(case (pat-ctor Left l)
|
||
(term-ctor Pair MkPair (term-ctor List Cons l (app Pair.fst rest)) (app Pair.snd rest)))
|
||
(case (pat-ctor Right r)
|
||
(term-ctor Pair MkPair (app Pair.fst rest) (term-ctor List Cons r (app Pair.snd rest)))))))
|
||
after:
|
||
(case (pat-ctor Cons h t)
|
||
(let rest (app partition_eithers t)
|
||
(match rest
|
||
(case (pat-ctor MkPair ls rs)
|
||
(match h
|
||
(case (pat-ctor Left l)
|
||
(term-ctor Pair MkPair (term-ctor List Cons l ls) rs))
|
||
(case (pat-ctor Right r)
|
||
(term-ctor Pair MkPair ls (term-ctor List Cons r rs))))))))
|
||
// rest destructured once; ls/rs each consumed once per independent match-arm.
|
||
```
|
||
|
||
## Components
|
||
|
||
- **`ailang-check::lib` (typecheck pass)** — `synth` gains the
|
||
`let_binder_types` out-param and one insert at the `Let` arm;
|
||
`check_fn` / `check_in_workspace` / `check_workspace` thread the table
|
||
out to the linearity dispatch (`lib.rs:1276`).
|
||
- **`ailang-check::linearity`** — `BinderState.fn_param_modes`; the
|
||
`Checker` gains an immutable `let_binder_types` reference and a scoped
|
||
`aliases` map; `callee_arg_modes` resolves locals + aliases;
|
||
`Term::Let` seeds `is_value` / `fn_param_modes` from the table and
|
||
records bare-Var aliases.
|
||
- **`.ail` fixtures** — the three RED→GREEN fixtures (classes 1–3), the
|
||
must-stay-RED double-consume, and the rewrite, under `examples/`.
|
||
- **`examples/std_either_list.ail`** — the `partition_eithers` rewrite
|
||
(plus any sibling corpus fn the migration reveals with the same
|
||
genuine-consume shape).
|
||
- **`design/contracts/0008-memory-model.md`** — the `:340` let-alias
|
||
carve-out updated to "ships".
|
||
|
||
No change to: the schema (`ParamMode`, `Type::Fn`), the parser, the
|
||
printer, codegen, the runtime, `is_heap_type`, or the
|
||
`over-strict-mode` lint.
|
||
|
||
## Data flow
|
||
|
||
**The type table.** The typecheck pass already synthesises every
|
||
`let`-binder's type (`lib.rs:3808`); today it is dropped when `check_fn`
|
||
returns `Result<()>`. The fix records `subst.apply(&v)` — the resolved
|
||
type — into `(def, binder) → Type` and threads it to linearity, which
|
||
runs strictly **after** a clean typecheck (`lib.rs:1254` gate), so the
|
||
table is fully populated before the walk starts. Linearity reads the
|
||
table only at the `Term::Let` introduction site; params and `lam`-params
|
||
keep reading their signature types. A binder whose teed type is not a
|
||
value `Type::Con` and not a `Type::Fn` defaults exactly as today
|
||
(`is_value = false`, `fn_param_modes = None`).
|
||
|
||
**Mode resolution.** For `(app callee args)`, `callee_arg_modes`
|
||
resolves the callee `Var` through the alias map, then prefers a tracked
|
||
binder's `fn_param_modes` over the global table. A global fn-ref callee
|
||
is untracked, so it still falls through to `self.globals` — no behaviour
|
||
change for the common case. A local function-typed binder now resolves
|
||
its declared arg modes, so a borrow-arg slot is walked `Borrow`.
|
||
|
||
**Alias soundness.** `(let a t body)` with `t` a tracked binder makes
|
||
`a` a redirect to `root(t)`. Every binder op on `a` (consume, borrow,
|
||
mode lookup) acts on the single root state, so: a borrow-position use of
|
||
`a` does not consume `t` (fixes the false positive), and a consume of
|
||
`a` marks `t` consumed (so a later consume of either is a real
|
||
`use-after-consume` — no false negative). Aliases are installed for the
|
||
body scope and removed on exit, like any binder.
|
||
|
||
## 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 local HOF-param applications (class 1),
|
||
borrowed-value `let`-aliases (class 2), or value-typed `let`-binders
|
||
(class 3). They continue to fire on the genuine double-consume (class
|
||
4, must-stay-RED) and on any real use-after-consume reached through an
|
||
alias. 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 fixes:
|
||
|
||
```text
|
||
c1_local_hof.ail : exit 1 error: [use-after-consume] filter_box: `h` ...
|
||
c2_let_alias.ail : exit 1 error: [consume-while-borrowed] count: `t` ...
|
||
c3_value_let.ail : exit 1 error: [use-after-consume] iterate: `xnew` ... (x2)
|
||
c4_double_consume.ail : exit 1 error: [use-after-consume] both: `rest` ...
|
||
(+ benign over-strict-mode warnings on fst/snd)
|
||
c4_rewrite.ail : exit 0 ok
|
||
```
|
||
|
||
- **RED→GREEN fixtures.** `c1_local_hof`, `c2_let_alias`, `c3_value_let`
|
||
land under `examples/`; each asserts its named diagnostic fires
|
||
**today** and is **clean** (exit 0) after the matching fix. These are
|
||
the RED side of fixes 1–3.
|
||
- **Must-stay-RED fixture.** `c4_double_consume` asserts the genuine
|
||
double-consume still fires after all fixes — the exemptions are
|
||
type-/alias-gated, not blanket. It is the analogue of spec 0063's
|
||
`real_consume`.
|
||
- **Class-4 corpus rewrite.** `examples/std_either_list.ail` checks and
|
||
runs clean after the `partition_eithers` rewrite; its existing
|
||
E2E/demo (`std_either_list_demo.ail`) output is unchanged.
|
||
- **Alias soundness unit test.** An in-source `#[cfg(test)]` case in
|
||
`linearity.rs`: a `(let a t (seq …consume a… …consume t…))` over an
|
||
`own` `t` still produces `use-after-consume` (the redirect does not
|
||
mask a real double-consume).
|
||
- **`std_list.filter` + importers.** `std_list.ail` and the seven
|
||
modules that import it (`kem_1_list_running_sum`, `nested_pat`,
|
||
`std_either_list`, `std_either_list_demo`, `std_list_demo`,
|
||
`std_list_more_demo`, `std_list_stress`) check clean once `filter`'s
|
||
signature is migrated to explicit modes (validated against the
|
||
migrated corpus; the analysis only activates with explicit modes).
|
||
- **Full corpus regression.** `cargo test --workspace` stays green, and
|
||
the `examples/` typecheck/codegen suite is the net for "no exemption
|
||
silenced a real consume". 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 (diagnostic-only change; no compile-baseline shift
|
||
expected).
|
||
|
||
## Acceptance criteria
|
||
|
||
1. A `(def, binder) → Type` table is teed from the typecheck pass and
|
||
threaded to linearity; `synth`'s `Let` arm records the resolved
|
||
binder type, and linearity reads it (no inference re-run in the
|
||
walk).
|
||
2. `c1_local_hof`, `c2_let_alias`, `c3_value_let` check **clean** (exit
|
||
0) after their fixes; each shipped as an `examples/` fixture
|
||
asserting its today→post transition.
|
||
3. `c4_double_consume` still fails with `use-after-consume` after all
|
||
fixes (exemptions are type-/alias-gated).
|
||
4. `callee_arg_modes` resolves a local function-typed binder's
|
||
`param_modes`; a borrow-mode HOF predicate param applied to a heap
|
||
element does not consume it.
|
||
5. A `let`-alias of a `borrow`-mode binder does not trip
|
||
`consume-while-borrowed`, and a `let`-alias of an `own` binder still
|
||
catches a real double-consume (alias soundness unit test).
|
||
6. `examples/std_either_list.ail` checks and runs clean after the
|
||
`partition_eithers` rewrite; output unchanged.
|
||
7. `cargo test --workspace` green; `bench/check.py` and
|
||
`bench/compile_check.py` green.
|
||
8. `design/contracts/0008-memory-model.md:340` is updated to record the
|
||
let-alias propagation as shipped.
|
||
9. No change to `ParamMode`, `Type::Fn`, the parser/printer, codegen,
|
||
the runtime, `is_heap_type`, or the `over-strict-mode` lint (grep /
|
||
diff clean).
|