Copying and Moving

Copy vs Move

Copy

let second := first

When first is copyable, second receives an independent value according to the type's copy semantics.

After a valid copy:

first     available
second    available

Move

let second :<- first

Ownership transfers to second.

After a successful move:

first     unavailable
second    available

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

Copy and Move Are Semantic Operations

Copy and move semantics are decided before backend lowering.

A semantic copy may lower to:

• register operations;
• memcpy;
• vector instructions;
• descriptor copying;
• no machine copy after optimization.

A semantic move may lower to:

• register forwarding;
• destination passing;
• stack-slot reuse;
• pointer/descriptor transfer;
• physical byte movement;
• no physical movement at all.

Copy Classification

Every resolved Sec type has a copy classification before ordinary copy syntax is validated.

The conceptual classifications are:

TriviallyCopyable
SemanticallyCopyable
ConditionallyCopyable
MoveOnly
ExplicitlyNonCopyable

These names describe compiler semantics. Most programs do not need to mention them directly.

What matters to normal source code is whether an ordinary copy is legal for the concrete resolved type at that use site.

Trivially Copyable Values

A trivially copyable value can be duplicated without:

• type-defined behavior;
• allocation;
• failure;
• ownership transfer;
• observable side effects.

Typical examples include:

• scalar primitive values;
• ordinary fieldless enums;
• RawPtr[T] as an address value;
• shared references where their reference rules permit copying;
• aggregates whose complete resolved contents are trivially copyable.

“Trivial” is a semantic classification. A large trivial value may still be implemented with an efficient bulk-copy instruction.

Semantically Copyable Values

Some values may be safely copied even when the representation is not equivalent to naïve byte duplication.

An implicit semantic copy must remain:

• infallible;
• allocation-free;
• free from observable side effects;
• safe with respect to ownership and mutable aliasing.

An arbitrary method named Copy, Clone, Duplicate or similar does not define implicit copy semantics.

Explicit duplication methods remain ordinary explicit operations and may allocate, fail, duplicate external resources or return a different type.

Conditionally Copyable Types

Generic and aggregate types may be copyable only for some concrete forms.

type Pair[T, U] struct {
    First: T,
    Second: U,
}

Whether Pair[T, U] is implicitly copyable depends on the resolved semantics of T, U and the nominal type itself.

The compiler resolves that classification at the concrete use site before accepting ordinary copy syntax.

Lack of proof is not permission to copy.

Move-Only Values

A move-only value can transfer ownership but cannot be implicitly duplicated.

Examples commonly include:

• owning dynamic arrays T[];
• owning dynamic collection values unless their contract explicitly defines safe copy semantics;
• ref mut T reference holders;
• closures that own move-only captures;
• consuming callable values;
• resource-owning nominal types;
• types explicitly marked non-copyable.

This is invalid for a move-only value:

let second := first

Use an explicit move when ownership should transfer:

let second :<- first

@noCopy

A nominal type may explicitly prohibit implicit copying:

@noCopy
type FileHandle struct {
    ...
}

@noCopy means that ordinary copy syntax is forbidden for the annotated type and for containing classifications that must conservatively include it.

@noCopy does not forbid moving.

Sec 0.1 does not define a general @noMove or @affine source annotation.

Copyability is also separate from:

• pinning;
• address stability;
• thread transferability;
• destruction complexity;
• physical relocatability.

Derived Copyability

Compound types derive copyability from their complete semantic contract.

Physical fields alone are not always enough. A nominal type may deliberately remain non-copyable because it represents one unique external identity even when its raw fields would be easy to duplicate.

Fixed Arrays and Aggregates

A fixed array T[N] is implicitly copyable only when:

• T is implicitly copyable;
• the array type introduces no stronger ownership restriction.

let first: int[3] := [1, 2, 3]
let second := first

A struct containing a move-only owned field is not implicitly copyable as a complete value.

type Session struct {
    Name: string,
    Connection: Connection,
}

If Connection is move-only, ordinary copying of Session is not legal merely because Name is copyable.

Option and Result

Option[T] is implicitly copyable only when its payload semantics permit copying T.

Result[T, E] is implicitly copyable only when both active payload domains are copyable.

Must-use behavior is independent from copyability. A copyable Result may still require explicit handling.

References and Raw Pointers

Shared ref T values may be copied when the reference rules permit it:

let first := ref item
let second := first

This copies the reference value, not item.

ref mut T is move-only because copying an exclusive reference holder would violate exclusivity.

RawPtr[T] is trivially copyable as an address value. Copying a raw pointer never implies ownership of the pointed storage.

string Is Implicitly Copyable

Sec 0.1 defines string as immutable and implicitly copyable under its canonical representation contract.

let first := "Sec"
let second := first

The implicit copy must remain:

• infallible;
• allocation-free;
• side-effect-free;
• free from mutable aliasing.

The implementation may use immutable backing, a descriptor representation, Arena-backed immutable storage or another representation satisfying those guarantees.

Copyable string does not require hidden reference counting.

Dynamic Owning Collections

Owning dynamic collections are move-only unless their canonical type contract explicitly defines an infallible, allocation-free independent copy.

For the fundamental dynamic array:

int[]

ordinary assignment does not silently deep-copy backing storage.

If an owning collection provides an explicit duplication operation, using that operation does not make normal := or = into implicit copies.

Non-owning slices and views follow reference/view semantics instead of owning-container copy rules.

Closures and Function Values

A plain named function value is copyable.

A closure derives copyability from:

• its capture modes;
• the copyability of owned captures;
• its callable capability.

A closure that owns a move-only capture is move-only.

A closure capturing ref mut is move-only unless the operation is a valid reborrow rather than a copy.

A consuming callable value is move-only even if all stored captures would otherwise be copyable.

Ordinary Initialization Copies Reusable Sources

let destination := source

When source is an existing reusable Place, this syntax means Copy.

It is legal only when the source value is implicitly copyable in that context.

Sec never reinterpret ordinary := as Move merely because the source happens to be move-only.

This is intentionally invalid:

let destination := moveOnlySource

when an independent copy cannot be produced.

Ordinary Assignment Copies Reusable Sources

destination = source

For an existing reusable source, ordinary assignment uses copy semantics.

After a valid copy assignment:

source         available
destination    owns its resulting value

If destination was already available, its previous value is replaced according to destruction rules.

If destination was unavailable and mutable, the assignment reinitializes it.

Move Initialization

Move initialization with inferred destination type uses:

let destination :<- source

After a successful move from a reusable source:

source         unavailable
destination    available

The source's storage may still physically exist. What ended is the source Place's ownership of that value.

Typed Move Initialization

When the destination type is written explicitly, the type annotation and move operator remain separate parts of the declaration:

let destination: Buffer <- source

Compare the inferred-type form:

let destination :<- source

In both cases the source is consumed after successful transfer.

Move Assignment

Move assignment or move replacement uses:

destination <- source

If the destination is already available, the old destination value is replaced after the incoming transfer is ready to commit.

If the destination is unavailable and mutable, the move reinitializes it.

An immutable unavailable destination cannot be reinitialized.

Copyable Values May Still Be Explicitly Moved

Explicit move syntax is meaningful even for a type that could have been copied:

let first := 10
let second :<- first

Because the programmer explicitly requested Move, the source becomes unavailable.

The compiler must not silently turn the operation back into Copy merely because the type is copyable.

This is useful when source availability itself is part of the intended ownership flow.

Move Does Not Reset the Source

Moving from a source does not perform:

source = default
source = 0
source = None
source = null

The source simply becomes unavailable as an owned value.

A mutable unavailable Place may later be explicitly reinitialized:

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

resource = OpenResource()

The Reusable-Source Visibility Rule

A reusable named or projected Place must never be silently consumed.

Examples of reusable sources:

resource
package.Payload
state.Connection

If ownership leaves such a source and execution may continue in the source scope, the consuming source must be visibly marked.

Consume(<-resource)

let payload :<- package.Payload

destination <- state.Connection

This rule applies even when the value is copyable if the programmer explicitly chooses to move it.

Fresh Temporaries Do Not Need Redundant Move Syntax

A fresh temporary has no reusable source Place to preserve.

Therefore:

Consume(CreateBuffer())

is preferred over synthetic move syntax around the temporary.

Likewise:

let buffer := CreateBuffer()

receives the fresh returned value directly.

The language does not require ownership-transfer notation at both ends of an already-obvious fresh-value transfer.

Ordinary By-Value Parameters Do Not Implicitly Consume

fn Inspect(value: Buffer) void {
    ...
}

Passing an existing reusable source to an ordinary by-value parameter requires a legal copy:

Inspect(buffer)

If Buffer is move-only, this call is invalid.

The compiler does not reinterpret the ordinary parameter as consuming merely because copying is unavailable.

This keeps API ownership semantics visible in the function signature.

Consuming Parameters

A parameter that intentionally takes ownership uses ->:

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

An existing reusable caller source must use <-:

Consume(<-buffer)

This is invalid:

Consume(buffer)

when buffer is an existing reusable Place.

The call-site marker is required even when Buffer is copyable. A consuming parameter is an API ownership contract, not merely a fallback for non-copyable values.

A fresh temporary may be passed directly:

Consume(CreateBuffer())

Fallible Argument Evaluation and Transfer Commit

Function arguments evaluate left to right.

Ownership transfer from reusable caller-owned Places into the outer callee commits only after all arguments required for call entry have been prepared successfully.

try Send(
    <-message,
    ResolveDestination(),
) {
    Err(error) => Handle(error)
}

If ResolveDestination() fails before Send begins, the outer call has not consumed message.

However, ownership effects completed inside evaluation of an earlier argument expression are real completed effects and are not rolled back merely because a later outer argument fails.

Pending transfer also reserves the relevant source Place against conflicting sibling argument use until the outer call either commits or fails.

Return Is an Intrinsically Transferring Boundary

Every non-reference return transfers or creates one result value owned by the caller.

The canonical form is simply:

fn Create() Buffer {
    let buffer := CreateBuffer()
    return buffer
}

A move-only local may therefore be returned without a return-site move marker.

Receiving the result also needs no move marker:

let buffer := Create()

Terminal Return Construction

The intrinsic return-transfer context propagates through structural construction that directly forms the returned value.

return Some(resource)

return Packet.Data(resource)

return Response {
    Body: resource,
}

return Ok(Response {
    Body: resource,
})

A reusable move-only local may flow through these direct return-construction paths without an inner move marker.

This rule is specific to the terminal return boundary.

An ordinary function call inside the return expression keeps its declared parameter modes:

return Transform(resource)

If Transform has an ordinary by-value parameter, resource must still be copyable. If it has a consuming parameter, the call still requires visible call-site transfer from a reusable source.

Return Does Not Grant Ownership of Borrowed Storage

Terminal return transfer only applies to values the current function actually owns.

From borrowed storage:

fn ReadName(person: ref Person) string {
    return person.Name
}

this is valid only when Name can be copied under ordinary copy rules.

A move-only owned field cannot be removed from borrowed storage simply because the access occurs in return.

Return context also does not grant ownership of:

• static storage;
• foreign storage;
• volatile/MMIO storage;
• unavailable Places;
• otherwise non-movable storage.

Aggregate Field Transfer

Ordinary aggregate construction copies reusable sources when they are copyable:

let packet := Packet {
    Id: id,
    Name: name,
}

A reusable move-only source transferred into an owning field must be explicit:

let session := Session {
    Name: name,
    File: <-file,
}

The compiler never infers destructive field transfer solely because file is non-copyable.

A fresh temporary may flow directly:

let session := Session {
    Name: name,
    File: OpenFile(),
}

When the aggregate directly forms a returned result, the terminal return rule applies.

Option Payload Transfer

Outside a terminal return boundary, a reusable move-only source transferred into Some must be explicit:

let value := Some(<-resource)

Plain:

let value := Some(resource)

copies when resource is copyable and is invalid when ownership transfer would be required.

Direct return construction uses the terminal return rule:

return Some(resource)

Result Payload Transfer

Outside a terminal return boundary:

let result := Ok(<-resource)

explicitly transfers a reusable move-only value into the Result payload.

The same rule applies to Err payloads.

When the Result directly forms the returned value:

return Ok(resource)

the return boundary owns the transfer. No inner return-site move marker is required.

Union Payload Transfer

A union owns its active owning payload according to the union contract.

A reusable move-only source transferred into a union payload uses visible transfer:

let message := Message.Data(<-payload)

Moving a complete union transfers ownership of its active payload without exposing or duplicating the representation.

Direct return construction remains concise:

return Message.Data(payload)

Closure Capture

Plain owned capture means copy capture:

capture(value)

The source must therefore be copyable.

Consuming capture uses:

capture(<-value)

This consumes the source even when an ordinary copy would have been possible.

Borrow captures are separate:

capture(ref value)
capture(ref mut value)

and follow borrowing and lifetime rules rather than owned-copy/move rules.

Replacement Commit Ordering

Copy or move assignment into an already available mutable destination replaces the existing destination value.

Conceptually, Sec preserves this order:

1. evaluate the source expression;
2. validate conversions, contracts, borrows, overlap and ownership;
3. complete fallible preparation;
4. end or destroy the old destination value;
5. install the new value;
6. establish destination ownership;
7. if the source was moved, commit source unavailability.

The old destination must not be destroyed before a fallible incoming operation is known to be ready to commit.

Reinitialization

Assignment to an unavailable mutable destination creates a new owned value there without destroying a nonexistent old value.

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

resource = OpenResource()

Copy or move assignment can both reinitialize when their respective source rules are satisfied.

An immutable unavailable Place cannot be reinitialized by assignment.

Self-Move and Overlap

Copy self-assignment may be legal for copyable values and may be optimized away:

value = value

Move self-assignment is invalid:

value <- value

More generally, a move is invalid when source and destination overlap in a way that would break transfer or destruction ordering.

Backend use of memcpy or memmove does not define whether an overlapping source-language operation is valid.

Partial Moves

A field or independently tracked sub-Place may be moved explicitly:

let payload :<- package.Payload

A partial move is legal only when:

• the source aggregate is owned;
• the projected Place can be tracked precisely enough;
• no conflicting borrow exists;
• the storage model permits the transfer;
• destruction rules permit partial ownership;
• no stronger type rule forbids it.

A type with custom free does not permit partial moves from its fields in Sec 0.1.

An immutable aggregate may still undergo a legal explicit partial move. Immutability prevents later repair, not the ownership transfer itself.

Already-moved fields are never destroyed by the former aggregate owner.

Copy/Move State Is Path-Sensitive

Moving a value on one branch affects only paths that actually performed the move.

let resource := OpenResource()

if condition {
    Consume(<-resource)
    return
}

Use(resource)

The consuming path terminates. The continuing path still owns resource.

When continuing paths disagree, ownership may become conditionally available as described in the Ownership chapter.

Moves in Loops

Loop ownership uses fixed-point analysis across:

• the loop body;
• continue edges;
• backedges;
• break exits.

A Place moved in one iteration must be reinitialized on every path that attempts to use or move it on a later iteration.

for condition {
    Consume(<-resource)

    resource = OpenResource()
}

Whether this is valid depends on every path reaching the next iteration with the required availability.

match Payloads

Pattern syntax determines whether a payload is copied, moved or borrowed.

Whole-payload by-value binding in match may move a move-only payload because pattern matching itself defines that ownership mode.

This is different from ordinary construction or function-call syntax, which never silently consumes a reusable source.

A guarded prospective move commits only if the guard succeeds and that arm is selected.

switch does not silently consume its subject.

discard Is Not Move

discard place intentionally ends ownership in that Place:

discard resource

Move transfers ownership to another owner. discard does not.

Discard may perform required destruction when the value is still owned.

It is therefore a distinct semantic operation and must not be implemented as a move to an invisible temporary.

Consuming Result Projections

The compiler/core-defined:

result.Ok()
result.Err()

are consuming transformations of an owned Result[T, E].

The active retained payload transfers into the resulting Option. The inactive side ends according to ordinary destruction rules.

No hidden clone is permitted for move-only payloads.

After consuming .Ok() or .Err() from an owned reusable Result Place, that complete Result Place is unavailable unless legally reinitialized.

Methods and self

Ordinary methods do not consume the complete self.

Whole-instance lifetime termination belongs to destruction and free.

A method with sufficient mutable/exclusive receiver authority may consume an owned member when partial-move and borrowing rules permit it:

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

Sec 0.1 does not introduce a general expression form such as:

(<-resource).Method()

for consuming complete method receivers.

Volatile Storage and Local Snapshots

Volatile is a storage-access property, not a copy/move classification of the local value produced by the access.

let first := device.Status
let second := first

If device.Status is a volatile register read:

• the first statement performs one volatile access;
• first is then an ordinary local Sec value snapshot;
• copying or moving first does not perform another hardware read.

The physical MMIO storage itself is not an ordinary Sec-owned reusable value that can be moved out with <-.

FFI, Channels and Concurrent Transfer

Copyability and cross-thread/process transferability are separate properties.

FFI ownership transfer must come from the foreign contract. It is not inferred from ABI representation.

A channel may transfer ownership of a move-only value only when the channel operation's contract says so.

Fallible transfer must define ownership on both success and failure paths. A failed send must not silently lose the sender's value.

Multi-path transfer constructs such as select must commit ownership only to the path actually selected.

Generics and Copyability

Generic code may perform an implicit copy only when the concrete specialization proves that the value is copyable.

Generic code must not treat “copyability unknown” as permission to copy.

Monomorphization may specialize the machine implementation of copy or move, but it does not change the source ownership contract.

An owned erased interface value is move-only unless its concrete interface/value representation contract proves a valid independent copy.

Borrowed interface references follow normal reference rules and do not transfer ownership of the referent.

Copyability and Destruction Are Separate

Whether a type can be copied and whether a type requires non-trivial destruction are separate classifications.

A type may be:

• move-only but trivially destructible;
• copyable but require representation-aware cleanup;
• non-copyable because of unique identity despite simple raw storage;
• trivially copyable and trivially destructible.

Copy/move lowering must always obey the independent destruction contract.

Legal Copies Can Still Be Expensive

A copy does not become semantically invalid merely because it is large.

fn Inspect(value: LargeBuffer) void {
    ...
}

If LargeBuffer is copyable, passing an existing reusable value by ordinary by-value syntax remains legal.

Compiler analysis may still recommend a non-owning API:

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

or a slice/view form when an independent copy is unnecessary.

Such diagnostics are performance guidance, not ownership corrections.

Copy and Move Elision

The compiler may eliminate physical copies and moves when all source semantics remain intact.

Possible optimizations include:

• copy elision;
• move elision;
• return-value optimization;
• destination passing;
• buffer reuse;
• in-place update;
• register forwarding;
• stack-slot reuse;
• bulk memory operations;
• target-specific transfer instructions.

But optimization may not change:

• source availability;
• destination ownership;
• destruction count;
• borrow validity;
• external ownership;
• volatile effects;
• address-stability guarantees.

Diagnostics

Important copy/move diagnostics include:

• copy of a non-copyable value;
• use after move;
• move while borrowed;
• invalid self-move;
• overlapping move;
• reinitialization of an immutable Place;
• unsupported partial move;
• move from non-owned storage;
• move from fixed or volatile storage;
• missing consuming call-site marker;
• implicit consuming payload construction;
• invalid whole-self consumption;
• copyability not proven for a concrete generic specialization.

Copy of a move-only value

cannot copy `buffer`

`Buffer` is move-only, so `let next := buffer` would require an independent copy

help: move ownership with `let next :<- buffer`
help: borrow with `ref buffer` when ownership transfer is not intended

Missing call-site transfer

`Consume` takes ownership of `buffer`

the argument is an existing reusable value, so the transfer must be explicit

help: write `Consume(<-buffer)`

Use after move

`buffer` is unavailable here

ownership was moved earlier by:
    Consume(<-buffer)

help: use the new owner
help: reinitialize `buffer` if it is mutable and a new value is intended

Move from borrowed storage

cannot move this value out of borrowed storage

the current access grants a borrow, not ownership

help: borrow the value
help: redesign the API to transfer ownership explicitly

LSP hover and analysis should be able to expose:

• copy classification;
• whether an operation is Copy or Move;
• the source Place;
• the ownership destination;
• the consuming parameter or payload boundary;
• source availability after transfer;
• partial aggregate state;
• safe borrow/move alternatives where provable.

Best Practices

• Use ordinary := and = only when a reusable source is meant to be copied.
• Use :<- for inferred-type move initialization.
• Use Type <- source after an explicit type annotation for typed move initialization.
• Use <- at the reusable source position for consuming calls and owning payload construction.
• Do not add move markers to fresh temporaries merely for ceremony.
• Do not add a move marker at the return boundary; return already transfers ownership.
• Prefer borrowing when a callee does not need an independent value or ownership.
• Use explicit duplication methods when an owning collection or resource needs a deliberate independent duplicate.
• Remember that moving a copyable value still consumes the source when explicit move syntax is used.
• Do not assume moving resets the source to a default value.
• Do not move values out of borrowed, static, volatile or foreign storage without an explicit ownership-taking contract.
• Keep large-copy performance advice separate from semantic copy legality.

Summary

• Copy duplicates a value and keeps the source available.
• Move transfers a value or ownership responsibility and makes a reusable consumed source unavailable.
• Copy and Move are semantic operations independent of backend instruction choice.
• A move does not write a default, zero, None or null value back to the source.
• Every resolved type has a copy classification before ordinary copy syntax is accepted.
• Conceptual copy classifications include trivially copyable, semantically copyable, conditionally copyable, move-only and explicitly non-copyable.
• Implicit semantic copy must be infallible, allocation-free and free from observable side effects.
• Arbitrary user methods such as Clone do not define implicit copy semantics.
• @noCopy forbids implicit copying but does not forbid moving.
• Sec 0.1 has no general @noMove or @affine annotation.
• Fixed arrays derive copyability from their elements and complete type contract.
• A struct containing a move-only owned field is not implicitly copyable as a whole.
• Option[T] and Result[T, E] derive copyability from their possible payloads.
• Shared ref T values may be copyable; ref mut T is move-only.
• RawPtr[T] is trivially copyable as an address value and carries no ownership merely by being copied.
• string is immutable and implicitly copyable under its canonical allocation-free copy contract.
• Owning dynamic arrays and other owning dynamic collections are move-only unless their canonical contract explicitly says otherwise.
• Non-owning slices and views follow reference/view rules rather than owning-container copy rules.
• Closures derive copyability from their captures and callable capability.
• let destination := source copies an existing reusable source and never silently moves it.
• destination = source uses copy/replacement semantics for an existing reusable source.
• Inferred-type move initialization uses let destination :<- source.
• Typed move initialization uses let destination: Type <- source.
• Move assignment uses destination <- source.
• Explicit move syntax may consume even a copyable value.
• Reusable source Places must never be silently consumed.
• Fresh temporaries may forward directly into their first owner without redundant move syntax.
• Ordinary by-value parameters require Copy from existing reusable arguments.
• A move-only argument is not silently consumed by an ordinary by-value parameter.
• Consuming parameters use ->.
• An existing reusable argument to a consuming parameter uses <- at the call site.
• The consuming call-site marker is required even for copyable values.
• Fresh temporaries may be passed directly to consuming parameters.
• Arguments evaluate left to right.
• Outer-call ownership transfer commits only after all required arguments are ready and call entry can occur.
• A later argument failure cancels uncommitted outer-call transfer reservations.
• Ownership effects completed inside earlier argument expressions are not rolled back.
• return is intrinsically transferring for non-reference results.
• A move-only owned local is returned as return value.
• Sec does not use a return-site <- marker.
• Fresh returned values are received without a move marker.
• Terminal return context propagates through direct structural construction such as aggregates, unions, Some, Ok and Err.
• Ordinary function calls inside return expressions retain their declared argument ownership modes.
• Return context does not grant ownership of borrowed, static, foreign, volatile, MMIO or unavailable storage.
• Owning aggregate fields require explicit transfer from reusable move-only sources outside terminal return construction.
• Some(<-resource), Ok(<-resource) and owning union payload construction visibly transfer reusable move-only values.
• Plain closure capture copies and therefore requires copyability.
• capture(<-value) consumes the captured source.
• Borrow captures use ref or ref mut and do not transfer referent ownership.
• Replacement validates the incoming operation before destroying the old destination value.
• Move source unavailability commits as part of the successful replacement/transfer operation.
• Assignment to an unavailable mutable Place is reinitialization.
• Move self-assignment is invalid.
• Overlapping moves are rejected when transfer/destruction order would be invalid.
• Partial moves must be explicit at the moved sub-Place.
• Partial move requires owned source, precise Place tracking, compatible borrowing and compatible destruction semantics.
• Types with custom free do not permit partial field moves in Sec 0.1.
• Immutable aggregates may be explicitly partially moved but cannot later repair the moved field by assignment.
• Copy/move state is path-sensitive.
• Loops require fixed-point ownership analysis across backedges and exits.
• match pattern syntax may define payload copy, move or borrow behavior directly.
• discard is a distinct terminal ownership-ending operation, not Move.
• Result.Ok() and Result.Err() are consuming transformations of an owned Result.
• Ordinary methods cannot consume complete self.
• Methods may consume owned members when receiver authority, borrowing and partial-move rules permit it.
• Volatile access produces an ordinary value snapshot; later copy/move of the snapshot does not repeat the volatile read.
• Physical volatile/MMIO storage is not an ordinary movable owner.
• FFI ownership transfer must be explicit in the foreign contract.
• Channel transfer commits ownership only according to the channel operation's contract.
• Fallible transfer must preserve or transfer ownership correctly on every outcome.
• Generic code may copy only after concrete copyability is proven.
• Copyability and destruction classification are independent.
• A legal copy may be expensive without becoming semantically invalid.
• The compiler may recommend borrowing instead of a large legal copy.
• Copy/move elision may change machine implementation but not source availability, ownership or destruction behavior.