Ownership and Memory Safety

<!-- verified-against: seed-llvm; examples: docs-examples-test -->

seed uses ownership, move-only resources, lexical loans/provenance, structural capabilities, deterministic cleanup, linear t, and regions. It has no GC, borrow-checker lifetime syntax, or exception unwinding. The authoritative semantic rules are in seed/compiler/llvm/SEMANTIC_RULES.md; current limits are tracked in Current Status.

Copy, move, borrow, clone

Scalars and aggregates containing only copy fields copy. string, bytes, shared_bytes, user-destructor owners, resource aggregates, and linear t obey their move/clone/cleanup capabilities.

shared_bytes is not bitwise-copyable: .clone() explicitly retains another handle without copying the payload. Cloning owned string/bytes or aggregates containing them may allocate. Clone allocation effects and capabilities survive source-elided .sdi compilation.

Places and partial ownership

The compiler tracks locals, fields and nested fields, known fixed-array indexes, active ADT payloads, raw-union fields, tuple/array/nominal aggregates, generic instances, option/result, function values, channels/tasks, aliases, blocks, calls, returns, and control-flow joins.

A partial move makes the moved place unavailable and prevents whole-owner use when completeness is required. Independent remaining fields stay usable when a user destructor does not require a complete owner. Dynamic-index moves of resource elements remain rejected because the cleanup set would be runtime dependent.

Cleanup

Cleanup is planned from typed HIR ownership facts, verified separately, and lowered onto normal structured exits. Live owners clean exactly once in reverse successful initialization order. Reassignment cleans the previous live owner before storing the replacement. Loops use dataflow fixed points across entry, back edges, break, continue, and return.

Panic, trap, and abort terminate without unwinding. They do not run lexical cleanup or user destructors.

Destructors

fn TypeName.drop() receives implicit consuming self. It must be unique and return void. Calling value.drop() manually consumes the owner, preventing a second automatic call. Returned owners transfer their cleanup obligation to the caller. Cleanup/resource globals are rejected because global teardown is not an implicit language service.

ADT cleanup dispatches only over the active variant. Raw unions require unsafe active-field discipline; safe tagged alternatives should use ADTs or an audited wrapper.

Closure ownership

A plain |...| closure owns compiler-generated stack capture storage. Capture initialization follows first lexical-use order: copy-capable values copy and other owned values move. Captures are immutable; a moved resource capture makes the closure itself move-only. The owner drops live captures exactly once in reverse initialization order.

Plain closures are reusable and non-escaping. They cannot capture values that cannot remain safely stored after a call, including views, mutable captures, region-bound values, raw/reference values, format_args, or already-moved places. They cannot be returned, retained in an outer scope, sent to a task, or passed through a platform function-pointer boundary.

box |...| allocates capture storage explicitly and returns Result<box fn(...) -> T, alloc_error>. The boxed owner can be returned or stored but remains move-only, non-cloneable, and non-sendable. Allocation failure drops transferred captures once; successful drop runs the capture drop thunk and frees the environment once. A boxed closure allocated under region(...) cannot escape that region.

Linear values

linear t preserves t's representation and adds an exactly-once obligation. It removes copy/clone/shared capability while retaining valid move, borrow, send, sync, and cleanup facts. The implementation propagates the obligation through aliases, blocks, aggregates, option/result, ADTs, generics, channels, function values and indirect calls, task capture, parameters/returns, and schema-17 .sdi.

Leaving a linear value live at scope exit, consuming it twice, cloning it, discarding it, overwriting it, or storing it into pre-existing non-linear storage is rejected.

Text, buffers, and views

• literal text is static borrowed str;
• string is owned valid UTF-8 and moves;
• bytes is a unique mutable binary owner and moves;
• shared_bytes is a shared read-only handle with explicit clone;
• owned string automatically borrows as str when expected;
• owner-derived str, []t, and mut []t views carry provenance;
• a live view prevents conflicting move, overwrite, free, reallocation, or mutation of its backing owner; a write is checked against foreign loans only, so writing through the live exclusive view that owns the place (or through a partition sibling of the same partition group) is that view's own authority, while any other overlapping active loan makes the write illegal even when the written element is Copy;
• mut []t.split_at_mut(index) checks index <= len, allocates nothing, and returns two exclusive lexical views; match bindings may use mut name;
• the backing owner cannot be read, moved, resized, or freed while the partition tuple is live; nested partitions remain confined to their parent;
• returning or storing a view is allowed only when its static/input/receiver provenance proves sufficient lifetime;
• conditional selection carries the finite union of all possible origins; the implementation bounds this set at eight origins and turns overflow or unsupported indirect provenance into unknown, never into a lifetime proof;
• direct .sdi call summaries preserve these symbolic origins across modules; HIR cache schema 9 stores the same target-independent records, while every safety family reruns after cache reuse;
• local/temporary-derived views cannot escape through returns, globals, containers, tasks, or dynamic-library ABI.

There is no lifetime syntax. @borrow receiver methods create shared lexical loans; returned views remain tied to the receiver through .sdi summaries. Free functions may also return static or input-derived str/slice views; an owner-derived view from a local string/bytes remains a V001 escape. @mut receiver methods create an exclusive call-scoped loan and mutate the caller's place directly. Immutable receivers and overlapping live views are rejected; no move or clone is hidden by the call.

Regions

fn work() -> Result<i64, alloc_error> {
    region(4096) {
        // allocating operations use the active checked bump allocator
        Ok(42)
    }
}

Capacity is evaluated once, aligned allocation is overflow checked, and exhaustion is returned as alloc_error by fallible APIs. Nested regions are LIFO. Body resources clean before the backing storage is released. Safe owners, views, and pointers tied to a region cannot escape through result, return, or assignment to an outer binding.

Spawned work captures allocator context. Region-bound tasks remain structured and join before region cleanup.

Task transfer

spawn records copy/move capture mode. Keeping the original and a task value requires an explicit clone. Crossing a task boundary requires send; shared access also requires sync. Mutable global state cannot be captured. Each task group drains before its lexical owner cleans resources.

if let and while let are surface forms over match: both desugar to a two-arm match whose second arm is the complement, so binding, ownership transfer, exhaustiveness, and cleanup are exactly the match rules. if let Some(x) = e names its complement None; another variant pattern keeps a wildcard arm, which is rejected when the scrutinee carries a move-only payload because a wildcard arm does not complete that payload's ownership obligation — write the explicit match arms there. An irrefutable pattern makes the complement arm unreachable and is rejected. A repeat array literal [value; count] expands to count elements of one literal value and takes its element type from the expected array type, so let slots: [4]usize = [0; 4] needs no cast; the value must be a literal, a cast of a literal, or an array of those, and the count is a positive integer literal of at most 65536.

Unsafe boundary

Raw allocation, pointer access, FFI, syscalls, atomics, volatile access, address-space casts, raw union access, and raw assembly require unsafe. Unsafe code does not disable ownership for surrounding safe values; it assumes specific obligations that should be hidden behind narrow audited safe wrappers.

unsafe struct parameters: an unsafe struct with a raw pointer field and @repr("null_niche") is a resource type that cannot be passed by value as a function parameter. Passing it by value moves the underlying owner, making it unavailable for subsequent use. Methods with @mut receiver require a mutable place and cannot be called on a moved value. To use such a type across function boundaries, inline the logic or return the owner alongside the result.

What release changes

--release and --release-small optimize the same safe semantics. Bounds, discriminant, provenance, ownership, and cleanup checks remain unless proven redundant. No unchecked release profile is implemented.

Ownership cookbook

These are the twenty recurring construction patterns used by the Grove and compiler fixtures. The important part of each pattern is the invariant it preserves; when a value cannot satisfy that invariant, keep the operation in a narrow unsafe adapter instead of weakening the owner model.

For a worked diagnostic example, start with the consuming span in S001, then apply the smallest pattern above that restores a single owner. The compiler must continue to reject dynamic moves, region escapes, unsafe callbacks, and missing cleanup even when a different construction would be shorter.

Worked S001 example (move across a call and a branch)

A new user moves title into report at the struct construction and then consumes the moved binding inside a later branch:

struct Report {
    title: string
}

fn main() -> Result<i64, alloc_error> {
    let title = "quarterly".to_string()?
    let report = Report { title: title }
    if len(report.title) == 9 as usize {
        let again = title
        Ok(0)
    } else {
        Ok(1)
    }
}

The compiler resolves this from the diagnostic alone: error[S001] names the ownership path (title), a note: ownership path declared here points at the binding, a note: move occurred here points at the consuming struct construction, and the help: line states the repair direction (clone 'title' explicitly before moving). The smallest fix clones the title into the report and moves the original to its final owner before the branch, so every branch exits with the same resource availability:

struct Report {
    title: string
}

fn main() -> Result<i64, alloc_error> {
    let title = "quarterly".to_string()?
    let report = Report { title: title.clone() }
    let again = title
    if len(report.title) == 9 as usize {
        let total = len(again) + len(report.title)
        Ok(if total == 18 as usize { 0 } else { 1 })
    } else {
        let rest = len(again)
        Ok(if rest == 9 as usize { 2 } else { 3 })
    }
}

Every pattern above (and both halves of this worked example) is an executable corpus program verified by make -C seed/compiler/llvm gate47-cookbook-test; the corpus lives in seed/compiler/llvm/tests/cookbook/.