tracking: ADR-022 Polonius origin/region variables — implementation M1–M4 (lib/borrow_polonius/) #553

Why this issue exists

ADR-022 (docs/decisions/0022-polonius-origin-variables.adoc, merged via PR #407, 2026-05-27) is the declared residual behind the CORE-01 closure (#177 / PR #473) — yet as of 2026-06-11 it had no open tracking issue, lib/borrow_polonius/ does not exist on main, and the M1 sketch existed only as a local unpushed branch. This issue is the tracking record.

Current state

• Ratification vs doc status: PR docs(adr): ADR-022 — origin variables + Polonius-style loan solver (Refs #177) — surgical refile of #398 #407's thread records owner ratification of the architectural bundle (2026-05-27: custom OCaml datalog solver in lib/borrow_polonius/, surface syntax elided for v1, M1–M4 gates) — but the ADR's Status:: field still reads Proposed (0022:9; also META.a2ml). Flip the field or note the ratification inline.
• Implementation: 0%. No origin/region-variable machinery anywhere in lib/ (ast.ml:60-62 TyRef/TyMut are bare constructors).
• M1 sketch: now preserved at branch core-01/polonius-m1-sketch (b28757c, "M1 of ADR-022 — origin_var option on TyRef/TyMut + b_origin") — pushed 2026-06-11 from the previously-local-only branch noted in SESSION-HANDOFF-2026-05-27.adoc:24-26.

Scope (from ADR-022)

• M1 — origin_var option on TyRef/TyMut, behaviour-neutral.
• M2 — fresh origins at borrow sites.
• M3 — subset constraints + datalog-style loan-live-at-point solver, parallel-run diff against the lexical checker (lexical checker is the merge oracle through M3).
• M4 — cutover; deletes ~30–40% of lib/borrow.ml including state.moved / ref_bindings / callee_owned_params / merge_arm_results.

Why this is soundness, not precision

ADR-022's own context section concedes the lexical checker cannot reason about cross-function borrows (callee_owned_params is a name-set heuristic, "not a constraint discharge") and loop soundness is a 2-iteration heuristic. A probe-verified false negative now demonstrates the gap is live — see the companion soundness issue (filed same day). The ADR's "residual = precision" framing should be corrected to "residual = soundness".

Related

• Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner) #515 (borrow-graph soundness proof) explicitly defers Polonius — that proof formalises the lexical checker, not this.
• lib/borrow.ml:1756-1768 "Still deferred" trailer (includes the quantity-checker integration note for captured linears).

Filed from the 2026-06-11 whole-picture survey.