Memory management / Borrow validation
Borrow validation runs after HIR generation. It writes analysis facts beside HIR without changing it. Lifetime topology is a separate later analysis.
Checked proof-budget research records an open proposal for opt-in deeper analysis. It does not change the current safety contract or make ordinary code less checked.
Borrow validation runs after HIR generation. It reads coherent, validated HIR, enforces source-language access safety and optional affine-transfer safety, and publishes solver-independent facts beside HIR.
It doesn't rewrite HIR, choose the final memory strategy, perform backend lowering or decide lifetime topology. Borrow validation supplies facts. Lifetime analysis and memory planning own the later decisions. Lifetime owners, retained edges, escapes and cycles belong to Lifetime regions and escape validation.
Last-use analysis is central to the memory model. Its facts let later stages transfer affine cleanup responsibility, prove candidate cleanup frontiers and select physical representations without treating ordinary aliases as counted obligations. The later stages make those decisions after validating the complete topology.
Recoverable numeric, cast and fallible-operation paths are already explicit HIR branches, locals and exits before borrow validation.
Every borrow solver must publish the same semantic handoff even when its internal representation and algorithm differ. The stable downstream facts are:
These are semantic facts rather than a required lattice, root table or solver storage format. A different solver can compute them differently without changing source semantics. The handoff never selects REC, constructs a physical memory plan or emits runtime instructions.
src/compiler_frontend/analysis/borrow_checker/mod.rssrc/compiler_frontend/analysis/borrow_checker/engine.rssrc/compiler_frontend/analysis/borrow_checker/state.rssrc/compiler_frontend/analysis/borrow_checker/transfer.rssrc/compiler_frontend/analysis/borrow_checker/transfer/src/compiler_frontend/analysis/borrow_checker/types.rssrc/compiler_frontend/analysis/borrow_checker/diagnostics.rsHirModule.Borrow validation doesn't reparse source syntax, solve generics or traits, or see AST-only generic or trait state.
Every analysed place is normalised to a semantic place with explicit projections and an overlap relation. The overlap facts state which places may designate the same storage. A solver may report overlap conservatively when it cannot prove disjointness, but downstream consumers don't depend on a particular root-set representation.
Value origins and preliminary provenance identify where a value came from and which place or result may be observed. Alias bindings carry those facts rather than creating independent copies. Root tracking is analysis metadata, not source-visible reference identity.
These are analysis lattice states. They are not Moth source types and do not directly prescribe one backend runtime representation.
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.
Production Stage 6 still checks conflicts against overlapping storage roots; the feature-gated Boracle reference solver instead evaluates typed OriginRelations provenance.
Alias activity is path-sensitive and control-flow-sensitive. Shared aliases, and exclusive aliases that have a reachable holder use, use non-lexical activity. Whether an issued but never-used exclusive capability may be elided remains an explicit experimental question; the reference baseline keeps that capability conservative until canonical semantics adopt the stronger rule.
get() results don't become Retained Edge Counting obligations.These points are locked accepted design and are independent of the solver used to derive them.
Cleanup responsibility is affine: it may move or be discharged, but it never duplicates. Borrow validation supplies candidates and proofs. It doesn't make the final physical affine decision.
Borrow validation supplies facts. Lifetime analysis and memory planning own the later decisions.
Fact | Consumer |
|---|---|
a shared or exclusive access may still be used | borrow conflict validation |
no later source use exists on every relevant path | optional affine transfer |
no capable source alias survives | cleanup-frontier proof |
a final-use persistent store commits | affine root to persistent edge reclassification |
a stored value is detached into an owned result | persistent edge to affine root reclassification |
a final loop iteration is statically known | final-iteration responsibility transfer |
no observer or recreating source survives an epoch | inferred-region epoch completion |
edge sets are mutually exclusive across paths or epochs | avoid a false cycle coexistence result |
The table describes data flow, not a transfer of ownership. Borrow validation supplies the facts. Lifetime topology validates retained-edge and cycle legality, and the memory planner decides physical reclassification and cleanup plans.
Future-use analysis answers whether a semantic place or value 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:
An optional transfer candidate is valid only with the relevant path-sensitive proof. It must also preserve any dependent temporary borrow and must not leave a capable source alias that could recreate a retained edge beyond a candidate cleanup frontier.
Inferred transfer is optional. When safe transfer isn't 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 isn't a source diagnostic. Path-dependent optional transfer always backs off to borrowing in the accepted design.
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 isn't valid for ordinary optional transfer.
Internal inconsistent-analysis or impossible metadata uses CompilerError.
Borrow validation consumes and produces:
Borrow validation doesn't produce final result provenance, retained-parameter constraints, retention cardinality, detached stored-result effects, whole-domain kills, outcome-sensitive retention effects, frontier-enabling effects or outlives summaries. It may provide candidate-frontier capability-death proof as a stable fact, but retained-edge analysis owns the final frontier-enabling decision and those retained-edge effects.
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 doesn't 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 doesn't 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 dependencies or runtime names.
The read-only side-table handoff carries every fact listed under Stable downstream fact contract, plus the function, block and statement context needed to key those facts to HIR identity.
These facts are read-only outputs keyed by HIR identity. They don't become a second semantic IR and must not mutate HIR. A solver may use additional internal state or tooling statistics, but consumers depend on the semantic facts rather than that storage.
The alpha side table may emit advisory DropIfOwned drop candidates. DropIfOwned names the current Wasm scaffolding instruction and its migration debt only. These candidates aren't stable handoff facts, lifetime topology, exact release permission or final cleanup decisions.
The permanent conceptual conditional operation is discharge_if_owned. The memory planner owns final transfer, discharge, destroy and bulk-reclaim plans.
Reactivity V1 precision:
Reactive invalidation and observability facts are part of the stable handoff. They're distinct from builder-owned page/mount lifetime roots.
Borrow validation supplies the next analysis with:
Lifetime-region and escape validation then decides one lifetime owner, retained-edge legality, escapes, cycles, edge coexistence and outlives constraints. It reasons about committed retained-edge states rather than treating every analysis fact as a physical decision. See Lifetime regions and escape validation.
Retained-edge liveness is part of lifetime topology, not a separate runtime ownership system. Borrow validation supplies the alias-liveness substrate it depends on:
Retained-edge analysis owns the semantic facts about direct persistent edges, their cardinality, outcome-specific commit effects, whole-domain kills, detached stored-result provenance and final frontier-enabling effects. The compiler-owned memory planner decides REC selection, concrete obligation transitions, root-to-edge or edge-to-root reclassification, cleanup and destruction. Backend lowering encodes that plan only.
That last guarantee allows Retained Edge Counting to ignore temporary aliases entirely rather than adding a second safety mechanism. Borrow validation never decides which allocation families are counted. Ordinary aliases, parameters, temporary projections and get() results never contribute REC obligations.
Borrow validation may be conservative. Stronger field-, projection-, region- or path-level production solvers may accept more programs or unlock more optimisation, but they must not change the stable handoff or the semantics of already-valid programs.
Boracle is a permanent reference solver and experiment facility. It may improve precision and test alternative algorithms without changing the stable handoff or source semantics. The memory model doesn't depend on Boracle running during normal compilation, and a production solver need not reuse Boracle's storage or algorithm.
Missing optional transfer proof falls back to borrowing. Missing mandatory topology proof remains a topology diagnostic rather than a physical-strategy fallback.
Everything in this section describes the current alpha algorithm or its scaffolding. It isn't the solver-independent architecture above and may be replaced without changing the stable handoff or source semantics.
The current alpha lattice uses these states:
The current root approximation is centred on LocalId. Fields and indexes resolve conservatively through their base roots. Alias bindings carry root sets, and merged control flow may union those sets. This metadata isn't source-visible reference identity and isn't a permanent downstream representation.
The current checker precomputes per-block may/must future-use facts and runs a forward fixed-point transfer over reachable HIR blocks. Branches are visited independently. Joins conservatively combine incoming alpha states and root sets, retaining activity when any incoming path may still use an alias. Loops use the same fixed-point transfer until the current result stabilises.
Branch-local aliases are removed when they leave visibility. The current transfer implementation records returns, breaks and region exits for advisory cleanup-candidate generation. An infinite path without an exit doesn't receive an exit candidate merely because it loops.
Current advisory drop candidates are implementation hints for the alpha lowering path. They don't prove lifetime topology, exact release permission or a final destruction point. Stronger production analysis may replace their derivation or omit them entirely.
CompilerDiagnostic values.CompilerError.