soundness: use-after-move through a callee-returned borrow is accepted end-to-end (post-CORE-01 hole) #554

Probe (verified twice: original survey + independent critic re-run, 2026-06-11)

This program passes the full pipeline (typecheck → borrow → quantity, "Type checking passed", exit 0):

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);   // a is moved here
  let v = *r;               // read through r AFTER the move — accepted
  return v;
}

Control probe (plain double-consume of an own param) is correctly rejected with "use of moved value" — so move-tracking is live and this is a genuine false negative, not a Copy exemption.

Root cause (three interacting decisions in lib/borrow.ml)

1. Temporary call-argument borrows are released at call end (borrow.ml:893-896).
2. ref_source_borrow matches only direct &p forms — a call result (ExprApp) never registers as a borrow source (borrow.ml:553-566).
3. Returning &(ref-param) from a callee is intentionally allowed (borrow.ml:1675) — contradicting the model comment at ~borrow.ml:847-849 ("AffineScript's value model does not let a callee retain a borrow past return").

The borrow graph therefore has no edge from r to a; the loan returned by pick is invisible. This is precisely the loan-propagation problem ADR-022's Polonius origins solve (tracking: #553).

Requested actions

• Add this hole to the known-gaps trailer in lib/borrow.ml (it is currently absent from the "Still deferred" block) — same day as triage, per the doc-truthing discipline.
• Correct ADR-022's framing: residual = soundness, not precision (see tracking: ADR-022 Polonius origin/region variables — implementation M1–M4 (lib/borrow_polonius/) #553).
• Refresh the CAPABILITY-MATRIX borrow row in the same PR (per the matrix's own change-control rule). ⚠️ Note the trap: README.adoc:36 / CAPABILITY-MATRIX:213 still say "known soundness gap (CORE-01)" — stale, but accidentally still true because of this hole. Do not refresh those lines to "closed" without this issue documented first, or stale-conservative becomes active overclaim (the DOC-16 ratchet only catches overclaims, so it cannot catch that transition).
• Land the probe as a regression artifact. The test tree has no skip/xfail mechanism (no Skip/xfail anywhere in test/), so options: (a) unwired fixture in tests/borrow/ (12 existing unwired .affine files set precedent) with a pointer here, or (b) wire it as an expected-reject E2E Borrow Graph case once the fix lands.

Formal counterpart

#515 (borrow-graph soundness, Lean 4) is the proof obligation this hole would have falsified — a useful concrete counterexample for whoever picks that up. The 416-test green gate did not catch this; that is the operational-only soundness story's known limit (#513).

Filed from the 2026-06-11 whole-picture survey; probe verified by execution.