CORE-01: complete borrow checker Phase-3 (borrow-graph validation)

Headline soundness gap. lib/borrow.ml has place/borrow/move infra but borrow-graph validation is incomplete; some medium-severity aliasing bugs may not be caught. Add graph validation + regression fixtures under tests/. Ledger: docs/TECH-DEBT.adoc CORE-01 (S1).

docs: truth CORE-01 part 1 (PR #240) in the ledger (Refs #175 #176 #177)

docs: authoritative ledger — CAPABILITY-MATRIX/ECOSYSTEM/TECH-DEBT (R…

fix(borrow): CORE-01 — borrow-graph validation; ownership enforced fr…

fix(borrow): CORE-01 pt2 — return-escape of borrow rooted at callee-o…

feat(parser): CORE-01 pt2 — &mut e exclusive-borrow surface (Refs #177)…

Scope reminder + staged-ADR plan (session 2026-05-21 — recorded so the next session doesn't re-discover it).

The CORE-01 deferred-work comment at `lib/borrow.ml:1193-1198` lists three named items under the "NLL" umbrella, very different in size:

Full region inference (Polonius-style) — research-grade subsystem; thousands of LOC; the canonical "NLL". Cannot land in one session.
Flow-sensitive escape via `outer = &x` — the named tractable slice. The current `StmtAssign` handler (`lib/borrow.ml:1083`) checks LHS mutability + use + active-borrow conflict, but does not check whether the RHS is a borrow rooted at a callee-owned/block-local binding being shoved into a caller-owned place (`mut`-param, or a binding declared in an enclosing block). Same defect class as the pt2 return-escape, just via assignment. Reuses `find_borrowed_owner` / `state.callee_owned_params` / `state.block_local_syms`. ~1 PR shape (fixture + OK-anti-regression fixture + 2 alcotests in "E2E Borrow Graph"), Refs CORE-01: complete borrow checker Phase-3 (borrow-graph validation) #177.
Tighter quantity-checker integration for captured linears — overlaps `quantity.ml`; scope harder to bound without a probe.

For (1), the repo convention for subsystems this big is a staged ADR (cf. ADR-013 CPS, ADR-015 WASI, ADR-016 effect-sites): PR1 = "ADR + design doc + S1..Sn plan, no code, gate-neutral", then PR2..PRn = staged implementation behind a flag. The ADR would be ADR-020 (ADR-019 is the latest in `docs/specs/SETTLED-DECISIONS.adoc`); the design doc home would be `docs/specs/region-inference-polonius.adoc`. PR1 contents sketched in conversation but not committed this session.

No code shipped against this issue today.

feat(borrow): NLL last-use expiry for ref-bindings (CORE-01 pt3 Slice…

Merge origin/main into claude/upbeat-gauss-D5f72

feat(borrow): flow-sensitive escape via `outer = &y` (CORE-01 pt3 Sli…

feat(borrow): CFG-join for ExprHandle + ExprTry catch arms (CORE-01 p…

fix(borrow): whole-place assignment clears move-record (Refs #177)

fix(borrow): whole-place assignment clears move-record (Refs #177) (#399

fix(borrow): self-assign guard + return-escape coverage for ref-to-re…

feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on …

feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by …

docs(adr): ADR-022 — origin variables + Polonius-style loan solver (R…

docs(tech-debt): mark CORE-01 (S1) borrow-checker Phase-3 DONE — closes

docs: truth-refresh after CORE-01 closure + 2026-06-11 survey — matri…

docs: truth-refresh after CORE-01 closure + 2026-06-11 survey (matrix…

Navigation Menu

Repository navigation

CORE-01: complete borrow checker Phase-3 (borrow-graph validation) #177

2 remaining items

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

CORE-01: complete borrow checker Phase-3 (borrow-graph validation) #177

Description

Activity

hyperpolymath commented on May 21, 2026

2 remaining items

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions