Arenas

Core Model

Every Arena allocation belongs to:

• one ArenaDomain;
• the Arena's current validity epoch;
• one concrete bounded allocation extent;
• one storage/memory-space contract;
• one allocation site.

Ordinary allocation advances Arena allocation state but does not change the validity epoch.

Reset() ends the current epoch, reuses the domain and backing, and starts a new epoch.

Release() ends the ArenaDomain completely.

Arena is bulk-reclamation storage management. Sec 0.1 does not provide per-allocation Arena deallocation.

Arena Is a Semantic Builtin

Arena is a compiler-known semantic builtin type. Its existence does not require an ordinary imported source declaration.

The compiler owns the semantics of:

Arena.FromBuffer(...)
Arena.WithCapacity(...)
Arena.Growable(...)
arena.New[T]()
arena.Alloc[T](count)
arena.Reset()
arena.Release()

Core or target libraries may provide helper implementations, but helpers do not redefine the language contract.

Arena operations are compiler-known because they affect ownership, domain identity, epochs, ordered effects, task/thread dependencies and lowering.

Lowercase arena Is an Ordinary Identifier

Sec 0.1 does not reserve lowercase arena as a keyword.

let mut arena := try Arena.WithCapacity(4096)

The language defines no special:

arena {
    ...
}

scoped-arena syntax in Sec 0.1.

ArenaDomain

ArenaDomain is the compiler-visible identity of one Arena allocation domain.

It is:

• stable across Arena ownership moves;
• stable across ordinary allocations;
• stable across Reset();
• terminated by Release() or destruction.

Domain identity is independent of the physical address of the backing storage.

If a later Arena happens to reuse the same physical bytes, it receives a distinct ArenaDomain identity. Old references or handles never become valid again merely because an address is reused.

ArenaDomain is compiler semantics, not source-level region syntax.

Arena State Version and Validity Epoch Are Different

A mutating Arena operation produces a new compiler-visible Arena state version.

The validity epoch answers a different question: which incarnation of Arena allocations is currently valid?

This distinction lets the compiler model repeated allocation without falsely treating every allocation as invalidating previous references.

Arena Ownership Is Move-Only

An Arena cannot be copied.

let second := first    // invalid when first: Arena

Ownership may be moved:

let second :<- first

After the move:

• second owns the same ArenaDomain;
• the same validity epoch remains current;
• the same backing remains controlled;
• the allocation state continues;
• first is unavailable.

Moving the Arena owner does not invalidate references into its allocations.

A move may be purely semantic and need no physical runtime relocation.

Types Containing an Arena Become Move-Only by Composition

type WorkerStorage struct {
    arena: Arena
}

Moving WorkerStorage transfers Arena ownership with the containing value.

Destruction of the containing value destroys the Arena field when it is still owned.

Arena Domain Ownership Is Not Always Backing Ownership

Every Arena owns and controls its ArenaDomain. It does not necessarily own the physical backing bytes.

Arena backing relationships include conceptually:

Owned
Borrowed
Static
TargetProvided

These categories describe how backing is acquired and released. They do not replace the general storage-origin model.

A growable Arena may control several stable backing segments while still representing one ArenaDomain.

Arena.FromBuffer

A borrowed fixed Arena is created from mutable contiguous storage:

let mut arena := Arena.FromBuffer(ref mut buffer)

Conceptual compiler-known shape:

fn FromBuffer(
    buffer: ref mut byte[],
) Arena

FromBuffer:

• creates a fresh ArenaDomain;
• uses the supplied mutable storage as fixed backing;
• does not allocate new backing;
• is infallible when the safe input view already satisfies required static conditions;
• takes exclusive allocation authority over that backing for the Arena lifetime;
• does not destroy or deallocate the backing owner when the Arena ends.

The supplied storage must remain:

• mutable;
• contiguous;
• addressable;
• live for the complete Arena lifetime;
• representably bounded;
• compatible with the required address space;
• capable of satisfying requested alignment.

Direct conflicting use of the borrowed backing is invalid while the Arena controls it.

A Zero-Capacity Borrowed Arena Is Valid

A zero-length mutable backing view may create a valid Arena.

Such an Arena:

• is live;
• has zero byte capacity;
• may satisfy zero-element allocations;
• cannot satisfy positive-storage allocations;
• may be reset;
• may be released.

Zero capacity is not by itself a semantic error.

Arena.WithCapacity

An owned fixed Arena requests backing from the active target/profile provider:

let mut arena := try Arena.WithCapacity(4096)

Conceptual compiler-known shape:

fn WithCapacity(
    capacity: uint,
) Result[Arena, AllocationError]

The resulting Arena has fixed capacity and does not grow.

Creation may fail and is available only when the active CompilationPlan provides a compatible backing provider.

Provider effects and trust provenance remain visible to analysis.

Release/destruction returns owned backing through the matching provider contract.

Arena.Growable

Where supported by the active profile, Sec 0.1 may expose a growable Arena:

let mut arena := try Arena.Growable(4096)

Conceptual shape:

fn Growable(
    initialCapacity: uint,
) Result[Arena, AllocationError]

A growable Arena remains one ArenaDomain while acquiring additional stable backing.

Growth policy may include an initial capacity, segment strategy, maximum capacity, provider, alignment restrictions and memory-space restrictions.

Not every target/profile is required to expose growable Arenas.

Growth Must Never Relocate Existing Live Allocations

Permitted strategies include:

• additional stable segments;
• reserved virtual address space;
• target-provided non-relocating extension;
• another plan-defined stable strategy.

This strategy is forbidden while prior allocations remain live:

allocate a larger buffer
copy existing Arena objects
change their addresses
continue using old references

Growth preserves:

• ArenaDomain identity;
• current validity epoch;
• existing allocation addresses;
• existing bounds;
• safe-reference validity;
• ownership and dependency facts.

Growth is not Reset.

Capacity Is Measured in Bytes

Arena capacity is a backing-storage quantity measured in bytes.

Compiler-visible quantitative facts may include:

• reserved capacity;
• used capacity;
• current-segment capacity;
• total acquired growable capacity;
• maximum capacity;
• alignment padding;
• peak logical demand.

Sec 0.1 does not require every one of these facts to be exposed as a public Arena property.

For typed allocation, the element count is converted to byte demand using the target-resolved layout of T.

Every Allocation Obeys the Alignment of T

For:

let values := try arena.Alloc[int32](100)

the conceptual calculation is:

alignedOffset = AlignUp(currentOffset, AlignOf(int32))
payloadSize   = CheckedMultiply(100, int32.SizeOf)
endOffset     = CheckedAdd(alignedOffset, payloadSize)

Alignment padding consumes Arena capacity.

The implementation must not assume that:

• T.SizeOf == AlignOf(T);
• all alignments are powers of two;
• the current cursor is already aligned;
• every backing base can satisfy every possible type alignment.

Dynamic inability to satisfy required alignment produces AllocationError. A statically impossible alignment is a compile-time error.

Typed Safe Allocation API

The canonical safe operations are:

let value := try arena.New[Value]()
let values := try arena.Alloc[Value](count)

Conceptual compiler-known signatures:

fn New[T]() Result[ref mut T, AllocationError]

fn Alloc[T](
    count: uint,
) Result[ref mut T[], AllocationError]

These are Arena instance operations.

They temporarily require mutable authority over Arena control state. That mutable borrow ends when the allocation operation returns.

The returned reference or slice retains a dependency on the ArenaDomain and current epoch, but does not retain an exclusive mutable borrow of the entire Arena controller.

Repeated allocation is therefore valid while capacity and other constraints allow it.

arena.New[T]()

New[T] allocates storage for exactly one T.

It:

• validates T, layout and alignment;
• checks fixed capacity or performs permitted non-relocating growth;
• fully initializes one T;
• returns ref mut T;
• never exposes an uninitialized T;
• returns AllocationError on allocation failure.

The successful reference is:

• non-null;
• bounded to exactly one T;
• associated with the current ArenaDomain;
• associated with the current validity epoch;
• mutable;
• non-owning with respect to backing storage;
• not individually deallocatable.

arena.Alloc[T](count)

Alloc[T](count) allocates exactly count values of T.

count is an element count, not a byte count.

The operation:

• checks count arithmetic;
• checks layout and alignment;
• checks capacity or performs valid non-relocating growth;
• fully initializes every element;
• returns ref mut T[];
• never returns a shorter slice;
• never exposes partial initialization;
• returns AllocationError on failure.

The returned slice has exactly the requested number of elements and bounds matching the complete allocation.

Safe New[T] and Alloc[T] Have Type Requirements

Sec 0.1 requires:

• complete layout under the active CompilationPlan;
• a sized T;
• known supported alignment;
• a valid compiler-defined default;
• safe initialization;
• trivial destruction classification.

The parameterless safe forms do not allocate a type that lacks an infallible valid default.

They also do not directly allocate non-trivially-destructible T in Sec 0.1.

A future explicit initializer or placement-construction API would require separate language semantics.

Safe Arena Allocation Exposes Only Fully Initialized Values

Full initialization means:

• every result value satisfies its canonical default semantics;
• every readable field or element is valid;
• required type invariants are established.

It does not necessarily mean:

• every physical byte is zero;
• padding has defined contents;
• the implementation used memset;
• the all-zero bit pattern is a valid representation.

The compiler may initialize using field stores, loops, vectorized stores, target intrinsics, valid bulk zeroing or proof-driven store elimination.

Direct Safe Arena Allocation Requires Trivial Destruction in Sec 0.1

New[T] and Alloc[T] require T to be trivially destructible.

This restriction exists because Arena is a bulk-reclamation mechanism, not an implicit per-allocation destructor registry.

Arena does not automatically record:

• destructor callables;
• per-allocation type metadata;
• element counts for destruction;
• initialization masks;
• destruction ordering records.

A type directly owning files, locks, sockets, owning collections, custom-free resources or another non-trivial lifecycle is therefore rejected by these direct safe allocation forms unless its canonical destruction classification is trivial.

This does not forbid an owning container from using Arena-backed raw/element storage when that container itself tracks logical elements and performs their required destruction.

Zero-Element Allocation Is Valid

let values := try arena.Alloc[int](0)

The operation:

• succeeds;
• returns a valid empty mutable slice;
• consumes no capacity;
• requires no Arena growth;
• creates no dereferenceable element;
• does not advance the validity epoch.

A literal zero count is not inherently suspicious.

Zero-Sized Types Preserve Semantic Count

When the layout rules permit a concrete zero-sized T, Alloc[T](count) may consume no payload bytes.

The result still retains its semantic element count and bounds.

A positive element count does not by itself imply distinct dereferenceable byte locations when the element type has zero size.

Allocation Failure Uses AllocationError

Arena creation and typed allocation report ordinary allocation failure through AllocationError.

let values := try arena.Alloc[Packet](count)

Failure must not silently:

• return null;
• return an invalid safe reference;
• return a shorter slice;
• expose partial initialization;
• fall back to an unrelated allocator;
• select another Arena;
• panic merely because capacity is exhausted;
• terminate the process merely because capacity is exhausted.

Callers handle or propagate failure using normal Result and try semantics.

The public source signature retains Result even when compiler proof eliminates the runtime failure path.

Arena Allocation Is Atomic from Program Semantics

Conceptually, the operation:

1. validates Arena state;
2. validates T;
3. computes checked payload size;
4. computes alignment padding;
5. ensures the complete capacity/growth requirement;
6. reserves the complete range;
7. fully initializes every result value;
8. publishes the resulting reference or slice.

If failure happens before publication:

• the Arena remains live;
• the ArenaDomain is unchanged;
• the validity epoch is unchanged;
• the allocation cursor is unchanged;
• prior allocations remain valid;
• no partial result is published;
• no partial requested capacity remains consumed.

Growable Arena segment acquisition is similarly atomic: a new segment joins the Arena only after complete successful acquisition.

Repeated Allocation Does Not Invalidate Earlier Allocations

let first := try arena.Alloc[byte](100)
let second := try arena.Alloc[byte](200)

Both allocations remain valid in the current epoch.

Positive-sized allocation ranges do not overlap. The compiler may use that fact in alias analysis.

Zero-sized and zero-element cases do not imply distinct dereferenceable byte ranges.

Sec 0.1 Has No Individual Arena.Free

Ending a reference lifetime does not reclaim Arena bytes.

Storage consumed by a successful allocation remains consumed in the current epoch until Reset(), Release() or a future explicitly defined bulk-reclamation operation.

arena.Free(value)    // no such Sec 0.1 operation

arena.Reset()

arena.Reset()

Conceptual shape:

fn Reset() void

Reset():

• keeps the Arena owner live;
• keeps the same ArenaDomain;
• ends the current validity epoch;
• invalidates prior allocations;
• resets allocation cursors;
• retains reusable backing;
• starts a new validity epoch;
• allows later allocation.

Reset is an ordinary mutable Arena operation. It does not consume whole Arena ownership.

Reset is not Release.

No Validity-Preserving Dependency May Cross Reset()

Dependencies that can block Reset include:

• ordinary shared or mutable references;
• slices and views;
• nested Arenas;
• containers using Arena backing;
• closure captures;
• task captures;
• thread arguments;
• deferred operations;
• foreign-retained dependencies;
• strong validity-preserving handles;
• returned/result values still depending on Arena storage.

Valid after final use:

let values := try arena.Alloc[int](100)
Process(values)

arena.Reset()

Invalid:

let values := try arena.Alloc[int](100)
arena.Reset()
Process(values)

Final-use / non-lexical lifetime analysis decides whether the dependency still crosses the Reset point. Mere lexical scope does not keep a dead reference dependency alive.

Reset Advances the Validity Epoch

Ordinary references from the old epoch must be dead before Reset.

Explicit stale-capable weak handles may survive when their own contract permits fallible resolution after Reset.

A stale handle does not block Reset merely because the handle value remains live.

Epoch rekeying must never let stale references or handles become valid again through wraparound or physical-address reuse.

Runtime epoch metadata may be eliminated when static proof makes it unnecessary.

Reset Retains Arena Capacity

For a fixed Arena, Reset:

• sets used capacity/cursor back to zero;
• retains total capacity;
• retains backing;
• retains ArenaDomain identity;
• advances the validity epoch.

A borrowed Arena retains its exclusive control of the borrowed backing. Reset does not return the buffer to its owner.

A growable Arena retains already acquired stable segments and resets their allocation cursors.

Reset does not automatically trim growable backing.

Reset Does Not Require Zeroing the Backing

After Reset, old typed object lifetimes have ended. Later safe typed allocations must fully initialize new values before exposing them.

A compiler or profile may clear memory for security, debug or performance policy, but complete zeroing is not the base semantic meaning of Reset.

Reset itself is atomic from Sec program semantics; code cannot observe a mixed old/new allocation state.

arena.Release()

arena.Release()

Release() is a compiler-known terminal lifecycle operation.

It:

• consumes Arena ownership;
• terminates the ArenaDomain;
• invalidates validity-preserving dependencies;
• returns owned backing to its provider where required;
• ends borrowed-backing control;
• permits no later use of the Arena value.

After Release, the source Arena Place is unavailable.

Release() returns void and is non-fallible in the base Arena contract.

No validity-preserving reference or dependency may cross Release.

Release Behavior Depends on the Backing Relationship

The ArenaDomain ends even when physical bytes remain present.

Explicit Release() Is Usually Optional

The programmer does not need to call Release() on every normal path.

Destruction of a still-owned Arena performs terminal Release semantics.

This can occur through:

• normal scope exit;
• early return;
• error-propagation cleanup;
• field destruction;
• task/thread cleanup;
• another canonical ownership boundary.

If explicit Release already consumed the Arena, implicit cleanup does not release it again.

Double Release is invalid.

Arena Reclamation Does Not Replace Logical Value Destruction

Arena controls storage. Logical values may have separate ownership and lifecycle responsibilities.

Destroying a value does not necessarily reclaim its Arena bytes.

Reset or Release also cannot silently skip required non-trivial logical destruction.

This is the reason direct safe New/Alloc are restricted to trivially destructible types in Sec 0.1.

Specialized owning containers may use Arena-backed storage when they themselves track and destroy logical elements before the Arena dependency ends.

Returning a Reference into a Local Arena Is Invalid

fn Invalid() Result[ref int, AllocationError] {
    let mut arena := try Arena.WithCapacity(1024)
    let value := try arena.New[int]()

    return Ok(value)    // invalid
}

The local Arena is destroyed when the function exits, so the returned reference would outlive its ArenaDomain.

Sec does not repair this through hidden Arena or heap promotion.

An Arena-backed reference may escape only when its ArenaDomain already outlives the returned value through an external owner or allocation context.

Returning Arena Ownership Is Valid

fn CreateArena() Result[Arena, AllocationError] {
    let arena := try Arena.WithCapacity(4096)
    return Ok(arena)
}

The return boundary transfers ownership of the Arena value.

The same ArenaDomain and current validity epoch continue.

Returning the Arena owner does not by itself invalidate Arena-backed storage.

Self-Referential Arena Owner/Reference Aggregates Are Not Automatic

Sec 0.1 does not automatically validate shapes such as:

type ArenaResult struct {
    arena: Arena
    value: ref int
}

where value points into storage controlled by the Arena stored in the same ordinary movable aggregate.

Such a design requires explicit self-reference, relocation and ownership semantics not introduced by the base Arena model.

Field order is not proof that a self-reference remains valid after moves.

Nested Arenas Need No Special Syntax

let childBuffer := try parent.Alloc[byte](4096)
let mut child := Arena.FromBuffer(childBuffer)

The child Arena has:

• its own ArenaDomain;
• its own validity epoch;
• borrowed backing from one parent allocation;
• a dependency on the parent ArenaDomain and parent epoch.

The parent cannot Reset or Release while the child remains live.

Releasing the child ends the child domain and its borrow of the backing. It does not individually reclaim the parent allocation.

A later parent Reset may reclaim that parent allocation once the child dependency has ended.

Arena Cleanup Participates in Normal defer Ordering

let mut arena := try Arena.WithCapacity(4096)

defer {
    arena.Release()
}

let values := try arena.Alloc[int](100)

defer {
    FinalUse(values)
}

LIFO cleanup runs FinalUse(values) before arena.Release().

A cleanup plan that releases an Arena before a required dependent cleanup use is invalid.

Explicit Release is often unnecessary because normal Arena destruction already performs terminal Release semantics, but an explicit defer may be useful when the intended cleanup order should be written directly.

Panic cleanup occurs only where the panic/destruction policy guarantees cleanup.

Tasks Preserve Arena Dependencies

Capturing an Arena-backed reference into a task keeps a dependency on:

• ArenaDomain;
• validity epoch;
• allocation bounds;
• capture and borrow authority.

The parent cannot Reset or Release the Arena while the task may still access that storage.

A canonical completion boundary such as await, join or structured-scope completion may discharge the task's execution-local dependency.

Merely observing that a task “probably finished” is not sufficient.

For example:

let task := try spawn Process(values)
discard await task

arena.Reset()

Reset is valid only if no Arena dependency survives through the task result or elsewhere.

Task completion ends execution-local captures, but a result carrying an Arena-backed reference continues to carry that dependency.

Threads Follow the Same Lifetime Rule Plus Physical-Thread Constraints

Borrowing Arena-backed storage into another physical thread additionally requires proof of:

• storage lifetime beyond thread execution;
• valid access authority;
• exclusive mutation where needed;
• no conflicting Arena mutation;
• no Reset or Release during use;
• transferability;
• required memory synchronization;
• address-space compatibility;
• target thread support.

A canonical join/completion boundary may end execution-local dependencies when no result or other dependency remains.

An Arena may itself be moved into a task or thread when the relevant transfer rules, backing provider and target profile permit it:

let task := try spawn Worker(<-arena)

After committed transfer, the parent no longer owns the Arena. The ArenaDomain itself remains the same.

Ordinary Arena Does Not Support Concurrent Mutation

Without a distinct synchronization abstraction, Sec 0.1 forbids:

• concurrent New/Alloc;
• concurrent Reset;
• concurrent Release;
• allocation concurrent with Reset or Release;
• Reset/Release concurrent with access requiring the old epoch;
• conflicting parent/child Arena mutation through shared backing.

Ownership, borrowing and concurrency analysis reject these cases.

A future synchronized or concurrent Arena would be a distinct explicit abstraction, not a silent extension of ordinary Arena.

Arena and Allocation Context Are Related but Distinct

Every callable invocation has zero or one active allocation context according to the general allocation model.

The allocation context is compiler-visible semantic state. It is not:

• a source global;
• an automatically visible Arena variable;
• a universal thread-local allocator;
• an implicit heap;
• a mandatory runtime object.

Arena is a primary concrete realization of an allocation domain, but an explicit Arena value and the ambient allocation context are not the same concept.

MayAllocate and RequiresAllocationContext Are Different Facts

MayAllocate means reachable execution may perform allocation.

RequiresAllocationContext means a callable reaches implicit allocation that needs an ambient allocation context.

fn Fill(
    arena: ref mut Arena,
) Result[ref mut byte[], AllocationError] {
    return arena.Alloc[byte](1024)
}

Fill may allocate through its explicit Arena parameter without requiring an ambient allocation context.

A string or collection operation that allocates without an explicit Arena may instead require the ambient context.

The Compiler Does Not Guess an Ambient Arena from Lexical Scope

let temporaryArena := ...
let outputArena := ...

let result := try Build()

The compiler does not silently choose either visible Arena for Build().

Likewise, passing an Arena as an ordinary explicit argument does not automatically rebind the ambient allocation context.

Allocation-context selection conceptually recognizes:

• an explicit Arena selected by the operation;
• a propagated ambient allocation context;
• a compiler-managed local Arena with proven backing and non-escape;
• a target-provided context;
• no valid context, which is a compile-time error.

Context selection happens before physical lowering.

Spawned Execution Gets a New Allocation Context

A spawned task or thread does not automatically inherit the parent's mutable Arena context.

Its allocation capability comes from:

• a task/thread-specific profile or target context;
• an explicitly transferred Arena;
• an explicit execution contract;
• or no allocation capability.

A process receives a separate address-space allocation context.

An ISR has no ordinary allocation context unless the target/interrupt rules explicitly provide and permit one.

Foreign code likewise does not automatically provide a Sec allocation context.

An exported Sec function that requires one needs an explicit Sec-aware ABI, wrapper or target-provided context; the compiler must not silently add a hidden Arena parameter to an ordinary foreign ABI.

Arena Operations Are Ordered Semantic Effects

Conceptually:

ArenaCreate(A, policy)
ArenaAllocate(A, size)
ArenaReset(A)
ArenaRelease(A)

These events are associated with ArenaDomain identity and their order matters.

This sequence is valid:

ArenaCreate(A)
ArenaAllocate(A)
ArenaReset(A)
ArenaAllocate(A)
ArenaRelease(A)

This is invalid:

ArenaRelease(A)
ArenaAllocate(A, size)

Branches, loops, defer, destruction, tasks, threads, implicit allocation-context operations and provider calls all participate in ordered-effect analysis.

Arena allocation is not a pure operation. CSE must not merge two distinct allocations merely because their arguments are equal.

@noAlloc and Arena

Arena typed allocation is allocation for Sec effect semantics.

Therefore current Sec 0.1 semantics treat reachable:

arena.New[T]()
arena.Alloc[T](count)

as incompatible with @noAlloc.

This remains true even when the Arena backing was already reserved.

Arena.FromBuffer itself creates an Arena domain over existing backing and does not add backing allocation.

Sec 0.1 defines no separate @noBackingAlloc attribute.

Target Profiles May Change Implementation Capability, Not Arena Semantics

Profiles may differ in:

• available Arena constructors;
• backing providers;
• growth support;
• capacity-proof strictness;
• runtime epoch metadata;
• provider failure guarantees;
• thread transfer;
• ISR use;
• memory spaces.

They may not weaken:

• unique Arena ownership;
• ArenaDomain identity;
• validity epochs;
• failure atomicity;
• safe-reference validity;
• non-relocating growth.

Hosted

A hosted profile may support borrowed, owned and growable Arenas plus a compiler-managed ambient allocation context.

Embedded fixed

Embedded profiles may prefer borrowed fixed Arenas, static backing, caller-provided backing or target-provided fixed pools.

Bare-metal bounded

A bounded profile may require statically bounded demand, no OS provider, no hidden growth and no allocation context without explicit or provable backing.

When all offsets, lifetime and identity facts are static, the compiler may eliminate the physical Arena descriptor entirely.

No-allocation

A no-allocation profile may still permit Arena.FromBuffer because it does not acquire new backing.

New and Alloc nevertheless retain their canonical allocation effect under the Arena rule.

Compiler and IR Requirements

The compiler must preserve distinctions equivalent to:

ArenaCreateBorrowed
ArenaCreateOwnedFixed
ArenaCreateGrowable
ArenaNew
ArenaAlloc
ArenaReset
ArenaRelease
ArenaDestroy

Semantic IR must also retain or relate:

• Arena owner state;
• ArenaDomain identity;
• Arena state version;
• validity epoch;
• allocation context;
• backing relation and growth policy;
• Arena dependencies;
• ordered effects;
• provider calls;
• task/thread transfer and completion;
• capacity and demand facts;
• failure paths.

Conceptually, mutating Arena control uses one continuing SSA owner state:

arena1 = create
arena2, result1 = allocate(arena1)
arena3, result2 = allocate(arena2)
arena4 = reset(arena3)
release(arena4)

This compiler representation does not change the ordinary source syntax.

Arena semantics must remain explicit through high-level Sec MLIR until Arena-specific planning, lifetime, capacity and validity reasoning are complete.

The backend must not flatten Arena operations into generic allocation too early.

Diagnostics

Arena copy

cannot copy `Arena`

`Arena` is the unique owner/controller of one allocation domain

help: move ownership instead:
    let next :<- arena

Reset with live reference

cannot reset `arena`

`values` still depends on the current Arena validity epoch

the later use is here:
    Process(values)

help: move Reset after the final use of `values`

Release with live dependency

cannot release `arena`

a live nested Arena still borrows backing from this ArenaDomain

help: release or destroy the child Arena first

Use after Release

`arena` is unavailable

the Arena was consumed by:
    arena.Release()

Unsupported type for direct safe allocation

cannot use `arena.Alloc[Connection](count)`

`Connection` is not trivially destructible

Arena.Alloc does not register per-element destructors in Sec 0.1

help: use an owning container with an explicit lifecycle protocol
help: use another storage/lifecycle abstraction

Missing default

cannot use `arena.New[Config]()`

`Config` has no valid infallible default required by Arena.New

Insufficient capacity

Arena allocation failed

requested:
    128 Packet values

the fixed Arena has insufficient remaining aligned capacity

Returning local Arena reference

cannot return `value`

`value` depends on local Arena `arena`

`arena` is destroyed when this function exits

Sec does not promote the allocation into hidden longer-lived storage

Concurrent Arena mutation

concurrent Arena mutation is not permitted

one execution may allocate from this Arena while another may reset it

Diagnostics should identify ArenaDomain/epoch dependencies and the source operation keeping them live whenever that improves the explanation.

LSP and Analysis

The LSP consumes compiler-owned Arena analysis rather than implementing an independent model.

Tooling may expose:

• backing relationship and provider;
• capacity;
• ArenaDomain and current epoch;
• active target/profile;
• allocation origin;
• live dependencies;
• what currently blocks Reset or Release;
• task/thread captures;
• capacity-demand summary;
• allocation-context origin;
• effect paths;
• physical-lowering plan;
• peak demand and utilization where known.

Analysis must invalidate cached Arena facts when relevant capacity, layout, call graph, control flow, effects, task/thread capture, Reset/Release placement, provider contracts or storage/reference rules change.

Best Practices

• Use Arena.FromBuffer when you already own suitable mutable backing and want deterministic fixed capacity.
• Use Arena.WithCapacity when the active profile provides an owned backing provider and fixed capacity is sufficient.
• Use Arena.Growable only where target/profile support and non-relocating growth semantics are appropriate.
• Keep Arena lifetime larger than every ordinary reference, view, nested Arena and task/thread dependency into it.
• Place Reset() only after final use of all dependencies from the old epoch.
• Prefer automatic Arena destruction unless an explicit Release() improves required cleanup ordering.
• Do not call Release twice or use an Arena after Release.
• Remember that Reset retains backing while Release terminates the domain.
• Do not expect Reset to zero memory.
• Do not use direct New/Alloc for non-trivially-destructible types in Sec 0.1.
• Use an owning container when Arena-backed storage needs a separate logical element lifecycle.
• Do not expect Arena to free one individual allocation.
• Do not package an Arena and a direct self-reference into an ordinary movable value without explicit future self-reference semantics.
• Do not let the compiler guess which visible Arena should become the ambient allocation context.
• Do not share one ordinary mutable Arena concurrently between tasks or threads.
• Use canonical completion boundaries before resetting storage captured by asynchronous work.
• Remember that @noAlloc currently rejects reachable Arena typed allocation even when backing is pre-reserved.

Summary

• Arena is a compiler-known move-only owner/controller of one ArenaDomain.
• ArenaDomain identity is independent of physical backing address.
• ArenaDomain identity survives ownership moves, ordinary allocation and Reset.
• Release/destruction terminates the ArenaDomain.
• Ordinary allocation changes Arena control state but does not change the validity epoch.
• Reset changes the validity epoch while preserving ArenaDomain identity.
• Release ends the domain instead of merely advancing the epoch.
• Sec 0.1 Arena is bulk-reclamation storage management.
• Sec 0.1 Arena is not garbage collection or reference counting.
• Sec 0.1 defines no individual Arena.Free.
• Sec 0.1 Arena does not perform hidden heap promotion or relocating compaction.
• Sec 0.1 Arena is not a general destructor registry.
• Sec 0.1 provides no general safe uninitialized typed Arena storage.
• Lowercase arena remains an ordinary identifier.
• Sec 0.1 introduces no special scoped arena { ... } syntax.
• Arena is non-copyable and ownership is moved with ordinary canonical move syntax.
• Moving Arena ownership preserves the same ArenaDomain, epoch, backing and existing reference validity.
• A type containing Arena becomes move-only by composition.
• Arena always owns/controls its allocation domain but may own or merely borrow its physical backing.
• Backing relationships include owned, borrowed, static and target-provided forms.
• A growable Arena may control several stable backing segments within one ArenaDomain.
• Arena.FromBuffer(ref mut buffer) creates a fixed Arena over borrowed mutable contiguous storage.
• FromBuffer does not allocate new backing.
• Borrowed backing remains owned by its original owner and is not deallocated by Arena Release.
• A zero-capacity borrowed Arena is valid.
• Arena.WithCapacity(capacity) creates a fixed owned Arena where a provider is available.
• WithCapacity returns Result[Arena, AllocationError].
• Arena.Growable(initialCapacity) may be available under profiles supporting stable non-relocating growth.
• Growable Arena must never relocate existing live allocations.
• Growth preserves ArenaDomain, epoch, addresses, bounds and reference validity.
• Arena capacity is measured in bytes.
• Typed allocation count is an element count rather than byte count.
• Allocation size arithmetic and alignment arithmetic are checked.
• Alignment padding consumes Arena capacity.
• arena.New[T]() returns Result[ref mut T, AllocationError].
• arena.Alloc[T](count) returns Result[ref mut T[], AllocationError].
• Typed allocation temporarily borrows Arena control state mutably.
• The returned reference retains ArenaDomain/epoch dependency but not an exclusive borrow of the Arena controller.
• Repeated Arena allocation is therefore permitted.
• Safe direct Arena allocation requires a complete sized type, supported alignment, valid infallible default, safe initialization and trivial destruction.
• Safe typed Arena allocation publishes only fully initialized semantic values.
• Full initialization does not require every physical byte or padding byte to be zero.
• Direct safe New/Alloc do not support non-trivially-destructible T in Sec 0.1.
• Owning containers may use Arena-backed storage when the container separately tracks and destroys logical elements.
• Alloc[T](0) succeeds with a valid empty mutable slice and consumes no capacity.
• Valid zero-sized types retain semantic element count even when payload bytes are zero.
• Arena creation/allocation failure uses AllocationError.
• Arena allocation never reports ordinary failure by returning null, invalid references or shorter slices.
• Capacity exhaustion is not automatically panic or process termination.
• The source Result signature remains stable even if proof removes the runtime failure path.
• Arena allocation is atomic from program semantics.
• Failed allocation leaves the prior Arena allocation state and existing allocations valid.
• Successful positive-sized allocations do not overlap and do not invalidate earlier allocations.
• Ending a reference does not reclaim Arena bytes.
• Reset retains the Arena owner, ArenaDomain and backing while ending the current validity epoch.
• Reset invalidates allocations from the old epoch and starts a new epoch.
• No validity-preserving dependency may cross Reset.
• Final-use analysis can prove a reference dead before Reset even when its lexical scope continues.
• Explicit stale-capable weak handles may survive Reset under their own fallible-resolution contract.
• Epoch reuse must never revive stale references or handles.
• Runtime epoch metadata may be eliminated when static proof is sufficient.
• Fixed Arena Reset resets used capacity while retaining total capacity.
• Borrowed Arena Reset retains the borrow of the backing.
• Growable Arena Reset retains acquired stable segments unless another future trim operation is explicitly used.
• Reset does not require backing bytes to be zeroed.
• Reset is atomic from program semantics.
• Release() is a compiler-known terminal consuming lifecycle operation.
• Release terminates the ArenaDomain and makes the source Arena unavailable.
• Release is non-fallible and returns void in the base Arena contract.
• Release's whole-self consumption is a compiler-known Arena special case and does not enable ordinary consuming user methods.
• No validity-preserving dependency may cross Release.
• Owned backing is returned to its provider at Release.
• Borrowed/static backing is not deallocated merely because the ArenaDomain ends.
• Arena destruction performs Release semantics automatically while ownership is still held.
• Explicit Release prevents a second implicit Release.
• Double Release is invalid.
• Arena storage reclamation does not replace required logical value destruction.
• A returned reference cannot depend on a local Arena destroyed on function exit.
• Sec never repairs such an escape through hidden promotion.
• Returning the Arena owner itself is valid and preserves its ArenaDomain/epoch.
• Sec 0.1 does not automatically support ordinary movable values containing both an Arena owner and a direct self-reference into that Arena.
• Nested Arenas require no special syntax.
• A nested child Arena has its own domain/epoch but depends on the parent allocation/domain/epoch providing its backing.
• The parent cannot Reset or Release while a child Arena remains live.
• Releasing a child does not individually reclaim its backing allocation from the parent.
• Arena operations participate in the common LIFO defer/destruction cleanup model.
• Dependent deferred uses must execute before Arena Release invalidates their storage.
• Task captures of Arena-backed storage preserve domain, epoch, bounds and borrow dependencies.
• Reset/Release remain invalid until canonical task completion proves the task can no longer access the storage.
• Task result payloads may continue carrying Arena dependencies after task completion.
• Arena may be moved exclusively into a task or thread when the concurrency/provider/profile rules permit it.
• Moving Arena ownership across execution contexts preserves the ArenaDomain identity.
• Thread borrowing additionally requires transferability and memory-synchronization proof.
• Ordinary Arena does not support concurrent mutation.
• Concurrent allocate/reset/release operations require a future distinct synchronization abstraction.
• Arena is a primary allocation-domain realization but is not identical to the ambient allocation context.
• Each callable has zero or one ambient allocation context under the general allocation rules.
• MayAllocate and RequiresAllocationContext are separate semantic facts.
• An explicit Arena argument can allocate without requiring ambient allocation context.
• The compiler never guesses an ambient Arena merely from visible Arena variables.
• Passing an Arena argument does not implicitly rebind the ambient allocation context.
• Spawned task/thread execution receives a new allocation context rather than automatically inheriting the parent's mutable context.
• Processes receive separate address-space allocation contexts.
• ISRs have no ordinary allocation context unless target rules explicitly provide and permit one.
• Foreign entrypoints do not automatically receive a hidden Sec Arena context.
• Arena operations are ordered semantic effects associated with ArenaDomain identity.
• Arena allocation is not pure and distinct allocations must not be merged by CSE.
• Arena.New/Arena.Alloc carry the canonical allocation effect.
• Current Sec 0.1 @noAlloc semantics reject reachable Arena typed allocation even when backing is already reserved.
• Arena.FromBuffer creates an Arena domain without adding backing allocation.
• Target profiles may vary providers, growth, capacity policy, metadata, thread transfer, ISR availability and memory spaces.
• Profiles may not weaken ownership, domain/epoch identity, failure atomicity, safe-reference validity or non-relocating growth.
• Bare-metal bounded profiles may eliminate runtime Arena descriptors when all relevant facts are static.
• Semantic IR must preserve Arena creation form, typed allocation, Reset, Release, destruction, domain identity, epochs and dependencies.
• Arena control may be represented as unique SSA state internally without changing source syntax.
• High-level Arena semantics remain explicit until Arena-specific optimization and validity analysis are complete.
• LSP and sec analyse consume compiler Arena analysis rather than maintaining a separate model.