Borrow validation

Design contract

Borrow validation runs after HIR generation. It reads coherent, validated HIR, enforces source-language access safety and optional transfer safety, and writes analysis facts beside HIR.

Recoverable numeric, cast and fallible-operation paths are already explicit HIR branches, locals and exits before borrow validation.

It doesn't rewrite HIR, choose the final allocation strategy, perform backend ownership lowering, or decide lifetime topology. Lifetime owners, retained edges, escapes and cycles belong to Lifetime regions and escape validation.

Main compiler paths

src/compiler_frontend/analysis/borrow_checker/mod.rs
src/compiler_frontend/analysis/borrow_checker/engine.rs
src/compiler_frontend/analysis/borrow_checker/state.rs
src/compiler_frontend/analysis/borrow_checker/transfer.rs
src/compiler_frontend/analysis/borrow_checker/transfer/
src/compiler_frontend/analysis/borrow_checker/types.rs
src/compiler_frontend/analysis/borrow_checker/diagnostics.rs

Inputs

Validated HirModule.
Explicit functions, blocks, regions, locals, places and terminators.
Access and effect metadata.
External package registry and boundary classifications.
External call parameter access rules.
Return-alias metadata.
Source locations and string table for diagnostics.

Borrow validation doesn't reparse source syntax, solve generics or traits, or see AST-only generic or trait state.

Analysis model

Accepted abstract states:

uninitialized: local has no valid value.
slot: local may own independent storage.
alias: local observes roots owned elsewhere.
slot + alias: conservative control-flow result where either shape may arrive.

These are analysis lattice states. They are not Moth source types and do not directly prescribe one backend runtime representation.

Access roots and aliases

Every analysed place resolves to one or more storage roots. Fields and indexes currently resolve conservatively through their base roots. Alias bindings carry root sets. Merged control flow can union root sets. Shared and mutable conflicts are checked against overlapping roots.

Root tracking is analysis metadata, not source-visible reference identity.

Alias activity

Shared and exclusive aliases use non-lexical, control-flow-sensitive activity.

A shared alias blocks overlapping mutation only until its last potential use on the relevant path.
An unused shared alias does not block later mutation.
Branches are analysed independently.
Joins conservatively retain activity when any incoming path may still use the alias.
Loops use fixed-point future-use reasoning.

Exclusivity validation

Many shared accesses can coexist.
Exclusive access conflicts with overlapping active shared access.
Exclusive access conflicts with another overlapping exclusive access.
Mutation of an alias writes through to the referent where source semantics permit it.
Invalid immutable mutation is rejected before backend lowering.
GC doesn't relax exclusivity rules.
Map alias rules use the same conflict machinery.

Future-use and optional transfer safety

Future-use analysis answers whether a root is required again after the current program point. It is a sufficient basis for optional transfer eligibility, not a source-visible lifetime system.

Semantic classification:

no future use on every relevant path: transfer is eligible as an optimisation.
future use: the operation remains a borrow.
path-dependent or imprecise: the operation remains a borrow conservatively.

Inferred transfer is optional. When safe transfer is not proven on every relevant path, the operation remains a borrow. Failure to prove an ownership optimisation must not make an otherwise valid source program invalid.

Transfer proof failure is not a source diagnostic. Path-dependent optional transfer always backs off to borrowing in the accepted design.

The current checker precomputes per-block may/must future-use facts and runs a forward fixed-point transfer over reachable HIR blocks. Current path-dependent rejection behaviour is implementation drift tracked for a later compiler plan.

No ordinary mandatory-consuming operation

Current source syntax has no mandatory-consuming ordinary-value operation. There is no move keyword, consuming parameter spelling or owned signature variant.

A user-facing use-after-consumption diagnostic is reserved for a future accepted mandatory-consuming surface. It is not valid for ordinary optional transfer.

Internal inconsistent-analysis or impossible metadata uses CompilerError.

Control flow and joins

Branches are analysed independently.
Loops participate in fixed-point analysis.
Joins conservatively combine possible states and roots.
Branch-local aliases are removed when they leave visibility.
Returns, breaks and region exits inform advisory destruction planning.
Infinite paths without exits don't require an exit drop merely because they loop.

Function and external-call summaries

Borrow validation consumes and produces:

parameter access mode
mutation effects
transfer eligibility / effect category
return-alias summaries
fresh result roots
alias of one or more parameters
unknown or imprecise alias result
reactive effects
external function access rules
external return-alias metadata

Lifetime constraints are produced and validated by the separate lifetime-region analysis.

All runtime value parameters, immutable or mutable, may be eligible for inferred responsibility transfer. Parameter access mode remains separate from optional ownership effect. An immutable parameter receiving ownership remains read-only. A mutable parameter receiving ownership may mutate according to the source contract.

Closed external boundary profiles override this general rule. WIT value-only calls are non-consuming. Restricted host-value crossings are non-consuming, and mutable opaque-handle access does not transfer Moth storage through the ordinary Moth ownership ABI.

MayConsume, NeverConsumes and AlwaysConsumes are analysis/lowering categories, not source-visible signature categories.

A MayConsume summary means the call path can receive responsibility when the caller proves a safe transfer. It does not let a callee unpredictably invalidate a borrowed argument.

AlwaysConsumes may describe a specialised already-proven call path. It must not turn a source function into a mandatory-consuming API.

Call transfer uses resolved metadata, not source imports or runtime names.

Side-table outputs

function summaries
block-entry states
block-exit states
statement-entry states
source access facts
transfer eligibility facts
return alias facts
reactive invalidation facts
advisory drop candidates
aggregate statistics where useful for tooling

These facts are read-only outputs keyed by HIR identity. They don't become a second semantic IR and must not mutate HIR.

Advisory drop candidates are not lifetime topology and not exact release permission.

Reactive subscriptions and invalidation

A subscription is a read-only dependency.
A subscription isn't an active borrow.
A subscription doesn't grant mutation.
A subscription doesn't extend a source-language lifetime category.
Writes, place mutations, map mutations and mutable arguments can create invalidation facts.
Ordinary alias and exclusivity checks still apply.
Ownership-aware lowering must not destroy an observable source or mounted state too early.

Reactivity V1 precision:

invalidation is source-level today
field, item and path granularity is future precision
subscription observability is consumed by lifetime validation

Reactive invalidation facts are distinct from builder-owned page/mount lifetime roots.

Handoff to lifetime validation

Borrow validation supplies the next analysis with:

validated access and alias facts
optional-transfer eligibility facts
return-alias and projection facts
reactive invalidation and observability facts
external boundary classifications already resolved for access

Lifetime-region and escape validation then decides one lifetime owner, retained-edge legality, escapes, cycles and outlives constraints. See Lifetime regions and escape validation.

Conservative precision and extension points

Borrow validation may be conservative. Stronger field-, projection-, region- or path-level analysis may accept more programs or unlock more optimisation, but it must not change the semantics of already-valid programs.

The accepted design permits conservative analysis. The current analysis shape includes:

Projections may share their base root conservatively.
Map lookup aliases the map conservatively.
Joined control flow may retain mixed slot/alias state.
Advisory drop sites are candidates, not exact source lifetimes.
Exact region destruction may be refined later.

These are precision choices, not permanent source-language restrictions.

Diagnostics

Access conflicts remain user-facing CompilerDiagnostic values.
Diagnostics carry source locations and structured reasons.
Lack of optional move/transfer proof is not a diagnostic.
Internal malformed-HIR or impossible-analysis state uses CompilerError.
Conflicting mutable/shared access, duplicate exclusive access and invalid place access need distinct reasons.
Diagnostics must not be stored as analysis state.

What borrow validation must not do

Mutate HIR.
Repair malformed HIR.
Decide lifetime topology, escapes or region owners.
Reject a program merely because optional transfer is unavailable.
Restrict transfer eligibility to mutable parameters.
Choose GC versus ownership allocation.
Emit runtime drops or frees.
Decide pointer tagging.
Solve generics or traits.
Parse source syntax.
Introduce source lifetimes.
Treat reactive subscriptions as active borrow lifetimes.
Skip validation because the target uses GC.

Common mistakes

Equating analysis slot state with guaranteed runtime ownership.
Treating aliases as independent copies.
Allowing GC to bypass invalid aliasing.
Using diagnostics as transfer state.
Mutating HIR to insert drops.
Deciding runtime ABI inside the checker.
Assuming May future use is always safe to consume.
Treating advisory drop sites as exact lifetimes or validated release permission.
Rejecting path-dependent optional transfer instead of borrowing.
Folding lifetime topology into borrow validation.