fix(borrow): close #554 use-after-move through a callee-returned borrow

A call whose result borrows one of its arguments now registers the
borrow-graph edge that was missing. Each function carries a return-borrow
summary (compute_ret_borrow_params): the parameter indices whose borrow may
flow out via the return value (a returned `&p` / `return p` for a `ref`/`mut`
parameter, directly, via a let-bound ref-local chain, or through an
`if`/`match`/block tail in return position). At a call site those argument
borrows stay live exactly like a plain `&` borrow — claimed into the result
binder (NLL-governed) or lingering to block exit — so
`let r = pick(a); consume(a); *r` is now MoveWhileBorrowed while the
legitimate NLL reorderings still pass. The control (plain double-consume) and
the whole pre-existing valid corpus are unaffected: only calls to functions
that actually return a borrow of a parameter change behaviour.

Hardened across two adversarial-verification rounds: the aggregate-storage,
assign-path, summary-via-arm-tail, and `return`-statement-form holes a first
cut missed were all found and closed. Residuals — interprocedural-through-
call-result; the branch-merged / copy-out claim (proven `&`-symmetric, a
pre-existing lexical limitation inherited not introduced); and a reassign
old-loan over-rejection (sound direction) — are documented in-code and closed
properly by Polonius (#553); the mechanized proof is tracked as #515.

7 regression fixtures + Alcotest cases added; full suite 393/393 green.
ADR-022 reframed (residual = soundness, not precision; status ratified).

Closes #554.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

docs/decisions/0022-polonius-origin-variables.adoc

@@ -6,7 +6,7 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toclevels: 2
 :icons: font
 
-Status:: Proposed
+Status:: Accepted (architecture ratified in PR #407 thread, 2026-05-27; staged implementation tracked in #553)
 Date:: 2026-05-26
 Issue:: https://github.com/hyperpolymath/affinescript/issues/177[CORE-01 #177]
 Series:: Settled-decisions ledger; companion entry in `.machine_readable/6a2/META.a2ml`.
@@ -36,7 +36,14 @@ type. The checker can prove what it sees locally; it cannot reason about:
 
 * Cross-function borrows that outlive a returned struct field. The current
   return-escape rule (`callee_owned_params`) is a name-set heuristic, not
-  a constraint discharge.
+  a constraint discharge. This residual is *soundness*, not merely
+  precision: issue #554 exhibited a probe-verified false negative
+  (`let r = pick(a); consume(a); *r` — a use-after-move through a
+  callee-returned borrow — accepted end-to-end). It was closed in the
+  lexical checker on 2026-06-14 by per-function return-borrow summaries
+  (`compute_ret_borrow_params`, `lib/borrow.ml`); the full constraint-based
+  discharge of the general interprocedural case remains this ADR's job
+  (#553), and its mechanized proof is #515.
 * True reborrows through indirection (`r2 = r1` where `r1` is itself a
   ref-binder, RHS is not a direct `&place`) — see the matching residual
   TODO immediately above the Polonius one (`record_ref_binding` does not

lib/borrow.ml

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 — aggregate-storage variant (found by adversarial verification). A
+// callee-returned borrow stored into a tuple (record / array behave the
+// same) must keep the aliased argument borrowed: storing `pick(b)` into a
+// tuple, moving `b`, then reading `*(pair.0)` is a use-after-move and must
+// be rejected. A first cut released unclaimed escaping borrows at statement
+// end, which silently dropped protection here; the borrow now lingers like
+// a plain `&` borrow until block exit.
+
+module BorrowCalleeReturnedBorrowAggregate;
+
+fn pick(ref x: Int) -> ref Int {
+  return &x;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let b: Int = 9;
+  let pair = (pick(b), 0);
+  let _gone = consume(b);
+  let v = *(pair.0);
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_aggregate.affine

@@ -0,0 +1,30 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 — summary-via-arm-tail variant (found by adversarial verification).
+// The return-borrow summary must recognise a borrow returned through a bare
+// `match` (or `if`) arm tail, not only a direct `return &x`. Here `pickm`
+// returns `&x` via both match arms, so a caller that moves the argument
+// while the result is live must be rejected. The summary walker treats
+// arm-tail positions as return positions (walk_tail).
+
+module BorrowCalleeReturnedBorrowMatchArm;
+
+fn pickm(ref x: Int, flag: Bool) -> ref Int {
+  match flag {
+    true => &x,
+    false => &x,
+  }
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 7;
+  let r = pickm(a, true);
+  let _gone = consume(a);
+  let v = *r;
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_match_arm.affine

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 anti-over-rejection guard. Same shape as the use-after-move probe,
+// but `*r` is read BEFORE `a` is moved. Under NLL last-use, `r`'s borrow on
+// `a` is released after `let v = *r` (r's last mention), so moving `a`
+// afterwards is legal. Must pass — the #554 fix must not degrade into a
+// lexical-only over-rejection that keeps the callee-returned borrow alive
+// to block exit.
+
+module BorrowCalleeReturnedBorrowNllOk;
+
+fn pick(ref x: Int) -> ref Int {
+  return &x;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 7;
+  let r = pick(a);
+  let v = *r;
+  let _gone = consume(a);
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_nll_ok.affine

@@ -0,0 +1,32 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 — assign-path variant (found by adversarial verification). Re-binding
+// a mutable ref-binder to a callee-returned borrow (`r = other(b)`) must keep
+// `b` borrowed for the lifetime of `r`: moving `b` and then reading `*r` is a
+// use-after-move and must be rejected. The escaping borrow lingers on the
+// borrow set exactly as a plain `&b` would.
+
+module BorrowCalleeReturnedBorrowReassign;
+
+fn pick(ref x: Int) -> ref Int {
+  return &x;
+}
+
+fn other(ref y: Int) -> ref Int {
+  return &y;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 1;
+  let b: Int = 2;
+  let mut r = pick(a);
+  r = other(b);
+  let _gone = consume(b);
+  let v = *r;
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_reassign.affine

@@ -0,0 +1,28 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 — return-STATEMENT-through-branch variant (found by second-pass
+// adversarial verification, and the most idiomatic spelling). A borrow
+// returned via `return if d { &x } else { &x };` must register in the
+// return-borrow summary just like the bare-tail form `if d { &x } else { &x }`.
+// The summary walker treats a returned value as a tail position regardless of
+// where the `return` keyword sits (walk_expr's ExprReturn delegates to
+// walk_tail). Moving the argument while the result is live must be rejected.
+
+module BorrowCalleeReturnedBorrowReturnStmt;
+
+fn pickr(ref x: Int, d: Bool) -> ref Int {
+  return if d { &x } else { &x };
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 7;
+  let r = pickr(a, true);
+  let _gone = consume(a);
+  let v = *r;
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_return_stmt.affine

@@ -0,0 +1,29 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 — soundness regression. A use-after-move through a callee-returned
+// borrow must be rejected. `pick` returns a borrow of its `ref` (caller-
+// owned) parameter, so `let r = pick(a)` makes `r` borrow `a`; moving `a`
+// (into the `own` parameter of `consume`) while `r` is still live — its
+// last use `*r` comes later — must raise MoveWhileBorrowed. Pre-fix this
+// passed the full pipeline ("Type checking passed") because the borrow
+// graph had no edge from `r` to `a`: the loan returned by `pick` was
+// invisible.
+
+module BorrowCalleeReturnedBorrowUam;
+
+fn pick(ref x: Int) -> ref Int {
+  return &x;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 7;
+  let r = pick(a);
+  let _gone = consume(a);
+  let v = *r;
+  return v;
+}

test/e2e/fixtures/borrow_callee_returned_borrow_uam.affine

@@ -0,0 +1,26 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 precision guard. `read_ref` takes a `ref` parameter but returns a
+// *value* (`*a`), not a borrow — so its return-borrow summary is empty and
+// the call-argument borrow is still released at call end (pre-existing
+// behaviour). The argument `a` therefore stays movable afterwards. Must
+// pass: the fix must scope strictly to callees that actually return a
+// borrow of a parameter.
+
+module BorrowCalleeValueReturnOk;
+
+fn read_ref(ref a: Int) -> Int {
+  return *a;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 7;
+  let y = read_ref(a);
+  let _g = consume(a);
+  return y;
+}

test/e2e/fixtures/borrow_callee_value_return_ok.affine

@@ -5155,6 +5155,101 @@ let test_slice_d_captured_nonlinear_ok () =
                     spuriously rejected — the new rule must scope to \
                     @linear only: " ^ Borrow.format_borrow_error e)
 
+(* #554 — soundness: use-after-move through a callee-returned borrow.
+   `pick(ref x) -> ref Int` returns a borrow of its parameter, so
+   `let r = pick(a)` makes `r` borrow `a`.  Moving `a` while `r` is still
+   live must be rejected; pre-fix the borrow graph had no `r -> a` edge so
+   the move slipped past the full pipeline.  Three tests pin: (1) the
+   use-after-move is now caught (MoveWhileBorrowed); (2) the NLL-reordered
+   form (read `*r` before the move) still passes — no lexical over-
+   rejection; (3) a `ref`-param callee that returns a *value* leaves the
+   argument movable (empty return-borrow summary). *)
+let test_borrow_callee_returned_borrow_uam () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_uam.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554: expected MoveWhileBorrowed (move of `a` while the \
+                    callee-returned borrow held by `r` is live), got: "
+                   ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 regressed: use-after-move through a callee-returned \
+                   borrow was accepted — the result binder did not borrow \
+                   the argument"
+
+let test_borrow_callee_returned_borrow_nll_ok () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_nll_ok.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("#554 anti-over-rejection: reading `*r` before moving `a` \
+                    must pass under NLL last-use, got: "
+                   ^ Borrow.format_borrow_error e)
+
+let test_borrow_callee_value_return_ok () =
+  match borrow_result (fixture "borrow_callee_value_return_ok.affine") with
+  | Ok () -> ()
+  | Error e ->
+    Alcotest.fail ("#554 precision: a `ref`-param callee that returns a \
+                    *value* has an empty return-borrow summary, so the arg \
+                    stays movable, got: " ^ Borrow.format_borrow_error e)
+
+(* #554 hardening — three variants found by adversarial verification that a
+   first cut of the fix missed. All must be rejected: (1) the callee-returned
+   borrow stored into an aggregate (tuple) must still keep the arg borrowed;
+   (2) reassigning a mutable ref-binder to a callee-returned borrow must keep
+   the new target borrowed; (3) a borrow returned through a bare `match` arm
+   tail must register in the return-borrow summary. *)
+let test_borrow_callee_returned_borrow_aggregate () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_aggregate.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554 aggregate: expected MoveWhileBorrowed (move of `b` \
+                    while the borrow stored in the tuple is live), got: "
+                   ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 aggregate regressed: a callee-returned borrow stored \
+                   into a tuple did not keep the argument borrowed — \
+                   use-after-move accepted"
+
+let test_borrow_callee_returned_borrow_reassign () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_reassign.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554 reassign: expected MoveWhileBorrowed (move of `b` \
+                    while `r = other(b)` holds its borrow), got: "
+                   ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 reassign regressed: reassigning a ref-binder to a \
+                   callee-returned borrow did not keep the new target \
+                   borrowed — use-after-move accepted"
+
+let test_borrow_callee_returned_borrow_match_arm () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_match_arm.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554 match-arm summary: expected MoveWhileBorrowed (the \
+                    borrow returned via the match arm must be summarised), \
+                    got: " ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 match-arm summary regressed: a borrow returned via a \
+                   bare match-arm tail was not recorded in the return-borrow \
+                   summary — use-after-move accepted"
+
+(* #554 — the idiomatic `return if/match { ... };` spelling. The returned
+   value is in tail position no matter where `return` sits, so the summary
+   must still record the arm-tail borrow. A first cut walked the returned
+   value as a non-tail expression and missed it. *)
+let test_borrow_callee_returned_borrow_return_stmt () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_return_stmt.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554 return-stmt summary: expected MoveWhileBorrowed (a \
+                    borrow returned via `return if d { &x } else { &x };` \
+                    must be summarised), got: " ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 return-stmt summary regressed: a borrow returned via \
+                   a `return <branch>;` statement was not recorded in the \
+                   return-borrow summary — use-after-move accepted"
+
 let borrow_tests = [
   Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
     `Quick test_borrow_outlives_owner;
@@ -5212,6 +5307,20 @@ let borrow_tests = [
     `Quick test_slice_d_captured_linear_param_rejected;
   Alcotest.test_case "Slice D anti-regression: non-linear capture still OK (#177 pt3)"
     `Quick test_slice_d_captured_nonlinear_ok;
+  Alcotest.test_case "#554: use-after-move through callee-returned borrow rejected"
+    `Quick test_borrow_callee_returned_borrow_uam;
+  Alcotest.test_case "#554 anti-over-rejection: NLL reorder of callee-returned borrow OK"
+    `Quick test_borrow_callee_returned_borrow_nll_ok;
+  Alcotest.test_case "#554 precision: value-returning ref-param callee leaves arg movable"
+    `Quick test_borrow_callee_value_return_ok;
+  Alcotest.test_case "#554 aggregate: callee-returned borrow stored in tuple keeps arg borrowed"
+    `Quick test_borrow_callee_returned_borrow_aggregate;
+  Alcotest.test_case "#554 reassign: r = call() keeps the new target borrowed"
+    `Quick test_borrow_callee_returned_borrow_reassign;
+  Alcotest.test_case "#554 summary: borrow returned via match-arm tail is tracked"
+    `Quick test_borrow_callee_returned_borrow_match_arm;
+  Alcotest.test_case "#554 summary: `return if/match {..};` statement form is tracked"
+    `Quick test_borrow_callee_returned_borrow_return_stmt;
 ]
 
 (* ============================================================================