Borrow checker: precision & soundness (NLL Problem Case #3) — index

Index for the borrow-checker soundness and precision work. All soundness and precision items are closed; what remains is the encoding work (#265) and its blocker (#267).

Analysis: borrow_checker_precision_analysis.md · Design of record: borrow_checker_architecture.md · Encoding design: borrow_checker_parameter_provenance.md

Where we are

The question this issue opened with: does Vx handle NLL Problem Case hiraditya/Vx.1#3 — the get-or-insert map pattern that Rust's NLL rejects and Polonius is designed to accept?

Full reduced-case matrix, re-run against e6183067:

¹ Rust rejects the signature outright — ambiguous lifetime elision, "expected named lifetime parameter."

Every unsound program rejects and every sound program compiles. The only refusal of a sound program is bc8, the documented location-sensitivity limit (non-goal, below).

Two results worth keeping:

• bc2 — NLL Problem Case hiraditya/Vx.1#3 — is accepted, soundly, while its unsound twin bc9 is rejected. NLL rejects bc2. Vx reaches it not by location sensitivity but by a different decomposition: program-order liveness for conflicts plus a provenance summary for the return, instead of propagating a region variable into the return type.
• bc11 is accepted without a lifetime annotation. fn pick(a : &Map, b : &Map) -> &i32 is a signature rustc cannot compile without one (elision fails; you must write 'a on b). Vx accepts the signature and answers its use precisely.

Fixed

• Reborrows through reference parameters untracked (bc9) — 6661d502. Passing a reference by name to a reference parameter now records a borrow against the underlying storage. E4003/E4004.
• No escape analysis on returned references (bc4) — 6661d502. Reference bindings carry a RefProvenance; returning a Local is E4005.
• Architecture doc was stale — 8c79f9a3 + 6661d502. It described lexical scope-popping; the implementation releases loans at last use. Both docs now cross-reference each other.
• Codegen ICE on integer-literal match arms (bc6) — a47c9600. Unrelated to borrows; was hiraditya/Vx.1#257 / hiraditya/Vx.1#263, both closed.
• #264 — per-parameter provenance (bc10/bc11) — 0a42af51 + 96c0d95c. A call returning a reference no longer borrows from every reference argument. Implemented as a per-function summary in src/hir/provenance.rs (ReturnProvenance::{NotAReference, FromParams(u32), AnyParam}); the bitset handles more than four reference parameters, which the inline 4-slot design could not.
• #268 — reborrows through unresolvable callees (bc15, bc17, bc18) — 97d495b1 (generics) + cabfd7d5 (function pointers / closure values). Rather than defaulting unresolvable callees to AnyParam, the signature is recovered from the callee value's type (Type::Function / Type::Closure) via self.lookup — which function the pointer holds is irrelevant to the aliasing.
• #269 — escape rule over-rejected a sound closure-return (bc19) — 66664309. The synthetic closure-environment argument is skipped in the provenance join. Side benefit: unsound closure reborrows are now caught by the aliasing rule (E4003) rather than incidentally by the escape rule.
• #270 — codegen ICE on a function-pointer local (bc20) — 4ec8727e. let f = probe; f(..) no longer panics at src/codegen/lower/expr.rs:2135.
• #266 — unresolvable-callee coverage sweep — closed; every kind is now either fixed (generics, fn pointers, closures), gated behind unsafe (externs), or vacuous in Vx today (dyn/trait objects, intrinsics returning references).

Fixtures: borrow_reborrow_param_alias.vx, borrow_return_local_ref.vx, borrow_loan_dead_before_mut.vx, borrow_reborrow_through_param.vx, borrow_return_param_ref.vx, borrow_multiparam_deriving_conflict.vx, borrow_multisource_return_conflict.vx, borrow_unsafe_provenance_conservative.vx, borrow_reborrow_generic_{alias,ok}.vx, borrow_reborrow_fnptr_{alias,value_ok}.vx, borrow_reborrow_closure_alias.vx, borrow_closure_return_param.vx, fnval_indirect_call.vx.

Open

• #265 — inline the provenance in the TypeId encoding. Keeps the cross-module check a masked word compare. This is the half with paper weight — without it the result is "we made the borrow checker more precise," which rustc already achieves by charging an annotation. The encoding is what makes annotation-free and O(1) hold simultaneously.
• #267 — the 4095 region sentinel. Blocks hiraditya/Vx.1#265. 4095 already carries two meanings today — the parser's unassigned default (src/parser/types.rs:99) and the saturating clamp past 4095 nesting levels (src/hir/expr.rs:246) — so a deeply-nested region and an unassigned one are already indistinguishable, before any narrowing.

Explicit non-goal: location sensitivity (bc8)

bc8 stays rejected by design. The Region ID is a 12-bit lexical scope depth packed into word 2 of the TypeId; a scalar cannot express "live at P₁, dead at P₂." Location sensitivity would require regions to be sets of program points — the representation the fast path exists to avoid.

That trade — constant-time subtyping in exchange for an NLL-grade precision ceiling — is the design's central tension and should be stated plainly wherever this work is written up rather than left for a reviewer to find. See borrow_checker_precision_analysis.md §6.

Start with docs/discussions/borrow_checker_precision_analysis.md and docs/discussions/borrow_checker_architecture.md, then read the encoding design in docs/discussions/borrow_checker_parameter_provenance.md. Inspect the 4095 handling at src/parser/types.rs:99 and src/hir/expr.rs:246, and follow issues #265 and #267; done means the remaining encoding work and sentinel blocker are resolved.