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

Replaces the lexical "ref-binding lives until block exit" rule with a
proper non-lexical lifetime: a ref-binding's underlying borrow is now
released after the binder's *last use* statement, not at block exit.

The lexical rule made `let r = &x; print(*r); x = 2` an unavoidable
`MoveWhileBorrowed` even though `r` is provably dead before the
assignment. Under NLL the borrow on `x` has expired by the time the
assignment is checked, so the program type-checks — matching Rust's
NLL semantics for the same shape.

Mechanics in lib/borrow.ml:

- `compute_last_use_index` (new): forward pre-pass that returns a
  `(sym_id -> int)` table mapping each symbol to the greatest statement
  index that mentions it (the block's tail expression counts as the
  n-th statement, where n = |stmts|). Visits every expression / stmt /
  block / lambda body / handler arm / unsafe op so a use buried inside
  a nested block or an `if`/`match` branch still pins the outer stmt's
  index. Symbols never mentioned are absent → callers treat as -1.

- `check_block` now runs the pre-pass and, after each statement, calls
  `expire_dead_ref_bindings i` to release any ref-binding *introduced
  in this block* whose binder's last use is ≤ i. Outer-block
  ref-bindings are deliberately preserved — they expire only at their
  own block's exit. Expiry both `end_borrow`s the held borrow and
  drops the (sym, b) entry from `state.ref_bindings`, so subsequent
  checks see a clean borrow set.

Soundness preserved: the anti-aliasing rules
(`MoveWhileBorrowed` / `UseWhileExclusivelyBorrowed` / `ConflictingBorrow`)
still fire for any statement that reads or assigns the owner *before*
the binder's last use, because the borrow is still on `state.borrows`
at that point. The new `borrow_nll_still_rejects_live_borrow.affine`
fixture pins this — a binder used in the tail must keep the borrow
alive across the intervening assignment.

Tests (E2E Borrow Graph, +3):
- `borrow_nll_assign_after_last_use.affine` — assign after a shared
  borrow's last use is now OK
- `borrow_nll_read_after_mut_last_use.affine` — read after an
  exclusive borrow's last use is now OK
- `borrow_nll_still_rejects_live_borrow.affine` — assign while the
  binder is still live (mentioned in tail) is still rejected

Pre-existing fixtures audited end-to-end against the new flow:
return-escape (`borrow_return_escape_{local,param}`) still fires
because `check_return_escape` runs against `state.ref_bindings` *during*
check_stmt for `StmtExpr (ExprReturn ...)`, before that statement's
expire pass; block-tail `&local` (`borrow_outlives_owner`) still fires
because the in-block tail check uses `ref_target`, not `ref_bindings`;
the `&mut` conflict/use-while fixtures still fire because the
violations are detected before the binder's last-use index. No change
to the over-rejection corpus.

Multi-day Phase-3 plan (Slices B–D remaining):
  B — flow-sensitive escape via `outer = &x` (assignment must update
      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

Docs: STATE.a2ml `borrow-checker`, CAPABILITY-MATRIX.adoc, TECH-DEBT.adoc
CORE-01 row updated to "pts 1–3 Slice A landed".

NOTE: this commit was authored in a remote container without an OCaml
toolchain installed, so `dune build` / `dune runtest` were not run
locally; CI is the source of truth. The change is mechanically scoped
to the borrow checker, with the AST visitor covering all 24 expr / 5
stmt / 5 unsafe_op variants.

Author: claude

.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
+}