feat(ADR-022 M3): model loan-vs-loan exclusivity in the Polonius extractor

Closes the borrow-vs-borrow divergence class (2 of the 9 allowlisted
extractor↔lexical disagreements). The extractor now emits a conflict for a
direct read of a place while a live `&mut` (exclusive) loan covers it:

  * `let b = &mut x` reads x at its creation point while the first `&mut x`
    is still live  → borrow_mutref_conflict now AGREES;
  * `let y = x` (plain read) while `&mut x` is live → borrow_mutref_use_while
    now AGREES.

Implementation: add rl_excl to the loan record (threaded from rhs_borrows);
a post-pass scans use_at × loans and, for each read of var v while an
EXCLUSIVE loan rooted at v is live, emits conflict_at — excluding the loan's
own birth point (that read IS the creation) and reads through the borrow
(`*a` has root a, not x, via PlaceDeref). Emission is liveness-gated by the
solver, so NLL last-use shortening keeps valid code accepted; shared `&`
loans never trigger it.

Tests: t_extract_mutref_conflict / _use_while (flagged), t_extract_shared_
read_ok (new fixture — read-while-shared-borrowed accepted, anti-over-reject).
Allowlist 9→7; corpus parallel-run gate green (no new divergence). 528 tests.

Remaining M3 divergences: return-escape/outlives-owner (4, needs escape
analysis), captured-linear (2), call-aliasing mut-param-arg (1).

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

Author: hyperpolymath

lib/borrow_extract.ml

@@ -137,7 +137,13 @@ let moved_places (ctx : Borrow.context) (symbols : Symbol.t) (e : expr)
         | _ -> []) args)
     | None -> []) (apps e)
 
-type rloan = { rl_id : int; rl_place : Borrow.place; rl_binder : Symbol.symbol_id option }
+type rloan = {
+  rl_id : int;
+  rl_place : Borrow.place;
+  rl_binder : Symbol.symbol_id option;
+  rl_excl : bool;  (** [&mut] (exclusive) vs [&] (shared) — drives the
+                       use-while-exclusively-borrowed conflict rule. *)
+}
 
 (** Extract the Polonius facts for one (straight-line) function body. *)
 let extract_fn (ctx : Borrow.context) (symbols : Symbol.t) (fd : fn_decl) : PF.facts =
@@ -207,11 +213,11 @@ let extract_fn (ctx : Borrow.context) (symbols : Symbol.t) (fd : fn_decl) : PF.f
     in
     let record_binder_loans (pt : int) (sym : Symbol.symbol_id) (rhs : expr) : unit =
       let kp = kill_for sym pt (pt + 1) in
-      List.iter (fun (place, _excl) ->
+      List.iter (fun (place, excl) ->
         let l = fresh next_loan in
         borrow_at   := (l, pt) :: !borrow_at;
         loan_origin := (l, fresh next_origin) :: !loan_origin;
-        loans       := { rl_id = l; rl_place = place; rl_binder = Some sym } :: !loans;
+        loans       := { rl_id = l; rl_place = place; rl_binder = Some sym; rl_excl = excl } :: !loans;
         killed      := (l, kp) :: !killed)
         (rhs_borrows ctx symbols rhs @ alias_places rhs)
     in
@@ -373,6 +379,28 @@ let extract_fn (ctx : Borrow.context) (symbols : Symbol.t) (fd : fn_decl) : PF.f
     in
     List.iteri moves_stmt blk.blk_stmts;
     (match blk.blk_expr with Some e -> do_point nstmts e; moves_expr nstmts e | None -> ());
+    (* M3 loan-vs-loan: use-while-exclusively-borrowed. A direct read of a place
+       while an EXCLUSIVE [&mut] loan covering it is live is a conflict. This
+       single rule subsumes both diverging mutref shapes:
+         - a second overlapping borrow — [let b = &mut x] reads [x] at its
+           creation point while the first [&mut x] is still live;
+         - a plain read — [let y = x] (or [x] in any read position) while
+           [&mut x] is live.
+       The read at the exclusive loan's OWN birth point is the borrow creation
+       itself (not a conflicting use), so loans born at [pt] are excluded. Reads
+       THROUGH the borrow ([*a]) have root [a] (PlaceDeref → root of the holder),
+       never the borrowed-from root [x], so they never match. Emission is
+       liveness-gated by the solver ([loan_invalidated_at] requires the loan to
+       be live at the point), so NLL last-use shortening keeps valid code
+       accepted — only [&mut], never [&], triggers it. *)
+    List.iter (fun (v, pt) ->
+      List.iter (fun rl ->
+        if rl.rl_excl
+           && (match Borrow.root_var rl.rl_place with Some rv -> rv = v | None -> false)
+           && not (List.exists (fun (l, p) -> l = rl.rl_id && p = pt) !borrow_at)
+        then conflict_at := (rl.rl_id, pt) :: !conflict_at)
+        !loans)
+      !use_at;
     { 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/e2e/fixtures/borrow_shared_read_ok.affine

@@ -0,0 +1,13 @@
+// M3 anti-over-rejection (#553 ADR-022): a SHARED borrow does NOT forbid
+// concurrent reads of the borrowed place. `let a = &x; let y = x; *a` is valid
+// under both the lexical checker and the Polonius extractor — only `&mut` is
+// exclusive. The use-while-exclusively-borrowed rule must fire ONLY for `&mut`,
+// never for `&`, so this program must be accepted (pol = lex = false).
+module BorrowSharedReadOk;
+
+fn ok() -> Int {
+  let x = 5;
+  let a = &x;
+  let y = x;
+  *a + y
+}

test/test_borrow_polonius.ml

@@ -160,6 +160,27 @@ let t_extract_value_return_ok () =
   Alcotest.(check bool) "Polonius: no loan, no error" false pol;
   Alcotest.(check bool) "agrees with lexical verdict" lex pol
 
+(* M3 loan-vs-loan exclusivity (#553 ADR-022): two simultaneously-live `&mut`
+   borrows of the same place — the second `&mut x` reads `x` at its creation
+   point while the first is still live, so it conflicts. *)
+let t_extract_mutref_conflict () =
+  let (pol, lex) = polonius_vs_lexical "borrow_mutref_conflict.affine" in
+  Alcotest.(check bool) "Polonius flags &mut/&mut overlap" true pol;
+  Alcotest.(check bool) "agrees with lexical" lex pol
+
+(* a plain read of `x` while `&mut x` is live (use-while-exclusively-borrowed) *)
+let t_extract_mutref_use_while () =
+  let (pol, lex) = polonius_vs_lexical "borrow_mutref_use_while.affine" in
+  Alcotest.(check bool) "Polonius flags use-while-&mut-borrowed" true pol;
+  Alcotest.(check bool) "agrees with lexical" lex pol
+
+(* a SHARED `&x` does NOT forbid reads — `let a = &x; let y = x; *a` is valid
+   under both tiers (only `&mut` is exclusive). Guards against over-rejection. *)
+let t_extract_shared_read_ok () =
+  let (pol, lex) = polonius_vs_lexical "borrow_shared_read_ok.affine" in
+  Alcotest.(check bool) "Polonius accepts read-while-shared-borrowed" 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 () =
@@ -288,12 +309,14 @@ let t_extract_reassign_uam () =
    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 =
-  [ (* unmodeled: borrow-vs-borrow conflicts — two simultaneously live borrows
-       violating shared-XOR-exclusive. The extractor models access-vs-loan
-       conflicts (move/write over a live loan), not loan-vs-loan. *)
-    "borrow_mutref_conflict.affine", "conflicting &mut/&mut borrows";
-    "borrow_mutref_use_while.affine", "use while &mut borrowed";
-    "borrow_use_while_excl.affine", "use while exclusively borrowed";
+  [ (* 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)";
     (* unmodeled: return-escape / borrow-outlives-owner (no escape analysis) *)
     "borrow_outlives_owner.affine", "borrow-outlives-owner";
     "borrow_return_escape_local.affine", "return-escape (local)";
@@ -351,6 +374,9 @@ let tests =
     Alcotest.test_case "extract+solve: #554 UAM flagged, agrees with lexical" `Quick t_extract_uam;
     Alcotest.test_case "extract+solve: NLL-safe accepted, agrees with lexical" `Quick t_extract_nll_ok;
     Alcotest.test_case "extract+solve: value-return no error, agrees with lexical" `Quick t_extract_value_return_ok;
+    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;
     (* 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;