feat(ADR-022 M3): model mut-param call-aliasing in the Polonius extractor

Close the call-aliasing divergence (borrow_use_while_excl): passing `x` to
a `mut` parameter and reading `x` again in the SAME call —
`mut_then_read(x, x)` — was flagged by the lexical checker
(UseWhileExclusivelyBorrowed) but not by the Polonius extractor, so the
fixture sat on the parallel-run allowlist.

The extractor now mirrors the lexical checker's left-to-right argument
fold: a `mut`-param argument that denotes a place mints a CALL-SCOPED
exclusive loan (born at the enclosing point, killed at point+1 so it never
reaches the next statement), and any LATER argument of the SAME call whose
place overlaps an earlier `mut`-arg's loan emits a conflict. Order- and
call-scoped, exactly matching the fold: it cannot fire across statements,
so `just_mut(x); read_int(x)` stays accepted, and it over-approximates only
toward MORE real same-call conflicts the lexical checker also reports — no
false positive. The loans are emitted as raw borrow_at/killed/conflict_at
facts only (not pushed onto the loan list), so the generic use-while rule
and the move passes are untouched; the solver invalidates them via liveness.

Allowlist 7 -> 6 (borrow_use_while_excl pruned). Corpus parallel-run gate
stays green (117 fixtures, zero unexpected divergence). Adds two hardening
tests: the call-aliasing flag, and the call-scoped anti-over-rejection case.
528 -> 530 tests green.

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

Author: hyperpolymath

lib/borrow_extract.ml

@@ -401,6 +401,85 @@ let extract_fn (ctx : Borrow.context) (symbols : Symbol.t) (fd : fn_decl) : PF.f
         then conflict_at := (rl.rl_id, pt) :: !conflict_at)
         !loans)
       !use_at;
+    (* M3 call-aliasing (mut-param argument). The lexical checker folds a call's
+       arguments left-to-right: a [mut] parameter's argument takes a CALL-SCOPED
+       EXCLUSIVE borrow ([record_borrow … Exclusive]) and every SUBSEQUENT
+       argument's read trips [find_aliasing_exclusive] — so [mut_then_read(x, x)]
+       is rejected, while the borrow's release after the call keeps
+       [just_mut(x); read_int(x)] accepted. We mirror that exactly: per call,
+       fold the args in order; mint a call-scoped exclusive loan (born at the
+       enclosing point [pt], killed at [pt+1] so it never reaches the next
+       statement) for each [mut]-param arg that denotes a place, and emit a
+       conflict for any LATER arg of the SAME call whose place overlaps an
+       exclusive loan minted by an EARLIER arg. Order- and call-scoped, matching
+       the fold: it cannot fire across statements, and (over-approximating only
+       toward MORE real same-call conflicts the lexical checker also sees) cannot
+       introduce a false positive. These loans are emitted as raw facts only — not
+       pushed onto [!loans] — so the generic use-while rule above and the move
+       passes are unaffected; the solver needs just [borrow_at]/[killed]/
+       [conflict_at] to invalidate them. *)
+    let process_call pt fname args =
+      match Hashtbl.find_opt ctx.Borrow.fn_sigs fname with
+      | None -> ()
+      | Some sg ->
+        let owns = sg.Borrow.fn_param_ownerships in
+        ignore (List.fold_left (fun excls (i, arg) ->
+          let ap = Borrow.expr_to_place symbols (peel arg) in
+          (match ap with
+           | Some p ->
+             List.iter (fun rl ->
+               if Borrow.places_overlap p rl.rl_place then
+                 conflict_at := (rl.rl_id, pt) :: !conflict_at) excls
+           | None -> ());
+          match (List.nth_opt owns i, ap) with
+          | (Some (Some Mut), Some p) ->
+            let l = fresh next_loan in
+            borrow_at   := (l, pt) :: !borrow_at;
+            loan_origin := (l, fresh next_origin) :: !loan_origin;
+            killed      := (l, pt + 1) :: !killed;
+            { rl_id = l; rl_place = p; rl_binder = None; rl_excl = true } :: excls
+          | _ -> excls)
+          [] (List.mapi (fun i a -> (i, a)) args))
+    in
+    let call_here pt e =
+      match peel e with
+      | ExprApp (f, args) ->
+        (match peel f with ExprVar id -> process_call pt id.name args | _ -> ())
+      | _ -> ()
+    in
+    let rec alias_stmt pt s =
+      match s with
+      | StmtLet sl -> alias_expr pt sl.sl_value
+      | StmtExpr e -> alias_expr pt e
+      | StmtAssign (l, _, r) -> alias_expr pt l; alias_expr pt r
+      | StmtWhile (c, b) -> alias_expr pt c; alias_block pt b
+      | StmtFor (_, it, b) -> alias_expr pt it; alias_block pt b
+    and alias_expr pt e =
+      call_here pt e;
+      match peel e with
+      | ExprApp (f, args) -> alias_expr pt f; List.iter (alias_expr pt) args
+      | ExprUnary (_, x) -> alias_expr pt x
+      | ExprBinary (a, _, b) | ExprIndex (a, b) -> alias_expr pt a; alias_expr pt b
+      | ExprField (b, _) | ExprTupleIndex (b, _) -> alias_expr pt b
+      | ExprTuple xs | ExprArray xs -> List.iter (alias_expr pt) xs
+      | ExprIf ei ->
+        alias_expr pt ei.ei_cond; alias_expr pt ei.ei_then;
+        (match ei.ei_else with Some e -> alias_expr pt e | None -> ())
+      | ExprMatch em ->
+        alias_expr pt em.em_scrutinee;
+        List.iter (fun a -> alias_expr pt a.ma_body) em.em_arms
+      | ExprBlock blk -> alias_block pt blk
+      | ExprTry et ->
+        alias_block pt et.et_body;
+        (match et.et_catch with Some arms -> List.iter (fun a -> alias_expr pt a.ma_body) arms | None -> ());
+        (match et.et_finally with Some b -> alias_block pt b | None -> ())
+      | _ -> ()
+    and alias_block pt blk =
+      List.iter (alias_stmt pt) blk.blk_stmts;
+      (match blk.blk_expr with Some e -> alias_expr pt e | None -> ())
+    in
+    List.iteri alias_stmt blk.blk_stmts;
+    (match blk.blk_expr with Some e -> alias_expr nstmts e | None -> ());
     { PF.empty_facts with
       borrow_at = !borrow_at; loan_origin = !loan_origin;
       killed = !killed; cfg_edge = base_cfg @ !extra_edges; conflict_at = !conflict_at;

test/test_borrow_polonius.ml

@@ -181,6 +181,24 @@ let t_extract_shared_read_ok () =
   Alcotest.(check bool) "Polonius accepts read-while-shared-borrowed" false pol;
   Alcotest.(check bool) "agrees with lexical" lex pol
 
+(* M3 call-aliasing: passing `x` to a `mut` parameter AND a plain parameter in
+   the SAME call — `mut_then_read(x, x)`. The `mut`-arg mints a call-scoped
+   exclusive loan; the second arg reads `x` while it is live ⇒ conflict. Both
+   tiers must flag it. *)
+let t_extract_call_alias_excl () =
+  let (pol, lex) = polonius_vs_lexical "borrow_use_while_excl.affine" in
+  Alcotest.(check bool) "Polonius flags mut-param call-aliasing" true pol;
+  Alcotest.(check bool) "agrees with lexical" lex pol
+
+(* anti-over-rejection: a `mut`-param borrow is CALL-SCOPED, so a use of `x` in a
+   LATER, separate call is fine — `just_mut(x); read_int(x)` is valid under both
+   tiers. Guards the new call-aliasing rule against leaking the loan past its
+   call. *)
+let t_extract_call_arg_then_use_ok () =
+  let (pol, lex) = polonius_vs_lexical "borrow_call_arg_then_use.affine" in
+  Alcotest.(check bool) "Polonius accepts mut-arg then later use" false pol;
+  Alcotest.(check bool) "agrees with lexical" lex pol
+
 (* expression-level branches (issue-draft 08 conditional-origin family): the RHS
    borrows the UNION of its arm sources. Polonius must now match the lexical fix. *)
 let t_extract_cond_if () =
@@ -302,21 +320,21 @@ let t_extract_reassign_uam () =
    regression gate M3 exists to provide. The extractor is NOT wired into
    bin/main.ml; this gate guards the equivalence claim, not the build verdict.
 
-   Each allowlist entry is (fixture, reason). 16 are sound UNDER-reporting —
-   features the extractor does not model yet, where lexical flags an error and
-   Polonius (conservatively) does not. 1 is a known false positive
-   (reassign_old_ok) awaiting the reborrow/loan-release increment. As later
-   increments land, entries graduate OFF this list; an allowlisted fixture that
-   has started AGREEING is logged (prune it) but does not fail the gate. *)
+   Each allowlist entry is (fixture, reason). All remaining entries are sound
+   UNDER-reporting — features the extractor does not model yet, where lexical
+   flags an error and Polonius (conservatively) does not, so the divergence is
+   never a false positive. As later increments land, entries graduate OFF this
+   list; an allowlisted fixture that has started AGREEING is logged (prune it)
+   but does not fail the gate. *)
 let known_divergences : (string * string) list =
   [ (* loan-vs-loan exclusivity (use-while-exclusively-borrowed) is now modeled
        by the extractor (a direct read of a place while a live [&mut] loan
        covers it is a conflict), so borrow_mutref_conflict / borrow_mutref_use_while
-       AGREE and were pruned. borrow_use_while_excl is the call-aliasing shape
-       (passing [x] to a [mut] param and reading [x] in the same call) — a
-       [mut]-param argument is not yet modeled as a call-scoped exclusive loan,
-       so it stays here. *)
-    "borrow_use_while_excl.affine", "mut-param-arg aliasing (call-scoped excl borrow not modeled)";
+       AGREE and were pruned. The call-aliasing shape (borrow_use_while_excl:
+       passing [x] to a [mut] param and reading [x] in the same call) is now
+       modeled too — a [mut]-param argument mints a call-scoped exclusive loan
+       and a later same-call arg reading [x] conflicts — so it also AGREES and
+       was pruned. *)
     (* unmodeled: return-escape / borrow-outlives-owner (no escape analysis) *)
     "borrow_outlives_owner.affine", "borrow-outlives-owner";
     "borrow_return_escape_local.affine", "return-escape (local)";
@@ -377,6 +395,8 @@ let tests =
     Alcotest.test_case "extract+solve: &mut/&mut overlap flagged (loan-vs-loan)" `Quick t_extract_mutref_conflict;
     Alcotest.test_case "extract+solve: use-while-&mut-borrowed flagged" `Quick t_extract_mutref_use_while;
     Alcotest.test_case "extract+solve: read-while-&-shared accepted (no over-reject)" `Quick t_extract_shared_read_ok;
+    Alcotest.test_case "extract+solve: mut-param call-aliasing flagged" `Quick t_extract_call_alias_excl;
+    Alcotest.test_case "extract+solve: mut-arg then later use accepted (call-scoped)" `Quick t_extract_call_arg_then_use_ok;
     (* M3 branch extraction: conditional-origin family (issue-draft 08) *)
     Alcotest.test_case "extract+solve: if-bound UAM, agrees with lexical" `Quick t_extract_cond_if;
     Alcotest.test_case "extract+solve: block-bound UAM, agrees with lexical" `Quick t_extract_cond_block;