Ownership

The Ownership Model

Ownership is mandatory semantic analysis in Sec. It is not an optional lint and is not reconstructed later from generated machine code.

For every owned value, the compiler tracks facts such as:

• where ownership began;
• the current owner;
• whether the relevant Place is available;
• whether an operation copies or consumes;
• whether an active borrow blocks the operation;
• whether part of an aggregate has already been consumed;
• whether availability differs across continuing control-flow paths;
• where ownership transfers or ends;
• which remaining value must eventually be destroyed.

The detailed distinction between copyable and move-only types is covered in Copying and Moving. Borrow overlap and borrow live ranges are covered in Borrowing.

What Is an Owner?

An owner is the semantic location responsible for a value's lifetime.

Owners may include:

• a local binding;
• a parameter binding;
• a struct field;
• an independently owned aggregate element;
• a union payload;
• a closure environment field;
• a returned result;
• a task or thread handle holder;
• another rulebook-defined owning location.

For example:

let session := OpenSession()

the local Place named session owns the returned Session value until ownership is transferred or its lifetime ends.

One Current Owner

Ordinary Sec ownership is exclusive: one semantic owner is responsible for each owned value at a time.

Ownership transfer changes that owner. It does not create a second owner.

let first := OpenResource()
let second :<- first

After the transfer:

second    // owns the Resource
first     // unavailable

If a type needs shared ownership, that behavior must come from an explicit type or API whose contract defines shared retention and release semantics.

Sec does not silently convert exclusive ownership into shared ownership.

Ownership Is Not a Physical Address

Ownership exists before backend storage placement is chosen.

A semantic owner may be represented by:

• an SSA value;
• a machine register;
• automatic storage;
• static storage;
• Arena-backed storage;
• allocator-backed storage;
• a descriptor owning separate backing storage;
• a target-specific resource representation.

A move may transfer ownership without physically moving any bytes.

Conversely, physical relocation can occur without changing semantic ownership.

Ownership Is One of Several Independent Dimensions

Sec keeps these questions separate:

This means:

• an immutable Place may be available;
• an immutable Place may become unavailable after ownership transfer;
• a mutable Place may be unavailable and later reinitialized;
• an available Place may temporarily be inaccessible because of a borrow;
• a valid reference generation does not prove ownership availability.

Availability

Availability describes whether a Place currently contains an owned value usable on the current execution path.

The source-semantic states are:

Uninitialized
Available
PartiallyAvailable
Unavailable
ConditionallyAvailable

These are ownership states, not user-defined enum values and not a replacement for Option[T].

Uninitialized

An uninitialized Place exists but does not yet contain a constructed value.

let mut resource: Resource

An uninitialized Place cannot be:

• read;
• copied;
• moved;
• borrowed;
• destroyed as though a value were present.

If the Place is mutable and later receives a valid value, it becomes Available.

Available

An available Place currently contains a valid owned value.

let resource := OpenResource()

Normal operations may use the value subject to its ordinary:

• mutability;
• copy/move classification;
• borrow state;
• type contracts;
• storage and platform rules.

Availability therefore does not mean that every possible operation on the value is legal.

Partially Available

An aggregate becomes partially available when one independently tracked owned sub-Place is unavailable while another remains available.

type Package struct {
    Header: Header,
    Payload: Buffer,
}

let package := LoadPackage()
let payload :<- package.Payload

After the transfer:

package.Payload    unavailable
package.Header     available
package            partially available

The compiler preserves that distinction rather than treating the complete aggregate as either entirely alive or entirely gone.

Unavailable

An unavailable Place no longer contains a value owned by that Place.

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

After the committed transfer, resource cannot be:

• read;
• copied;
• borrowed;
• moved again;
• destroyed as though it still owned the value.

The binding may still be lexically in scope. Scope and availability are different concepts.

A mutable unavailable Place may later be reinitialized.

Conditionally Available

A Place becomes conditionally available when continuing control-flow paths disagree about whether the owner still owns the value.

let package := LoadPackage()

if condition {
    Consume(<-package.Payload)
}

After the if, one continuing path still owns package.Payload and another does not.

The field is therefore not safe to use as an ordinary definitely available value until control flow refines or converges the ownership state.

Why a Place Became Unavailable

Availability and the reason for unavailability are separate facts.

Examples of unavailability reasons include:

Moved
Discarded
Detached

The reason improves diagnostics and ownership provenance.

It does not create a different top-level state for every possible cause. For continued ordinary use, a moved Place and a discarded Place are both unavailable.

Mutability and Availability Are Independent

Sec's default immutability does not prevent ownership transfer.

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

This is valid because a move is not ordinary assignment.

Likewise, an immutable aggregate may lose ownership of an independently movable field:

let package := LoadPackage()
let payload :<- package.Payload

What immutability prevents is later ordinary replacement or reinitialization:

package.Payload = CreateBuffer()    // invalid: immutable root

A mutable aggregate can repair the field:

let mut package := LoadPackage()
let payload :<- package.Payload

package.Payload = CreateBuffer()

Consumption of Reusable Sources Is Visible

A reusable source Place is a source that the programmer could otherwise expect to use again after the current expression.

Examples include:

resource
package.Payload
items[0]

When ownership leaves such a source, Sec requires the destructive transfer to be visible at the source position.

Consume(<-resource)

Ordinary source spelling must never silently become a destructive transfer merely because the type happens to be move-only.

The full syntax and copyability matrix are covered in the next chapter.

Fresh Temporaries Do Not Need Redundant Move Markers

A fresh temporary has no reusable source Place that could surprise the programmer by disappearing.

These are natural ownership-forwarding forms:

let buffer := CreateBuffer()

Consume(CreateBuffer())

let optional := Some(CreateBuffer())

let packet := Packet {
    Payload: CreateBuffer(),
}

The compiler may forward the temporary directly into its first owner without materializing an intermediate object.

Ordinary By-Value Parameters Own Their Parameter Value

fn Process(value: T) void {
    ...
}

Inside the call, value is an owned callee-local parameter value.

How the caller supplies that owned value depends on copy/move classification: a reusable copyable source may be copied; a reusable non-copyable source requires visible ownership transfer.

Borrowing uses ref T or ref mut T instead and does not transfer ownership of the referent.

Explicit Consuming Parameters

A parameter may state that the API intentionally consumes its argument:

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

A reusable caller-owned source must visibly transfer ownership:

Consume(<-resource)

This contract is independent of whether T would otherwise be copyable.

A fresh temporary can be passed directly:

Consume(CreateResource())

There is no reusable caller-owned source whose disappearance needs additional marking.

Call Ownership Transfer Commits at Call Entry

A consuming call with several arguments must not prematurely take ownership from the caller before all required call arguments are ready.

let resource := OpenResource()

try Use(
    <-resource,
    LoadConfiguration(),
) {
    Err(error) => Handle(error)
}

Arguments evaluate left to right.

Conceptually, Sec performs:

1. resolve the callable;
2. evaluate arguments left to right;
3. validate conversions, borrows and ownership-transfer requirements;
4. reserve reusable sources prepared for transfer;
5. if a later argument fails, cancel the outer call's pending reservations;
6. once all arguments are ready, commit the transfers exactly once;
7. enter the callee.

If LoadConfiguration() fails before Use begins, the outer call has not taken ownership of resource.

Pending transfer blocks overlapping use

A reusable Place prepared for transfer cannot be reused by a later overlapping sibling argument while the outer call is being prepared.

This can be valid when fields are proven disjoint:

Use(
    <-package.Payload,
    Inspect(package.Header),
)

But overlapping whole-aggregate use is invalid:

Use(
    <-package.Payload,
    Inspect(package),
)

A successful ownership transfer completed inside a nested argument expression is an already-completed effect and is not rolled back merely because a later outer argument fails.

Owning Payloads

Struct fields, union variants, Option and Result may own values stored in their payloads.

A reusable source that transfers ownership into such a payload uses visible consumption:

let optional := Some(<-resource)

let result := Ok(<-buffer)

let message := Message {
    Payload: <-payload,
}

Fresh temporaries can flow directly into their new owner:

let optional := Some(CreateResource())

Construction never infers a destructive transfer solely because the payload type happens to be non-copyable.

Return Ownership

A non-reference function result becomes owned by the caller.

Returning an owned local is therefore an intrinsically terminal transfer:

fn Create() Resource {
    let resource := OpenResource()
    return resource
}

The return boundary does not require the caller-side move notation used for continuing reusable-source transfers.

The same terminal ownership context can flow through structural return construction:

return Some(resource)

return Response {
    Body: resource,
}

return Ok(resource)

This exception belongs to the terminal return boundary. It does not turn ordinary calls, assignments or non-terminal payload construction into implicit destructive moves.

A borrowed Place still does not grant permission to remove a move-only owned value from borrowed storage merely because the expression appears in a return statement.

Partial Ownership of Aggregates

Sec tracks independently owned sub-Places where the relevant type and storage rules permit independent ownership.

type Package struct {
    Header: Header,
    Payload: Buffer,
}

let package := LoadPackage()
let payload :<- package.Payload

The transfer changes only the ownership state of package.Payload.

package.Payload    unavailable
package.Header     available
package            partially available

This makes partial ownership useful without pretending that the complete aggregate remains an ordinary intact value.

Whole-Value Use vs Sub-Place Use

After moving package.Payload:

Use(package.Header)    // may be valid
Use(package)           // invalid while package is partial

This rule applies recursively to nested ownership where independent tracking is legal.

Immutable Aggregates May Be Partially Consumed

Immutability does not freeze ownership responsibility in place.

let package := LoadPackage()
let payload :<- package.Payload

This may be valid even though package is immutable.

What immutability prevents is later ordinary repair:

package.Payload = CreateBuffer()    // invalid

The remaining owned fields continue to be the responsibility of package.

Mutable Aggregates Can Repair Partial Ownership

let mut package := LoadPackage()
let payload :<- package.Payload

package.Payload = CreateBuffer()

The assignment reinitializes the unavailable field.

After successful reinitialization:

package.Payload    available

If every required sub-Place is again available, the complete package becomes available again.

Types with Custom free Cannot Be Partially Moved in Sec 0.1

A custom destructor may rely on invariants over the complete valid instance. Sec 0.1 therefore forbids dismantling such a value through partial moves.

type ResourcePair struct {
    First: Resource,
    Second: Resource,
}

impl ResourcePair {
    free {
        ...
    }
}

This is invalid:

let first :<- pair.First

The compiler must not silently replace the type's whole-value cleanup contract with ad-hoc field cleanup after partially dismantling the instance.

Ownership Is Path-Sensitive

Sec merges ownership facts at control-flow joins. Only paths that actually continue to the join participate.

If every continuing path agrees:

all Available   -> Available
all Unavailable -> Unavailable

If continuing paths disagree, the result becomes conditionally available.

A terminating moved path does not poison the continuation:

let package := LoadPackage()

if condition {
    Consume(<-package.Payload)
    return
}

Use(package)

The path that consumed Payload never reaches Use(package). The continuing path still has the complete package.

is available and is not available

Sec provides ownership-state tests:

place is available
place is not available

Example:

if package.Payload is available {
    Use(package.Payload)
}

The true branch refines the exact tested Place to available unless another operation changes its ownership state.

Negative form:

if package.Payload is not available {
    RecoverWithoutPayload()
}

These tests answer whether the exact tested Place contains a complete currently owned value usable as an ordinary value on that path.

They are not null or Option tests

is available does not ask:

• whether an Option is Some;
• whether a raw pointer is null;
• whether a reference generation is current;
• whether a borrow currently permits access;
• whether a value's own data represents an empty state.

Whole aggregate availability

A partially available aggregate is not available as a whole.

package is available

is false when package.Payload has been moved even if package.Header remains available.

Testing package.Header is available observes that exact sub-Place instead.

Availability Tests Are Resolved Statically When Possible

The compiler must not emit runtime ownership-state machinery when control-flow facts already prove the answer.

If an availability test is statically known, normal constant/unreachable control-flow behavior applies.

This keeps ownership semantics strong without turning every owned value into a runtime-tagged object.

Conditional Ownership May Require Runtime State

Some genuinely path-dependent ownership programs cannot be implemented correctly from static facts alone at every later decision point.

In such cases an implementation may use local bookkeeping such as:

existing control-flow state
SSA state
hidden local ownership/drop flag
equivalent compiler-owned representation

This state is an implementation detail.

It must not:

• change the public source type;
• turn T into Option[T];
• be interpreted as nullable storage;
• make ordinary references generational merely for ownership tracking;
• change public ABI layout merely because one function needs local ownership bookkeeping.

Targets May Require Fully Static Ownership Decisions

Sec supports environments where hidden dynamic ownership bookkeeping is unacceptable, such as some bare-metal and real-time targets.

A strict target/project policy may reject code only when correct ownership semantics genuinely require forbidden runtime state.

Merely producing a conditionally available state is not automatically enough to reject the program if every later ownership-sensitive decision can still be resolved statically.

When explicit convergence can remove the requirement, diagnostics should suggest it.

discard Converges Ownership

discard place means:

After this statement, the programmer intentionally owns no value in this Place.

For an available discardable Place:

discard resource

performs any required destruction and leaves the Place unavailable.

Discarding an already unavailable Place is a valid no-op with respect to destruction.

Discarding a conditionally available Place destroys the value only on paths where the value is still owned and converges every outgoing path to unavailable.

let mut package := LoadPackage()

if condition {
    Consume(<-package.Payload)
}

discard package.Payload
package.Payload = CreateBuffer()

After discard, the field is definitely unavailable. The following assignment is therefore reinitialization.

discard does not bypass a type's non-discardable lifecycle obligations.

Assignment to an Unavailable Mutable Place Is Reinitialization

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

resource = OpenResource()

No old value remains in resource to destroy.

After successful initialization, resource becomes available again and takes responsibility for the new value.

Assignment to an Available Mutable Place Is Replacement

let mut buffer := CreateBuffer()
buffer = CreateBuffer()

The existing destination value is ended according to ordinary destruction rules before the new value becomes the destination's owned value.

Hosted Sec code does not require an explicit discard before normal replacement.

The complete incoming operation must be semantically valid before destructive commitment to the old destination occurs.

A conditionally available mutable Place may also be repaired by assignment. The implementation destroys an old value only on paths where one is still owned, then installs the new value and converges the Place to available.

A strict static-ownership target may instead require explicit discard convergence before such replacement.

Ownership of self in Methods

Ordinary instance methods do not have a source-language receiver mode that consumes the complete self.

Ending the entire instance lifetime belongs to lifecycle destruction, including a custom free where one exists.

A method may consume or discard owned members when receiver authority and partial ownership rules permit it:

impl Package {
    fn ReleasePayload() void {
        Destroy(<-self.Payload)
    }
}

The compiler derives the mutable/exclusive receiver authority required by such a body.

Compiler-known terminal lifecycle operations may have special ownership semantics when their dedicated rulebook defines them. They do not create a general facility for user-defined whole-self-consuming methods.

Borrowing Does Not Transfer Ownership

A reference borrows access to an owned value:

let view := ref resource
let writable := ref mut value

Neither reference becomes owner of the referent.

Ownership transfer or discard requires authority to remove the value from the source Place and is rejected while an incompatible live borrow overlaps that Place.

A ref mut T holder may itself have move-only value semantics while remaining merely borrowed authority over T.

Destruction Responsibility Follows Current Ownership

An unavailable Place is never destroyed again by its former owner.

let package := LoadPackage()
Consume(<-package.Payload)

At scope exit:

package.Payload    not destroyed by package
package.Header     destroyed if required by Header

A partially available aggregate destroys exactly the still-owned available sub-Places where field-wise destruction is valid.

This is one of the fundamental protections against double destruction.

Detailed destruction order, trivial/non-trivial destruction and custom free behavior are covered in the Destruction chapter.

try, match and Ownership

Error handling and pattern matching use the ordinary ownership model. They do not introduce a second move system.

By-value payload bindings follow normal copy/move rules. ref and ref mut payload bindings borrow.

A guarded prospective move does not commit merely because the structural pattern matched. Ownership commits only when the guard succeeds and the arm is actually selected.

After a try or match, only continuing paths participate in the ownership-state merge.

Propagating error paths that leave the function do not make a value conditionally unavailable in code they never reach.

Hardware, Fixed-Address and Foreign Storage

Not every storage-backed Place is an ordinary movable owner.

MMIO registers, volatile fixed-address storage and foreign storage follow their dedicated access and ownership contracts.

They are not movable merely because they can be represented as a Place.

A compiler-known hardware mapping may itself be an owning move-only resource: moving the mapping transfers responsibility for the mapping lifetime, while typed register views borrow that owner.

FFI ownership may cross the language boundary only through explicit foreign contracts or wrappers that define retention and ownership behavior.

Raw Pointers Do Not Imply Ownership

RawPtr[T]

is a raw address value.

Possessing one does not by itself mean that code owns:

• the pointed-to object;
• the allocation;
• a hardware mapping;
• the right to destroy the object;
• the right to deallocate the storage;
• privilege or security-domain authority.

Ownership must come from an explicit semantic contract, never from the mere existence of an address.

Ownership Does Not Require a Runtime Ownership Table

Sec's ownership model is primarily a compiler semantic model.

Most ownership facts may disappear completely after semantic analysis and optimization.

Runtime state is needed only when the actual source program leaves a dynamic ownership decision that later behavior must observe.

Even then, the implementation is not required to use one universal representation. It may use control flow, SSA facts, a local flag or another equivalent mechanism.

Ownership bookkeeping is never permission to alter public source type identity or ABI layout silently.

Ownership Diagnostics

Ownership errors should be explained in programmer terms.

A useful diagnostic identifies:

1. which value or Place cannot be used;
2. which earlier operation changed its ownership state;
3. why the requested operation is invalid;
4. what correction is likely appropriate.

Missing visible transfer

`Consume` takes ownership of `resource`.

Passing this value will make `resource` unavailable, so the ownership transfer
must be written explicitly.

help: write `Consume(<-resource)`

Use after transfer

`resource` is no longer available here.

ownership was transferred earlier by:
    Consume(<-resource)

help: use the new owner instead
help: borrow the value if ownership transfer was not intended

Conditional availability

`package.Payload` may no longer be available here.

it was consumed on one possible execution path

help: test `package.Payload is available`
help: restructure the control flow so availability is known statically

Whole aggregate after partial transfer

`package` is only partially available.

`package.Payload` no longer contains an owned value.
`package.Header` is still available.

help: use an available field directly
help: reinitialize the missing field when the aggregate is mutable

LSP hover and analysis may expose whether a Place is available, unavailable, partial or conditional; the reason for unavailability; and whether a call argument is copied, borrowed or consumed.

Best Practices

• Think of ownership as lifetime responsibility, not as an address or allocation strategy.
• Use borrowing when a callee only needs temporary access.
• Make destructive transfer from reusable values visible.
• Do not assume immutability prevents ownership transfer.
• Remember that an immutable partially consumed aggregate cannot be repaired by assignment.
• Use the still-available sub-Places of a partially available aggregate instead of treating the whole value as intact.
• Use is available only for ownership-state refinement.
• Do not use availability tests as substitutes for Option, null checks or reference validity.
• Use discard when intentional ownership convergence makes later control flow clearer.
• Prefer control flow that lets the compiler resolve ownership statically.
• Do not infer ownership from RawPtr[T], MMIO addresses or foreign pointers.
• Let destruction follow the owner that actually remains responsible for each value.

Summary

• Ownership defines which Place is responsible for an owned value's lifetime.
• Every ordinary tracked owned value has one current owner unless an explicit contract defines shared ownership.
• Ownership is semantic and independent of physical address or backend storage choice.
• Ownership transfer does not necessarily move bytes.
• Mutability, ownership availability, borrow authority and reference validity are separate dimensions.
• Ownership availability states are Uninitialized, Available, PartiallyAvailable, Unavailable and ConditionallyAvailable.
• An uninitialized Place contains no constructed value.
• An available Place currently owns a complete usable value, subject to other language rules.
• A partially available aggregate has at least one unavailable owned sub-Place and at least one available one.
• An unavailable Place no longer contains a value owned by that Place.
• A conditionally available Place has different ownership states on continuing control-flow paths.
• Unavailability reason is tracked separately from availability state.
• Initial unavailability reasons include moved, discarded and detached.
• An immutable value may still be explicitly consumed.
• An immutable aggregate may be partially consumed when partial ownership is legal.
• Immutability prevents ordinary reinitialization or replacement after such consumption.
• A mutable aggregate may reinitialize a moved field and restore whole-value availability.
• Destructive transfer from a reusable source must be visible in source code.
• Ordinary source syntax must never silently consume a reusable move-only value.
• Fresh temporaries do not need redundant move syntax when forwarded directly to their first owner.
• Ordinary by-value parameters own their parameter value inside the callee.
• An explicit -> parameter declares consuming API semantics.
• A reusable caller-owned source passed to a consuming parameter uses visible <- transfer.
• Call ownership transfer commits only when all outer call arguments are ready and call entry can occur.
• A pending transfer reserves its source against later overlapping sibling-argument use.
• A later outer-argument failure cancels the outer call's uncommitted transfer reservation.
• A successful nested ownership transfer is not rolled back by a later outer-call failure.
• Struct, union, Option and Result payloads may become owners of transferred values.
• The return boundary intrinsically transfers an owned result to the caller.
• Terminal structural return construction may forward ownership without repeating ordinary continuing-flow move syntax.
• Return context does not grant ownership over borrowed, static, volatile, MMIO or otherwise restricted storage.
• Partial ownership is tracked by independently owned sub-Place where the type and storage model permit it.
• Whole-value operations require complete availability.
• Sub-Place operations require only the selected sub-Place to be available.
• Types with custom free do not permit partial moves in Sec 0.1.
• Ownership analysis is path-sensitive and merges only continuing paths.
• A terminating path that consumed a value does not poison a continuation it never reaches.
• place is available tests ownership availability of the exact Place.
• place is not available is the logical negation of whole availability, not necessarily proof that every sub-Place is unavailable.
• A partially available aggregate tests false as a whole even when some fields remain available.
• Availability tests are not Option, null, reference-generation or borrow checks.
• The compiler resolves ownership state statically whenever possible.
• Genuinely dynamic ownership decisions may use local hidden implementation state.
• Ownership bookkeeping must not change public source types or ABI layout.
• Strict targets may reject only code that genuinely requires forbidden dynamic ownership bookkeeping.
• discard place intentionally converges ownership to unavailable.
• Discarding an available discardable value performs required destruction.
• Discarding an already unavailable Place is semantically harmless.
• Discarding a conditionally available Place destroys only on paths that still own the value and converges all paths.
• Assignment to an unavailable mutable Place is reinitialization.
• Assignment to an available mutable Place is replacement.
• Replacement validates the incoming operation before destructive commitment to the old value.
• Ordinary instance methods cannot consume the complete self.
• Methods may consume owned members when receiver authority and partial-ownership rules permit it.
• Borrowing does not transfer ownership.
• An incompatible live borrow blocks ownership transfer or discard.
• Destruction responsibility follows current ownership.
• An unavailable Place is never destroyed again by its former owner.
• Partial aggregate destruction cleans only the still-owned sub-Places where field-wise destruction is valid.
• try and match reuse the ordinary ownership model.
• A guarded move commits only when the guard succeeds and its arm is selected.
• MMIO, fixed-address and foreign storage are not automatically ordinary movable owners.
• RawPtr[T] does not imply ownership or deallocation authority.
• Ownership semantics do not require a universal runtime ownership table.