Values, Places and Storage

Why This Model Matters

The distinctions in this chapter explain behavior that otherwise looks surprising.

For example:

• moving ownership does not necessarily move bytes;
• destroying an object does not necessarily reclaim its storage;
• a local value does not necessarily live on a physical stack;
• two objects may reuse the same numeric address without being the same object;
• a storage location may remain valid after the previous object in it has ended;
• a live source binding may remain in scope while its former value is unavailable after a move;
• a reference may become stale even if a later object happens to appear at the same address.

Sec keeps these differences explicit in semantic analysis so that the backend is never asked to reconstruct ownership or lifetime meaning from machine addresses.

Value

A value is a typed semantic entity.

10
true
Point { X: 10, Y: 20 }
Status.Ready

A value does not necessarily occupy addressable memory.

For example:

let total := left + right

the computed result may remain entirely in compiler SSA form or a machine register. Sec does not require every intermediate value to have a stable memory address.

Type identity belongs to the value's semantics and is not derived from where the value happens to be stored.

Object

An object is a materialized value whose object lifetime has begun in storage.

let mut device := Device {
    Id: 10,
}

If device is materialized in storage, the live Device instance is an object.

Object lifetime begins when a valid object is initialized or constructed.

It may end through operations such as:

• replacement;
• move-out where permitted;
• explicit lifecycle destruction;
• automatic destruction;
• union variant change;
• owner termination.

Ending the object's lifetime does not necessarily end the storage lifetime.

Binding

A binding associates a source name with a semantic entity.

let count := 10
let mut connection := new Connection()

count and connection are bindings.

A binding is not the value itself and is not the storage itself.

This distinction matters after ownership transfer:

let resource := OpenResource()
Consume(<-resource)

The source name resource still exists lexically after the call, but the value it previously owned is unavailable.

Scope and ownership state are therefore separate facts.

Place

A Place is a source-level location expression that identifies a value-bearing location or another addressable operation target.

Examples include:

value
person.Name
array[index]
matrix[row, column]
object.Property

A Place is where operations such as read, write, borrow, replacement or move may be directed when that particular Place supports the operation.

Indexing chapters already use this model:

values[index]

is a Place, while the surrounding expression determines whether that Place is read, borrowed or written.

Not Every Expression Is a Place

Temporary computations do not automatically identify reusable storage.

left + right
Compute()
value * 2

Such expressions may produce values without producing a source-level Place.

The compiler may materialize temporary storage when a canonical operation requires addressability, but materialization is not permission to invent a longer lifetime or hidden dynamic allocation.

Root Places

A root Place is a Place that is not projected from another source Place.

Typical roots include:

• local bindings;
• parameter storage;
• static bindings;
• thread-local bindings;
• allocation roots;
• foreign objects;
• fixed-address platform bindings.

Example:

let mut packet := Packet {
    Header: header,
    Payload: payload,
}

packet is the root Place for accesses projected from this binding.

Sub-Places

A sub-Place identifies a location within another Place.

packet.Header
packet.Header.Length
values[3]
matrix[row, column]

The compiler conceptually tracks the root plus one or more projections.

Projections may come from:

• fields;
• constant indexes;
• dynamic indexes;
• ranges and slices;
• union payloads;
• reference dereference;
• shaped views;
• compiler-known access rules.

This lets Sec reason about partial moves and independent borrows without pretending that an entire aggregate is always one indivisible memory location.

Place Capabilities Are Independent

A Place is not simply “valid” or “invalid”. Different operations require different capabilities.

A Place may independently be:

• readable;
• writable;
• addressable;
• movable;
• shared-borrowable;
• mutable-borrowable;
• volatile;
• atomic;
• fixed-address;
• partially available;
• conditionally available.

These are not one combined flag.

For example, an immutable field may be readable and borrowable but not writable. A register field may be addressable only through platform-defined semantics. A moved field may retain storage while no longer being readable by its previous owner.

Place Relationships

Memory analysis must reason about whether two Places overlap.

Conceptually, Sec may determine that two Places are:

• the same Place;
• provably disjoint;
• one containing the other;
• possibly overlapping;
• unknown.

Separate fields are usually disjoint:

pair.Left
pair.Right

Distinct constant array elements can be disjoint:

values[0]
values[1]

But runtime indexes require proof:

values[leftIndex]
values[rightIndex]

The compiler cannot assume that these are different merely because the source expressions are spelled differently.

These relationships are later consumed by borrowing, move analysis, destruction and race analysis.

Storage

Storage is capacity in which a materialized representation may exist.

Storage can exist without currently containing a live object.

This is why storage and object are separate concepts.

For example:

let mut resource: Resource

depending on the type and initialization rules, there may be a storage location associated with the binding before a particular object's lifetime begins.

Similarly, after an object is moved out or destroyed, the storage location may continue to exist and later be reinitialized.

Object Lifetime vs Storage Lifetime

Object lifetime is the interval during which a valid object exists. Storage lifetime is the interval during which the underlying storage domain exists.

They are related but not identical.

let mut value := ResourceA()

value = ResourceB()

Replacing value ends the old object's lifetime and begins the new object's lifetime.

The compiler may reuse the same underlying storage location for both objects.

A later object in the same storage is not the previous object resurrected.

Storage Is Not an Initialized Value

Merely having enough bytes for T does not create a valid readable T.

A safe read requires a live initialized value with a representation valid for its type.

Default initialization is semantic and type-specific. It is not automatically “all bits zero”.

Partial initialization must be tracked at the granularity required by the type. Destruction may run only for subobjects whose lifetime actually began.

Replacement and Reinitialization

Assignment to an available mutable Place performs replacement.

let mut connection := first
connection = second

Replacement:

1. validates the new operation;
2. performs required cleanup of the old value;
3. ends the old object lifetime;
4. establishes the replacement value.

Assignment to an unavailable mutable Place is reinitialization rather than replacement.

Reinitialization does not destroy an old object that is no longer present.

The storage identity can remain the same across both operations.

Availability vs Storage

Availability answers whether the current owner has a usable value in a Place on the current path.

Storage availability is a different question.

let resource := OpenResource()
Consume(<-resource)

After the consuming call, the source Place may still have a valid storage slot, while resource is unavailable as an owned value.

This is one reason place is available is not a null check and not a storage-address check.

Ownership availability is covered in detail in the Ownership chapter.

Storage Identity

Sec assigns semantic identity to storage domains independently of their current physical address.

Storage identity tells the compiler which storage lifetime, backing relation, invalidation rules and other storage properties an access depends on.

This identity is used by references, borrowing, collection backing, mappings, Arena reset, relocation and safe reclamation.

Numeric Address Is Not Storage Identity

Two different storage lifetimes may use the same numeric address at different times.

Conceptually:

storage A at address 0x1000
storage A ends

storage B later appears at address 0x1000

Storage B is not storage A.

A stale reference to A does not become valid merely because the numeric address now contains B.

Storage Domains

A storage domain is the compiler-visible identity for one storage lifetime and its governing properties.

A domain may correspond to concepts such as:

• one activation's automatic storage;
• one static storage location;
• one Arena domain;
• one allocator-backed allocation;
• one mapping;
• one collection backing store;
• one fixed-address platform region.

The exact physical implementation may differ by target, but the semantic domain identity must remain available to safety analysis.

Validity Epochs

A storage domain may have multiple distinct live incarnations over time. Sec models this with a validity epoch.

Examples of events that may invalidate an earlier epoch include:

• Arena reset;
• deallocation;
• reusable-slot reuse;
• dynamic collection backing replacement;
• mapping remap or unmap;
• owner-control-block invalidation.

A runtime generation number is one possible implementation of epoch validation, but it is not the language definition itself.

When static proof is sufficient, no runtime generation metadata is required.

Backing Storage

Some values use storage separate from their ordinary descriptor or enclosing value. That separate storage is backing storage.

Examples include:

• dynamic-array elements;
• list elements;
• map entries;
• Arena allocation backing;
• mapped regions;
• foreign buffers.

For a dynamic array:

let mut values: int[]

the owning array value may contain descriptor state while live elements occupy separate backing storage.

The compiler preserves the semantic relation between the owning value and that backing storage.

Backing Relationships

Sec distinguishes several important relationships between a value and backing storage.

Exclusive access to borrowed backing does not automatically make the borrower the backing-storage owner.

A borrower cannot deallocate, relocate, reset or extend backing lifetime unless the governing contract explicitly grants that authority.

Storage Origins

Sec's canonical storage model classifies the primary origin of a storage root.

The core origin categories are:

Automatic
Static
ThreadLocal
Arena
AllocatorBacked
Unknown

These are semantic categories used by the compiler. They are not source keywords that programmers attach to arbitrary variables.

Storage origin is only one dimension of storage. It does not by itself say whether storage is mutable, volatile, atomic, pinned, fixed-address, foreign or thread-safe.

In particular, “stack”, “mapped”, “device”, “volatile”, “atomic” and “pinned” are not storage origins in this model.

Automatic Storage

Automatic storage belongs to an active execution or call context.

It may represent:

• materialized local variables;
• parameters;
• temporaries;
• compiler-generated local storage;
• caller-provided result storage associated with a call.

The same source-level local may lower to:

• an SSA value with no physical slot;
• a machine register;
• a stack slot;
• caller-provided return storage;
• no storage at all after optimization.

These lowering choices do not change the source-level lifetime or ownership rules.

Static Storage

Static storage belongs to a static storage domain.

It may include:

• module-level static storage;
• function-local static storage where defined;
• type-associated static let/static let mut storage;
• target-provided static regions with explicit contracts.

Static duration does not imply:

• immutability;
• thread safety;
• atomicity;
• synchronization;
• shared ownership;
• one permanent object lifetime.

An object in static storage may be replaced while the storage itself remains.

Thread-Local Storage

Thread-local storage has separate storage identity for each physical thread.

Its lifetime is tied to that physical thread.

A task migrating between physical threads does not carry the physical thread-local storage identity with it.

References to thread-local storage therefore cannot cross suspension or migration when same-thread resumption cannot be proven.

Arena Storage

Arena storage belongs to a specific Arena allocation domain.

Individual Arena-backed objects may have ordinary object lifetimes while their raw bytes remain part of the larger Arena domain.

Resetting an Arena may advance its validity epoch and invalidate references to objects from the previous epoch even though the Arena object itself remains live.

Releasing the Arena ends the storage domain.

Destroying one Arena-backed object does not normally reclaim its individual bytes.

Allocator-Backed Storage

Allocator-backed storage comes from one explicit individual allocation governed by an allocator or compatible provider.

The storage contract must preserve enough information to match the allocation with its correct provider, extent, alignment, memory space and reclamation rules.

AllocatorBacked does not mean “the global heap”.

Possible providers include:

• platform allocators;
• operating-system services;
• fixed-block pools;
• target allocators;
• verified runtime helpers;
• other explicit allocation providers.

Reusing the same numeric address for a later allocation does not revive safe references to the previous allocation.

Addressability

Addressability means that a canonical operation may obtain an address or reference to materialized storage.

Not every value is inherently addressable.

let total := left + right

The result may never need a physical address.

If a valid operation requires an address, the compiler may materialize storage when the language semantics permit it.

Materializing automatic storage for addressability is not the same as dynamically allocating memory.

Physical Relocation Is Not Ownership Move

These are two different operations.

Ownership move

Transfers semantic ownership from one source to another.

Consume(<-resource)

This may require no physical byte movement at all.

Physical relocation

Changes the physical storage location used by an object or backing store.

A dynamic array may relocate backing storage while remaining the same owning array value under its collection semantics.

Address Stability

Storage may have different address-stability guarantees.

Conceptually, storage may be:

• Movable — relocation is permitted by the governing contract;
• Stable — the address remains unchanged for a defined stability interval;
• Fixed — the address/location is part of the storage contract;
• Unknown — no positive stability guarantee exists.

Stable address does not mean permanent lifetime.

Fixed address does not mean the compiler owns the storage or may reclaim it.

A direct live reference may constrain relocation for the reference's live range.

Pinning

Pinning is a temporary storage constraint that prevents relocation for a defined interval.

A pin may also prevent reclamation when the pin contract explicitly says so.

Pinning does not automatically mean:

• ownership transfer;
• permanent lifetime;
• thread safety;
• synchronization.

Sec 0.1 does not introduce a general source-level pin keyword through the storage model.

Specialized APIs may provide pin guards or equivalent compiler-known contracts where required.

Memory Spaces

A memory space describes storage with distinct access or transfer rules.

Common categories include:

Ordinary
MMIO
TargetDefined

Ordinary memory supports normal Sec loads, stores, references, copying, moving and borrowing subject to the language rules.

MMIO may require target-defined widths, volatile behavior, ordering, barriers, side-effect semantics and restrictions on ordinary references.

Targets may also define accelerator-local, secure, non-secure, GPU, DSP, foreign or other memory spaces.

Crossing memory spaces must be explicit when material transfer or representation changes are semantically required.

Fixed-Address and Hardware Storage

Fixed-address placement is a storage/address contract, not an ownership category.

@address(Platform.GPIOA)
let mut gpio: GpioRegisters

The fixed address does not imply:

• that Sec owns the hardware region;
• that scope exit should clear or deallocate it;
• that the object lifetime is permanent;
• that access is automatically atomic;
• that volatile semantics imply synchronization.

Hardware and MMIO rules add their own platform contracts on top of the same underlying storage model.

Destruction vs Reclamation

Destruction ends the lifecycle responsibility of an initialized object or resource.

Reclamation makes storage unavailable for its previous purpose.

They are different operations.

For example, an Arena-backed object may be destroyed:

object lifetime ends
owned resource cleanup runs

while its raw bytes remain part of the Arena until:

Arena reset
Arena release

Conversely, raw storage reclamation never replaces required destruction of live initialized objects.

Allocation Creates Storage, Not Automatically an Object

Allocation establishes or provides storage through an allocation-capable operation.

A valid typed object exists only after its initialization or construction rules are satisfied.

Conceptually:

allocate storage
initialize representation
begin object lifetime

These steps may be combined by a higher-level operation, but the language keeps their semantics distinct.

No Hidden Allocation

Sec does not silently allocate merely to make an otherwise invalid lifetime work.

In particular, the compiler does not repair an escaping local reference by moving the local to a heap or Arena behind the programmer's back.

Likewise, these operations do not inherently allocate:

• copy;
• move;
• borrow;
• reference creation;
• parameter passing;
• return;
• ordinary lifetime analysis.

A particular type's explicit semantic copy or collection growth operation may allocate when its own contract says so.

Temporaries

Compiler-created temporaries have semantic lifetimes determined by the expression and control flow that require them.

Consume(BuildValue())

The result of BuildValue() must remain valid through the required call and cleanup behavior.

The compiler may eliminate physical temporary storage entirely when the observable semantics remain preserved.

Materializing a temporary does not give it permission to escape farther than its semantic lifetime permits.

Why References Need Storage Identity

A safe reference is more than a numeric address.

Reference validity depends on facts such as:

• where the reference originated;
• whether the object lifetime is still active;
• whether the storage domain still exists;
• whether the relevant validity epoch is still current;
• whether relocation preserved the reference contract;
• whether borrow authority remains valid;
• whether bounds and initialization still hold;
• whether the memory space permits the access.

This is why a stale reference does not become valid again when a new object later reuses the same address.

The next chapter develops the source-level ref T and ref mut T model in detail.

Why Ownership Is Separate from Storage

Ownership answers who is responsible for a value or resource lifecycle.

Storage answers where a materialized representation may exist and which storage lifetime/invalidation rules govern it.

The same owning semantics may be implemented using different storage origins.

Conversely, owning an object does not necessarily mean owning the physical backing bytes.

For example:

owned object
Arena-backed storage

the value may own its object/resource lifecycle while the Arena owns reclamation of the raw storage.

Ownership is therefore never inferred merely from address possession or deallocation authority.

Worked Examples

Local scalar

let count := 10

count is a binding. The value 10 may remain as an SSA/register value and may never need an addressable object.

Mutable struct

let mut point := Point {
    X: 10,
    Y: 20,
}

point.X = 30

point is a root Place. point.X is a sub-Place. Replacement of X changes the object stored in that sub-Place without requiring the containing storage root to change identity.

Dynamic array

let mut values: int[]
try values.Append(10)
try values.Append(20)

The dynamic array is an owning value. Its elements may live in separate backing storage. Growth may replace that backing storage while preserving the owning array's semantic identity.

Slice

let view := ref values[..]

view borrows the current backing storage. It does not own or reclaim it. Operations that would invalidate the backing conflict with the live slice.

Move

let resource := OpenResource()
Consume(<-resource)

Ownership moves to the callee. The source binding remains in source scope but its former owned value is unavailable. No physical byte relocation is required by the meaning of move itself.

Same address, different storage identity

// Conceptual lifecycle:
//
// allocation A -> address 0x1000
// allocation A reclaimed
// allocation B -> address 0x1000

A safe dependency on allocation A remains invalid after A ends. Allocation B is a new storage identity even though the numeric address is reused.

Diagnostics

Storage-related diagnostics should distinguish between problems such as:

• value unavailable because ownership moved;
• object lifetime ended;
• storage lifetime ended;
• reference tied to an invalid storage epoch;
• backing storage replaced or relocated;
• operation requires stable address but storage is movable;
• borrowed backing incorrectly treated as owned;
• attempted reclamation through the wrong authority;
• illegal reference escape from automatic storage;
• cross-memory-space operation without the required transfer;
• fixed-address or MMIO contract violation.

Diagnostics should not collapse all of these into a vague “invalid memory” message.

For example:

cannot return this reference

the referenced object uses automatic storage whose lifetime ends when this function returns

help: return an owned value
help: return a reference derived from storage that outlives the call

Or:

cannot grow values while view is live

view depends on the current dynamic-array backing storage
Append may replace that backing storage

help: end the borrow before calling Append

The compiler and LSP may expose storage origin, backing relation, address stability, memory space and invalidation cause when that information helps explain a diagnostic.

Best Practices

• Think in terms of values and ownership first, not machine addresses.
• Use Place reasoning for fields, elements and other addressable subobjects.
• Do not assume every local is physically stack-allocated.
• Do not assume new means heap allocation.
• Do not assume moving a value means copying bytes to another address.
• Do not assume destruction automatically reclaims the backing storage.
• Do not use numeric address equality as a safe identity test.
• Keep borrowed views short-lived when their owner may replace or relocate backing storage.
• Keep object lifecycle and raw-storage reclamation responsibilities conceptually separate.
• Use platform storage contracts rather than guessing MMIO, volatility or fixed-address behavior from ordinary values.
• Let the compiler prove safe lifetimes rather than relying on hidden allocation.

Summary

• A value is a typed semantic entity and need not occupy addressable storage.
• An object is a materialized value whose object lifetime has begun.
• A binding associates a source name with a semantic entity; it is not the value or storage itself.
• A Place identifies a value-bearing source location or operation target.
• Locals, parameters, statics, allocation roots and fixed-address bindings can form root Places.
• Fields, indexes, ranges, payloads, dereferences and views can form sub-Places.
• Place capabilities such as readable, writable, addressable, movable and borrowable are independent.
• Separate Places may be same, disjoint, containing, overlapping or unknown.
• Dynamic index expressions are not assumed disjoint without proof.
• Storage is capacity in which a materialized representation may exist.
• Storage may exist without containing a live object.
• Object lifetime and storage lifetime are distinct.
• A later object may occupy storage previously used by another object.
• Storage alone does not make a valid initialized readable value.
• Replacement ends one object lifetime and begins another.
• Reinitialization creates a new object in an unavailable Place without destroying an absent old value.
• Ownership availability is distinct from storage existence.
• Storage identity is independent of numeric address.
• Reusing the same numeric address does not resurrect an old storage identity or reference.
• A storage domain identifies one semantic storage lifetime and its governing properties.
• A validity epoch identifies one live incarnation of an invalidation domain.
• Generation numbers are one possible runtime representation of epochs, not the language model itself.
• Backing storage is separate storage used for elements, entries, payloads or other representation state.
• Backing relationships distinguish none, embedded, owned and borrowed backing.
• Exclusive access to borrowed backing does not make the borrower the backing owner.
• Canonical storage origins include Automatic, Static, ThreadLocal, Arena, AllocatorBacked and Unknown.
• Storage origin is independent of mutability, volatility, atomicity, mapping, pinning and thread safety.
• Automatic storage does not mean physical stack allocation.
• Automatic values may lower to SSA, registers, stack slots, caller-provided storage or no physical storage.
• Static duration does not imply immutability, synchronization or permanent object lifetime.
• Thread-local storage identity belongs to a physical thread.
• Arena reset may invalidate an earlier storage epoch while the Arena remains live.
• Allocator-backed storage does not imply one universal heap.
• Addressability may require materialization but does not inherently require dynamic allocation.
• Ownership move and physical relocation are different operations.
• A move may require no byte movement at all.
• Address stability may be movable, stable, fixed or unknown under the governing contract.
• Stable address does not imply permanent lifetime.
• Fixed address does not imply Sec ownership.
• Pinning constrains relocation; it does not automatically transfer ownership or provide synchronization.
• Memory spaces may impose different access and transfer semantics.
• MMIO and fixed-address behavior are platform/storage contracts rather than ordinary ownership facts.
• Destruction ends object/resource lifecycle responsibility; reclamation ends storage availability for the previous purpose.
• Destroying an object does not necessarily reclaim its storage.
• Reclaiming raw storage does not replace required destruction of live objects.
• Allocation provides storage; valid object lifetime begins only after valid initialization/construction.
• Sec does not silently allocate to repair an illegal lifetime escape.
• Temporaries have semantic lifetimes even when physical storage is optimized away.
• Safe references require storage identity, lifetime, provenance, borrow and validity facts beyond a numeric address.
• Ownership responsibility and backing-storage reclamation authority are distinct.