References

The Safe Reference Model

A valid safe reference represents more than an address.

Depending on the access, its validity may require:

• live storage;
• a live initialized value;
• correct type and alignment;
• correct storage identity;
• valid provenance;
• spatial bounds;
• borrow compatibility;
• access authority;
• relocation correctness;
• address-space compatibility;
• execution-context validity;
• concurrency correctness.

Satisfying one of these guarantees does not imply the others.

For example, a generation check can help prove that the expected storage incarnation is still current, but it cannot prove that a mutable borrow is exclusive.

Shared References: ref T

ref T is a safe, typed, non-null shared reference to one valid T.

fn Name(user: ref User) string {
    return user.Name
}

A valid ref T grants:

• read authority;
• shared access compatible with the borrow rules;
• typed access to the referenced T and valid subobjects;
• no ownership of the referenced value.

Multiple compatible shared references may coexist.

ref T does not mean that the underlying storage is globally immutable. It means this reference does not grant mutable authority.

Mutation through another path is legal only when the ordinary borrow, ownership, concurrency and platform rules permit it.

Mutable References: ref mut T

ref mut T is a safe, typed, non-null reference with exclusive mutable authority for its borrow live range.

fn Reset(counter: ref mut Counter) void {
    counter.Value = 0
}

A valid mutable reference grants:

• read authority;
• write authority when the underlying storage is writable;
• exclusive mutable access to the overlapping Place;
• the ability to create compatible shared or mutable reborrows;
• no ownership of the referenced value.

While an overlapping mutable borrow is live, conflicting shared or mutable access through another path is not permitted.

References Are Non-Owning

Creating or passing a reference does not transfer ownership of the referenced value.

let mut device := Device {
    Enabled: true,
}

let view := ref device

view refers to device; it does not become the owner of the Device.

Destroying the reference value does not destroy the referent.

Likewise, storing a reference inside another struct does not make that struct the owner of the referenced storage.

Safe References Are Non-Null

Scalar safe references are never null as source-level values:

ref T
ref mut T

Code that has a ref T has a valid reference value under the safe reference contract.

Sec does not use a null sentinel to represent “no safe reference”.

Raw pointers are different and follow their own nullable/raw-address rules.

Optional References

Optionality is explicit:

let current: Option[ref Device]

None means that no reference value is present.

It does not mean:

• the referenced object was moved;
• a generation became stale;
• hardware disappeared;
• a raw address became invalid;
• the referent is conditionally available.

A stale ordinary safe reference is a violated reference guarantee, not an ordinary None state.

Creating References

Create a shared reference with:

let packet := ref value

Create a mutable reference with:

let packet := ref mut value

The source must be a valid Place for the requested access.

Creating a reference does not consume the source Place.

Creating a mutable reference establishes exclusive mutable borrow authority for the overlapping Place while that borrow remains live.

Reference creation does not silently allocate memory and does not extend the lifetime of the referenced object.

The Source Place Must Be Available

A safe reference may be created only from a Place containing a valid live value that is available on the current path.

An unavailable Place cannot be referenced.

A conditionally available Place must first be refined to an available path:

if package.Payload is available {
    let payload := ref package.Payload
    Use(payload)
}

is available is an ownership-state test.

It does not by itself prove:

• borrow compatibility;
• reference epoch validity;
• hardware access permission;
• device liveness;
• synchronization;
• foreign retention safety.

Provenance

Every safe reference has compiler-known provenance: evidence describing where the reference came from and which storage identity and location it may access.

Possible origins include:

• local or parameter Places;
• caller-owned parameters;
• static storage;
• Arena or allocation identities;
• fixed-address storage;
• runtime mappings;
• union, Option or Result payload Places;
• returned-reference relationships;
• valid subobjects derived from another reference.

Safe field, index, range and slice derivation preserves or narrows provenance.

Numeric address equality does not create provenance.

Ordinary safe source code does not require programmer-written provenance annotations.

Reference Lifetime

A reference may not outlive the live value and storage on which it depends.

A reference may have a much shorter lifetime than its owner.

let mut value := 10

{
    let view := ref value
    Use(view)
}

value += 1

Once the reference's final proven use has ended, its borrow relationship may also end even if the reference binding remains lexically in scope.

Sec does not require visible lifetime parameters in ordinary source code.

Lifetime analysis derives the valid relationship from storage origins, control flow, calls, captures, returns and invalidating operations.

Reference Parameters

Reference mutability is part of a function signature:

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

fn Update(value: ref mut Packet) void {
    ...
}

A ref T parameter receives shared borrowed access.

A ref mut T parameter receives exclusive mutable borrowed access for the required live range.

Passing either reference does not transfer ownership of the referenced T.

A callable may not retain a passed reference beyond the lifetime relationship proven by its contract.

Unknown retention behavior is treated conservatively.

Returning References

Returning a reference is valid only when every possible returned origin remains valid after the callee returns.

This is invalid:

fn Invalid() ref int {
    let value := 42
    return ref value
}

value uses ordinary callee-local storage whose lifetime ends when the function returns.

Returning a reference derived from caller-owned input is valid when the relationship can be proven:

fn Identity(value: ref Item) ref Item {
    return value
}

Returning a reference derived from a receiver may likewise be valid when the receiver-backed storage outlives the returned reference.

References May Have Multiple Proven Origins

A returned reference does not need to come from exactly one syntactic source in every path.

fn Choose(
    left: ref Item,
    right: ref Item,
    useLeft: bool,
) ref Item {
    if useLeft {
        return left
    }

    return right
}

This can be valid because the compiler can retain a finite set of possible returned origins and prove every candidate.

Distinct origins are not inherently unsafe.

If any candidate origin cannot satisfy the required lifetime, borrow, type, spatial or storage guarantees, the returned reference is rejected.

References Inside Aggregates

Safe references may appear inside structs, fixed arrays, unions, Option, Result and other aggregate values when their referenced origins remain valid.

type Selection struct {
    Current: ref Item,
}

The aggregate does not become an owner of Item.

Copying or moving an aggregate preserves the reference semantics of the contained reference value.

Returning an aggregate containing a reference is subject to the same lifetime and escape rules as returning that reference directly.

A reference to callee-local storage cannot be hidden inside a caller-owned aggregate to evade lifetime analysis.

Copying Shared Reference Values

A shared ref T reference value is copyable under the reference copy/move rules.

let first := ref item
let second := first

This copies the reference value and its provenance/validity dependencies.

It does not copy the referenced Item.

Both shared references remain bounded by the same underlying storage lifetime and other validity requirements.

Moving Mutable Reference Values

A ref mut T reference value is not implicitly copyable.

Explicitly moving a reusable mutable-reference holder transfers the reference holder and its active borrow obligation:

let next :<- current

After the move, the moved-from reference Place is unavailable according to the ordinary ownership rules.

Moving the reference value does not move the referenced T.

Reborrowing

An existing reference can provide temporary derived borrow authority without transferring ownership of the reference holder.

A shared reference may create another shared reference:

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

Passing a shared reference to Inspect may create a shared reborrow.

A mutable reference may create a shared reborrow:

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

fn Use(value: ref mut Item) void {
    Read(value)
}

During the shared child reborrow, conflicting mutable use through the parent is restricted.

A mutable reference may also create a mutable reborrow:

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

Passing an existing ref mut Item to a borrowed ref mut Item parameter is a reborrow, not a move of the caller's reference holder.

After the call-bounded child reborrow ends, the parent mutable reference may become usable again if no other validity rule prevents it.

Subreferences Narrow Access

A safe reference derived from another safe reference may retain or narrow:

• authority;
• bounds;
• lifetime;
• provenance;
• address-space scope.

Safe derivation may never upgrade shared authority to mutable authority.

A reference to one field or element also cannot be used to reconstruct unrestricted access to the entire containing object through ordinary safe semantics.

Field References

A field may be borrowed directly:

let identifier := ref packet.Header.Id

The resulting reference preserves the relevant storage identity and narrows access to the selected field Place.

A mutable field borrow similarly requires mutable authority over that field:

let counter := ref mut state.Counter

Proven disjoint fields may be borrowed independently according to the borrowing rules.

Element References

Indexing may produce a borrowable element Place:

let item := ref values[index]

For mutable access:

let item := ref mut values[index]

Constant indexes may allow straightforward disjointness proof. Runtime indexes require the compiler to prove non-overlap before simultaneous mutable references can coexist.

The reference remains limited to the authorized element and valid subobjects.

Slices Are Bounded Reference Views

A slice is a non-owning reference category whose complete valid range is part of its semantic contract.

ref T[]
ref mut T[]

Slices share the same fundamental validity requirements as scalar references while additionally carrying a bounded element range.

An empty slice may use a hidden null or sentinel physical base internally when its length is zero, but this representation detail does not make scalar ref T nullable.

Spatial Validity

Every safe reference access must remain within the spatial extent authorized by the reference.

For ref T, safe access is limited to the referenced T and valid subobjects derived from it.

For slices, element access is limited to the slice bounds.

A live allocation does not make an out-of-bounds reference valid.

Spatial validity may be proven statically or preserved using the checked access semantics of the relevant collection or shaped type.

Temporal Validity

A reference must remain valid for the complete period in which it may be used.

Operations that can end the required validity include:

• destruction;
• deallocation;
• Arena reset;
• mapping removal;
• backing-storage replacement;
• physical relocation that cannot preserve the reference;
• replacement of the referenced object;
• another invalidating storage event.

A reference that is spatially in bounds may still be temporally invalid.

Likewise, temporal validity does not prove that an index or subobject access is in bounds.

Storage Identity

Safe references identify semantic live storage, not merely a numeric address.

Conceptually:

allocation A -> address 0x1000
allocation A ends

allocation B -> address 0x1000

A reference to allocation A does not become a valid reference to allocation B.

The reused numeric address does not preserve the previous storage identity.

Validity Epochs and Generations

Storage domains that may be invalidated and reused can use an epoch or generation to distinguish live incarnations.

Examples include:

• allocator-backed allocations;
• Arena resets;
• reusable slots;
• collection backing replacement;
• runtime mappings;
• owner control blocks.

A generation belongs to an invalidation domain, not merely to one numeric address.

Runtime generation metadata is not mandatory when static proof already prevents stale use.

Generation validity also does not replace:

• borrow exclusivity;
• bounds;
• initialization;
• type validity;
• relocation correctness;
• address-space correctness;
• concurrency proof.

Ordinary Safe References Should Not Become Stale

Safe Sec code should normally prevent stale ordinary ref values from being created or used.

The compiler uses ownership, borrowing, lifetime analysis, storage facts, Arena analysis, collection rules, relocation restrictions and target knowledge to prove validity.

Runtime validation may still be used by hardened profiles or dynamic storage models.

A detected stale ordinary safe reference is not normal business failure.

Dereferencing such a stale reference follows the deterministic panic or target-trap semantics of the active profile.

The programmer is not expected to write try around every normal safe reference access.

try does not turn stale ordinary reference use into normal recoverable application logic.

Relocation

A live direct reference must continue to identify the correct storage if the referenced object physically relocates.

If the implementation cannot preserve the direct reference through relocation, relocation is forbidden while that dependency remains live.

A generation check alone does not solve relocation. A perfectly matching generation attached to an old physical address would still point to the wrong location.

This distinction matters for dynamic collection backing, compacting storage, mappings and other relocatable domains.

Pinning

Pinning prevents physical relocation for a defined interval.

Pinning may be required by operations such as:

• foreign retained access;
• DMA;
• OS registration;
• hardware descriptors;
• intrusive data structures;
• self-referential layouts;
• target-specific address contracts.

Pinning does not itself imply:

• ownership;
• permanent lifetime;
• thread safety;
• copyability;
• allocation;
• reference counting.

Sec 0.1 does not define one universal source-level pin syntax in the reference model. Specialized APIs may provide pin guards or equivalent contracts.

Address Spaces

A safe reference belongs to a compiler- or target-recognized address space.

Examples include:

• ordinary RAM;
• flash;
• MMIO;
• DMA-visible storage;
• secure and non-secure memory;
• device-local memory;
• foreign address spaces.

Numerically equal addresses in different address spaces are not automatically interchangeable.

Safe conversion across address spaces requires compiler-known semantic compatibility. Raw conversion requires the explicit unsafe boundary defined by the relevant raw-pointer and platform rules.

Reference Equality

Safe-reference equality compares semantic referenced identity.

Two safe references compare equal when they identify:

the same live storage identity
and
the same semantic location within that storage

Numeric address equality alone is insufficient.

Two references to different live incarnations that reused one physical address are not equal as safe references.

Raw-pointer equality is different: it follows raw-address semantics and does not imply safe-reference equality.

Reference Validity Does Not Imply Race Freedom

A valid reference can still be used incorrectly in concurrent code.

Reference validity does not replace:

• synchronization;
• atomic access rules;
• memory ordering;
• race analysis;
• safe concurrent reclamation;
• ISR coordination.

A generation check followed by a load is not sufficient when another execution context can reclaim or invalidate the object between the check and the access.

ref mut exclusivity remains required even when runtime generation metadata exists.

Closures, Callbacks and Escaping Execution

Capturing a reference preserves its lifetime dependency.

A closure may escape only when every captured reference remains valid for the complete closure use.

Returning a closure that captures a reference to ordinary creator-local storage is invalid.

Passing a reference through a callback is only call-bounded when the callback contract proves that the reference is not retained.

Tasks, threads, events, deferred work, callbacks and other later-execution paths are escaping uses when they may execute after the creating call returns.

The compiler does not silently heap-promote local storage to repair an illegal escape.

References in Interrupt Contexts

Interrupt handlers use the ordinary Sec safe-reference model.

@isr and @interrupt do not introduce a special pointer type.

A reference used by an ISR must remain valid for the complete actual interrupt use.

A reference to handler-local storage cannot escape the handler execution lifetime.

Deferred work must not smuggle a borrow to ISR-local storage into another execution context.

A temporally valid reference may still be illegal in an ISR when the accessed operation violates interrupt, synchronization, runtime or hardware-access rules.

Fixed-Address and Hardware-Backed References

A physical address does not by itself prove a safe reference.

Safe access to fixed-address storage requires the platform's canonical lifetime, mapping, availability and access contract.

Having a ref or ref mut does not independently grant hardware-register access permission.

Volatile semantics are also separate from reference ownership and lifetime semantics.

A mapped register view must not outlive the mapping or platform contract that validates it.

External device presence, power, readiness and bus validity are not equivalent to reference lifetime or Place availability.

FFI Retention

Foreign declarations must distinguish call-bounded use from retained access where the ABI or foreign contract permits retention.

A non-retaining foreign call may borrow from a safe reference for the proven duration of the call when the FFI conversion rules allow it.

Retained foreign access requires:

• a lifetime covering the full retention period;
• compatible borrow authority;
• address stability where the foreign code retains a direct address;
• appropriate pinning or an equivalent mechanism when required;
• an explicit FFI contract.

A raw pointer returned from foreign code does not automatically establish safe provenance.

Unknown foreign retention is treated conservatively rather than assumed call-bounded.

Raw Pointer Boundary

Safe references and raw pointers are distinct types and semantic categories.

ref T
ref mut T
RawPtr[T]

There is no implicit conversion between them.

Converting a safe reference to a raw pointer requires the explicit unsafe/FFI mechanism defined by the raw-pointer rules.

A raw pointer does not inherit safe-reference guarantees merely because it came from a safe reference.

Converting RawPtr[T] into a safe reference requires an unsafe or compiler-trusted boundary that establishes every required guarantee, including as applicable:

• non-nullness;
• alignment;
• initialized valid representation;
• bounds;
• live storage;
• provenance;
• borrow authority;
• ownership compatibility;
• address-space compatibility;
• foreign-retention compatibility;
• relocation safety.

No Single Mandatory Runtime Representation

Sec defines safe-reference semantics independently of one physical representation.

A compiler may represent a reference using:

• an address;
• an address plus length;
• an address plus expected epoch;
• a slot identity plus generation;
• a capability pointer;
• a target-specific tagged pointer;
• a side-table key;
• another representation preserving the required semantics.

For a short-lived, statically proven reference, a hosted optimized target may lower ref T to an address only.

A hardened profile may retain epoch, capability, tag or side-table validation.

Constrained bare-metal targets may omit runtime metadata when validity is statically proven and reject safe patterns they cannot preserve.

Stable and Weak Handles

The lower-level reference model also defines stable-handle and weak-handle semantics for cases where direct references are not the right long-lived identity mechanism.

Stable handle

A stable handle may identify a domain, slot and expected generation and resolve the current physical target address indirectly.

This can allow identity to survive target relocation.

A stable handle does not imply ownership unless its specific handle kind explicitly defines retention or ownership.

Weak handle

A weak handle does not keep its target alive. Resolution failure is ordinary fallible program behavior.

Conceptually, resolution may produce something like:

Option[ref T]
Result[ref T, StaleReferenceError]

The exact public stable/weak-handle APIs are not fixed by the Sec 0.1 reference rulebook.

Ordinary short-lived ref T must not be replaced by stable handles by default.

Destroying a Reference Does Not Destroy the Referent

Safe reference holders are non-owning.

When a ref T or ref mut T holder reaches the end of its lifetime, only the reference value ends.

The referenced object remains alive according to its actual owner and storage lifetime.

Conversely, the owner cannot be destroyed or invalidated while a live safe reference still requires that storage unless another canonical mechanism preserves the reference's validity.

Reinitializing a Place begins a new value lifetime and does not revive references to the previous object that occupied the same storage.

Diagnostics

Reference diagnostics should distinguish causes such as:

• attempt to reference an unavailable Place;
• mutable reference requested without mutable authority;
• shared-to-mutable authority upgrade;
• overlapping mutable borrows;
• mutable and shared borrow conflict;
• returned reference to callee-local storage;
• escaping reference captured by a later-running closure or task;
• reference outliving a mapping or Arena epoch;
• backing storage relocation while a direct reference is live;
• stale reference detected by a hardened/runtime-validating profile;
• invalid address-space transition;
• hardware access lacking a platform contract;
• unsafe raw-to-safe conversion missing a required proof;
• foreign retention exceeding the proven lifetime.

Diagnostics should lead with programmer concepts rather than compiler-internal jargon.

For example:

cannot return this reference

the reference points to local value `item`
`item` is destroyed when this function returns

help: return an owned value
help: return a reference derived from caller-owned or longer-lived storage

Or:

cannot grow `items` while `current` is live

`current` refers directly to the current backing storage
Append may relocate that backing storage

help: end the reference before the structural mutation

LSP hover may expose reference kind, mutability, origin, borrow live range, storage domain, epoch dependency and returned-reference relationship when useful.

Best Practices

• Use ref T when code needs temporary read-only access without ownership transfer.
• Use ref mut T only when exclusive mutation is genuinely required.
• Keep reference lifetimes as short as practical.
• Prefer borrowing over ownership transfer when the callee only needs temporary access.
• Do not use Option[ref T] to model stale references or ownership availability.
• Return references only when their origin clearly outlives the result.
• Borrow fields or elements narrowly when whole-object access is unnecessary.
• Remember that moving a mutable-reference holder does not move the referent.
• Use reborrowing for temporary delegated access instead of moving a reusable mutable-reference holder.
• Do not assume numeric address equality means safe-reference identity.
• End direct references before operations that may invalidate or relocate backing storage.
• Do not assume reference validity provides synchronization or race freedom.
• Use the explicit raw/unsafe boundary when a required operation cannot preserve safe-reference guarantees.

Summary

• ref T and ref mut T are safe, typed, non-null, non-owning reference values.
• A safe reference provides temporary access to existing live storage.
• ref T grants shared read authority.
• ref mut T grants exclusive mutable authority for its borrow live range.
• A mutable reference is not ownership.
• Reference creation does not consume the source Place.
• Reference creation does not silently allocate or extend referent lifetime.
• Scalar safe references are never null.
• Optional references use Option[ref T].
• None is not a stale-reference state and is not an ownership-availability state.
• A reference may be created only from an available valid Place with sufficient authority.
• Safe references preserve compiler-known provenance to live storage origins.
• Numeric address equality does not create provenance.
• A reference may not outlive the value and storage on which it depends.
• Reference live ranges may end at final proven use rather than lexical scope end.
• Reference parameters borrow; they do not transfer ownership of the referent.
• A callable may retain a passed reference only when the contract proves the longer lifetime.
• Returning a reference to ordinary callee-local storage is invalid.
• Returning a reference derived from caller-owned input may be valid.
• Returning one of several finite proven origins may be valid.
• Aggregates may contain safe references without becoming owners of the referents.
• Copying ref T copies the reference value, not the referent.
• ref mut T is not implicitly copyable.
• Moving a mutable-reference holder transfers the holder and borrow obligation, not the referenced object.
• Passing an existing mutable reference to a borrowed mutable-reference parameter may reborrow rather than move the holder.
• Subreferences preserve or narrow authority, bounds, lifetime and provenance.
• A shared reference cannot become mutable through safe derivation.
• Field and element references narrow access to the selected sub-Place.
• Slices are bounded non-owning reference views.
• Spatial and temporal validity are independent requirements.
• Safe-reference identity depends on live storage identity, not only numeric address.
• Validity epochs or generations may distinguish reused storage incarnations.
• Runtime generation metadata is optional when static proof is sufficient.
• Generation validity never replaces borrowing, bounds, initialization, relocation or concurrency proof.
• Ordinary safe references should normally never become stale in valid safe code.
• A detected stale ordinary reference uses deterministic panic/trap semantics rather than ordinary try-based business logic.
• Live direct references may forbid physical relocation that would invalidate them.
• Generation matching alone does not solve relocation.
• Pinning constrains relocation but does not imply ownership or permanent lifetime.
• References belong to recognized address spaces and cannot be safely interchanged across spaces merely by numeric address.
• Safe-reference equality means same live storage identity and same semantic location.
• Raw-pointer equality is not safe-reference equality.
• Reference validity does not imply race freedom or synchronization.
• Escaping closures, callbacks, tasks and deferred work preserve captured reference lifetime dependencies.
• Interrupt handlers use the ordinary reference model.
• Fixed-address hardware storage still requires platform lifetime and access contracts.
• FFI retention must be explicit and lifetime-safe.
• There is no implicit conversion between safe references and RawPtr[T].
• Raw-to-safe conversion must explicitly establish all required guarantees.
• Sec does not mandate one physical runtime representation for safe references.
• A proven short-lived reference may lower to an address only.
• Hardened or dynamic profiles may retain epoch, generation, tag or side-table metadata.
• Target profiles may change representation cost but may not weaken source-level ref semantics.
• Stable and weak handles are separate mechanisms from ordinary direct references.
• The exact public stable/weak-handle APIs are not fixed by the Sec 0.1 reference rulebook.
• Destroying a reference holder never destroys its referent.