Arrays

Two Array Kinds

Slices are not a third owning array form. A slice is a borrowed view and is covered separately in the next chapter.

Fixed Arrays T[N]

A fixed array uses postfix length syntax:

byte[256]
int[4]
Packet[32]

N is the exact number of logical elements.

The element type must have a known size because the complete fixed-array layout is determined at compile time.

Fixed Array Type Identity

The element type and length both participate in fixed-array type identity.

These are distinct types:

int[4]
int[5]
uint[4]

N must be a non-negative compile-time integer representable by uint.

The compiler rejects:

• negative lengths;
• non-integer lengths;
• runtime-dependent lengths;
• constant-evaluation overflow;
• lengths not representable by uint;
• complete array layouts exceeding the target's layout limits.

Zero-length arrays are valid:

byte[0]

Fixed Array Layout

A T[N] value owns N contiguous elements of T.

The fixed array itself contains no hidden runtime:

• pointer;
• length field;
• capacity field;
• allocator identity.

Its length comes from the type.

Complete layout arithmetic is checked. An array whose total byte layout cannot be represented safely for the target is rejected.

Nested Arrays

Fixed arrays may contain fixed arrays:

int[3][4]

Sec writes postfix dimensions from outermost to innermost.

The type above means:

3 outer elements
each outer element has type int[4]

Every dimension participates in type identity and checked layout.

For example:

let matrix: int[3][4]

represents three int[4] elements.

Fixed Array Default Construction

A mutable fixed array may omit its initializer when every element can be validly default-constructed:

let mut values: int[4]

This creates four valid default int elements.

If T is not defaultable, a non-empty T[N] cannot use this form.

A zero-length array is defaultable without constructing any element:

let mut empty: Resource[0]

Safe Sec never exposes a fixed array containing readable but uninitialized elements.

If non-trivial element construction fails part-way through construction, already initialized elements are tracked and cleaned up according to ordinary ownership rules.

An immutable fixed-array declaration requires an initializer.

Array Literals

Fixed-array literal syntax is:

[expression, expression, expression]

A trailing comma is permitted:

[1, 2, 3,]

Target-typed literals

let bytes: byte[3] := [1, 2, 3]
let percentages: Percent[2] := [10, 20]

The target type supplies both the element type and required length.

Every literal element must be valid for the target element type, and the final literal element count must match the target length exactly.

Inference without a target

let values := [10, 20, 30]

infers:

int[3]

This inference is available when:

• the literal contains at least one element;
• all elements resolve to one element type;
• the inferred length is the literal element count.

Empty literal

An empty bracket literal needs target context:

let empty: int[0] := []

There is no element from which an unconstrained empty literal could infer its type.

Spread in Fixed-Array Literals

Fixed-array literals may use the canonical spread operator:

let middle: int[4] := [2, 3, 4, 5]
let all: int[6] := [1, ...middle, 6]

Multiple fixed-array spreads are permitted when the complete result length is known at compile time and matches the target array length exactly.

Spread does not turn a fixed array into a dynamically sized array.

Ownership and copy/move behavior of each spread source follow the general spread rules.

Dynamic Owning Arrays T[]

A dynamic owning array uses:

T[]

Examples:

byte[]
Packet[]
User[]

A dynamic array is a first-class owning value type.

It is distinct from:

T[N]
ref T[]
ref mut T[]
list[T]

Its current length is runtime state and is not part of its type identity.

Dynamic Array Ownership

Every T[] is:

• owning;
• move-only;
• non-trivially destructible;
• responsible for the lifetime of every live logical element.

This remains true even if T itself is trivially copyable.

let mut values: int[]

is still an owning move-only collection value.

Ordinary assignment, parameter transfer, aggregate transfer and return do not implicitly deep-copy a dynamic array.

Dynamic Array Empty Default

A mutable dynamic array may omit its initializer:

let mut values: int[]

This creates a valid empty owner with:

Len = 0
live elements = none
backing storage = none
allocation = none

The empty default is valid even when T itself has no default value.

No element exists yet, so no T needs to be constructed.

An immutable T[] declaration requires an initializer expression that produces a valid owning dynamic array.

Internal Capacity Is Not Public Array State

A dynamic array may internally reserve more storage than its current Len.

That capacity is an implementation detail in Sec 0.1.

T[] does not expose canonical members named:

Capacity
Reserve()
Resize()

Nor does Sec define the exact growth factor or allocator over-allocation as source-language semantics.

The semantic invariant is:

0 <= Len <= internal capacity
live initialized elements = [0, Len)
capacity-only slots contain no live T

A reserved but unused slot is not a default-constructed hidden element.

Allocation and Growth

A non-empty dynamic-array operation may require backing allocation.

Sec does not assume one hidden global heap merely because T[] exists. A valid allocation context must be resolved before lowering an operation that needs new backing storage.

Growth is transactional.

If growth fails:

• the original array remains valid;
• Len is unchanged;
• existing live elements remain owned by the original array;
• partially prepared new backing does not become observable;
• the incoming element is not silently lost.

Collection-facing structural/resource failures use CollectionError.

Storage Identity and Invalidation

References, raw pointers and slices derived from a dynamic array depend on its current backing storage incarnation.

Ordinary in-place replacement of an element does not by itself change backing identity.

A structural operation that grows or relocates backing may invalidate dependencies into the previous backing storage.

Such an operation is illegal while a conflicting live reference or slice requires the old backing incarnation to remain valid.

This is enforced by static ownership, borrowing and lifetime analysis. Sec does not add a runtime borrow checker to dynamic arrays.

Shared Array Properties

Both fixed and dynamic arrays expose these read-only properties:

Len
IsEmpty
Ptr
SizeOf

These are properties, not method calls.

Len

Len has type:

uint

For a fixed array:

let values: int[4] := [1, 2, 3, 4]
let count := values.Len

Len is the compile-time constant 4.

For a dynamic array:

let count := values.Len

Len is the current number of live logical elements.

It never means byte size or allocated capacity.

IsEmpty

IsEmpty is a read-only bool property:

if values.IsEmpty {
    return
}

It is semantically equivalent to:

values.Len == 0

For T[N], the result is a compile-time constant because N is part of the type.

Instance SizeOf

For contiguous arrays, instance SizeOf is the represented logical payload extent in bytes.

let values: int32[10]

let elements := values.Len
let bytes := values.SizeOf

Conceptually:

payload byte size = Len * element layout stride

Instance value.SizeOf is not the size of a dynamic-array descriptor.

It is also different from asking for the physical layout size of one type:

int32.SizeOf

Ptr

Arrays have contiguous addressable element storage and therefore expose the unsafe read-only Ptr property.

let pointer := values.Ptr

Ptr does not:

• transfer ownership;
• extend lifetime;
• pin storage;
• prevent dynamic-array relocation;
• create a safe Sec reference;
• make an FFI descriptor stable.

A pointer obtained from relocatable dynamic-array backing becomes invalid if a later legal storage transition replaces that backing.

For an empty array, the raw pointer value is implementation-defined under the raw-pointer rules and must not be dereferenced.

ToString

Arrays may expose the common formatting members:

value.ToString()
value.ToString(format)

Ordinary no-argument array formatting is type-oriented rather than an implicit dump of all stored elements.

Canonical type-oriented forms include:

int[4]  -> "int[4]"
int[]   -> "int[]"

Exact char[] and rune[] text conversions are intentional special cases governed by the string conversion rules.

A formatting operation that exposes array data must borrow rather than implicitly consume an owning array.

Dynamic Array Append

Append adds one element at logical index Len.

Its semantic result is:

Result[void, CollectionError]

Typical use:

try values.Append(value)

or with local handling:

try values.Append(value) {
    Err(error) => Handle(error)
}

The operation may require allocation and relocation.

Len increases only after element transfer and any required growth complete successfully.

Failure is atomic with respect to collection validity: the existing array remains valid and the incoming element is not silently discarded.

The canonical method name is Append. Push is not an alias.

Dynamic Array Clear

values.Clear()

Clear():

• destroys every live element;
• destroys elements in reverse logical index order;
• sets Len to zero;
• may retain reusable backing storage;
• does not allocate;
• does not expose or return internal capacity.

Clear() is infallible under the ordinary destruction rules.

Dynamic Array RemoveAt

RemoveAt removes ownership of one logical element:

let removed := values.RemoveAt(index)

Its result is:

Option[T]

An invalid index returns:

None

Ordinary absence is not an error.

A valid index:

• moves the removed element out;
• shifts every later live element one slot left;
• decrements Len;
• leaves no readable hole;
• does not default-construct a replacement;
• does not allocate;
• returns Some(removed).

For:

[A B C D E F G H]

removing index 5 produces:

[A B C D E G H]

and returns:

Some(F)

Order-preserving compaction is intentionally proportional to the number of later elements. T[] is not a sparse array.

Indexing

Arrays use zero-based indexing:

let first := values[0]

Valid fixed-array bounds are:

0 <= index < N

Valid dynamic-array bounds are:

0 <= index < Len

A statically known invalid index is a compile-time error. Runtime indexing follows Sec's checked access rules.

Indexing produces a place when the source and access mode permit it, so a mutable array element can be replaced through indexed assignment.

The complete indexing, checked-access, replacement and range-slicing rules are covered in the Indexing chapter.

Move-Only Elements Are Not Moved Out by Ordinary Indexing

Reading an indexed element does not silently extract ownership from the array.

If T is move-only, ordinary indexing cannot simply move values[index] out and leave an uninitialized hole behind.

Borrow the element when access is needed without ownership transfer.

For T[], RemoveAt(index) is the explicit owning extraction operation defined by the collection model.

Arrays and Slices

Both array kinds may act as sources for borrowed contiguous slices.

Slice types are:

ref T[]
ref mut T[]

Slice creation is explicit and uses reference syntax rather than helper methods.

Arrays do not require canonical methods named:

AsSlice()
AsMutableSlice()
Slice()

The Slices chapter defines slice creation, lifetime, mutability and invalidation in detail.

Iteration

Both fixed and dynamic arrays are directly iterable:

for item in values {
    Process(item)
}

Index plus element is also available:

for index, item in values {
    Process(index, item)
}

Borrowed iteration:

for ref item in values {
    Inspect(item)
}

Mutable borrowed iteration where authority permits:

for ref mut item in values {
    item.Reset()
}

Plain by-value iteration copies elements and therefore requires the element type to be copyable.

Iteration never silently moves move-only elements out of an owning array.

Structural operations that may relocate or resize a dynamic array are not permitted while active iteration depends on the current structure.

Equality

Fixed arrays support == and != when the element type supports equality.

let left: int[3] := [1, 2, 3]
let right: int[3] := [1, 2, 3]

if left == right {
    ...
}

Comparison is element-by-element in increasing index order.

Both operands must have the same fixed-array type, including the same length.

Dynamic-array content equality is not implied merely by the storage representation. Do not assume T[] has ordinary content == unless a relevant core/collection rule explicitly defines such an operation.

Parameters and Return Values

Fixed arrays

A fixed array passed by value follows the ordinary copy/move classification derived from its element type.

fn Consume(values: int[4]) void {
    ...
}

When the complete fixed-array type is copyable, ordinary by-value transfer may copy it. If its elements make it move-only, the array follows move semantics.

Dynamic arrays

A by-value T[] parameter receives ownership of the dynamic array:

fn ConsumeOwned(values: Packet[]) void {
    ...
}

Because T[] is move-only, reusable named owners follow the normal explicit consuming-transfer rules at consuming boundaries.

Borrowing arrays

When a function only needs a borrowed contiguous sequence, use a slice parameter:

fn Sum(values: ref int[]) int {
    ...
}

fn ClearBytes(values: ref mut byte[]) void {
    ...
}

This avoids transferring ownership of the array.

Destruction

Fixed arrays

A fixed array destroys live elements in reverse index order.

N - 1
...
1
0

Array destruction follows the element type's ordinary destruction semantics.

Dynamic arrays

A dynamic array destroys live elements in reverse logical index order.

After element destruction, its owning storage lifetime ends and backing reclamation follows the resolved allocation/reclamation policy.

Element ownership and raw backing reclamation are separate responsibilities. For example, an arena-backed dynamic array still owns and destroys its live element objects even when an arena policy owns raw storage reclamation.

Choosing Fixed or Dynamic Arrays

Use T[N] when:

• the number of elements is part of the type contract;
• layout must be known at compile time;
• inline fixed-size representation is desirable;
• the array must participate in exact binary or aggregate layout;
• growth is neither required nor meaningful.

Use T[] when:

• the element count is runtime state;
• the collection must grow;
• simple ordered contiguous ownership is sufficient;
• the minimal Append/Clear/RemoveAt surface is appropriate.

If a richer sequence API is required, use list[T] rather than turning T[] into a general-purpose collection framework.

Dynamic Array vs list[T]

T[] is intentionally a small fundamental dynamic owning array.

Its canonical mutable surface is centered on:

Append(value)
Clear()
RemoveAt(index)

It deliberately does not expose the richer sequence-management surface expected from list[T].

In particular, T[] does not expose public source-visible capacity, reserve or resize operations in Sec 0.1.

This keeps the fundamental array model small while allowing list[T] to own richer collection behavior.

Diagnostics

Important array diagnostics include:

• negative or non-integer fixed-array length;
• runtime-dependent fixed-array length;
• fixed-array length constant overflow;
• fixed-array layout exceeding target limits;
• non-defaultable element type in an uninitialized non-empty mutable fixed array;
• immutable array declaration without required initialization;
• array literal element-count mismatch;
• array literal element-type mismatch;
• empty literal without enough target context;
• fixed-array spread whose final length does not match the target;
• implicit copy attempt of move-only T[];
• dynamic-array growth without a valid allocation context;
• structural mutation while a conflicting reference, slice or iteration dependency is live;
• invalid array index;
• attempt to move a move-only element out through ordinary indexing;
• use of non-canonical members such as Push, Reserve or AsSlice.

For example:

error: Packet[] is move-only

this assignment would require an implicit deep copy of the owning dynamic array

help: move the owner at a consuming boundary
help: borrow it as ref Packet[] when ownership transfer is not intended

Tooling should distinguish clearly between:

T[N]
T[]
ref T[]
ref mut T[]

because they have different ownership and lifetime semantics even when all describe contiguous elements.

Best Practices

• Use T[N] when the element count belongs in the type contract.
• Use T[] for simple runtime-sized owning contiguous storage.
• Use list[T] when a richer dynamic sequence API is needed.
• Use ref T[] or ref mut T[] when a function only needs borrowed contiguous access.
• Prefer array literals for concise fixed-array initialization.
• Remember that an inferred [1, 2, 3] is a fixed array, not a dynamic owner.
• Use Append, not Push, for T[].
• Handle Append failure because growth may require resources.
• Use RemoveAt when ownership of one dynamic-array element must be extracted.
• Do not depend on hidden capacity or growth policy.
• Do not retain raw Ptr across operations that may relocate dynamic-array backing.
• Use explicit slices rather than helper methods such as AsSlice().

Summary

• Sec has two owning array forms: fixed T[N] and dynamic T[].
• T[N] has compile-time length and contiguous owned elements.
• The fixed length participates in type identity.
• Fixed-array length must be a non-negative compile-time integer representable by uint.
• Zero-length fixed arrays are valid.
• A fixed array has no hidden pointer, length field, capacity field or allocator identity.
• Nested fixed arrays use postfix dimensions from outermost to innermost.
• A mutable fixed array may omit its initializer only when every element can be default-constructed.
• Zero-length fixed arrays are defaultable even when the element type is not.
• Immutable fixed arrays require initialization.
• Bracket literals such as [1, 2, 3] construct fixed arrays under the fixed-array literal rules.
• A non-empty literal may infer T[N] when all elements resolve to one type.
• An empty bracket literal requires target context.
• Spread is allowed in fixed-array literals when the complete resulting length is compile-time known and matches the target.
• T[] is a first-class owning dynamic array.
• Dynamic-array length is runtime state and is not part of type identity.
• Every T[] is move-only regardless of whether T is copyable.
• A mutable T[] may default-construct as an empty owner without allocation.
• The empty dynamic default does not require T to be defaultable.
• Dynamic-array internal capacity is not public Sec 0.1 state.
• T[] does not expose canonical Capacity, Reserve or Resize members.
• Growth may require allocation, but Sec does not assume one hidden global heap.
• Dynamic-array growth is transactional.
• Backing relocation may invalidate references, slices and raw pointers tied to the old backing.
• Both array kinds expose read-only Len, IsEmpty, Ptr and SizeOf.
• Len is a logical element count of type uint.
• Instance SizeOf describes logical payload bytes, not a dynamic-array descriptor size.
• Ptr is unsafe and does not extend lifetime or pin storage.
• Ordinary array ToString() is type-oriented; exact char/rune text conversions are special cases.
• Dynamic-array Append returns Result[void, CollectionError].
• Append is atomic with respect to array validity on failure.
• Push is not an alias for Append.
• Clear() destroys all live elements in reverse order and resets Len to zero.
• RemoveAt(index) returns Option[T].
• A valid RemoveAt moves the removed element out and compacts later elements left.
• An invalid RemoveAt index returns None; normal absence is not an error.
• Arrays use zero-based indexing.
• Ordinary indexing never silently moves a move-only element out of an owning array.
• Dynamic-array RemoveAt is the explicit owning extraction operation.
• Arrays can provide explicit borrowed slices; slices do not own their elements.
• Arrays do not require AsSlice(), AsMutableSlice() or Slice() helpers.
• Fixed and dynamic arrays are directly iterable.
• Plain iteration copies elements and therefore requires copyable element values.
• Borrowed iteration uses ref or ref mut where permitted.
• Fixed arrays support element-wise ==/!= when T supports equality.
• Dynamic-array content equality is not implied merely by representation.
• Fixed-array by-value transfer follows the complete array's ordinary copy/move classification.
• Dynamic-array by-value transfer moves ownership.
• Fixed and dynamic arrays destroy live elements in reverse logical index order.
• T[] is intentionally smaller than the richer list[T] collection.