Lifetimes

Core Invariant

Conceptually:

use lifetime
    <= reference lifetime
    <= referent value lifetime
    <= required storage validity

Additional bounds may include:

• ownership availability;
• borrow authority;
• allocation lifetime;
• Arena epoch validity;
• mapping lifetime;
• address stability;
• platform validity;
• execution-context authority;
• foreign retention contracts.

Satisfying one bound does not prove the others.

Physical bytes may remain present after a semantic value or reference lifetime has ended. Safe Sec code still treats the old value or reference as dead.

Sec 0.1 Has No Programmer-Written Lifetime Syntax

Ordinary Sec source does not require:

lifetime names
lifetime parameters
lifetime arithmetic
explicit region annotations
outlives clauses

The compiler derives the needed relationships from existing source semantics.

Internal lifetime variables, graph nodes, regions, SCCs and dataflow states are implementation techniques. They do not become source-language features.

This is deliberate: lifetime complexity belongs primarily in compiler analysis rather than in ordinary user-facing signatures.

Several Different “Lifetimes” Must Not Be Collapsed into One

The compiler distinguishes at least:

value lifetime
storage lifetime
ownership duration
availability state
reference lifetime
borrow live range
temporary lifetime
resource lifetime
allocation lifetime
mapping lifetime
closure-environment lifetime
callback retention lifetime
platform validity
address stability
generation/epoch validity
lexical scope
physical stack-frame lifetime
backend lifetime metadata

These concepts interact, but they are not interchangeable.

Lexical Scope Is Not Lifetime

Lexical scope is a source-code region. It often provides an upper bound for locals, but semantic lifetime may end earlier.

A value may end before scope exit because it is:

• moved;
• discarded;
• destroyed;
• replaced;
• deallocated;
• invalidated;
• proven dead under the destruction rules.

A borrow may also end before lexical scope exit after its final proven use and after every derived dependency has ended.

Storage Lifetime Is Not Value Lifetime

let mut value := CreateFirst()

value = CreateSecond()

The storage represented by the Place may continue across the assignment.

The first value's lifetime ends before the second value's lifetime begins.

Reusing storage never means the previous semantic value is still alive there.

Resource Lifetime Is Not Wrapper Lifetime

A wrapper object may remain physically valid while the external resource it once represented has already ended.

Examples include:

• files;
• sockets;
• device mappings;
• interrupt registrations;
• foreign handles;
• other externally owned resources.

Storage validity alone therefore cannot prove that the external resource remains live.

Lifetime Sources and Bounds

Lifetime constraints may arise from:

• local declarations;
• parameter validity;
• caller-owned storage;
• return-value ownership;
• reference provenance;
• aggregate ownership;
• active union/Option/Result state;
• temporaries;
• loop iterations;
• static/global storage;
• thread-local storage;
• allocation owners;
• Arena epochs;
• closure environments;
• callback registration;
• foreign retention;
• fixed-address contracts;
• runtime hardware mappings;
• platform availability.

When several bounds apply, usable lifetime ends at the earliest invalidating bound on each control-flow path.

Unknown or opaque bounds are handled conservatively unless a compiler-visible canonical contract provides stronger facts.

Value Lifetime

A value lifetime describes the period during which one particular semantic value exists in a Place or owned value position.

Value lifetime is independent from whether the physical bytes remain allocated.

A Value Lifetime Begins When the Value Becomes Validly Initialized

Construction starts a value lifetime only when the relevant value or subvalue becomes valid under its type rules.

During permitted partial construction, aggregate fields may begin their lifetimes independently.

Reinitializing an unavailable Place starts a new value lifetime in that Place.

A Value Lifetime Ends When the Current Value Ceases to Exist

A current value lifetime may end through:

• destruction;
• move out;
• discard;
• replacement;
• ownership transfer;
• deallocation;
• a canonical invalidating operation;
• loss of active variant state.

A move does not replace the source with None, null, zero or a default value.

The former value lifetime ends at the source Place, and ownership analysis marks that Place unavailable.

Replacement ends the old lifetime before the new lifetime begins.

Partial Values May Have Different Sub-Place Lifetimes

let payload :<- packet.Payload

When the partial move is legal, the lifetime of packet.Payload ends at that source Place.

Proven-disjoint sibling fields may remain live and owned.

Reinitializing the moved field starts a new field lifetime and may restore whole-value availability when all required parts are live again.

Storage Lifetime

Storage lifetime is the period during which a storage location is valid for the uses allowed by its storage contract.

Storage may be controlled by:

• the current invocation;
• the caller;
• an allocation owner;
• an Arena;
• the static program image;
• thread-local storage;
• a runtime mapping;
• a foreign system;
• a platform or device contract.

Lifetime analysis consumes canonical storage-origin and storage-domain facts. It does not guess “stack versus heap” merely from syntax.

No Hidden Lifetime Extension

The compiler does not extend a local value's source-level lifetime by secretly promoting it to heap or Arena storage merely to make an escaping reference compile.

This remains invalid:

fn Invalid() ref Value {
    let value := CreateValue()
    return ref value
}

Backend escape analysis may choose a different physical placement only when the source program already has a valid ownership/storage lifetime.

Physical stack-to-heap placement is therefore an implementation choice only after the semantic lifetime has already been proven.

Ownership Availability and Lifetime Are Separate Facts

Ownership analysis tracks whether a Place currently owns a live value:

value is available
value is not available

Available means the current owner still owns a value in that Place on the current path.

Unavailable means the owner no longer owns a live value there, for a specific reason such as move, discard or destruction.

ConditionallyAvailable means different reachable paths have different ownership states.

Availability does not prove:

• borrow authority;
• Arena epoch validity;
• mapping validity;
• device liveness;
• platform access permission;
• thread synchronization.

Reference Lifetime

A safe reference cannot begin before its referent is validly initialized and available.

It cannot remain usable after any event that ends the required semantic validity, including:

• referent destruction;
• move;
• discard;
• incompatible replacement;
• deallocation;
• invalidating remap;
• Arena epoch invalidation;
• loss of required platform validity.

A safe reference does not own its referent and does not automatically extend the referent's lifetime.

ref mut T provides exclusive authority; it does not itself keep T alive longer.

Reference Representation Bits May Physically Remain After Validity Ends

A machine address may still numerically point into memory after a reference becomes semantically invalid.

Safe Sec still rejects later use.

Lifetime validity is therefore not defined by “the pointer still points somewhere” or by whether the bytes have been overwritten yet.

Borrow Lifetime

Borrow lifetime is the period during which borrowed authority must remain reserved.

It may be shorter than the lexical scope of the reference holder.

It may also be extended by derived references, captures, returned references, views, aggregate fields or deferred uses.

Sec Uses Non-Lexical Borrow Analysis

let value := CreateValue()
let view := ref value

Inspect(view)

Consume(<-value)

If Inspect(view) is the final use of view and no derived dependency survives, the shared borrow ends before the later consuming call.

The compiler uses the narrowest provably correct live range rather than extending every borrow to the closing brace.

Reborrows and Reference Holders Carry Derived Lifetime Obligations

A reborrow cannot outlive the source reference or the source borrow authority from which it derives.

Moving a ref mut holder transfers that holder's borrow obligation rather than ending the underlying exclusive borrow.

Copying a shared reference may keep the shared borrow live through the copied holder.

Move, destruction, replacement or discard of the referent remains illegal while an overlapping live borrow requires that value.

Proven-disjoint Places remain independent where the borrowing rules have already established disjointness.

Temporary Lifetimes

A temporary exists for the semantic region required to complete its containing expression and every transfer, borrow, cleanup or result-position use required by that expression.

The compiler does not silently extend a temporary merely to satisfy an escaping reference.

A reference to a temporary is invalid when the reference would outlive that temporary's semantic expression lifetime.

Specialized source rules may reject borrowing a non-addressable temporary entirely.

Fresh Owned Returns Have a New Receiving Lifetime

Returning a fresh owned value transfers that owned value into the receiving lifetime:

fn Create() Buffer {
    return BuildBuffer()
}

No return-site move marker is required for the fresh owned return.

This is fundamentally different from returning a reference into the callee's local storage.

Lifetime Analysis Is Flow-Sensitive and Path-Sensitive

Branching constructs preserve the facts of each continuing path.

This includes:

• if;
• switch;
• match;
• try;
• short-circuit expressions;
• loops;
• other branching constructs.

A path that exits through return, propagated failure, panic/termination or another non-continuing edge does not constrain later code that cannot be reached from it.

Every Continuing Incoming Path Must Support a Use After a Join

At a control-flow join, a later reference use is valid only when all incoming paths that reach that use preserve the required validity.

The compiler may keep a finite path-disjunctive set of provenance/lifetime alternatives when that improves precision.

If alternatives become too complex for the deterministic implementation bound, the compiler may conservatively widen and reject a use that needs stronger proof.

It may not choose one convenient incoming path and ignore another.

Loops Require a Lifetime Fixed Point

Loop analysis accounts for:

• entry state;
• zero iterations where possible;
• normal fallthrough;
• continue;
• backedges;
• break.

Iteration-local bindings begin fresh lifetimes for each iteration.

A reference that is valid in the first iteration but becomes invalid because of a later iteration is rejected at the operation where validity is lost, with the causal earlier operation identified when practical.

Aggregate Lifetimes Are Place-Sensitive

When ownership and borrowing permit independent sub-Place reasoning, lifetime analysis follows fields and other sub-Places independently.

A reference to a field depends on:

• that field's current value lifetime;
• the containing storage;
• the ownership/mapping/allocation path required to reach the field.

A legal partial move may end one field's lifetime while disjoint siblings remain live.

A type whose custom free forbids partial moves remains one ownership and lifetime unit for those transfers.

Slices and Views Follow Underlying Storage Lifetime

let slice := ref values[..]

Copying or moving the slice descriptor does not extend the lifetime of values.

The descriptor may physically live longer than the referenced storage and still be unusable after the backing lifetime ends.

Proven-disjoint ranges may carry independent borrow constraints while sharing one allocation/storage lifetime.

References into Union Payloads Depend on the Active Variant

A reference into a union payload remains valid only while:

• that payload is still the active semantic variant;
• the union's storage remains valid;
• all ordinary borrow and ownership requirements continue to hold.

Replacing the active union variant ends references into the prior payload even when the union occupies exactly the same storage address.

Borrowed match payloads normally remain bounded by the matching arm/guard unless the general returned-reference or capture rules establish a longer valid relation.

Function Calls Carry Lifetime Semantics

Before a call commits, the compiler resolves relevant:

• argument value lifetimes;
• borrow regions;
• ownership transfers;
• alias relationships;
• invalidation effects;
• retention/escape behavior;
• returned-reference relationships.

Argument preparation failure must not prematurely commit ownership or borrow state to a call that never occurs.

After the call, lifetime state is updated from the resolved callable contract rather than guessed from the return type alone.

Borrowed Parameters Are Call-Bounded Unless the Contract Says More

fn Inspect(value: ref Item) void {
    ...
}

fn Modify(value: ref mut Item) void {
    ...
}

The normal borrowed-parameter contract grants borrowed authority for the call.

A callable may extend the relationship by returning a derived reference or by an explicit compiler-visible retention contract.

An imported or opaque function cannot be assumed non-retaining merely because its implementation body is unavailable locally.

Consuming Parameters End the Caller-Side Source Lifetime When the Call Commits

fn Consume(-> value: Buffer) void {
    ...
}

Consume(<-buffer)

The caller-side <- is the ownership transfer marker.

Once the consuming call commits, the previous value lifetime at buffer has ended and the source Place becomes unavailable.

Lifetime analysis consumes that ownership fact; it does not redefine move syntax.

Returned References Require an Exportable Lifetime Relation

A returned safe reference must derive from storage that remains valid after the call for the complete caller-visible use.

Sec infers unambiguous returned-reference relations and exports them as compiler/module metadata.

The user does not write lifetime names into the function signature.

Returning a Reference to Ordinary Local Automatic Storage Is Invalid

fn Invalid() ref Value {
    let value := CreateValue()
    return ref value
}

value stops existing when the function exits.

The compiler rejects the function even if a particular optimization could physically keep the bytes somewhere longer.

Safe alternatives include returning an owned value or borrowing storage supplied by the caller.

A Reference Derived from a Borrowed Parameter May Be Returned

fn First(value: ref Pair) ref Item {
    return ref value.First
}

The returned reference depends on the caller-owned Pair and specifically on the lifetime of its First field/storage.

The function's exported metadata records the relation so callers can validate it even when the function body is unavailable.

A Returned Reference May Derive from self

A borrowing method may return a reference into its receiver when the relation is representable and safe.

The returned lifetime is bounded by the receiver's referent and any narrower field, allocation, mapping or epoch validity.

Multiple Possible Return Sources Require a Conservative Representable Relation

A function may select a returned reference from several borrowed inputs.

The exported lifetime relation must remain safe for every path.

Sec 0.1 prefers a conservative lifetime intersection or rejection when no stable, caller-visible relation can represent the alternatives soundly.

The compiler does not invent source lifetime annotations to rescue an ambiguous API.

A Returned Mutable Reference Extends Exclusive Borrow Authority

A ref mut result derived from a ref mut input may continue the exclusive borrow after the call returns.

The caller's original granting authority remains restricted for the complete live range of the returned mutable reference.

A shared input cannot be used to manufacture a mutable returned reference.

Lifetime Relations Are Exported in Compiler Metadata

Public/importable callable metadata preserves every caller-relevant relation that cannot be reconstructed safely from ordinary source types alone.

Examples include:

• returned-reference origin;
• receiver-derived result;
• parameter-derived result;
• finite multi-source result;
• retention/non-retention;
• captured dependency escape;
• invalidation effects;
• mapping/view dependency;
• storage-domain dependency;
• Arena epoch dependency.

Bodyless declarations such as interfaces and extern functions may need dedicated source contract syntax where ordinary types are insufficient.

This lifetime model deliberately does not invent such syntax prematurely.

Methods and Receiver Lifetime

A borrowing receiver may return references into self when the relation is safe.

A mutable method may invalidate references into fields that it replaces, moves, destroys or structurally invalidates.

Proven-disjoint stable fields may remain valid when the canonical method-effect summary proves the mutation does not touch them.

Ordinary Sec methods do not consume whole self. Specialized lifecycle operations such as Arena Release() remain explicit exceptions.

Closure Capture Lifetime Follows the Capture Mode

capture(value)
capture(<-value)
capture(ref value)
capture(ref mut value)

An owned copied or moved capture lives according to the closure environment's owned lifetime.

A borrowed capture never extends the referent's lifetime.

Lifetime analysis consumes the capture mode resolved by the lambda/ownership rules.

Escaping Callables Cannot Borrow Shorter-Lived Local Data

A callable proven to execute only during the current call may borrow data that remains valid for that call.

A callable that may be stored, returned, scheduled, retained or invoked later is an escaping execution use.

Such a callable cannot carry a borrowed reference to ordinary shorter-lived local storage.

Owned captures may allow escape when the closure environment itself owns storage and destruction for the complete required lifetime.

Callable types/summaries must preserve retention and lifetime relations across indirect calls.

Registered defer Creates a Delayed Lifetime Dependency

let resource := Open()

defer {
    Use(resource)
}

Consume(<-resource)    // invalid

Once the defer is registered, resource must remain valid until the deferred use executes.

Lifetime analysis therefore rejects move, discard, destruction, replacement, deallocation or other invalidation that would break the later cleanup use.

Place precision still applies: a defer using one field should not keep unrelated disjoint sibling fields live without reason.

Lifetime analysis also respects the unified LIFO ordering between deferred cleanup and automatic destruction.

Allocation Lifetime Bounds References into Allocated Storage

An allocation lifetime begins when allocation succeeds and ends when the owning allocation domain deallocates or invalidates it.

A reference into allocated storage is bounded both by:

• the allocation's validity;
• the narrower semantic value lifetime of the referred object within that storage.

A RawPtr[T] does not extend allocation lifetime.

Arena References Are Bounded by Domain and Epoch

let values := try arena.Alloc[int](100)

Process(values)

arena.Reset()

The reference may remain valid until the final use before Reset.

This is invalid:

let values := try arena.Alloc[int](100)

arena.Reset()

Process(values)

Reset starts a new Arena validity epoch. References tied to the previous epoch are no longer valid even though the same physical backing bytes may still exist and be reused.

Control-flow joins conservatively merge epoch state.

Arena Epoch Validity Is Not Ownership Availability

These questions are different:

Does this owner still own a value in this Place?
Is this reference still tied to the current valid storage epoch?

value is available answers the first question.

Arena/reference generation metadata answers the second.

Neither fact substitutes for the other.

Static and Global Storage May Live Long, but Access Still Has Rules

Static or global storage may have program-long or target-defined lifetime.

Long storage lifetime does not imply unrestricted safe access.

Mutable static/global references remain subject to:

• initialization;
• borrow authority;
• synchronization;
• target access rules;
• shutdown lifetime;
• other storage-specific validity conditions.

Lifetime correctness alone does not prove race freedom or synchronization correctness.

Thread-Local Storage Has an Execution-Context Lifetime Bound

A reference into thread-local storage is additionally tied to the thread/execution contract of that storage.

Such a reference cannot simply cross into another thread or execution context because the underlying bytes may physically continue to exist.

A specialized thread-local rule must prove that storage identity and access remain valid for the destination context.

A Fixed Address Does Not Mean an Infinite Lifetime

@address(Peripheral.GPIOA)
let mut GPIOA: GPIORegisters

The physical address may be stable while other validity conditions remain bounded.

A fixed address alone does not prove:

• initialization;
• ownership;
• availability;
• device liveness;
• mapping validity;
• access authority;
• permanent safe use.

AddressStability.Fixed prevents relocation under its contract. It does not create ownership or extend another lifetime.

A source-level fixed-address name referring to platform-owned storage does not make the program the owner of that storage.

Runtime Mappings Own Mapping Lifetime

When a platform API returns an owning mapping resource, that resource's contract controls the lifetime of the mapping.

A typed register or memory view derived from the mapping is normally non-owning.

The view cannot outlive the mapping owner.

Destroying, unmapping or invalidating the owner therefore invalidates dependent views.

A remap that changes physical realization ends old views unless the platform contract proves preserved identity and address stability.

The compiler never retargets a live safe view to different physical storage merely because the new mapping has compatible type and layout.

Volatile Access Is Not Lifetime

Volatile semantics control observable physical access. They do not themselves extend or shorten a Sec value or reference lifetime.

A value read from volatile storage becomes an ordinary Sec value snapshot:

let status := Device.Status

The later lifetime of status follows ordinary value rules even if the hardware changes the underlying register immediately afterward.

External hardware mutation is not automatically a Sec ownership transfer or borrow conflict.

Conversely, lifetime optimization must never remove, merge, duplicate, speculate or reorder volatile accesses in a way forbidden by the hardware-access contract.

RawPtr[T] Does Not Carry a Safe Lifetime

A raw pointer carries no automatic:

• ownership;
• non-null guarantee;
• bounds;
• borrow relationship;
• retention guarantee;
• safe lifetime.

Copying a raw pointer does not extend the lifetime of the pointed-to storage.

Converting a raw pointer into a safe reference requires proof of the complete safe reference lifetime, bounds, provenance and authority obligations.

Raw pointer semantics are covered fully in the Unsafe and Raw Pointers chapters.

FFI Requires Explicit Lifetime and Retention Contracts

C/C++ pointer types alone are not enough to establish safe Sec lifetime behavior.

Foreign contracts may need to distinguish:

• call-bounded borrow;
• retained pointer;
• returned owned pointer;
• returned borrow derived from input;
• static foreign storage;
• valid-until-next-call storage;
• explicit-release lifetime;
• callback retention;
• foreign thread-local storage.

A safe wrapper translates those behaviors into Sec ownership/reference semantics.

Unresolved foreign uncertainty remains inside explicit unsafe code.

A pointer retained by foreign code cannot safely refer to an ordinary local Sec value unless the foreign retention is proven to end before that local lifetime ends.

Escaping Execution Contexts Need Storage That Outlives the Escape

Any callable, reference, view or captured dependency that may be used after the current call returns is an escaping lifetime use.

Examples include:

• task queues;
• threads;
• retained callbacks;
• event registrations;
• foreign callbacks;
• other deferred execution objects.

Such execution cannot borrow ordinary call-local storage beyond its valid lifetime.

Owned capture or transfer may be valid when the destination execution object owns storage and cleanup covering the complete use.

Sufficient lifetime still does not prove synchronization, race freedom, transferability, ISR safety or access-context legality. Those are separate analyses.

Interrupt Registration Is an Escaping Lifetime Boundary

A handler that may run after its registration call is an escaping execution context.

Ordinary references into registration-call local storage therefore cannot escape into the handler without a specialized interrupt contract that proves a valid arrangement.

Static, global and fixed-address storage may be long-lived enough, but still needs correct synchronization, volatile/hardware semantics, execution authority and ISR safety.

Long lifetime alone never makes data safe to access from an interrupt.

Error Handling Produces Ordinary Lifetime Control-Flow Edges

try, local handlers and propagation participate in the same lifetime analysis as other branches.

An unmatched propagated failure leaves the success continuation and therefore does not constrain later success-only code except through cleanup that executes on the failing path.

A handler that continues must establish a lifetime-valid recovery state.

References stored inside Result, Option or another payload-bearing union remain bounded by:

• their underlying referent/storage lifetime;
• the lifetime of the active payload variant;
• ordinary ownership/borrow validity.

Consuming .Ok() or .Err() ends the source Result value lifetime according to ownership rules.

Borrowed projections such as OkRef and ErrRef remain bounded by the Result payload and the underlying referent validity.

Generic Code Must Be Lifetime-Safe for Every Admitted Instantiation

Generic source cannot assume stronger lifetime behavior than its declared type, ownership and borrow contracts provide.

Concrete monomorphization may improve precision using:

• field layout;
• copyability;
• destruction classification;
• storage facts;
• reference provenance.

Compiler-internal lifetime relations may be symbolic or parameterized without adding programmer-written lifetime parameters to Sec source.

Separate Compilation Preserves Lifetime Summaries

A caller must remain safe even when the callee body is not locally available.

Importable function, method, callable, interface and generic metadata therefore keeps lifetime-relevant relations needed by the caller.

Recursive and mutually recursive summary inference uses a terminating fixed-point strategy with conservative widening where required.

Summary generation is deterministic and must not depend on source traversal order, map iteration order, worker scheduling or declaration ordering.

The Compiler May Internally Solve Lifetime Constraints

Conceptual constraints include:

reference R must not outlive target Place P

reborrow B must not outlive source reference S

borrow B must cover every use of holder H

returned reference R derives from parameter P

closure C must not outlive captured reference R

aggregate A must not outlive reference field F

mapping view V must not outlive mapping M

value V must remain live through deferred use D

Constraint direction matters. Reversing an outlives relation is a compiler correctness bug.

If the compiler cannot find a sound conservative lifetime assignment or a representable caller contract, the program is rejected.

It is not repaired using:

• hidden allocation;
• hidden retention;
• hidden ownership conversion;
• unsound metadata;
• backend accidents.

Semantic IR Preserves Lifetime Facts Until They Are No Longer Needed

Before lifetime-sensitive source semantics can be erased, the compiler retains facts such as:

• storage origin/domain;
• Place/provenance relations;
• reference/reborrow relations;
• borrow begin/end or equivalent live-range facts;
• ownership transfer and invalidation;
• replacement/reinitialization;
• allocation and mapping dependencies;
• generation/epoch constraints;
• returned-reference summaries;
• closure capture lifetime and escape;
• FFI retention facts;
• defer-delayed dependencies;
• partial/conditional availability interactions.

Semantic IR verification rejects impossible or contradictory lifetime states rather than relying on a lower backend to rediscover source semantics.

Backend Lifetime Metadata Does Not Define Sec Lifetimes

LLVM lifetime.start, lifetime.end and similar backend annotations are optimization metadata derived from already-proven Sec semantics.

The compiler must not emit an early lifetime-end marker while any Sec reference, borrow, defer, cleanup, mapping/view dependency or observable storage requirement still exists.

Likewise, alias metadata such as noalias may be emitted only to the extent proven by Sec borrow/provenance analysis.

Foreign aliases, volatile storage, hardware aliases, raw pointers and opaque calls must never receive stronger assumptions than their contracts justify.

Diagnostics

Lifetime errors are mandatory safety errors, not optional lints.

Diagnostics should explain the programmer-visible cause rather than showing internal region IDs as the primary model.

Returned local reference

cannot return this reference

`value` is local to `Invalid` and stops existing when the function returns

help: return an owned Value
help: return a reference derived from caller-owned storage

Use after Arena Reset

`values` is no longer valid

`values` refers to the Arena epoch that ended here:
    arena.Reset()

help: finish using `values` before Reset
help: acquire a new reference after Reset

Move while borrowed

cannot move `resource`

a live shared reference still depends on `resource`

borrow created here:
    let view := ref resource

later use:
    Inspect(view)

help: move `resource` after the final use of `view`

Deferred future use

cannot consume `resource`

a registered defer still requires it:
    defer {
        Use(resource)
    }

help: remove or restructure the deferred dependency
help: consume the resource before registering the defer

Mapping lifetime

cannot return `registers`

the register view depends on mapping `deviceMap`

`deviceMap` is destroyed when this function exits

help: return the mapping owner together with an owning abstraction
help: keep the mapping owner in a longer-lived scope

Escaping callback

callback may outlive captured reference `state`

`state` is local to this call

the callback contract allows retention after return

help: capture owned storage
help: use a non-retaining callback API
help: move the required owned state into the callback environment

A useful diagnostic identifies, where possible:

• the invalid value/reference/view;
• where its dependency began;
• the operation that ended or may end validity;
• the later rejected use;
• the relevant branch/path;
• one practical safe restructuring.

LSP and Tooling

The LSP consumes compiler/Sema lifetime facts rather than reimplementing lifetime inference independently.

Tooling may expose:

• reference origin;
• owner;
• borrow dependency;
• returned-reference source;
• Arena epoch;
• mapping owner;
• invalidation cause;
• final-use point;
• captured/retained dependency;
• lifetime-relevant callable summary.

Internal region IDs should not be the primary user-facing explanation.

A code action is appropriate only when the compiler can prove that the transformation preserves semantics and safety.

Tooling must not automatically:

• add hidden allocation;
• convert arbitrary borrowed data into owned copies;
• weaken hardware/volatile semantics;
• invent lifetime annotations that Sec does not have.

Best Practices

• Think in terms of ownership, references, storage and final use rather than manually naming lifetimes.
• Keep borrowed data tied to storage whose owner clearly outlives the borrow.
• Return owned values when returning a borrowed relation would be ambiguous or tied to local storage.
• When returning a reference, prefer a clear relation to one input reference or the receiver.
• Use final-use structure naturally; Sec can end borrows before lexical scope exit.
• Do not keep references alive unnecessarily if later moves or mutations need the underlying value.
• Do not rely on physical bytes remaining present after semantic lifetime ends.
• Do not use is available as proof of borrow, mapping, Arena epoch or synchronization validity.
• Remember that copying a reference/view does not extend the underlying storage lifetime.
• End all old-epoch dependencies before Arena.Reset().
• Keep runtime mapping owners alive for every derived register/memory view.
• Use owned capture/transfer for work that may execute after the current call returns.
• Make FFI retention explicit; never infer lifetime from a C pointer type alone.
• Treat fixed-address storage as a platform contract, not as automatically immortal memory.
• Remember that lifetime safety and concurrency safety are separate obligations.
• Let the compiler carry lifetime relations through module metadata instead of adding manual source annotations.

Summary

• Lifetime analysis is mandatory compile-time semantic analysis in Sec.
• It is not a lint, optimization mode or backend convenience.
• Sec 0.1 does not require programmer-written lifetime names, parameters, arithmetic or region annotations.
• The compiler derives lifetimes from ownership, borrowing, storage, control flow, calls, captures, allocation, mappings, platform contracts and unsafe/FFI boundaries.
• The core invariant is that every safe non-owning use remains within complete referent and storage validity.
• Use lifetime is bounded by reference lifetime, referent value lifetime and required storage validity.
• Additional bounds may include availability, borrow authority, allocation lifetime, epoch validity, mapping lifetime, address stability, platform authority and foreign retention.
• Satisfying one validity dimension does not prove the others.
• Physical bytes may remain after semantic lifetime ends without making the old value/reference safe to use.
• Value lifetime, storage lifetime, ownership duration, availability, reference lifetime and borrow live range are distinct concepts.
• Temporary lifetime, resource lifetime, allocation lifetime, mapping lifetime and closure/callback lifetime are also distinct.
• Lexical scope is not lifetime.
• A value or borrow may end before lexical scope exit.
• Storage may host several sequential values with distinct value lifetimes.
• External resource lifetime is not implied by the wrapper object's storage lifetime.
• When several lifetime bounds apply, the earliest invalidating bound limits safe use on that path.
• Unknown lifetime bounds are treated conservatively unless a canonical contract provides stronger facts.
• A value lifetime begins when the value is validly initialized.
• Reinitialization starts a new value lifetime.
• A value lifetime may end through destruction, move, discard, replacement, transfer, deallocation, invalidation or variant replacement.
• A move does not replace the source with None, null, zero or a default value.
• Partial aggregates may have independent sub-Place lifetimes where ownership rules permit.
• A legal partial move ends only the moved sub-Place lifetime.
• Reinitializing a moved field starts a new field lifetime.
• Storage lifetime is controlled by the relevant canonical storage owner/domain rather than guessed from syntax.
• The compiler does not secretly extend storage lifetime by promoting locals merely to make references escape.
• Backend stack/heap placement can change only after source-level lifetime is already valid.
• Ownership availability and lifetime are separate dimensions.
• is available does not prove borrow authority, epoch validity, mapping validity, device liveness or synchronization.
• A safe reference cannot begin before the referent is initialized and available.
• A safe reference cannot remain usable after destruction, move, discard, replacement, deallocation, remap or epoch invalidation.
• A safe reference does not own or automatically extend its referent lifetime.
• ref mut T exclusivity does not itself extend T's lifetime.
• Reference representation bits may physically remain after semantic validity ends.
• Sec uses non-lexical borrow analysis based on actual uses and derived dependencies.
• A borrow may end after its final proven use even while the holder remains lexically in scope.
• A reborrow cannot outlive its source reference/borrow authority.
• Moving a ref mut holder transfers the borrow obligation rather than ending it.
• Copying a shared reference may keep the shared borrow live.
• Move, replacement, destruction, discard or deallocation are invalid while an overlapping borrow remains live.
• Lifetime analysis preserves proven Place disjointness instead of collapsing everything to the root object.
• Temporary values live only for the semantic region required by their expression and dependent operations.
• Temporary lifetimes are not silently extended merely to satisfy an escaping reference.
• Fresh owned returns establish a receiving ownership lifetime without a return-site move marker.
• Owned return and borrowed return have different lifetime models.
• Lifetime analysis is flow-sensitive and path-sensitive.
• Terminated branches do not constrain unreachable later continuation.
• A use after a control-flow join must be safe for every incoming path that reaches it.
• The compiler may preserve finite path-disjunctive provenance when useful.
• Conservative widening is allowed when lifetime alternatives exceed deterministic implementation bounds.
• Loop analysis computes a fixed point including zero iterations, backedges, continue and break states.
• Iteration-local bindings begin fresh lifetimes each iteration.
• Aggregate/field lifetime analysis is Place-sensitive where independent sub-Place reasoning is legal.
• Slices and views follow the lifetime of their underlying elements/storage, not merely their descriptor.
• Copying or moving a view does not extend backing lifetime.
• A union payload reference is valid only while that payload remains the active variant and storage remains valid.
• Replacing a union variant invalidates references into the previous payload even if the storage address is unchanged.
• Calls resolve lifetime, borrow, transfer, retention and returned-reference relations before commit.
• Failed argument preparation must not prematurely commit a call's transfer state.
• Borrowed parameters are normally call-bounded unless the callable contract retains or returns a derived reference.
• Opaque/imported functions cannot be assumed non-retaining without compiler-visible metadata.
• A consuming -> parameter ends the caller source lifetime when the call commits.
• The caller-side <- remains the ownership transfer syntax.
• A returned safe reference must depend on storage valid for the complete caller-visible lifetime.
• Returning a reference to ordinary local automatic storage is invalid.
• The compiler rejects a returned local reference even if optimization could physically keep the bytes alive.
• A reference derived from a borrowed parameter may be returned when the relation is safe.
• A borrowing method may return a reference derived from self.
• Multiple possible returned-reference sources require a conservative representable relation or rejection.
• A mutable returned reference may extend an exclusive borrow beyond call return.
• Returned-reference and retention relations are exported in compiler/module metadata without source lifetime names.
• Bodyless declarations may eventually require dedicated lifetime-contract syntax where ordinary types are insufficient; the current lifetime model does not invent that syntax.
• A mutable method may invalidate references into fields it replaces, moves or destroys.
• Proven-disjoint stable fields may remain valid when method effects prove they are unaffected.
• Ordinary Sec methods do not consume whole self except for specialized compiler-known lifecycle operations defined elsewhere.
• Closure lifetime depends on explicit capture mode.
• Owned captures live with the closure environment.
• Borrowed captures never extend referent lifetime.
• A non-escaping callable may borrow call-local data that covers the call.
• An escaping callable cannot borrow shorter-lived local data.
• Callable summaries preserve lifetime-relevant retention information across indirect calls.
• A registered defer creates a delayed future lifetime dependency.
• Move, replacement, destruction or deallocation are invalid when they would break a later deferred use.
• Deferred lifetime dependencies preserve Place precision.
• Lifetime analysis respects the unified defer/destruction cleanup order.
• An allocation lifetime begins on successful allocation and ends when its allocation owner deallocates or invalidates it.
• References into allocations are bounded by both allocation validity and narrower object/value lifetime.
• RawPtr[T] does not extend allocation lifetime.
• Arena-backed references are bounded by ArenaDomain/epoch validity.
• Arena.Reset() invalidates references from the previous epoch even when backing bytes remain.
• Arena epoch validity and ownership availability are separate facts.
• Static/global storage may live a long time without implying unrestricted safe access.
• References into mutable static storage remain subject to initialization, borrowing, synchronization and shutdown rules.
• Thread-local storage adds a thread/execution-context lifetime bound.
• A fixed physical address does not by itself imply unlimited lifetime, ownership, initialization or safety.
• Address stability does not create ownership or extend another validity contract.
• Runtime register/memory views cannot outlive the mapping or owner establishing their validity.
• Remapping invalidates old views unless identity/address stability is explicitly preserved.
• Mapping lifetime and external device liveness are separate facts.
• Volatile semantics are not lifetime semantics.
• A volatile read produces an ordinary Sec value snapshot.
• Lifetime optimization must not violate required volatile/hardware access ordering.
• Raw pointers carry no automatic safe lifetime, ownership, bounds or retention guarantee.
• Raw-pointer-to-safe-reference conversion requires proof of all safe lifetime/authority obligations.
• FFI safe wrappers require explicit compiler-visible retention/lifetime contracts.
• C/C++ pointer types alone do not establish Sec lifetime relations.
• Foreign-retained pointers must not outlive borrowed Sec storage.
• Tasks, threads, callbacks, event handlers and other deferred execution contexts are escaping lifetime uses when they may run after the current call returns.
• Escaping execution requires storage/capture ownership that covers the full possible use.
• Sufficient lifetime does not imply race freedom, transferability, synchronization or ISR safety.
• Interrupt registrations are escaping contexts when handlers may run after registration returns.
• Long-lived static/fixed-address storage still requires interrupt-safe access semantics.
• try and error propagation create ordinary lifetime control-flow edges.
• A continuing error handler must establish a lifetime-valid recovery state.
• References inside Result/Option/union payloads remain bounded by referent and active-payload lifetimes.
• Consuming Result projections end the source Result lifetime according to ownership rules.
• Generic code must be lifetime-safe for every admitted concrete instantiation.
• Monomorphization may improve lifetime precision using concrete type/storage facts.
• Compiler-internal generic lifetime relations need not become source lifetime parameters.
• Separate compilation preserves returned-reference, retention, invalidation, mapping/storage-domain and epoch summaries.
• Recursive summary inference uses a terminating fixed-point strategy.
• Lifetime summaries must be deterministic.
• Compiler-internal constraint graphs do not create source-visible lifetime syntax.
• If no sound conservative assignment or exported relation exists, Sec rejects the program instead of inventing hidden allocation or retention.
• Semantic IR preserves lifetime relations until every later consumer has equivalent verified information.
• Semantic IR must reject impossible or contradictory lifetime states.
• LLVM lifetime markers are optimization hints derived from Sec semantics; they do not define Sec lifetime.
• Backend lifetime-end markers must never precede any remaining Sec dependency.
• Alias/noalias optimization may use only facts actually proven by Sec borrow/provenance analysis.
• Lifetime safety violations are compile errors and cannot be downgraded by lint configuration.
• Lifetime diagnostics should explain origin, invalidating event, rejected later use, path and practical safe restructuring.
• LSP lifetime information comes from compiler/Sema facts rather than an independent editor lifetime engine.
• Tooling should avoid exposing internal region IDs as the primary user model.
• Lifetime code actions must not add hidden allocation, arbitrary owned copies or weakened hardware semantics merely to silence an error.