Memory Allocation

Core Principles

• Only operations whose canonical contracts permit allocation may dynamically allocate.
• The compiler must not introduce dynamic allocation merely for implementation convenience.
• Allocation-context selection is normally compiler-managed.
• Allocation is separate from ownership transfer.
• Allocation is separate from initialization.
• Allocation is separate from destruction.
• Allocation is separate from raw-storage reclamation.
• Allocation is separate from safe-reference validity.
• Allocation is separate from MMIO, fixed-address binding and volatile access.
• Allocation semantics are resolved before backend lowering.

LLVM, MLIR and target code generation may implement an already-resolved allocation decision, but they must not invent a new source-level allocator policy.

Allocation-Capable Operations

An operation is allocation-capable only when the owning language, core-library, collection, shaped-type, string, platform or standard-library contract explicitly permits allocation.

Examples include operations such as:

let values := try list[int].WithCapacity(100)
let text := try string.From(source)

An API may be allocation-capable even though no allocator argument appears in normal source syntax.

Conversely, an operation defined as allocation-free must remain allocation-free in every conforming implementation.

Operations That Do Not Silently Allocate

The following operations must not dynamically allocate merely because the compiler finds allocation convenient:

Copy

let second := first

Assignment

target = source

Move

let second :<- first
destination <- source

Parameter passing

Inspect(value)
Consume(<-resource)

Return

return value

Reference and view creation

let item := ref value
let slice := ref values[..]

The same prohibition applies to allocation introduced merely because of:

• borrow analysis;
• control-flow merging;
• match;
• try;
• if, switch or loops;
• discard;
• ordinary destruction;
• escape analysis;
• lifetime repair;
• closure capture repair.

If one of these operations would only become valid by secretly moving data into longer-lived storage, the program is invalid instead.

new Does Not Mean Heap Allocation

In Sec, new selects lifecycle construction through init or another permitted construction path:

let point := new Point(10, 20)

let connection := try new Connection(address)

new is a construction marker, not an allocation keyword.

The resulting value may live in:

• SSA form;
• registers;
• stack storage;
• inline aggregate storage;
• another valid storage location chosen by ordinary placement rules.

Dynamic allocation occurs only when the selected construction semantics actually require an allocation-capable operation.

Default Dynamic-Allocation Model

Arena allocation is the default dynamic-allocation model for Sec 0.1.

When the active target and build profile permit dynamic allocation, the compiler maintains a canonical active allocation context for allocation-capable operations.

That context may be backed by:

• a compiler-managed local Arena;
• a caller-propagated Arena;
• an explicitly selected Arena;
• a target-provided Arena;
• another allocation domain defined by a canonical rule;
• no domain at all when the active profile forbids dynamic allocation.

The normal programmer is not required to add an Arena parameter to every ordinary function merely because a nested operation may allocate.

The detailed programmer-visible Arena model is covered in Arenas.

The Allocation Context Is a Compiler Semantic Fact

The active allocation context is not a source-level global variable.

It is compiler-visible semantic state associated with allocation-capable execution.

The compiler may propagate that context through call boundaries when the callable's contract permits allocation.

This allows ordinary source code to remain focused on the operation being requested rather than on plumbing allocator handles through every layer.

Implicit Allocation-Context Propagation

Allocation context is propagated only through operations whose semantic effects permit allocation.

A caller may therefore provide the active context to a callee without adding a visible Arena parameter to the ordinary source signature.

Imported functions, indirect calls, interface calls, generic specializations, recursive call graphs and bodyless declarations need sufficient allocation metadata for the compiler to reason about this correctly.

Unknown allocation behavior is treated conservatively when a caller or profile requires proof that no allocation occurs.

Allocation Is a Compiler-Visible Effect

A callable that may allocate carries a compiler-visible allocation effect.

Allocation effect is independent from other effect categories such as:

• panic;
• I/O;
• blocking;
• mutation;
• FFI;
• volatile access;
• synchronization.

A function may, for example, be panic-free while still allocating, or allocation-free while still performing I/O.

Effect summaries are shared by compilation, LSP, ISR analysis, project policy and lowering.

Explicit Arena Selection

Systems, embedded, allocator, FFI-wrapper and deterministic-memory code may select an Arena explicitly when the API offers that form:

let values := try Type.Create(ref mut arena, arguments)

The equivalent normal form may omit the Arena when implicit context selection is allowed:

let values := try Type.Create(arguments)

Passing ref mut arena is ordinary mutable borrowing. It gives the operation authority to update Arena allocation state for the call.

Explicit selection does not transfer ownership of the Arena unless the API separately declares a consuming contract.

Sec 0.1 introduces no general alloc keyword and no special scoped-Arena block syntax through the allocation model.

Manual Typed Allocation

The canonical safe manual allocation surface is provided by Arena.

Examples include:

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

Conceptually:

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

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

These are Arena instance methods. The Arena receiver is mutated during allocation, but the temporary mutable borrow of Arena control state ends when the call returns.

The returned reference or slice keeps a dependency on the Arena allocation domain rather than an exclusive borrow of the entire Arena control value.

Repeated allocation is therefore possible while capacity remains available.

Alloc[T](count) interprets count as a number of T elements, not an untyped byte count.

Exact Arena type restrictions, initialization rules, growth, reset and release are covered in chapter 41.

Allocation Failure Uses Ordinary Sec Error Handling

A safe dynamic allocation that may fail reports failure through the ordinary Sec fallibility model.

The standard error type is AllocationError where the owning API specifies it.

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

Failure is handled with normal Result, try and error rules.

Ordinary capacity exhaustion is not automatically a reason to panic or terminate the process.

An allocation may be treated as infallible only when the compiler/platform contract proves the necessary storage, capacity, layout, alignment and other preconditions.

Safe Allocation Failure Does Not Return null

A failed safe allocation must not:

• return null as a safe reference;
• return an invalid safe reference;
• return a shorter allocation without an explicit API contract saying so;
• expose partially initialized readable storage;
• silently select an unrelated allocator;
• silently select another Arena;
• panic merely because ordinary allocation failed;
• terminate the process merely because capacity was insufficient.

Safe references preserve their non-null validity model. Allocation failure remains an explicit typed failure.

No Hidden Escape Promotion

The compiler never allocates merely because a value or reference escapes its original scope.

This is invalid:

fn Invalid() ref byte[] {
    let data: byte[16] := [...]
    return ref data[..]
}

The returned reference would outlive its local backing storage.

The compiler must not “repair” the program by secretly moving data into:

• an Arena;
• a hidden heap object;
• a hidden box;
• a reference-counted cell;
• a closure environment;
• another longer-lived storage domain.

If the program needs escaping storage, an owning operation must intentionally create that storage through an allocation-capable API.

This rule applies equally to returns, closures, callbacks, tasks, threads, deferred work, ISR handoff, FFI retention and stored references.

Storage Ownership and Value Ownership Are Different

An allocation domain may control the raw storage while an ordinary Sec value owns the value stored in that memory.

allocation domain
    controls raw storage

owned value
    controls value lifetime and owned subresources

reference or slice
    borrows live initialized storage

Arena-backed storage therefore does not change the ordinary ownership rules for the value placed there.

Likewise, owning a value does not imply authority to reclaim the raw storage backing that value.

Allocation analysis must keep those responsibilities separate.

Allocation and Initialization Are Separate

Allocation produces storage. It does not by itself prove that a valid readable T exists in that storage.

A safe API that returns readable T or T[] must complete all required initialization before exposing the result.

Partial initialization follows the ordinary construction and destruction rules.

If initialization fails after storage was acquired, every already-initialized non-trivial subvalue must be cleaned up correctly.

Reclaiming raw bytes is not a substitute for required value destruction.

Destruction and Reclamation Are Separate

Destroying a value ends that value's lifetime and runs any required cleanup.

Reclaiming allocation-domain storage makes raw storage reusable or unavailable.

Those are not the same operation.

A value stored in Arena-backed memory is destroyed at its ordinary ownership boundary; the Arena does not automatically delay destruction until Reset or Release.

Conversely, Arena storage cannot be reclaimed while a live value or safe reference still requires it.

Arena is not an implicit registry of arbitrary destructors.

Arena Reset and Release Affect Storage Lifetime

The detailed rules belong to the next chapter, but the allocation model establishes the general relationship:

• Reset reclaims allocations tied to the affected Arena validity epoch while keeping the Arena alive;
• Release terminates the Arena allocation domain;
• live values, references, views, captures, deferred operations and returned dependencies may block reclamation;
• statically provable invalid Reset/Release is a compile-time error;
• runtime validity epochs may participate where static proof alone is insufficient under the selected profile.

Repeated ordinary allocation from one live Arena does not by itself invalidate earlier allocations.

Storage Origin Is Preserved Explicitly

Arena-allocated storage has Arena storage origin.

Storage origin is separate from:

• nominal type identity;
• foreign provenance;
• fixed-address status;
• address stability;
• mutability;
• volatility;
• reclamation authority;
• device liveness;
• interrupt accessibility.

Two references may therefore have the same Sec type while referring to storage with different origins and lifetimes.

The broader storage model is covered in chapter 22 and the later layout/storage chapters.

Collections and Other Dynamic Owning Values

Collection, shaped-type and string rulebooks define exactly which operations allocate.

For example:

• creating an empty owner may be allocation-free when its canonical representation permits it;
• growing an owning collection may allocate when the growth operation is declared allocation-capable;
• materializing a new owning value may allocate;
• borrowing or taking a view must not allocate when the operation is defined as allocation-free.

Those operations all consume the same canonical allocation-context and allocation-effect model.

String Operations Allocate Only When Their Contracts Permit It

Ordinary string operations such as copy, move, comparison, indexing, borrowing and iteration do not allocate merely because strings may sometimes own dynamic storage.

Operations that intentionally materialize new runtime string storage may allocate through the canonical allocation context.

Compile-time-folded string data stored in the output image is not a runtime dynamic allocation.

Allocation analysis tracks actual string storage facts rather than assuming every string is heap-backed.

Views and Non-Owning Transformations Stay Allocation-Free

Operations that merely produce a new view of existing storage must remain allocation-free when their owning contract says so.

Examples may include:

• slices;
• borrows;
• reshapes;
• transposes;
• other non-owning shaped views.

The backend must not allocate a hidden buffer merely because that would simplify implementation.

An operation that intentionally materializes new owning storage is a different operation and may be allocation-capable.

Closures and Escaping Execution Do Not Trigger Hidden Allocation

Closure capture cannot allocate merely to make an otherwise invalid captured reference live long enough.

If a closure representation is canonically allocation-capable, that fact belongs to its semantic effect and must preserve the declared capture ownership model.

The compiler never performs implicit heap promotion just because a closure escapes.

Long-lived owned closure storage must be created by an operation whose canonical contract explicitly creates such storage.

Foreign Allocation Is Not Automatically Sec Arena Allocation

Foreign libraries may allocate storage under their own ownership and reclamation rules.

A foreign allocation does not become Arena allocation simply because Sec stores or wraps the resulting handle.

FFI contracts independently describe:

• ownership;
• retention;
• lifetime;
• foreign deallocation responsibility;
• safe-wrapper conversion;
• failure behavior.

A wrapper may convert foreign allocation failure into a normal Sec Result.

A pointer returned by a foreign allocator does not automatically become a safe Sec reference.

Sec also does not silently copy foreign storage into an Arena merely to obtain safe provenance. Such materialization must be an explicit operation when desired.

Fixed-Address and Hardware Storage Are Not Dynamic Allocation

Storage existing at a physical or virtual device address is not Arena allocation merely because Sec provides a typed view of it.

@address(Peripheral.GPIOA)
let mut GPIOA: GPIORegisters

Fixed-address binding, MMIO and volatile access belong to platform/hardware storage semantics.

Mapping a device or OS memory region may itself be a fallible resource operation, but the physical backing is not thereby reclassified as Arena storage.

Volatile reads and writes are storage accesses, not allocations.

Target and Build Profiles May Restrict Allocation

Sec preserves the same ownership, borrowing, lifetime, destruction and reference semantics across different allocation capabilities.

Typical allocation configurations include:

hosted
    compiler-managed allocation context available

embedded-arena
    fixed or program/platform-supplied Arena available

noalloc
    dynamic allocation unavailable

A profile may also require that allocation is statically bounded or comes from a preallocated domain.

Runtime-free bare-metal Sec must remain possible.

Hosted Allocation

A hosted compilation plan may provide a compiler-managed active allocation context.

The concrete provider may ultimately use operating-system services, runtime support, target helpers or another verified backing strategy.

That provider choice does not change source-level ownership, error handling, reference validity or destruction semantics.

Ordinary Sec code still observes the allocation contract of the operation rather than the implementation details of the provider.

Embedded and Preallocated Arena Profiles

Embedded systems may use fixed or program/platform-provided Arena capacity instead of a general-purpose hosted provider.

Allocation-capable operations remain ordinary Sec operations but must fit the active domain's capacity and restrictions.

A compiler may prove sufficient capacity statically, or an allocation may fail normally with AllocationError when runtime capacity is insufficient.

The detailed Arena backing and capacity model is covered in chapter 41.

No-Allocation Profiles

A target or build profile may make dynamic allocation unavailable.

In such a plan, an unresolved reachable use of an allocation-capable operation is a compile-time error:

fn BuildMessage() string {
    ...
}

If BuildMessage reaches a string materialization operation that requires dynamic storage, the build cannot simply substitute an allocator that the profile forbids.

However, an allocation-capable source operation may still be accepted when the compiler completely proves that dynamic allocation can be eliminated while preserving every observable Sec semantic requirement.

@noAlloc

@noAlloc is a transitive compiler-verified guarantee for one callable:

@noAlloc
fn Process(
    buffer: ref byte[],
) Result[void, ProcessError] {
    ...
}

No reachable execution path may allocate dynamically.

Verification includes:

• direct operations;
• reachable callees;
• indirect/interface calls;
• generic specializations;
• closures;
• defer bodies;
• reachable destruction;
• foreign contracts;
• compiler-generated operations.

Using try around an allocating operation does not make the operation allocation-free. Allocation that succeeds still allocates.

A no-allocation build profile is a plan-wide capability restriction. @noAlloc is a callable-level verified guarantee.

Interrupt and Restricted Execution Contexts

ISR and interrupt policy may forbid dynamic allocation entirely.

Any allocation-capable operation reachable from such a root must therefore be rejected unless the applicable interrupt/target rule explicitly permits the selected preallocated domain.

The compiler must not hide allocation inside an apparently allocation-free helper reachable from ISR code.

This is why allocation effect must be visible to call-graph and ISR analysis.

Capacity, Size and Alignment

Allocation size is computed from the target-correct layout of the requested type.

For a typed count, the conceptual calculation includes:

payloadSize = CheckedMultiply(count, SizeOf(T))
alignedStart = AlignUp(currentOffset, AlignOf(T))
endOffset = CheckedAdd(alignedStart, payloadSize)

Alignment padding consumes capacity.

Required alignment comes from the canonical type/layout model for the active compilation plan.

A fixed-capacity domain fails an allocation that cannot fit unless the compiler has already proven the request impossible and reports that problem statically.

Allocation-Size Arithmetic Is Checked

Count, size, alignment and end-offset arithmetic must not silently wrap.

The compiler/runtime checks overflow before reserving storage.

This matters especially when a count is multiplied by a target-dependent SizeOf(T).

An impossible request must not become a smaller allocation merely because arithmetic overflowed.

Static Capacity Proof

A compiler or target profile may prove that a bounded allocation cannot fail.

A complete proof may need to account for:

• all allocation-capable operations;
• control-flow multiplicity;
• loops;
• recursion;
• call graph;
• target layout;
• alignment padding;
• simultaneously live allocations;
• profile capacity limits.

A successful proof may remove runtime allocation-failure checks.

It does not silently change the source-level API type.

The Compiler May Eliminate Dynamic Allocation After Proof

An allocation-capable source operation does not force the final machine code to call a dynamic allocator if all observable semantics can be preserved without doing so.

Valid optimization may eliminate allocation only when it preserves:

• storage lifetime;
• capacity;
• address stability;
• provenance;
• ownership;
• destruction timing;
• reference validity;
• failure behavior;
• concurrency and reentrancy correctness.

Allocation elimination is an optimization. It must never be used as hidden escape repair.

Stack or Static Placement May Replace Dynamic Storage Only When Proven Correct

The compiler may choose stack, static or another non-dynamic placement for an allocation-capable operation when the proof is complete.

The proof must account for:

• complete required lifetime;
• capacity;
• alignment;
• recursion;
• reentrancy;
• concurrency;
• ISR execution;
• multiple simultaneous live instances;
• address-stability requirements;
• failure semantics.

Static placement must never accidentally share one storage region between independent live values that require distinct identities.

Sec Allocation Does Not Require Garbage Collection or Reference Counting

Ordinary Sec allocation semantics do not require a mandatory garbage collector.

They also do not require mandatory reference counting.

Arena validity epochs are not GC handles or reference counts.

Ownership, deterministic destruction, Arena-domain reclamation and reference validity remain separate mechanisms.

A target may therefore implement Sec without a general managed runtime.

Compile-Time Allocation Is Separate from Runtime Dynamic Allocation

Semantic compile-time evaluation may use transient evaluator storage while computing a value.

That storage belongs to the compiler evaluator and is not a target runtime allocation.

Likewise, a compile-time-folded string or aggregate placed directly into the program image is not a runtime dynamic allocation merely because bytes exist in the final artifact.

The compiler must not confuse private evaluator storage with a program-visible Arena or runtime allocator resource.

Compile-time materialization is covered in chapter 39.

Allocation Semantics Are Fixed Before Backend Lowering

Every dynamic allocation that survives semantic analysis must carry explicit compiler facts describing at least:

• allocation kind;
• selected allocation domain/context;
• requested type;
• count and size;
• alignment;
• fallibility;
• resulting storage origin/domain;
• ownership/borrow mode;
• lifetime or validity-epoch dependency where needed;
• destruction responsibility;
• allocation effect.

Lowering preserves those facts until equivalent lower-level behavior exists.

MLIR/LLVM must not select a different allocator simply because it is easier to lower.

Backends may remove a dynamic allocation only after semantics-preserving proof.

Diagnostics

Allocation diagnostics should explain the allocating operation, the active profile, the allocation context and a practical alternative where possible.

Allocation disabled by the build

this call may allocate, but dynamic allocation is disabled for this build

`BuildMessage()` may call `string.Concat`, which requires an allocation context

help: use a preallocated buffer
help: select a build profile that permits allocation

Hidden escape promotion is not allowed

cannot return this reference

`data` is local storage and does not live long enough for the returned reference

Sec does not move escaping local storage into a hidden Arena or heap object

help: return an owning value
help: allocate the required storage explicitly through an allocation-capable API
help: borrow from storage whose lifetime already covers the return

Allocation effect violates @noAlloc

`Process` does not satisfy `@noAlloc`

call path:
    Process
    -> Normalize
    -> string.From

`string.From` may allocate

Insufficient Arena capacity

allocation cannot be proven to fit the selected fixed Arena

requested:
    256 elements of Packet

required size depends on:
    Packet.SizeOf
    target alignment
    allocation multiplicity

help: handle AllocationError at runtime
help: increase the Arena capacity
help: reduce the maximum allocation demand

Allocation-size overflow

allocation size overflows the target size domain

requested element count:
    count

element type:
    Packet

help: validate the requested count before allocation

Invalid allocation context

no compatible allocation context is available for this operation

active profile:
    noalloc

operation:
    list[int].WithCapacity(100)

Diagnostics should distinguish allocation failure from ordinary value construction failure, invalid lifetime/escape, destruction errors and target-address binding errors.

LSP and Analysis

The LSP and sec analyse consume the same canonical allocation facts as compilation.

Tooling may expose whether a callable:

• is proven allocation-free;
• may allocate;
• has unresolved allocation behavior;
• requires a particular allocation capability;
• receives an implicit allocation context;
• selects an explicit Arena;
• contains an allocation that can be statically eliminated.

Hover or analysis should be able to navigate from a transitive allocation warning to the operation that introduced the effect.

Incremental analysis must invalidate cached allocation summaries when relevant function bodies, imports, profiles or allocation-capable API contracts change.

Best Practices

• Prefer ordinary allocation-capable APIs and let the compiler propagate the active context in normal application code.
• Use an explicit Arena when storage lifetime, capacity or provider choice is intentionally part of the design.
• Do not pass Arena handles through every layer merely because a deeper operation may allocate.
• Use @noAlloc when allocation freedom is an actual verified API requirement.
• Remember that new selects construction; it does not request heap allocation.
• Do not assume copy, move, return, borrow or closure capture may allocate to repair lifetime problems.
• Design escaping data around an owning storage operation rather than relying on hidden promotion.
• Handle AllocationError as an ordinary typed failure where the operation may fail.
• Do not use null as the failure representation of a safe allocation.
• Keep value ownership separate from raw-storage reclamation authority.
• Keep initialization and destruction separate from raw storage acquisition/reclamation.
• Prefer views and borrows when no new owning storage is required.
• Use device/fixed-address APIs for hardware storage rather than treating MMIO as allocation.
• Use preallocated/fixed-capacity domains for deterministic embedded designs where appropriate.
• Let static capacity proofs remove failure paths when possible, but keep source contracts stable.
• Do not depend on a garbage collector or reference counter unless a separate library/runtime abstraction explicitly provides one.

Summary

• Dynamic allocation is explicit in the semantic operation being performed.
• Selection and propagation of the allocation context are normally implicit.
• Only canonically allocation-capable operations may allocate.
• An allocation-free operation must remain allocation-free in conforming lowering.
• Copy must not silently allocate.
• Ordinary assignment must not silently allocate.
• Move initialization and move assignment must not silently allocate.
• Parameter passing must not allocate merely because a value crosses a call boundary.
• Return must not allocate merely because a value or ownership crosses the return boundary.
• Creating a safe reference, slice or view must not allocate merely to make the reference legal.
• Control-flow constructs such as match, try, if, switch and loops do not gain hidden allocation semantics.
• Ordinary destruction does not allocate merely because cleanup analysis is complex.
• new selects lifecycle construction and does not imply heap allocation.
• A value constructed with new may live in SSA, registers, stack or inline storage.
• Dynamic allocation occurs during construction only when the selected construction semantics actually require it.
• Arena is the default Sec 0.1 dynamic-allocation domain.
• The compiler maintains an active allocation context where the selected target/profile provides one.
• The active allocation context is a compiler semantic fact, not a source-level global variable.
• Ordinary application code is not required to thread an Arena parameter through every call.
• Allocation context propagates only through call paths whose semantic effects permit allocation.
• Allocation is a compiler-visible semantic effect.
• Allocation effect is independent from panic, I/O, blocking, mutation, FFI, volatile and synchronization effects.
• Imported, indirect, interface, generic, recursive and bodyless callables require sufficient allocation-effect metadata or conservative treatment.
• Explicit Arena selection may be offered by an allocation-capable API.
• An explicit mutable Arena reference is ordinary borrowing of the Arena control value.
• Explicit Arena selection does not transfer Arena ownership unless the API separately declares that transfer.
• Sec 0.1 introduces no general allocation keyword or special scoped-Arena syntax through the allocation model.
• Manual safe typed allocation is provided by the canonical Arena API.
• arena.New[T]() returns Result[ref mut T, AllocationError].
• arena.Alloc[T](count) returns Result[ref mut T[], AllocationError].
• Alloc[T](count) interprets count as elements of T, not bytes.
• A temporary mutable borrow of Arena control state ends when the allocation operation returns.
• Returned Arena-backed references retain a storage-domain dependency.
• Allocation failure uses ordinary Result/try/error handling.
• AllocationError is the standard allocation failure type where the canonical API specifies it.
• Ordinary safe allocation failure does not return null.
• Ordinary safe allocation failure does not return an invalid reference or partial readable storage.
• Ordinary allocation failure must not panic or terminate the process merely because capacity was insufficient.
• An allocation can be treated as infallible only after proof of all required capacity/layout/alignment preconditions.
• The compiler never performs hidden escape promotion.
• An invalid escaping local reference is rejected rather than moved into an Arena, heap, hidden box or reference-counted cell.
• Escaping owned storage must be created intentionally by an allocation-capable operation.
• The no-hidden-promotion rule applies to returns, closures, callbacks, tasks, threads, defer, ISR handoff, FFI retention and stored references.
• Raw-storage ownership and value ownership are distinct.
• An Arena controls raw-storage reclamation while an ordinary owned value controls value lifetime and owned subresources.
• A reference or slice into Arena-backed storage is non-owning.
• Destroying an Arena-backed value does not necessarily reclaim its bytes immediately.
• Reclaiming raw Arena bytes does not replace required destruction of live non-trivial values.
• Allocation produces storage; initialization produces valid readable typed values.
• Safe APIs must fully initialize readable T/T[] storage before exposing it.
• Partial initialization follows ordinary construction/destruction cleanup rules.
• Destruction and raw-storage reclamation are different operations.
• Arena allocation does not delay ordinary value destruction until Reset/Release.
• Arena is not an implicit arbitrary-destructor registry.
• Reset and Release may reclaim/invalidate Arena storage according to Arena lifetime rules.
• Live values, references, views, captures and deferred uses may prevent reclamation.
• Repeated allocation from one live Arena does not by itself invalidate earlier allocations.
• Validity epochs are not garbage-collector handles or reference counts.
• Storage origin is separate from nominal type, provenance, fixed-address status, mutability, volatility and reclamation authority.
• Two references with the same Sec type may refer to storage with different origins and lifetimes.
• Collection, string and shaped-type rulebooks define which operations allocate.
• An empty owning collection may be allocation-free when its canonical representation permits it.
• Growing an owning collection may allocate only when the operation is canonically allocation-capable.
• Materialization of new owning storage may allocate.
• Slices, borrows, reshapes, transposes and other non-owning views remain allocation-free where their contracts define them that way.
• String copy, move, borrow, comparison, indexing and iteration do not allocate unless their owning rules explicitly permit it.
• Compile-time-folded constant string storage is not runtime dynamic allocation.
• Closure capture does not allocate merely to repair an invalid escaping reference lifetime.
• A closure representation may allocate only when that allocation is part of its canonical semantic effect.
• Sec does not perform automatic heap promotion for escaping closure captures.
• Foreign allocation does not automatically become Arena allocation.
• FFI allocation contracts independently define ownership, retention, lifetime and deallocation responsibility.
• A foreign allocated pointer does not automatically become a safe reference.
• Sec does not silently copy foreign storage into an Arena merely to manufacture safe provenance.
• Fixed-address storage, MMIO and hardware registers are not dynamic allocation.
• Volatile reads and writes are storage accesses, not allocations.
• Target/build profiles may permit, restrict or forbid dynamic allocation.
• Typical configurations include hosted, embedded-arena and noalloc.
• Ownership, borrowing, lifetime, destruction and reference semantics remain consistent across allocation profiles.
• A no-allocation profile rejects unresolved reachable dynamic allocation.
• Runtime-free bare-metal Sec remains possible.
• @noAlloc is a transitive compiler-verified callable guarantee.
• Using try around an allocation does not make the successful path allocation-free.
• ISR/interrupt policy may prohibit allocation and relies on the same allocation-effect facts.
• Allocation size uses target-correct type layout.
• Allocation-size arithmetic is checked for overflow.
• Alignment follows the allocated type and active target layout/ABI.
• Alignment padding consumes allocation capacity.
• A fixed-capacity domain fails or rejects allocations that do not fit.
• Static capacity proof may remove runtime failure checks only after complete proof.
• Capacity analysis must account for loops, recursion, call graph, multiplicity, layout and all relevant allocation-capable operations.
• The compiler may eliminate a dynamic allocation only when all observable Sec semantics are preserved.
• Allocation elimination must preserve lifetime, capacity, address stability, provenance, ownership, destruction and failure behavior.
• Stack/static placement may replace dynamic storage only after proof including recursion, reentrancy, concurrency and simultaneous live-instance requirements.
• Static placement must not accidentally share storage between logically independent live values.
• A no-allocation target may accept allocation-capable source when dynamic allocation is completely proven away.
• Ordinary Sec allocation requires neither mandatory garbage collection nor mandatory reference counting.
• Transient semantic-CTE allocation is compiler-evaluator storage, not target runtime allocation.
• Constant data emitted into the program image is not automatically runtime dynamic allocation.
• Every surviving dynamic allocation is explicit in the compiler's semantic representation before backend lowering.
• Lowering must preserve the selected allocation domain, alignment, overflow checks, capacity checks, lifetime dependencies and source-level failure semantics.
• MLIR/LLVM/backend stages may not invent or substitute a different allocator merely for convenience.
• LSP and sec analyse consume the same allocation effects and context facts as compilation.
• Tooling should trace transitive allocation causes and report the active allocation profile/domain where useful.