Third iteration of spec 0064 (the #55-cutover hardening, #57). Closes
false-positive class 2: Term::Let walked its value in Position::Consume,
so (let a t (match a …)) over a borrow-mode t consumed t at the binding
and tripped consume-while-borrowed -- a let-alias of a borrowed value
read in a borrow position is not a consume.
Fix: the Checker gains a scoped aliases: HashMap<String,String>. A
(let a t body) whose value is a bare Var resolving to a tracked binder
records a -> root(t) for the body scope and skips the consume walk of
the value. A new resolve_alias helper maps a name to its root,
preferring a real binder at each chain step -- so an inner binder named
`a` (nested let, pattern binder, lam param) automatically shadows the
alias with NO change to with_binder/walk_arm/Lam (the shadowing is
resolved centrally in the resolver, not at three scattered introduction
sites). Every binder-state lookup keyed by name resolves through the
map first: use_var, the App borrow bump + decrement (pushing the
resolved root to `lent` so the decrement matches), callee_arg_modes,
and the reuse-as source.
Design calls (orchestrator):
- Alias REDIRECT, not state clone (spec scope decision 3): consuming
the alias marks the single root consumed, so a real double-consume
through an alias is still caught. A clone would track two independent
binders and miss it (unsound). Pinned by the new
let_alias_of_owned_double_consume_still_errors unit test:
(let a p0 (seq a p0)) over an own heap p0 still fires
use-after-consume.
- resolve_alias prefers binders -> shadowing needs no edits to the
binder-introduction sites. Lower-risk than clearing aliases at each.
- reuse-as source (linearity.rs:663) is resolved through aliases too:
it is the 4th binder-state-reading site; the spec's Fix 3 named three
illustratively. Without it, (reuse-as <alias> …) would mis-fire
reuse-as-source-not-bare-var on what IS a Var. Faithful completion of
Fix 3.
The diagnostic now reports the resolved root name (the actual consumed
resource), not the surface alias.
Closes the design/contracts/0008-memory-model.md let-alias carve-out
(was "has not shipped yet") and extends its Ratified-by trailer to name
linearity.rs, where the propagation now lives -- a contract change
riding with the feature that forces it.
RED-first: examples/c2_let_alias.ail added to
harden_ownership_false_positives_are_clean (RED: consume-while-borrowed
on count's t); GREEN after. Verified: c2 RED->GREEN; 120 linearity unit
tests green; the soundness test fires; harden false-positive + heap
double-consume guards green; cargo test --workspace green;
bench/check.py 34/34, compile_check.py 24/24 stable. Diagnostic-only;
no schema/type/codegen change.
Class 4 (partition_eithers body rewrite) remains for the final
iteration of spec 0064.
refs #57
Brummel
be259f9d46