feat(borrow): NLL last-use expiry for ref-bindings (CORE-01 pt3 Slice A, Refs #177) (#335)

## Summary

CORE-01 Phase 3 **Slice A** — non-lexical lifetimes for ref-bindings.
The lexical "borrow lives until block exit" rule is replaced by
**last-use expiry**: a ref-binding's underlying borrow is released after
the binder's last mentioning statement, not at block exit.

- `compute_last_use_index` (new in `lib/borrow.ml`): forward AST
pre-pass returning `sym_id → max statement index that mentions it`.
Covers all 24 expr / 5 stmt / 5 unsafe_op variants; recurses through
nested blocks, lambdas, handler arms, try/finally.
- `check_block` now runs the pre-pass and expires ref-bindings
introduced *in this block* once their binder's last use has passed
(`end_borrow` + drop from `state.ref_bindings`). Outer-block bindings
are preserved.

**Unblocks** the canonical NLL patterns:

```affine
let mut x = 1;
let r = &x;
let y = *r;
x = 2;       // previously MoveWhileBorrowed; now OK
x + y
```

```affine
let mut x = 5;
let m = &mut x;
let y = *m;
x + y        // previously UseWhileExclusivelyBorrowed; now OK
```

**Soundness preserved**: anti-aliasing rules still fire against
statements that read or assign the owner *before* the binder's last use,
because the borrow is still on `state.borrows` at that point.

## Scope of this PR (Slice A of a multi-day plan)

This is **Slice A** of CORE-01 Phase 3. Future slices, separate PRs:

| Slice | Work |
|---|---|
| B | Flow-sensitive escape via `outer = &x` (assignment updates the
borrow graph the way `let r = &x` already does) |
| C | Origin/region variables (Polonius surface) + loan-live-at-point
dataflow across CFG joins |
| D | Tighter quantity-checker integration for captured linears |

## Tests (E2E Borrow Graph, +3)

| Fixture | Direction | Expected |
|---|---|---|
| `borrow_nll_assign_after_last_use.affine` | positive (NLL win) | Ok |
| `borrow_nll_read_after_mut_last_use.affine` | positive (NLL win,
exclusive) | Ok |
| `borrow_nll_still_rejects_live_borrow.affine` | anti-regression |
`MoveWhileBorrowed` |

Pre-existing fixtures audited end-to-end against the new flow and remain
green by construction — the violations they pin are all detected
*before* the binder's last-use index (return-escape runs during the
`StmtExpr (ExprReturn ...)` check, before that statement's expire pass;
block-tail `&local` uses `ref_target` not `ref_bindings`; the `&mut`
conflict/use-while fixtures conflict at borrow creation, before any
expire).

## Docs

- `STATE.a2ml` `borrow-checker` → `phase-3-part-3-slice-A-landed`
- `docs/CAPABILITY-MATRIX.adoc` borrow-checker row → "pts 1–3 Slice A"
- `docs/TECH-DEBT.adoc` CORE-01 row → records Slice A landing, residual
= Slices B–D

## Test plan

- [ ] CI `Build` (opam exec -- dune build) green
- [ ] CI `Run tests` (opam exec -- dune runtest) — `E2E Borrow Graph`
count is +3 (the 3 new NLL cases), all green
- [ ] CI `Run codegen WASM tests` green — the borrow checker runs in the
standard CLI pipeline, so any over-rejection regression would surface
here (full stdlib AOT exercises the corpus)
- [ ] CI `Check formatting` (`dune build @fmt`) green

**Local-build caveat**: the container this PR was authored in has no
OCaml toolchain installed, so `dune build` / `dune runtest` were not run
locally. CI is the source of truth.

Refs #177

---
_Generated by [Claude
Code](https://claude.ai/code/session_01TLERhquTknLCfyjv7eQU8b)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -68,7 +68,7 @@ test-files = 54
 # the feature is not enforced on user programs through the CLI pipeline.
 affine-types = "wired-and-reachable (Track A Manhattan plan complete 2026-04-10. Quantity semiring in lib/quantity.ml; invoked from typecheck.ml:1206 inside the standard CLI pipeline. Surface syntax per ADR-007 hybrid: @linear/@erased/@unrestricted attributes (Option C primary) on let/stmt-let/param/lambda-param, AND :1/:0/:ω numeric sugar (Option B) on let/stmt-let. Scaled Let rule per ADR-002 implemented in lib/quantity.ml ExprLet/StmtLet — closes BUG-001 (ω-let smuggles linear values) and BUG-002 (zero-let erasure). Four regression fixtures in test/e2e/fixtures/ exercise both surface forms. Behavioural enforcement verified via E2E Quantity test suite — 4 new passing tests, 0 regressions.)"
 linear-arrows = "enforced (2026-04-11): Three-part fix landed. (1) typecheck.ml lambda synth: |@linear x: T| e now synthesises T -[1]-> U (was always QOmega). (2) typecheck.ml lambda check mode: explicit param quantity annotation validated against expected TArrow quantity; unannotated params inherit context quantity. (3) quantity.ml ExprLambda: added env.errors accumulator; annotated lambda params declared via env_declare so env_use tracks them; usage verified with check_quantity after body walk; violations pushed to env.errors and drained at end of check_function_quantities (step 4). Saved/restored env.quantities entries to prevent scope leakage. Two E2E fixtures + 2 passing tests. 75 tests total, 0 regressions. Commit d2f9b7b pushed."
-borrow-checker = "phase-3-part-1-landed (CORE-01, PR #240 Refs #177, 2026-05-19, gate 263/263): borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut (owned/ref/mut discipline now enforced from real parsed source — closed a latent hole), call-arg borrows temporary, ref-binding graph tracked. Part 2+ deferred: NLL/region inference, flow-sensitive escape via `outer = &x`, tighter quantity integration. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
+borrow-checker = "phase-3-part-3-slice-A-landed (CORE-01, Refs #177, 2026-05-24): pt1 (#240, gate 263/263) borrow-graph validation wired — BorrowOutlivesOwner emitted (&local escaping its block), shared-XOR-exclusive enforced at use sites (UseWhileExclusivelyBorrowed), ownership derived from param type TyOwn/TyRef/TyMut (owned/ref/mut discipline now enforced from real parsed source — closed a latent hole), call-arg borrows temporary, ref-binding graph tracked. pt2 (gate 271→274 and 278→281) return-escape (return-of-ref-rooted-at-callee-owned-binding caught) + &mut e parser surface (zero Menhir conflict delta — exclusive borrow finally expressible from real source). pt3 Slice A NLL last-use expiry: forward pre-pass compute_last_use_index maps each symbol to its greatest mentioning statement index; check_block expires ref-bindings introduced in-block once their binder is dead, releasing the underlying borrow. Unblocks `let r = &x; print(*r); x = 2` and `let m = &mut x; let y = *m; x` while still rejecting same-block live aliasing (2 positive + 1 anti-regression hermetic tests in E2E Borrow Graph). Residual (Slices B–D): flow-sensitive escape via `outer = &x`, origin/region variables (Polonius surface) + loan-live-at-point dataflow across CFG joins, tighter quantity integration. Authoritative: docs/CAPABILITY-MATRIX.adoc + docs/TECH-DEBT.adoc CORE-01."
 row-polymorphism = "60% (records + effects rows implemented in typecheck/unify; not fully exercised end-to-end)"
 effects = "interpreter-complete (handler dispatch, PerformEffect propagation, ExprResume, multi-arg ops all wired in interp.ml 2026-04-11). WasmGC: ops registered as unreachable stubs; ExprHandle/ExprResume reject with UnsupportedFeature — full WASM dispatch needs EH proposal or CPS transform."
 dependent-types = "parse-only (TRefined AST node exists and refinement predicates parse, but predicates do not reduce; no SMT/decision procedure wired in)"

docs/CAPABILITY-MATRIX.adoc

@@ -84,16 +84,26 @@ enforced. Handlers: *interpreter-complete*; WasmGC dispatch is
 `UnsupportedFeature` pending the EH proposal or the CPS transform (the #225
 CPS line is closing the async slice of this).
 
-|Borrow checker |*partial — graph validation landed (CORE-01 pt 1)* |
+|Borrow checker |*partial — graph validation + NLL last-use landed
+(CORE-01 pts 1–3 Slice A)* |
 Place/borrow/move infra + use-after-move, conflicting-borrow,
 move-while-borrowed, lambda-capture. *CORE-01 part 1* (PR #240, Refs #177,
 gate 263/263): borrow-graph validation wired — `BorrowOutlivesOwner` now
 emitted (`&local` escaping its block); shared-XOR-exclusive enforced at
 *use* sites (`UseWhileExclusivelyBorrowed`); ownership now derived from the
 parameter *type* (`TyOwn/TyRef/TyMut`) so the owned/ref/mut discipline is
 actually enforced from real parsed source (closed a latent hole); call-arg
-borrows made temporary. *Deferred (CORE-01 pt 2+):* NLL/region inference,
-flow-sensitive escape via `outer = &x`, tighter quantity integration.
+borrows made temporary. *Part 2* (Refs #177): return-escape +
+`&mut e` parser surface (the exclusive borrow is finally expressible from
+source). *Part 3 Slice A* (Refs #177): non-lexical lifetimes —
+ref-bindings expire at their binder's *last use*, not at block exit
+(`compute_last_use_index` pre-pass + per-statement expiry in
+`check_block`). Patterns like `let r = &x; print(*r); x = 2` and
+`let m = &mut x; let y = *m; x` now type-check, while still-live borrows
+continue to block aliasing assignments. *Deferred (Slices B–D):*
+flow-sensitive escape via `outer = &x`; origin/region variables
+(Polonius surface) + loan-live-at-point dataflow across CFG joins;
+tighter quantity integration for captured linears.
 
 |Quantity / affine types |*enforced* |QTT semiring in `lib/quantity.ml`,
 invoked inside the standard CLI pipeline. `@linear`/`@erased`/`@unrestricted`

docs/TECH-DEBT.adoc

@@ -110,12 +110,23 @@ typed/codegen'd like `&e` — exclusivity is a static borrow property).
 `&`-in-`#{` literals and bare block-statements already parse on `main`;
 `-> &T`/`&T` *type* sigil deliberately **not** added — `ref T`/`mut T`
 keyword types already express reference types; a `&T` sigil is duplicate
-surface (ADR territory, not a soundness gap). *Part 2 residual — now the
-analysis, not surface:* NLL/region inference (Polonius) + flow-sensitive
-escape via `outer = &x` are now *expressible* (surface unblocked); the
-remaining work is the dataflow analysis itself. |S1 |pt1 #240 + pt2
-return-escape + `&mut` surface DONE (Refs #177); residual = NLL analysis
-— issue #177
+surface (ADR territory, not a soundness gap). *Part 3 Slice A — NLL
+last-use expiry LANDED* (Refs #177): a forward pre-pass
+(`compute_last_use_index`) maps each symbol to the greatest statement
+index that mentions it; after each statement, `check_block` expires any
+ref-binding introduced in that block whose binder is now dead, releasing
+the underlying borrow. Unblocks the canonical NLL patterns
+(`let r = &x; print(*r); x = 2`; `let m = &mut x; let y = *m; x`) while
+preserving soundness — the anti-aliasing rules still fire against
+statements that *do* use the binder (3 hermetic tests in "E2E Borrow
+Graph", two positive + one anti-regression). *Slices B–D residual:*
+flow-sensitive escape via assignment to an outer mutable
+(`outer = &x`); origin/region variables (Polonius surface) + loan-live-
+at-point dataflow across CFG joins; tighter quantity integration for
+captured linears. |S1 |pt1 #240 + pt2 return-escape + `&mut` surface +
+pt3 Slice A NLL last-use DONE (Refs #177); residual = Slices B–D
+(flow-sensitive escape, origin variables, quantity integration) —
+issue #177
 |CORE-02 |Effect-handler dispatch on WasmGC (currently `UnsupportedFeature`;
 EH proposal or CPS). The #225 CPS line closes the async slice. |S2 |partial
 (#225 line CLOSED PR1..PR3d+PR4; #234 generalises the recogniser —

lib/borrow.ml

@@ -562,6 +562,113 @@ let check_return_escape (state : state) (symbols : Symbol.t)
        Error (BorrowOutlivesOwner (b, owner))
      | _ -> Ok ())
 
+(** NLL last-use pre-pass (CORE-01 pt3 / #177 Slice A).
+
+    Returns a map [sym_id -> max statement index at which the symbol is
+    mentioned anywhere inside [blk] (including nested blocks, lambda
+    bodies, handler arms, etc.)]. Statement indices are 0-based; the
+    block's tail expression, if any, is treated as the [n]-th "statement"
+    (where [n = List.length blk.blk_stmts]).
+
+    Used by [check_block] to expire ref-bindings introduced in this block
+    once their binder is dead, instead of holding them until lexical block
+    exit. The expiry releases the underlying borrow, so subsequent
+    statements may legally read or assign through the (no-longer-borrowed)
+    owner — the canonical Rust-style "non-lexical lifetime" win.
+
+    A symbol that never appears is simply absent from the table; callers
+    treat that as [-1] (last-use precedes the first statement → expire
+    immediately after the declaration). *)
+let compute_last_use_index (symbols : Symbol.t) (blk : block)
+    : (Symbol.symbol_id, int) Hashtbl.t =
+  let tbl : (Symbol.symbol_id, int) Hashtbl.t = Hashtbl.create 8 in
+  let bump (sym : Symbol.symbol_id) (idx : int) : unit =
+    match Hashtbl.find_opt tbl sym with
+    | Some cur when cur >= idx -> ()
+    | _ -> Hashtbl.replace tbl sym idx
+  in
+  let mark_var (idx : int) (id : ident) : unit =
+    match lookup_symbol_by_name symbols id.name with
+    | Some s -> bump s.Symbol.sym_id idx
+    | None -> ()
+  in
+  let rec visit_expr (idx : int) (e : expr) : unit =
+    match e with
+    | ExprVar id -> mark_var idx id
+    | ExprLit _ | ExprVariant _ -> ()
+    | ExprSpan (e, _) -> visit_expr idx e
+    | ExprApp (f, args) ->
+      visit_expr idx f; List.iter (visit_expr idx) args
+    | ExprField (b, _) | ExprTupleIndex (b, _) -> visit_expr idx b
+    | ExprIndex (b, i) -> visit_expr idx b; visit_expr idx i
+    | ExprTuple es | ExprArray es -> List.iter (visit_expr idx) es
+    | ExprRecord r ->
+      List.iter (fun (_, eo) -> match eo with Some e -> visit_expr idx e | None -> ()) r.er_fields;
+      (match r.er_spread with Some e -> visit_expr idx e | None -> ())
+    | ExprRowRestrict (e, _) -> visit_expr idx e
+    | ExprBinary (l, _, r) -> visit_expr idx l; visit_expr idx r
+    | ExprUnary (_, e) -> visit_expr idx e
+    | ExprLet lb ->
+      visit_expr idx lb.el_value;
+      (match lb.el_body with Some b -> visit_expr idx b | None -> ())
+    | ExprIf ei ->
+      visit_expr idx ei.ei_cond; visit_expr idx ei.ei_then;
+      (match ei.ei_else with Some e -> visit_expr idx e | None -> ())
+    | ExprMatch em ->
+      visit_expr idx em.em_scrutinee;
+      List.iter (fun arm ->
+        (match arm.ma_guard with Some g -> visit_expr idx g | None -> ());
+        visit_expr idx arm.ma_body
+      ) em.em_arms
+    | ExprBlock blk -> visit_block idx blk
+    | ExprLambda lam -> visit_expr idx lam.elam_body
+    | ExprReturn (Some e) -> visit_expr idx e
+    | ExprReturn None -> ()
+    | ExprHandle eh ->
+      visit_expr idx eh.eh_body;
+      List.iter (fun arm ->
+        match arm with
+        | HandlerReturn (_, b) -> visit_expr idx b
+        | HandlerOp (_, _, b) -> visit_expr idx b
+      ) eh.eh_handlers
+    | ExprResume (Some e) -> visit_expr idx e
+    | ExprResume None -> ()
+    | ExprTry et ->
+      visit_block idx et.et_body;
+      (match et.et_catch with
+       | Some arms ->
+         List.iter (fun arm ->
+           (match arm.ma_guard with Some g -> visit_expr idx g | None -> ());
+           visit_expr idx arm.ma_body) arms
+       | None -> ());
+      (match et.et_finally with Some b -> visit_block idx b | None -> ())
+    | ExprUnsafe ops ->
+      List.iter (fun op ->
+        match op with
+        | UnsafeRead e -> visit_expr idx e
+        | UnsafeWrite (a, b) -> visit_expr idx a; visit_expr idx b
+        | UnsafeOffset (a, b) -> visit_expr idx a; visit_expr idx b
+        | UnsafeTransmute (_, _, e) -> visit_expr idx e
+        | UnsafeForget e -> visit_expr idx e
+      ) ops
+  and visit_stmt (idx : int) (s : stmt) : unit =
+    match s with
+    | StmtLet sl -> visit_expr idx sl.sl_value
+    | StmtExpr e -> visit_expr idx e
+    | StmtAssign (lhs, _, rhs) -> visit_expr idx lhs; visit_expr idx rhs
+    | StmtWhile (c, b) -> visit_expr idx c; visit_block idx b
+    | StmtFor (_, it, b) -> visit_expr idx it; visit_block idx b
+  and visit_block (idx : int) (b : block) : unit =
+    List.iter (visit_stmt idx) b.blk_stmts;
+    match b.blk_expr with Some e -> visit_expr idx e | None -> ()
+  in
+  List.iteri (fun i s -> visit_stmt i s) blk.blk_stmts;
+  let tail_idx = List.length blk.blk_stmts in
+  (match blk.blk_expr with
+   | Some e -> visit_expr tail_idx e
+   | None -> ());
+  tbl
+
 (** Check borrows in an expression *)
 let rec check_expr (ctx : context) (state : state) (symbols : Symbol.t) (expr : expr) : unit result =
   match expr with
@@ -1000,10 +1107,41 @@ and check_block (ctx : context) (state : state) (symbols : Symbol.t) (blk : bloc
      ref-bindings introduced here do not leak past block exit. CORE-01. *)
   let block_locals_at_entry = state.block_local_syms in
   let ref_bindings_at_entry = state.ref_bindings in
-  let* () = List.fold_left (fun acc stmt ->
-    let* () = acc in
-    check_stmt ctx state symbols stmt
-  ) (Ok ()) blk.blk_stmts in
+  (* NLL last-use pre-pass (CORE-01 pt3 / #177 Slice A): compute the last
+     statement index at which each symbol is mentioned. After each
+     statement we expire any ref-binding introduced in *this* block whose
+     binder's last use has already passed, releasing the underlying
+     borrow. This is the non-lexical-lifetimes win — patterns like
+     [let r = &x; print(*r); x = 2] now type-check, while the
+     anti-aliasing rules remain sound because the borrow is still live
+     across statements that *do* use the binder. *)
+  let last_use = compute_last_use_index symbols blk in
+  let last_use_of (sym : Symbol.symbol_id) : int =
+    match Hashtbl.find_opt last_use sym with
+    | Some i -> i
+    | None -> -1
+  in
+  let is_outer_binding (sym : Symbol.symbol_id) : bool =
+    List.exists (fun (sym', _) -> sym' = sym) ref_bindings_at_entry
+  in
+  let expire_dead_ref_bindings (stmt_idx : int) : unit =
+    let dying, still_live =
+      List.partition (fun (sym, _b) ->
+        (not (is_outer_binding sym)) && last_use_of sym <= stmt_idx
+      ) state.ref_bindings
+    in
+    List.iter (fun (_sym, b) -> end_borrow state b) dying;
+    state.ref_bindings <- still_live
+  in
+  let* () =
+    let indexed = List.mapi (fun i s -> (i, s)) blk.blk_stmts in
+    List.fold_left (fun acc (i, stmt) ->
+      let* () = acc in
+      let* () = check_stmt ctx state symbols stmt in
+      expire_dead_ref_bindings i;
+      Ok ()
+    ) (Ok ()) indexed
+  in
   let* () = match blk.blk_expr with
     | Some e -> check_expr ctx state symbols e
     | None   -> Ok ()
@@ -1190,10 +1328,24 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
    bare block-statements already parsed; the `-> &T`/`&T` *type* sigil was
    deliberately not added (`ref T`/`mut T` keyword types already exist).
 
-   Still deferred — now the *analysis*, no longer parser-gated:
-   - Non-lexical lifetimes with region inference (Polonius-style).
+   CORE-01 pt3 Slice A (NLL last-use): ref-bindings introduced in a
+   block now expire at the binder's *last use*, not at block exit. A
+   forward pre-pass (compute_last_use_index) maps each symbol to the
+   greatest statement index that mentions it (the tail expression
+   counts as the n-th statement); after each statement, check_block
+   releases the underlying borrow of any in-block ref-binding whose
+   binder is now dead. Unblocks the canonical NLL patterns
+   ([let r = &x; print(*r); x = 2] and [let m = &mut x; let y = *m; x]),
+   while still rejecting real conflicts (the anti-aliasing rules fire
+   against statements that *do* use the binder, before expiry).
+   Outer-block ref-bindings are deliberately preserved — they expire
+   only at their own block's exit.
+
+   Still deferred — region-/flow-sensitive remainder:
    - Flow-sensitive escape via assignment to an outer mutable
-     (`outer = &x`) — now *expressible* (`&mut`, assignment, blocks all
-     parse); the remaining work is the dataflow analysis itself.
+     (`outer = &x`): the assignment must update the borrow graph the
+     way [let r = &x] already does.
+   - Origin/region variables (Polonius surface) + loan-live-at-point
+     dataflow across CFG joins (Slice C).
    - Tighter integration with the quantity checker for captured linears.
 *)

test/e2e/fixtures/borrow_nll_assign_after_last_use.affine

@@ -0,0 +1,19 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice A / #177: NLL last-use expiry. Under purely lexical
+// lifetimes this program is rejected: the borrow held by `r` lives until
+// block exit, so the assignment `x = 2` triggers MoveWhileBorrowed. With
+// non-lexical lifetimes, `r` is dead after the `let y` statement (its
+// last mention), so the borrow on `x` has been released by the time the
+// assignment is checked. Expected: Ok.
+
+module BorrowNllAssignAfterLastUse;
+
+fn nll_assign() -> Int {
+  let mut x = 1;
+  let r = &x;
+  let y = *r;
+  x = 2;
+  x + y
+}

test/e2e/fixtures/borrow_nll_read_after_mut_last_use.affine

@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice A / #177: NLL last-use expiry for *exclusive*
+// borrows. Under lexical lifetimes the tail `x` is rejected as
+// UseWhileExclusivelyBorrowed because `m`'s exclusive borrow on `x`
+// lives until block exit. With NLL, `m` is dead after `let y`, so the
+// tail read of `x` is legal. Expected: Ok.
+
+module BorrowNllReadAfterMutLastUse;
+
+fn nll_excl() -> Int {
+  let mut x = 5;
+  let m = &mut x;
+  let y = *m;
+  x + y
+}

test/e2e/fixtures/borrow_nll_still_rejects_live_borrow.affine

@@ -0,0 +1,18 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell
+//
+// CORE-01 pt3 Slice A / #177 anti-regression: NLL last-use must NOT
+// release a borrow that is *still* used later. Here `r` is mentioned
+// in the tail `*r`, so its last-use index is after the assignment.
+// The assignment to `x` while `r` is alive must still be rejected
+// (MoveWhileBorrowed). This guards against an over-eager expiry that
+// would silently allow real aliasing bugs.
+
+module BorrowNllStillRejectsLiveBorrow;
+
+fn bad() -> Int {
+  let mut x = 1;
+  let r = &x;
+  x = 2;
+  *r
+}