Skip to content

Commit e1ef41d

Browse files
fix(borrow): CORE-01 — borrow-graph validation; ownership enforced from source (Refs #177) (#240)
Completes the actionable core of borrow-checker Phase-3. lib/borrow.ml had place/borrow/move infra but the graph-validation pass was never wired: BorrowOutlivesOwner was defined-but-dead, shared-XOR-exclusive was only checked at borrow creation, and — the dominant hole — parameter ownership was read solely from p_ownership, which the parser leaves None for surface `a: mut Int` (the mut/ref/own is in the *type* as TyMut/TyRef/TyOwn). So the owned/ref/mut borrow discipline was effectively unenforced from real source. Changes (lib/borrow.ml): - param_ownership: derive ownership from the parameter type (TyOwn/TyRef/TyMut), preferring an explicit p_ownership. Used by add_fn_signature and the check_function mut-seeding. This is the fix that makes the discipline reachable from parsed programs. - ExprApp: peel ExprSpan around the callee so ownership is found for real (span-wrapped) call targets, not only bare ExprVar. - Call-argument Ref/Mut borrows are now temporary — released after the call expression — making the lexical model precise instead of over-conservative (this is what makes use-site enforcement sound rather than corpus-breaking). - check_use: find_aliasing_exclusive — shared-XOR-exclusive enforced at USE sites (new UseWhileExclusivelyBorrowed error), not only at creation. - Reference-binding graph (state.ref_bindings) tracked for `let r = &p`, scoped to its block; block_local_syms tracked. - BorrowOutlivesOwner finally emitted: a block whose value is a reference to an owner declared inside that block is a dangling borrow. - record_move / record_borrow / end_borrow are now all live (the let _ = silencers removed). Regression fixtures (test/e2e/fixtures/, wired as "E2E Borrow Graph"): - borrow_outlives_owner.affine -> BorrowOutlivesOwner (positive) - borrow_use_while_excl.affine -> UseWhileExclusivelyBorrowed (positive) - borrow_call_arg_then_use.affine -> Ok (anti-over-rejection guard) Gate: opam exec --switch=. -- dune runtest --force = 263/263 (was 260; +3 new), zero regression — the strengthened ownership enforcement does not over-reject the existing valid corpus. Deferred to a later CORE-01 part (docs/TECH-DEBT.adoc): NLL/region inference, flow-sensitive escape via `outer = &x`, tighter quantity integration. Refs #177 (not Closes — requirements-target; owner closes). Co-authored-by: hyperpolymath <hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 78d7ec7 commit e1ef41d

5 files changed

Lines changed: 339 additions & 53 deletions

File tree

0 commit comments

Comments
 (0)