fix(borrow): round-3 hardening — ref-count Slice-B reassign + union reassigned-local summary

A third adversarial-verification pass on the #554 return-borrow work surfaced
two more reachable holes (and confirmed the interprocedural fixpoint is robust:
60-level wrapper chains, mutual recursion, and 3-cycles all terminate in ms and
summarise correctly).

- Slice-B `&` reassign (a PRE-EXISTING soundness bug, exposed by the #554 (c)
  block being more correct): `r = &b` ended the binder's old loan
  UNCONDITIONALLY, so `let r2 = r; r = &b; consume(a); *r2` dropped the borrow
  `r2` still aliased and accepted a use-after-move. Now ref-counted by b_id
  (mirroring the (c) block and expire_dead_ref_bindings), so an aliased loan
  survives the reassign. The `&mut` variant (exclusive aliasing) is caught too.

- Reassigned-local summary: the summary walker did not update a reassigned
  ref-local's origins, so `let mut t = pick(y); t = pick(x); return t`
  summarised the stale {y}. It now UNIONs origins on reassignment
  (conservative, flow-insensitive), summarising {x,y}.

Two low-severity residuals are documented in-code (Polonius #553 closes them):
a summary that cannot bootstrap an origin for a base-case-less divergent
recursion (unreachable — the function never returns), and a loop-body reassign
to an outer borrow (&-symmetric, predates #554).

Full suite 397/397 green; +2 regression fixtures (alias-survives-reassign,
reassigned-local-summary).

Refs #554.

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

Author: hyperpolymath

lib/borrow.ml

@@ -361,7 +361,22 @@ let compute_ret_borrow_params (lookup : string -> int list option)
     match s with
     | StmtLet sl -> walk_expr sl.sl_value; record_let sl.sl_pat sl.sl_value
     | StmtExpr e -> walk_expr e
-    | StmtAssign (l, _, r) -> walk_expr l; walk_expr r
+    | StmtAssign (l, _, r) ->
+      walk_expr l; walk_expr r;
+      (* A whole-var reassignment may change which parameters a ref-local
+         borrows.  UNION the new origins into the local's set (rather than
+         replace) so the flow-insensitive summary never *drops* a possible
+         origin — conservative, so [let mut t = pick(y); t = pick(x); return t]
+         summarises {x,y} not the stale {y}, closing the reassigned-local
+         false negative.  #554 round-3. *)
+      (match peel l with
+       | ExprVar id ->
+         let prior =
+           match Hashtbl.find_opt local_origins id.name with Some x -> x | None -> []
+         in
+         Hashtbl.replace local_origins id.name
+           (List.sort_uniq compare (prior @ origins_of_ref_source r))
+       | _ -> ())
     | StmtWhile (c, b) -> walk_expr c; walk_block b
     | StmtFor (_, it, b) -> walk_expr it; walk_block b
   and walk_block (blk : block) : unit =
@@ -1793,10 +1808,22 @@ and check_stmt (ctx : context) (state : state) (symbols : Symbol.t) (stmt : stmt
               when not rhs_is_self_binder
                 && is_reborrow_source state symbols rhs
                 && List.mem_assoc binder_sym state.ref_bindings ->
-              let old_borrow = List.assoc binder_sym state.ref_bindings in
-              end_borrow state old_borrow;
-              state.ref_bindings <-
-                List.filter (fun (s, _) -> s <> binder_sym) state.ref_bindings;
+              (* Ref-count the released loan(s) by [b_id]: only [end_borrow] an
+                 old borrow if no surviving ref-binding (e.g. a [let r2 = r]
+                 alias) still holds it — mirrors [expire_dead_ref_bindings] and
+                 the #554 (c) call-result reassign block.  Pre-fix this ended
+                 the borrow unconditionally, so [let r2 = r; r = &b] dropped the
+                 loan [r2] still names and accepted a later use-after-move of
+                 the old target.  (Found by #554 round-3 adversarial review;
+                 the bug predates #554 but the (c) block made the asymmetry
+                 visible.) *)
+              let old_entries, remaining =
+                List.partition (fun (s, _) -> s = binder_sym) state.ref_bindings
+              in
+              List.iter (fun (_, ob) ->
+                if not (List.exists (fun (_, b') -> b'.b_id = ob.b_id) remaining)
+                then end_borrow state ob) old_entries;
+              state.ref_bindings <- remaining;
               Some binder_sym
             | _ -> None
           in
@@ -2111,6 +2138,12 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
      loan (ref-counted by [b_id]) and rebinds to the escaping call result,
      so a later use of the old target is no longer spuriously rejected —
      symmetric with the plain-`&` Slice-B reborrow.
+   - *round-3 hardening* — the Slice-B `&` reassign path now ref-counts the
+     released loan by [b_id] too, so [let r2 = r; r = &b] keeps the borrow
+     [r2] still aliases (a *pre-existing* soundness bug the (c) block exposed
+     by being more correct); and the summary walker UNIONs a reassigned
+     ref-local's origins, so [let mut t = pick(y); t = pick(x); return t]
+     summarises {x,y} rather than the stale {y}.
 
    Still deferred:
    - Origin/region variables (true Polonius surface) — a region
@@ -2133,6 +2166,20 @@ let check_program (symbols : Symbol.t) (program : program) : unit result =
      same pre-existing through-branch / copy-out lexical limitation,
      inherited by the call-result path, not introduced by it.  A true
      flow-sensitive borrow graph (Polonius) discharges it uniformly.
+   - #554 minor residuals (round-3, both low-severity; Polonius #553 closes
+     them):
+       * *Divergent self/mutual recursion with no base case* — a function
+         whose only ref-return is its own recursive call (e.g.
+         [fn f(ref x) -> ref Int { let t = f(x); return t; }]) gets an empty
+         summary (the fixpoint cannot bootstrap an origin from a purely
+         self-transitive return), so a use-after-move through its result is
+         accepted.  Unreachable in practice: such a function never returns,
+         so the use never executes.  Any *terminating* recursion has a
+         non-recursive return path, which IS summarised.
+       * *Reassign inside a loop body to an outer borrow* —
+         [let mut r = pick(a); while … { r = pick(b) } consume(b); *r] is
+         accepted because the loop-body block drops its borrows at block exit
+         (predates #554, `&`-symmetric).
    - Tighter integration with the quantity checker for captured
      linears (Slice D).
 *)

test/e2e/fixtures/borrow_callee_returned_borrow_reassign_summary.affine

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// #554 reassigned-local summary (found by round-3 adversarial review). When a
+// returned ref-local is reassigned (`let mut t = pick(y); t = pick(x)`), the
+// return-borrow summary must UNION the origins so it does not go stale on the
+// initial binding. `wrap` here ultimately returns a borrow of `x`, so the
+// summary must include parameter 0; `let r = wrap(a, b); consume(a); *r` is a
+// use-after-move on `a` and must be rejected (the summary walker unions the
+// reassigned local's origins, conservatively).
+
+module BorrowCalleeReturnedBorrowReassignSummary;
+
+fn pick(ref x: Int) -> ref Int {
+  return &x;
+}
+
+fn wrap(ref x: Int, ref y: Int) -> ref Int {
+  let mut t = pick(y);
+  t = pick(x);
+  return t;
+}
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let a: Int = 1;
+  let b: Int = 2;
+  let r = wrap(a, b);
+  let _gone = consume(a);
+  let v = *r;
+  return v;
+}

test/e2e/fixtures/borrow_reassign_alias_survives.affine

@@ -0,0 +1,27 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2026 hyperpolymath
+//
+// Slice-B reassign ref-count (pre-existing soundness bug, found by #554
+// round-3 adversarial review). When a ref-binder is reassigned (`r = &b`),
+// its OLD loan must only be released if no surviving alias still holds it.
+// Here `let r2 = r` aliases `a`'s borrow into `r2`; after `r = &b`, `r2` still
+// borrows `a`, so moving `a` and then reading `*r2` is a use-after-move and
+// must be rejected. Pre-fix the Slice-B path ended the old borrow
+// unconditionally and the move slipped past.
+
+module BorrowReassignAliasSurvives;
+
+fn consume(own v: Int) -> Int {
+  return v;
+}
+
+fn main() -> Int {
+  let mut a: Int = 1;
+  let mut b: Int = 2;
+  let mut r = &a;
+  let r2 = r;
+  r = &b;
+  let _gone = consume(a);
+  let v = *r2;
+  return v;
+}

test/test_e2e.ml

@@ -5277,6 +5277,33 @@ let test_borrow_callee_returned_borrow_reassign_old_ok () =
                     target `a` must be movable again, got: "
                    ^ Borrow.format_borrow_error e)
 
+(* Slice-B reassign ref-count (pre-existing soundness bug found by #554
+   round-3): `let r2 = r; r = &b` must NOT drop the loan `r2` still aliases,
+   so a later move of the old target is rejected. *)
+let test_borrow_reassign_alias_survives () =
+  match borrow_result (fixture "borrow_reassign_alias_survives.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("Slice-B alias ref-count: expected MoveWhileBorrowed (r2 \
+                    still borrows `a` after `r = &b`), got: "
+                   ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "Slice-B alias regressed: reassigning `r` dropped the borrow \
+                   the `let r2 = r` alias still held — use-after-move accepted"
+
+(* #554 reassigned-local summary (found by round-3): a returned ref-local that
+   is reassigned must union its origins so the summary does not go stale. *)
+let test_borrow_callee_returned_borrow_reassign_summary () =
+  match borrow_result (fixture "borrow_callee_returned_borrow_reassign_summary.affine") with
+  | Error (Borrow.MoveWhileBorrowed _) -> ()
+  | Error e ->
+    Alcotest.fail ("#554 reassigned-local summary: expected MoveWhileBorrowed \
+                    (the reassigned local's origin must be unioned into the \
+                    summary), got: " ^ Borrow.format_borrow_error e)
+  | Ok () ->
+    Alcotest.fail "#554 reassigned-local summary regressed: the summary went \
+                   stale on the initial binding — use-after-move accepted"
+
 let borrow_tests = [
   Alcotest.test_case "BorrowOutlivesOwner: &local escapes its block"
     `Quick test_borrow_outlives_owner;
@@ -5352,6 +5379,10 @@ let borrow_tests = [
     `Quick test_borrow_callee_returned_borrow_interproc;
   Alcotest.test_case "#554 (c): reassign to call result releases old loan (precision)"
     `Quick test_borrow_callee_returned_borrow_reassign_old_ok;
+  Alcotest.test_case "Slice-B: reassign ref-counts old loan vs surviving alias"
+    `Quick test_borrow_reassign_alias_survives;
+  Alcotest.test_case "#554: reassigned returned ref-local unions summary origins"
+    `Quick test_borrow_callee_returned_borrow_reassign_summary;
 ]
 
 (* ============================================================================