You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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".
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
lib/borrow_polonius/, surface syntax elided for v1, M1–M4 gates) — but the ADR'sStatus::field still readsProposed(0022:9; also META.a2ml). Flip the field or note the ratification inline.lib/(ast.ml:60-62TyRef/TyMutare bare constructors).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)
origin_var optiononTyRef/TyMut, behaviour-neutral.lib/borrow.mlincludingstate.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_paramsis 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
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.