Static memory topology and backend representations

Moth separates two questions that often get bundled together:

Semantic legality: may the program access, retain and release these values?
Physical representation: which runtime storage and cleanup plan realises that legal program?

Borrow validation answers access questions. Lifetime-region and escape validation proves one legal lifetime topology. A memory-strategy planner then chooses a representation for each validated allocation family.

Garbage-collected representation can represent an already-proven topology, but garbage collection never supplies the proof. A capable full-control release backend must lower without a tracing or reachability collector.

The sentence to keep

Moth is reference-semantic by default, copy-explicit and move-inferred. It omits explicit reference types and lifetime syntax, not references themselves.

Moth keeps shared aliases and exclusive mutation in the language model without asking authors to write &T, &mut T or lifetime parameters. The compiler tracks those relationships and keeps source APIs small.

Two layers of memory safety

Access validation and lifetime validation work together, but they own different facts.

Borrow validation checks shared and exclusive access, alias activity, last potential use, optional affine transfer and reactive invalidation. It reads validated HIR and writes side tables.

Lifetime and retained-edge analysis checks one semantic lifetime owner, retained-edge outlives relationships, escapes, cycles, non-lexical intervals, cleanup frontiers, builder lifecycle roots and exported summaries.

Neither analysis depends on a collector. A GC backend must receive the same validated topology as a collector-free backend.

The proof pipeline

The accepted memory pipeline reads from one owner at each stage:

access and copy rules
    -> borrow and last-use facts
    -> lifetime topology and retained-edge summaries
    -> complete intervals, frontiers and epochs
    -> backend-neutral memory requirements
    -> target-affinity analysis and partition
    -> target-contract validation
    -> per-physical-variant family/layout refinement
    -> target/profile-aware compiler-owned memory planning
    -> ValidatedMemoryPlan
    -> backend lowering

The pipeline has one seam worth memorising: everything above backend-neutral memory requirements is shared, and everything below it is per physical variant.

Shared topology is target-independent and profile-independent. It decides what the program means and whether it is legal.
Backend-neutral memory requirements are the last shared artefact: family identity, owners, intervals, frontiers, retention facts, REC candidacy, declared-region membership. They deliberately contain no selected strategy.
Target partition is build-owned. It assigns functions to targets and, with target-contract validation, creates a candidate physical variant.
Variant-specific physical planning is compiler-owned. Only here does the planner know the target, the build profile and the backend's memory capabilities, so only here can it choose stack or inline placement, affine cleanup, an inferred region, a declared-region arena, REC or a garbage-collected representation. The planner does not only select a strategy: it also turns each semantic commit into one normalised per-family obligation transition, fuses same-family removals and additions, and decides root-to-edge and edge-to-root reclassification, all before lowering.
ValidatedMemoryPlan is that decision, one per physical variant.
Lowering realises the plan and encodes those planned transitions. It never picks a strategy of its own.

The selection changes memory quality, not source legality or observable behaviour. Two variants of one source function may end up with different physical representations and identical semantics.

check runs through creation and validation of the ValidatedMemoryPlan and stops before lowering.

When transfer proof is missing

Moth infers cleanup-responsibility transfer only at a proven final use. If analysis cannot prove transfer on every relevant path, the operation remains a borrow and the statically proven region retains responsibility.

unproven transfer
    -> borrow remains
    -> statically proven region retains responsibility

This fallback keeps the source program under the same legal topology. It does not ask a capable release backend to switch to tracing garbage collection.

One fact, several consumers

One set of last-use and retained-edge facts feeds several decisions while each stage keeps its own responsibility:

| 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 |

Borrow validation supplies the facts; lifetime analysis and memory planning own the decisions.

Explicit copies and declared regions

Existing values use shared access by default. copy creates an independent graph and preserves its internal alias topology. A copied acyclic graph may enter an inferred or declared destination region. A copied cyclic graph must enter one declared region as a whole because declared regions provide Moth's only source mechanism for direct cycles.

A declared region provides one hard, count-free bulk lifetime. Last-use analysis still checks access within it, but it never releases a declared-region-owned allocation early. Declared-region exit reclaims the domain together.

Backend representations

Backends realise the validated memory plan through different physical mechanisms:

Collector-free release: affine cleanup, inferred regions, declared regions and REC lower without tracing reachability.
Debug or GC-native representation: a collector may erase individual cleanup operations while preserving the same validated topology and source behaviour.
Retained Edge Counting: REC is selected because unresolved runtime-many persistent retained edges disappear independently and no earlier mechanism (static cleanup, inferred regions, frontiers, declared regions, field splitting or bounded retention) answers precisely enough. A selected counter carries the live counted persistent-edge obligations plus at most one affine-root obligation. REC is not general ARC or source-visible retain/release behaviour: ordinary aliases, parameters, temporary projections and get() results never contribute obligations, and REC never establishes legality. A final-use store can reclassify the affine root into one persistent edge, and a detached result can reclassify one persistent edge back into an affine root. Each has zero net counter traffic for that one reclassified edge. An operation that creates or removes several direct edges into the family still moves the count by the remainder. The planner fuses a same-family replacement, so the backend never emits a transient decrement to zero followed by an increment for that replacement.
Physical coalescing: a planner may keep storage slightly longer to reduce overhead. Coalescing never widens semantic topology, changes an outlives relationship or changes diagnostics.

Backends consume a validated memory plan. They do not infer source meaning, reconstruct lifetime topology or choose a new strategy when lowering.

Reactive and builder-owned lifetimes

Reactive subscriptions and mounted fragments can keep state observable after the function that created it returns. Builder lifecycle roots such as page, mount, request, frame and arena domains enter the same lifetime proof as source regions.

A collector-free backend can use those lifecycle regions directly. A GC backend may represent the already-proven lifecycle with reachability, but reachability does not define which topology the compiler accepts.

What can fail

conflicting shared and exclusive access
a retained edge into shorter-lived storage
an escape from a declared or inferred region
an unproven or illegal cycle
missing boundary or lifecycle metadata
a missing physical strategy after successful topology validation

Source failures use structured diagnostics. Missing compiler-owned metadata or a missing physical strategy uses CompilerError.

Roadmap and current status

Accepted design: static borrow and lifetime proof, explicit copies, inferred transfer, declared regions, direct source-created cycles requiring one declared region, REC as a narrow physical strategy and collector-free release on capable backends.
Current implementation: consult the memory rows in docs/src/docs/progress/@page.moth.
Deferred implementation: lifetime topology, complete retained-edge summaries, declared regions, REC, field splitting, builder lifecycle regions and collector-free verification remain separate implementation slices.
Implementation debt: current Wasm DropIfOwned paths may still consume advisory drop sites. Final lowering must consume the validated memory plan.

Exit state

You leave with one model: static proof defines legality, the validated memory plan defines physical cleanup and a collector remains an optional representation for a topology already proven legal.

Next: how borrow validation computes access and last-use facts over HIR.