Proof: borrow-graph soundness (no use-after-move + no conflict + BorrowOutlivesOwner)

[hyperpolymath]

Parent: #513

Statement

For the borrow checker in lib/borrow.ml, prove three soundness lemmas:

1. No use-after-move: if a borrow-graph derivation accepts a program, no execution of that program reads from a binding after it has been moved.
2. No conflicting borrows: no two live borrows of the same source can both be mutable, or one mutable and the other shared, at the same program point.
3. BorrowOutlivesOwner: a reference's borrow scope is a subset of the lexical scope of its owner.

Concretely

The borrow checker emits a borrow graph + a move set per program point. Stating soundness against the operational semantics from lib/interp.ml:

borrow_ok(prog)  ⟹  ∀ trace t of prog.  ¬ uses_after_move(t)         (1)
borrow_ok(prog)  ⟹  ∀ trace t of prog.  ¬ conflicting_borrow(t)      (2)
borrow_ok(prog)  ⟹  ∀ ref-binding r in prog.  borrow_scope(r) ⊆ owner_scope(r)  (3)

Mechanisation

Lean 4. Target: formal/Borrow/{BorrowGraph.lean, NoUseAfterMove.lean, NoConflict.lean, BorrowScope.lean}. Borrow graph is a finite relation between program points and borrowed locations — Mathlib.Data.Finset.Basic handles the carrier comfortably.

Recent landings to lean on:

• CORE-01 pt1 (no use-after-move): fix(borrow): CORE-01 — borrow-graph validation; ownership enforced from source (Refs #177) #240 — already operational, just needs the proof.
• CORE-01 pt2 (return-escape): feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph #395
• CORE-01 pt3 Slice A (NLL last-use): feat(borrow): CORE-01 Slice C' loop soundness — 2-iteration check on while/for (Refs #177) #396
• CORE-01 pt3 Slice C (CFG-join in try/catch): feat(borrow): CORE-01 Slice D (#177 pt3) — reject @linear capture by closure at borrow check #397
• Ref-to-ref borrow source: feat(borrow): CORE-01 ref-to-ref binding (#177 pt3) — let r2 = r / r = s alias the borrow-graph #395 (separate from return-escape but same PR)

Size

XL. Estimate: 4–6 weeks. Can be sliced lemma-by-lemma; each of (1)/(2)/(3) is its own milestone.

Polonius origin variables (deferred)

ADR-022 / #407 is the long-tail follow-on. Out of scope here; keep the soundness proof for the current lexical borrow checker first.

Status

NOT STARTED.

🤖 Generated with Claude Code