Destruction

Destruction, Cleanup, Resource Release and Deallocation Are Different

Destruction

Destruction ends the current owner's responsibility for a value and performs the cleanup required by the resolved type and current ownership state.

Cleanup

Cleanup is the compiler-generated sequence of automatic destruction and registered deferred work executed when Sec semantics leave a lifetime or control-flow region.

Resource release

Resource release is a type- or API-defined operation that releases an external or logical resource such as a handle, mapping, lock state, foreign object or device registration.

Deallocation

Deallocation returns owned allocation storage through the allocator or authority that owns that storage.

free

free is Sec's custom lifecycle cleanup member for a type whose complete cleanup cannot be expressed solely through automatic destruction of its owned fields.

It is not an ordinary method and is never called as value.free().

Every Resolved Type Has a Destruction Classification

Conceptually, the compiler classifies a concrete type as:

TriviallyDestructible
NonTriviallyDestructible

These names describe compiler semantics; they are not source-level enum members.

Trivially Destructible

A type is trivially destructible when ending an owned value's lifetime requires no observable cleanup action.

Typical examples include:

• ordinary scalar values;
• safe references;
• mutable references;
• RawPtr[T];
• fieldless enums;
• aggregates containing only trivially destructible owned fields.

Trivial destruction may lower to no machine instruction at all. The compiler still updates semantic ownership/lifetime state.

Non-Trivially Destructible

A type is non-trivially destructible when ending an owned value may require observable cleanup directly or recursively through owned subvalues.

Typical examples include:

• owning collections;
• owned allocations;
• resource wrappers;
• file, socket and device handles;
• runtime mappings;
• owned foreign resources;
• types defining custom free;
• aggregates containing non-trivially destructible owned fields.

Classification follows concrete ownership representation, not merely the source type name.

For example, a standard type such as string may have trivial or non-trivial destruction depending on its canonical representation and ownership state.

Destruction Classification Is Independent from Copyability

Copyability and destruction are separate semantic properties.

@noCopy does not automatically mean non-trivial destruction.

Likewise, a copyable type may require destruction when a valid copy produces an independently owned cleanup obligation.

Exact-Once Destruction

An owned non-trivial value that remains owned when its lifetime ends is destroyed exactly once.

The compiler must never:

• destroy a value after ownership moved elsewhere;
• destroy an unavailable Place again;
• destroy a value that never finished initialization;
• destroy a moved or discarded sub-Place through its former owner;
• omit the terminal action of a still-owned non-trivial value.

Double destruction is a compiler correctness defect, not an acceptable backend artifact.

Automatic Destruction

Ordinary owned values are destroyed automatically when their lifetime ends unless ownership already transferred or another canonical terminal action ended the owner's responsibility.

User code does not need explicit cleanup solely because a normal local variable reaches the end of its lifetime.

Automatic destruction is source-language semantics. It is not inferred later from “unused SSA values”.

Successful Initialization Registers Destruction Responsibility

When an owned value becomes successfully initialized, its current owner gains the corresponding destruction responsibility.

Legal reinitialization establishes a new responsibility for the new value.

Move, discard, return transfer, consuming argument transfer and other terminal ownership actions cancel the former owner's responsibility for the transferred or ended value.

Automatic Destruction and defer Share One LIFO Cleanup Order

fn Example() void {
    let first := OpenFirst()

    defer {
        Log("leaving")
    }

    let second := OpenSecond()
}

Conceptual registration order:

destroy first
defer Log
destroy second

Exit order:

destroy second
run defer Log
destroy first

Sec does not run “all defers” as a separate phase before or after all automatic destruction.

The common order follows source-semantic registration time.

Values May Still Be Destroyed at Their Earliest Legal Lifetime End

Unified cleanup ordering does not force every owned value to survive until invocation exit.

A value may be destroyed earlier when ownership, borrowing, deferred uses, control flow and observable ordering all permit it.

A defer that later reads a value extends that value's required lifetime until the deferred use.

Local Values Destroy in Reverse Successful Registration Order

Owned locals whose lifetimes otherwise overlap are destroyed in reverse successful initialization/cleanup-registration order.

A declaration whose initialization never completes is not destroyed as a completed value.

Struct Fields Destroy in Reverse Declaration Order

type Example struct {
    First: First
    Second: Second
    Third: Third
}

Compiler-derived field destruction order:

Third
Second
First

Optimization may not reorder observable field destruction.

Fixed Arrays Destroy Elements in Reverse Index Order

A fixed array destroys initialized still-owned elements from the highest relevant index down to the lowest.

Elements whose ownership already moved or ended are skipped.

Owned Temporaries Are Destroyed Deterministically

An owned temporary remains live through the enclosing full expression unless an earlier ownership transfer ends its responsibility sooner.

Use(CreateFirst(), CreateSecond())

With left-to-right argument evaluation, the conceptual order is:

CreateFirst
CreateSecond
Use
destroy remaining second temporary
destroy remaining first temporary

A temporary forwarded into its first owner is not also destroyed by the forwarding context.

Lifetime shortening must not change observable destruction order, reference validity, defer behavior, volatile effects or expression-evaluation order.

Move Cancels the Former Owner's Destruction Responsibility

let destination :<- source

Once the move commits, source no longer owns that value and must not destroy it later.

The new owner becomes responsible for the value's eventual terminal action.

Moved-from storage is not itself a live default value and receives no destruction.

Consuming Calls Transfer Destruction Responsibility at Commit

fn Consume(-> resource: Resource) void {
    ...
}

Consume(<-resource)

The caller keeps its destruction responsibility until the consuming transfer actually commits.

Fallible argument preparation must not cancel cleanup early if the call never reaches the ownership-transfer point.

After successful transfer commitment, the caller must not destroy the transferred value.

Returning an Owned Value Transfers Destruction Responsibility

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

The returned value becomes the responsibility of the result/caller owner.

The callee excludes that transferred value from its local cleanup.

Sec's canonical return syntax uses ordinary return value; there is no return-site move marker in the current language model.

Ownership Moved into an Aggregate or Variant Moves Cleanup Responsibility with It

When an owned payload is transferred into an owning aggregate, Result/Option/union variant or other owner, that new container becomes responsible for eventual destruction.

The former source Place must not later destroy the same payload.

Partial Destruction Destroys Only Still-Owned Sub-Places

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

At the later end of package's lifetime, package.Payload is not destroyed through package because ownership transferred earlier.

Other still-owned fields such as package.Header are destroyed normally when their types require it.

The rule applies recursively to nested Places where partial moves are legal.

Whole-value cleanup must therefore respect current per-sub-Place ownership state.

A Type with Custom free Does Not Permit Partial Field Moves in Sec 0.1

A custom free body is allowed to rely on the completed value's complete ownership invariant.

Therefore Sec 0.1 rejects partial moves from owned fields of a type that defines custom free.

This avoids invoking a completed-value cleanup routine against an object whose expected owned fields have already been removed.

Conditionally Owned Values Are Destroyed Only on Paths Where Ownership Remains

let mut package := LoadPackage()

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

After the branch, package.Payload may still be owned on one path and be unavailable on another.

Cleanup must destroy the payload only on runtime paths where the current owner still owns it.

The compiler resolves this statically whenever path facts are sufficient.

Conditional Destruction May Require Hidden Compiler Bookkeeping

When static control-flow facts cannot completely resolve conditional cleanup, a hosted implementation may use:

• hidden SSA state;
• a drop/availability flag;
• split cleanup blocks;
• another equivalent compiler representation.

This bookkeeping is compiler state and does not automatically become part of the source type's ABI layout.

A target or project policy may forbid dynamic ownership bookkeeping. In that case, the compiler rejects only programs whose correct semantics genuinely require such runtime state.

Source restructuring or explicit ownership convergence may eliminate the need.

is available Refines Ownership, Not Destruction by Itself

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

Availability tests refine the ownership state defined by the Ownership chapter.

They do not test:

• null;
• None;
• payload contents;
• borrow validity;
• Arena/reference epoch validity.

Destruction lowering may reuse the same resolved availability facts, but the language does not require one particular runtime representation.

discard Converges Ownership and Destruction

Legal discard of an available owned value ends that value, performs required destruction and leaves the Place unavailable.

discard resource

Discard of an already unavailable Place is a legal destruction no-op. No second destruction occurs.

Discard of a conditionally available Place destroys only runtime paths where ownership remains and leaves every outgoing path unavailable:

let mut package := LoadPackage()

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

discard package.Payload
package.Payload = CreateBuffer()

The final assignment is ordinary reinitialization because all paths have converged to unavailable first.

Destruction semantics do not make a non-discardable value discardable. Discard legality is checked first.

Reinitialization Performs No Old-Value Destruction

Assignment to an unavailable mutable Place is reinitialization.

let mut value := CreateFirst()
discard value
value = CreateSecond()

At the assignment, no old owned value exists in value, so there is nothing to destroy.

Successful reinitialization starts a new value lifetime and registers a new destruction responsibility.

Destruction does not grant reinitialization authority to immutable Places.

Replacement Destroys the Old Value Before the New Destination Ownership Commits

let mut value := CreateFirst()
value = CreateSecond()

Because value is still available, the assignment is replacement.

The compiler first validates the complete source expression, conversions, contracts, borrows, overlap rules and fallible preparation.

Only after the replacement is semantically ready to commit does the old destination value end according to its canonical destruction plan and the new value become owned by the destination.

Conditional replacement destroys the old value only on paths where the destination was still owned; unavailable paths behave as reinitialization.

Successful Construction Transfers Cleanup into the Completed Value

A successfully completed init establishes one complete valid instance.

Cleanup responsibilities for its owned fields/resources then belong to that completed instance.

Fallible Construction Cleans Only What Was Successfully Initialized

type Resources struct {
    First: First
    Second: Second
    Third: Third
}

If construction of Second fails after First succeeded:

• First is cleaned up;
• Second is not treated as a successfully initialized complete value;
• Third is never initialized and receives no destruction;
• cleanup follows reverse successful initialization/registration order.

The outer type's completed-value custom free does not run when the outer value itself never finished construction.

Every resource acquired during init must have a defined cleanup path on each later failure path and on successful lifetime completion.

Custom free

Most types should rely entirely on compiler-derived field destruction.

Define custom free only when the type owns a resource whose cleanup is not already expressed correctly by ordinary owned fields.

Typical cases include:

• foreign resources represented by raw/non-owning handles;
• platform handles whose release is not represented by the field type;
• runtime mappings;
• device registrations;
• other opaque ownership contracts.

impl DeviceMapping {
    free {
        PlatformUnmap(self.Handle)
    }
}

free is a lifecycle member, not an ordinary function.

This is invalid:

mapping.free()

The compiler invokes free automatically when destroying a completed still-owned value of that type.

self During free

At entry to free, the completed value remains initialized and is under exclusive compiler-controlled destruction authority.

The free body must not:

• return self;
• let self escape;
• resurrect the complete value;
• transfer whole self elsewhere;
• move owned fields out of self in Sec 0.1.

Whole-value lifetime termination is the purpose of free. Ordinary user-defined methods do not consume whole self.

Compiler-known lifecycle operations such as Arena.Release() remain narrowly defined exceptions and do not create a general consuming-method facility.

Owned Fields Remain Compiler-Managed During Custom free

Custom free should normally release resources not already represented by ordinary owned fields.

Owned fields are automatically destroyed after the free body unless a specialized canonical rule explicitly says otherwise.

Sec rejects a statically provable manual release that would cause the same owned resource to be released again during automatic field destruction.

defer is not permitted inside free. Locals and temporaries created inside the body still receive normal automatic destruction.

Completed Custom-free Destruction Order

Conceptually:

run custom free body
destroy remaining initialized owned fields in canonical field order
release/deallocate representation-owned storage where required

Custom free does not suppress automatic destruction of ordinary owned fields.

Fallible Close and Automatic free Are Different

free has no return value and cannot return Result.

Automatic destruction cannot require its former owner to recover from a cleanup error after the ownership lifetime has ended.

A resource whose meaningful close can fail should expose an explicit fallible method before automatic destruction when appropriate:

impl File {
    fn Close() Result[void, IOError] {
        return CloseHandleChecked(ref mut self.Handle)
    }

    free {
        CloseHandleBestEffort(self.Handle)
    }
}

A successful explicit close must update the value's lifecycle state so later automatic destruction does not release the same underlying resource twice.

free is not implicitly unsafe; unsafe operations still require an explicit unsafe context.

free also must not silently translate an ordinary recoverable cleanup failure into panic.

Result, Option and Tagged Unions Destroy Only the Active Retained Payload

Destroying Result[T, E] destroys the active payload still owned by the Result.

Destroying Option[T] destroys the payload only when the active state is Some and ownership has not already transferred.

A tagged union similarly destroys only its active initialized still-owned payload.

Consuming .Ok() or .Err() transfers the selected payload into the resulting Option and ends the other side according to ordinary destruction/discard rules.

The consumed Result owner must not later destroy a payload whose ownership moved through the projection.

The compiler does not guess active ownership for untagged foreign unions. Safe non-trivial ownership requires an explicit wrapper/contract.

Collections, Shaped Values and Strings Follow Their Ownership Representation

Structs

A struct without custom free derives destruction recursively from initialized still-owned fields.

Owning dynamic arrays and lists

An owning collection destroys initialized still-owned elements in its canonical order, then releases owned backing through the recorded allocation authority.

Capacity beyond the initialized logical element range is not destroyed as if it contained live values.

An element removed by ownership transfer is not later destroyed by the collection.

Owning shaped values

Owning tensor/matrix/vector representations destroy still-owned initialized elements/resources as required and release owned backing.

Borrowed tensor views and slices do not destroy backing elements or storage.

Strings

String destruction follows the canonical concrete string representation. Static/borrowed forms may be trivial while an owned form releases owned storage.

Ordinary string replacement may automatically end the prior owned representation; the programmer does not need to write discard merely because cleanup exists.

References and Borrowed Views Do Not Destroy Their Referents

Destroying or discarding a safe reference ends only the reference-holder value.

Destroying a borrowed slice or view likewise does not destroy its backing storage or elements.

Conversely, destruction of an owned referent is rejected while an incompatible live borrow requires that value or overlapping Place to remain valid.

A deferred read is a later use and may extend the referent's lifetime until the defer runs.

Reference generation/epoch validity and ownership availability remain separate concepts.

Control-Flow Exits Execute Only the Cleanup They Actually Exit

Return

The return result is established first. Still-owned non-transferred values are then cleaned according to the unified cleanup order.

return try

The success or failure payload is transferred/propagated first and excluded from the cleanup of the ownership context that transferred it.

Error propagation

Unmatched try propagation executes cleanup for still-owned values on the propagating path.

A recovery value that continues establishes ordinary new ownership/destruction responsibility.

break

Executes cleanup for every lifetime/scope region actually exited by the break edge.

continue

Cleans per-iteration values/regions that end before the next iteration but does not destroy loop-carried values that remain live.

match and switch

Each branch has its own destruction state. Branch-local owned values clean up when leaving the branch unless ownership transfers.

Loop Destruction Is Path- and Iteration-Sensitive

The compiler distinguishes:

• pre-loop owned values;
• per-iteration values;
• loop-carried values;
• conditionally initialized values;
• values moved during one iteration;
• values retained after loop exit.

A per-iteration value is destroyed once for every reached iteration unless ownership transfers elsewhere.

A Place moved in one iteration remains unavailable on later iterations unless valid control flow reinitializes it.

Loop fixed-point analysis must preserve exact-once destruction across entry, backedge, continue, break and zero-iteration paths.

The compiler rejects ownership states it cannot model safely instead of emitting speculative cleanup.

Destruction and Deallocation Are Separate

Destroying a value ends its semantic owned lifetime. Deallocation releases the storage backing an owning allocation.

Stack storage may disappear with its scope, but a non-trivial value living there must be semantically destroyed first.

Every explicit owning allocation must preserve enough information to select the matching deallocation authority.

Storage allocated by one allocator must not be released through an incompatible allocator.

RawPtr[T] alone never creates ownership or deallocation responsibility.

The compiler must not infer that a raw pointer should be freed merely because the raw pointer value reaches the end of its lifetime.

FFI Ownership Transfer Controls Destruction Responsibility

Foreign contracts distinguish cases such as:

• borrowed foreign pointers;
• caller-owned foreign resources;
• Sec-owned foreign resources;
• ownership transferred to foreign code;
• ownership transferred from foreign code;
• resources requiring a matching foreign release operation.

When ownership legally transfers to foreign code, the former Sec owner becomes unavailable and must not destroy the resource later.

A fallible ownership-transferring foreign call must define whether ownership was accepted on each outcome.

Ambiguous ownership transfer is rejected or isolated behind an explicit unsafe wrapper with a well-defined ownership contract.

An owning Sec wrapper may use custom free to call the matching foreign release operation exactly once.

Static and Global Destruction Requires a Deterministic Shutdown Plan

Sec does not assume that every hosted process automatically runs deterministic global cleanup at process exit.

Static/global owned values requiring destruction are valid only when the canonical program initialization/shutdown plan and target profile provide deterministic cleanup for that storage lifetime.

A target without supported deterministic static teardown must reject static/global owned values whose required destruction cannot otherwise be satisfied.

Freestanding/runtime-free targets do not gain a hidden global destruction registry merely to support static teardown.

Where deterministic static cleanup exists, order comes from the canonical dependency, use and shutdown plan rather than arbitrary source, import, linker, filesystem or worker order.

Normal Program Termination Runs the Defined Shutdown Cleanup

Returning normally from main executes the cleanup required by the canonical program shutdown plan.

A raw platform termination primitive explicitly defined not to unwind or clean callers does not promise cleanup after that termination point.

Abnormal hardware or operating-system termination cannot guarantee pending destruction.

Panic Cleanup Follows the Panic Policy

Destruction on panic paths is governed by the panic-domain and target/profile model.

The compiler does not assume that every pending destructor or defer executes on every panic path.

In particular, Sec destruction must not silently introduce a general exception-unwinding runtime.

When a panic policy does guarantee cleanup, that cleanup follows the same resolved destruction and defer ordering already established for the affected domain.

Destruction Does Not Imply Synchronization

Moving ownership to a task, thread or another execution owner transfers destruction responsibility with the ownership.

The former owner must not destroy the transferred value.

Transfer must be represented before cleanup placement is finalized.

A lifetime being long enough does not by itself make destruction race-free or synchronization-correct.

Shared/reference-counted destruction may exist through a specialized explicit type, but it is not Sec's default ownership model.

ISR/platform restrictions on blocking, allocation and device lifetime remain additional requirements on any destruction path.

Ordinary Destruction Does Not Invent Hardware Side Effects

Ending the lifetime of a local register snapshot or ordinary value does not perform a new volatile read or write.

Destroying a volatile/MMIO accessor, typed register view or shadow-bearing accessor does not implicitly:

• read hardware;
• write hardware;
• reset a device;
• clear status;
• acknowledge an interrupt;
• commit a shadow;
• flush a shadow.

A volatile read yields an ordinary Sec value snapshot. Destroying that snapshot later does not repeat the hardware access.

Physical hardware storage is not an ordinary owned movable Sec value merely because its bits are addressable.

A runtime mapping owner may perform only the explicit release/unmap cleanup defined by its mapping contract. Destroying a borrowed register view does not release the mapping or perform hardware I/O.

Owning Interface Values Destroy Their Concrete Payload

An owning interface value must destroy its owned concrete value through resolved type metadata, generated dispatch or an equivalent statically validated mechanism.

A borrowed interface view does not destroy the concrete value merely because the view ends.

Interface destruction does not require a global garbage-collected object model.

Lowering must preserve whether the interface representation owns or borrows its concrete payload.

Generic Destruction Is Resolved from the Concrete Instantiation

type Box[T] struct {
    Value: T
}

Box[int] and Box[File] may have completely different destruction plans.

Generic lowering must not assume trivial destruction before the concrete type arguments and representation prove it.

Monomorphization may inline a concrete cleanup plan or generate a specialized destruction helper.

Missing destruction-aware lowering is an implementation gap; it never removes the language's cleanup obligation.

Recursive Ownership May Require Recursive Destruction

Recursive owning types must represent a finite runtime ownership graph.

Direct infinitely sized recursive values are rejected by the type/layout rules.

Indirect recursive ownership may naturally require recursive cleanup.

A target/profile may restrict destruction recursion for stack or realtime constraints.

The compiler may transform recursive destruction into iterative cleanup when observable ordering and resource-release semantics remain equivalent.

Compile-Time Evaluation Performs Ordinary Semantic Destruction

Transient values created during semantic compile-time evaluation follow ordinary deterministic destruction and defer whenever those paths are semantically reached.

Reclamation of the compiler evaluator's private storage is a separate compiler-internal concern.

If a CTE result is separately materialized as a static/runtime object, that object follows the ordinary runtime/static destruction rules of its type.

Computing a value at compile time does not make its eventual materialized runtime destruction disappear.

Semantic IR Must Preserve Destruction Explicitly

Ownership-sensitive destruction is resolved before lowering may erase source ownership structure.

Semantic IR may need operations or equivalent facts such as:

DestroyValue
DestroyPlace
DestroySubPlace
DestroyActiveVariant
ConditionalDestroy
InvokeFree
DeallocateOwnedStorage
RegisterCleanup
ExecuteCleanup
CleanupRegion
CancelCleanupAfterMove
CancelCleanupAfterDiscard
Replace
Reinitialize
TransferToReturn
TransferToArgument

Exact operation names are an implementation detail; the semantic distinctions are not.

Source provenance remains sufficient to explain cleanup origin, ownership transfer, partial state, custom free and deallocation authority.

Every non-trivial owned value represented in executable semantics must still have one valid terminal ownership action on every path where it exists.

Sec MLIR, LLVM and Optimization Preserve Resolved Cleanup Semantics

Sec MLIR/lowering preserves:

• exact-once destruction;
• cleanup order;
• partial availability;
• conditional destruction;
• construction-failure cleanup;
• defer ordering;
• return/error transfer;
• allocator pairing;
• custom free.

Lowering may realize those semantics using direct calls, inline cleanup, cleanup blocks, loops, generated helpers, conditional flags, SSA state or target-specific release calls.

A target policy forbidding dynamic ownership bookkeeping is enforced before lowering introduces hidden runtime ownership state.

By LLVM translation, cleanup placement is already ordinary explicit control flow and operations. LLVM does not decide whether a Sec value should be destroyed merely because an SSA value is unused.

Valid optimizations include, when proven safe:

• removing trivial destruction;
• inlining cleanup;
• merging equivalent cleanup blocks;
• eliminating cleanup for never-initialized or already-moved values;
• scalarizing aggregate cleanup;
• eliminating allocation/deallocation pairs;
• devirtualizing interface destruction.

Optimization must never:

• change observable destruction order;
• skip required resource release;
• double destroy;
• destroy moved/discarded values;
• access unavailable sub-Places;
• reorder forbidden volatile effects;
• suppress required foreign release;
• change explicit fallible close behavior;
• introduce forbidden hidden allocation or runtime state.

Copy/move elision must preserve the same final destruction owner as the source semantics.

Diagnostics

Destruction diagnostics should explain the ownership/lifecycle problem in ordinary language and identify the relevant terminal action.

Use after ownership transfer

`resource` is no longer available

ownership moved here:
    Consume(<-resource)

the former owner cannot use or destroy the transferred value

Partial move from a custom-free type

cannot move field `Handle` out of `Connection`

`Connection` defines custom `free`

the cleanup body requires the completed value to retain its full owned-field invariant

help: expose an explicit lifecycle operation instead
help: redesign ownership so the field can be transferred safely

Conditional cleanup not permitted by the target policy

conditional destruction requires runtime ownership state

`package.Payload` is owned on one incoming path and moved on another

the selected profile forbids dynamic ownership bookkeeping

help: converge ownership explicitly:
    discard package.Payload

Mismatched deallocation authority

cannot release this allocation through the selected allocator

allocation origin:
    ForeignPool

required release authority:
    ForeignPool.Release

selected release:
    DefaultArena

Double resource release

resource may be released twice

explicit release occurs here:
    CloseNative(self.Handle)

automatic owned-field destruction would release the same resource later

help: update lifecycle state after successful explicit close
help: represent the handle as non-owning if custom free owns the release responsibility

Failed construction cleanup

construction of `Resources` failed while initializing `Second`

cleanup:
    destroy initialized field `First`

`Second` is not treated as a completed value
`Third` was not initialized

When practical, diagnostics identify:

• the affected value or Place;
• where ownership was established;
• where it moved, was discarded or was replaced;
• where destruction would occur or be duplicated;
• the relevant custom free or field;
• any borrow/defer keeping the value alive;
• the required allocator/release authority;
• a safe source-level restructuring.

LSP and Tooling

The LSP consumes the compiler's destruction analysis rather than inferring cleanup independently.

Tooling may expose:

• destruction classification;
• current cleanup owner;
• custom free;
• partial/conditional cleanup state;
• ownership-transfer origin;
• pending deferred uses;
• field/element cleanup order;
• allocation/deallocation authority;
• why a cleanup path is conditional;
• the terminal ownership action selected for a value.

Automatic code actions that insert discard, move cleanup or restructure ownership are appropriate only when semantic preservation is proven.

A statically redundant second discard remains semantically valid and may produce at most the configured redundancy advisory.

Best Practices

• Prefer compiler-derived destruction and ordinary owned fields whenever they fully describe cleanup.
• Define custom free only for cleanup obligations that cannot be represented by field ownership.
• Do not call free manually; use explicit lifecycle methods for user-controlled close operations.
• Use a fallible Close()-style API when the caller needs to observe cleanup failure.
• Ensure successful explicit close updates lifecycle state so automatic destruction cannot release the same resource twice.
• Remember that move transfers cleanup responsibility to the new owner.
• Use canonical <- at consuming call sites and move bindings, not at return sites.
• Use discard when you intentionally end ownership early or need to converge conditional ownership state.
• Do not use discard merely because ordinary replacement already handles old-value destruction.
• Keep deferred uses in mind: they may postpone the earliest legal destruction point.
• Do not partially move fields from a custom-free type in Sec 0.1.
• Let fallible construction cleanup already-initialized fields automatically.
• Keep allocator/deallocator authority paired explicitly for owning allocations.
• Do not infer foreign ownership from RawPtr alone.
• Do not expect scope exit of hardware views to commit, clear or acknowledge hardware.
• Do not depend on process-exit cleanup unless the selected initialization/shutdown profile guarantees it.
• Remember that panic cleanup depends on panic policy; not every panic path guarantees destruction.
• Treat destruction and synchronization as separate correctness obligations.

Summary

• Destruction is the deterministic semantic end of an owned Sec value's lifetime.
• Cleanup, resource release, deallocation, free and destruction are related but distinct concepts.
• free is a lifecycle declaration, not an ordinary method.
• Source code never calls value.free().
• Every concrete type has a compiler-derived trivial or non-trivial destruction classification.
• Trivially destructible values need no observable cleanup action.
• Non-trivial values may require resource release, recursive field cleanup or backing deallocation.
• Destruction classification is independent from copy classification.
• @noCopy alone does not imply non-trivial destruction.
• Every still-owned non-trivial value must reach exactly one valid terminal ownership action on every reachable path where it exists.
• A former owner never destroys a value after ownership transfer.
• An unavailable Place is never destroyed again by the former owner.
• A value that never completed initialization is not destroyed as a completed value.
• Automatic destruction is source-language semantics, not backend liveness inference.
• Successful initialization registers destruction responsibility.
• Reinitialization registers a new destruction responsibility for the new value.
• Move, discard, return transfer and consuming transfer cancel the former owner's cleanup responsibility.
• Automatic destruction and defer use one source-ordered LIFO cleanup model.
• Sec does not have a separate “all defers first” or “all destructors first” phase.
• Values may still be destroyed at the earliest legal lifetime end.
• A deferred use may extend the required lifetime of a value.
• Overlapping locals destroy in reverse successful cleanup-registration order.
• Struct fields destroy in reverse declaration order by default.
• Fixed arrays destroy initialized still-owned elements in reverse index order.
• Owned temporaries are destroyed deterministically in reverse remaining creation order after their full expression.
• A temporary transferred into another owner is not also destroyed by the forwarding context.
• Moving a value ends the former owner's destruction responsibility at transfer commitment.
• Consuming calls transfer cleanup responsibility only when the consuming transfer actually commits.
• Fallible argument preparation cannot cancel cleanup before a call commits.
• Returning an owned value transfers cleanup responsibility to the result/caller owner.
• Canonical return syntax is return value; Sec does not use a return-site move marker.
• Moving a payload into an owning aggregate or variant transfers destruction responsibility to the container.
• Partially available aggregates destroy only still-owned available sub-Places.
• Moved/discarded fields are skipped during later parent destruction.
• Partial destruction is recursive where partial moves are permitted.
• A custom-free type does not permit partial field moves in Sec 0.1.
• Conditionally available values destroy only on runtime paths where ownership remains.
• The compiler resolves conditional cleanup statically whenever path facts suffice.
• Hosted implementations may use hidden SSA/drop state when correct conditional destruction genuinely requires it.
• Hidden ownership bookkeeping does not automatically alter source ABI layout.
• Profiles may forbid dynamic ownership bookkeeping and reject only programs that truly require it.
• is available refines ownership state rather than null/Option/reference validity.
• Discarding an available owned value performs its required destruction and leaves the Place unavailable.
• Discarding an already unavailable Place is a legal destruction no-op.
• Discarding a conditionally available Place destroys only paths still owning the value and converges all paths to unavailable.
• Destruction semantics do not make non-discardable values discardable.
• Assignment to an unavailable mutable Place is reinitialization and performs no old-value destruction.
• Assignment to an available mutable Place is replacement.
• Replacement validates the incoming operation before committing destruction of the old destination.
• Conditional replacement destroys the old value only on paths where it still exists.
• Successful init transfers field/resource cleanup into the completed instance.
• Failed construction cleans only successfully initialized fields/resources and temporaries.
• Completed-value custom free does not run for an outer value that never completed construction.
• Fallible initialization cleanup runs in reverse successful initialization/registration order.
• Most types should define no custom free.
• Custom free is intended for opaque cleanup obligations not already modeled by ordinary owned fields.
• At free entry, the complete value is under compiler-controlled destruction authority.
• Whole self cannot escape, be returned, resurrected or transferred from free.
• Owned fields cannot be moved out of self during free in Sec 0.1.
• Ordinary user-defined methods cannot consume whole self.
• Compiler-known lifecycle operations such as Arena.Release() remain narrowly defined exceptions.
• Owned fields remain compiler-managed and are destroyed after the custom free body.
• Custom free does not suppress ordinary owned-field destruction.
• defer is forbidden inside free.
• Locals/temporaries created inside free still receive ordinary destruction.
• free has no ordinary return value and cannot return Result.
• Recoverable close failures should use an explicit fallible lifecycle method where appropriate.
• A successful explicit close must update lifecycle state to prevent double release during later destruction.
• free is not implicitly unsafe.
• free must not silently turn recoverable cleanup failure into panic.
• Result destroys only its active retained payload.
• Option destroys only an active retained Some payload.
• Tagged unions destroy only their active initialized still-owned payload.
• Consuming .Ok()/.Err() transfer the retained payload and prevent duplicate later destruction.
• The compiler does not guess active ownership inside untagged foreign unions.
• Structs without custom free derive cleanup recursively from fields.
• Owning dynamic collections destroy initialized elements then release backing through the recorded authority.
• Uninitialized spare capacity is not destroyed as live elements.
• Borrowed slices/views do not destroy backing storage or elements.
• Owning shaped values release owned elements/resources and backing according to their representation.
• String destruction follows the concrete canonical string representation.
• Reference-holder destruction never destroys the referent.
• Owned referent destruction is forbidden while incompatible live borrows still require it.
• Return establishes the result before cleaning non-transferred locals.
• return try establishes/transfers the success or failure payload before local cleanup.
• Unmatched error propagation cleans still-owned locals on the propagating path.
• break cleans only regions actually exited.
• continue cleans iteration-local values that end while preserving loop-carried values still required.
• match/switch branches maintain independent destruction state before ownership-state merge.
• Loop destruction analysis is iteration- and path-sensitive.
• Per-iteration values destroy once per reached iteration unless transferred.
• Zero-iteration paths never destroy iteration locals that were never created.
• Destruction and deallocation are distinct semantic actions.
• Owning allocations preserve the matching release/deallocation authority.
• Incompatible allocator/deallocator pairing is invalid.
• RawPtr[T] alone never creates deallocation responsibility.
• Foreign ownership transfer removes Sec destruction responsibility only when the foreign contract says transfer committed.
• An owning Sec foreign wrapper may use custom free for the matching release operation.
• Static/global destruction requires a deterministic target/program shutdown plan.
• Hosted targets do not automatically imply process-exit destruction for all globals.
• Runtime-free targets do not gain a hidden global destruction registry.
• Normal main return follows the canonical program shutdown cleanup plan.
• Raw forced termination and abnormal system/hardware termination do not guarantee pending cleanup.
• Panic cleanup follows the selected panic-domain/profile policy.
• Destruction never silently introduces a general exception-unwinding runtime.
• Destruction itself does not imply synchronization.
• Ownership transferred to another task/thread/execution owner transfers destruction responsibility.
• Shared/ref-counted cleanup is not Sec's default ownership model.
• Scope exit of hardware views does not invent volatile reads/writes, resets, clears, acknowledgements, commits or shadow flushes.
• Destroying a local volatile snapshot does not repeat the hardware read.
• A borrowed hardware/register view does not release its mapping merely because the view ends.
• Owning interface values destroy owned concrete payloads through resolved type-aware mechanisms.
• Borrowed interface views do not destroy concrete payloads.
• Generic destruction is resolved from concrete instantiated type arguments and representation.
• Different instantiations of one generic may have different destruction plans.
• Recursive owning structures may require recursive destruction.
• The compiler may lower recursive destruction iteratively when observable semantics are preserved.
• CTE-local values perform ordinary semantic destruction/defer when those paths are reached.
• Evaluator memory reclamation is not the same as Sec value destruction.
• Materialized runtime/static CTE results follow ordinary program destruction rules.
• Semantic IR preserves destruction, cleanup, transfer, replacement, reinitialization and deallocation facts explicitly.
• No unresolved destruction semantics may reach LLVM.
• Sec MLIR preserves exact-once cleanup, conditional/partial destruction, construction failure, defer order and allocator pairing.
• LLVM receives already-resolved cleanup control flow and does not infer Sec destruction from unused SSA.
• Optimization may remove or combine cleanup only when observable semantics remain unchanged.
• Optimization never skips required release, double-destroys, destroys moved values or changes observable cleanup order.
• Copy/move elision preserves the same terminal destruction owner.
• Destruction diagnostics identify ownership origin, terminal action, duplicate cleanup, custom free, borrow/defer dependency and release authority where relevant.
• LSP consumes compiler destruction state rather than maintaining an independent cleanup model.