20. Borrow Checker: Non-Lexical Lifetimes (NLL)

To achieve memory safety without a garbage collector, the compiler implements ownership and borrow checking powered by Non-Lexical Lifetimes (NLL). Inspired by the fact-generation model of Rust’s Polonius architecture—but utilizing a hypothetical SMT (Z3) solver for constraint resolution rather than Datalog—this system statically verifies memory safety without requiring the user to write lifetime annotations.

The Core Rules

The borrow checker enforces two independent guarantees:

1. Ownership: Every value has exactly one valid owner (name) at any point.
2. Borrowing: Code may temporarily create read-only (ref) or exclusive (mut ref) views onto owned data.

These are governed by strict rules:

1. A value has exactly one owner at a time.
2. Assignment (b = a) moves ownership from a to b. The variable a becomes invalid afterward.
3. A ref borrow provides read-only access. Any number of ref borrows on the same place may be live at once.
4. A mut ref borrow provides exclusive read/write access. While live, no other borrow on an overlapping place may be live.
5. Borrows on disjoint fields of the same struct (e.g., p.x vs p.y) do not conflict.
6. Using a moved variable is a compile-time error.

Syntax & Lifetime Boundaries

Unlike block-scoped lexical architectures, a borrow’s lifetime in this system is computed dynamically based on its usage in the Control Flow Graph (CFG).

A borrow is created via assignment:

r = ref p      # Shared borrow
m = mut ref p  # Mutable borrow

The borrow stays live exactly until the compiler determines its last usage. It does not artificially end at a block boundary ({}).

If a user needs to force a borrow to end earlier than its syntactic usage (e.g., to unlock a resource or allow a conflicting mutation), they can use an explicit drop:

drop(r) # Explicitly ends `r`'s liveness at this node

This explicit drop functions exactly as a loan_invalidated_at fact for the solver, ending the lifetime without requiring special language semantics.

Next Module: Checker Architecture