Indexing

Indexing Produces a Place

An index expression does not inherently mean “copy this value”.

These expressions begin from the same indexed place:

let value := values[index]
values[index] = replacement
let element := ref values[index]
let element := ref mut values[index]

The use context determines the operation:

This model is important for ownership. The compiler does not decide that every indexed read is a copy, and it does not silently move a move-only value out of an owning collection.

Valid Index Types

Linear sequence indexes may use:

• built-in signed integer types;
• built-in unsigned integer types;
• compatible named integer types without incompatible unit dimensions.

Examples:

let a := values[0]

let index: int := ReadIndex()
let b := values[index]

let unsignedIndex: uint := ReadUnsignedIndex()
let c := values[unsignedIndex]

type RowIndex uint

let row: RowIndex := RowIndex(2)
let d := values[row]

The index does not need to have one single mandated integer width. It must belong to a valid integer index category and be representable for the access being checked.

Invalid Index Types

These are not ordinary linear index types:

float
decimal
bool
string

For example:

values[1.5]       // invalid
values[true]      // invalid
values["first"]   // invalid

A unit-bearing numeric value is not automatically an index merely because its underlying numeric representation is integer-like.

Indexing represents a logical position, not a physical quantity. A named integer type may participate only when its semantic type is compatible with index use.

Zero-Based Indexing

Linear Sec collections use zero-based indexes.

For:

let values: int[4] := [10, 20, 30, 40]

the valid positions are:

values[0]    // 10
values[1]    // 20
values[2]    // 30
values[3]    // 40

This is outside the array:

values[4]

Negative signed indexes are also out of bounds:

values[-1]

Bounds

For a fixed array T[N]:

0 <= index < N

For a dynamic array, slice or list[T]:

0 <= index < Len

Bounds are part of Sec's safe indexing semantics.

Indexing does not become unchecked merely because the compiler eventually lowers it to pointer arithmetic or target address calculations.

Static Proof vs Runtime Check

Sec follows the same “static proof first” model for indexing that it uses for other checked language operations.

For example:

let values: int[4] := [10, 20, 30, 40]

let first := values[0]    // statically valid
let invalid := values[4]  // compile-time error

But:

fn Read(values: ref int[], index: int) int {
    return values[index]
}

requires a runtime bounds decision unless surrounding analysis has already proved the index valid.

Ordinary Checked Indexing

The ordinary form is:

let value := values[index]

When bounds cannot be proven statically, Sec emits a runtime check.

If the check fails, the ordinary operation follows Sec's panic-capable checked operation path.

This does not imply a mandatory exception runtime. The check may lower to inline branches, a target trap, a selected panic endpoint, or another valid target mechanism.

The important source-level guarantee is that safe ordinary indexing never performs an unchecked out-of-bounds memory access.

Fallible Indexing

Code that must remain panic-free may make the bounds failure explicit:

let value := try values[index]

A failed bounds check produces:

IndexError.OutOfBounds

The enclosing function must be able to propagate that error, or the expression must handle or map it according to the ordinary try rules.

For example:

fn Read(
    values: ref int[],
    index: int,
) Result[int, IndexError] {
    let value := try values[index]
    return Ok(value)
}

try converts the language-defined bounds check into fallible control flow. It is not exception catching.

Bounds Check Elimination

A source-level checked access does not imply that a runtime check must remain in generated code.

The compiler may prove safety through:

• constant evaluation;
• fixed array length;
• range contracts;
• branch refinement;
• assert refinement;
• loop induction;
• generic specialization;
• whole-program analysis.

If the compiler proves 0 <= index < Len, it may remove the runtime bounds check while preserving the exact source semantics.

The programmer does not need to switch to unsafe code merely to obtain efficient indexing.

Reading an Indexed Element

let value := values[index]

Reading through an indexed place follows ordinary value semantics.

If the element type is implicitly copyable, a normal value read can copy the element into the destination.

If the element is not copyable, ordinary indexed syntax does not gain special permission to remove ownership from the source.

Borrowing an Indexed Element

Create a shared element borrow with:

let element := ref values[index]

The source must provide stable addressable element storage and shared borrow authority.

The resulting ref T cannot outlive the source storage or the storage incarnation from which it was derived.

Normal aliasing and lifetime rules apply.

Mutable Element Borrows

Create an exclusive mutable element borrow with:

let element := ref mut values[index]

The source must provide mutable authority to that element place.

While the mutable borrow is live, conflicting direct or borrowed access is rejected.

Two runtime indexes are not assumed to refer to different elements merely because they are syntactically different:

let left := ref mut values[a]
let right := ref mut values[b]

The compiler needs a valid disjointness proof before both exclusive borrows may remain live together.

Indexed Assignment

A mutable indexed place may be replaced:

values[index] = replacement

Indexed assignment requires:

• a valid index;
• a mutable element place;
• a replacement assignable to the element type;
• no conflicting live borrow;
• valid ownership transfer for the replacement.

This is invalid:

let values: int[3] := [1, 2, 3]
values[0] = 10

because the array binding does not provide the mutable authority required for replacement.

This is also invalid:

let mut values: int[3] := [1, 2, 3]
values[1] = "two"

because the replacement value is not assignable to int.

Replacement Evaluation Order

Sec does not destroy the existing element before the replacement expression is ready.

Conceptually, indexed replacement performs:

1. evaluate the target and index as required by ordinary expression order;
2. validate or establish the indexed place;
3. fully evaluate the replacement value;
4. validate the ownership transfer;
5. destroy the old owned element exactly once;
6. install the replacement.

This prevents a failed replacement expression from leaving a readable collection element uninitialized.

For fallible bounds access, the check also occurs before destructive replacement can commit.

Move-Only Elements

Ordinary indexing never silently extracts a move-only value from an owning collection.

For a move-only Resource:

let value := resources[index]

is invalid if satisfying the read would require moving ownership out of the collection element.

Borrow instead:

let value := ref resources[index]

For a dynamic array, explicit owning extraction is provided by:

let removed := resources.RemoveAt(index)

A slice cannot extract ownership at all because the slice does not own its elements.

Fixed Array Indexing

For:

T[N]

the valid range is:

0..<N

Because N is part of the type, constant indexes can often be proven valid or invalid during compilation.

let values: int[4] := [10, 20, 30, 40]

let first := values[0]    // valid
let last := values[3]     // valid
let bad := values[4]      // compile-time error

Runtime integer indexes are still permitted and use the checked indexing model.

Dynamic Array Indexing

For an owning dynamic array:

T[]

the current valid range is:

0..<Len

Indexing does not expose internal capacity. A position between Len and hidden capacity is not a valid element.

Dynamic arrays may relocate their backing storage during structural growth. A direct element borrow therefore depends on the current backing incarnation and may block operations that could invalidate it.

Slice Indexing

For:

ref T[]
ref mut T[]

the valid range is:

0..<Len

Slice indexes are relative to the slice's logical origin, not necessarily to the original owner's index zero.

For example:

let values: int[5] := [10, 20, 30, 40, 50]
let middle := ref values[1..<4]

let first := middle[0]

middle[0] refers to the first represented slice element, which is values[1].

A shared slice supports reads and shared borrows. A mutable slice may additionally support mutable borrows and replacement.

list[T] Indexing

list[T] guarantees ordered logical element storage and supports ordinary linear indexing.

Bounds are:

0..<Len

The same integer index categories, checked access model, place semantics, borrowing rules and replacement rules apply.

Structural list operations remain separate from indexed element access. Indexing one element does not imply permission to insert or remove sequence elements.

Nested Fixed Arrays Use Chained Indexing

For:

int[2][3]

the outer element type is int[3].

Use chained indexing:

let mut matrix: int[2][3] := [
    [1, 2, 3],
    [4, 5, 6],
]

matrix[0][0] = 10
matrix[1][2] = 60

The first index selects the outer array element. The second index selects an element from that inner fixed array.

This is different from shaped matrix/tensor indexing, which uses one selector per axis in a single bracket expression.

Strings Are Not Indexable Arrays

string is not an implicit array of byte, char or rune.

Ordinary array indexing does not apply directly:

let character := text[index]    // not ordinary string indexing

String access uses the public string API and string iteration rules.

This avoids making an ambiguous promise about whether an integer string index would mean:

• UTF-8 byte offset;
• Unicode scalar index;
• grapheme-cluster index.

When byte-oriented access is required, convert or obtain the explicitly defined byte representation instead of treating string as byte[].

Map Indexing

Maps also use bracket syntax:

users[key]

But the expression means key lookup, not integer positional indexing.

For:

map[K, V]

the bracket expression accepts a key compatible with K and selects the associated V entry when one exists.

Map order is unspecified, so numeric map indexes have no positional sequence meaning unless the map's key type itself is numeric.

Map Indexed Lookup

let user := users[id]

A successful lookup produces the value place for the existing entry. The use context then determines whether the value is copied, shared-borrowed or mutable-borrowed.

Examples:

let user := users[id]
let user := ref users[id]
let user := ref mut users[id]

A missing key is a checked access failure using the canonical map key-access error family.

The panic-free form may use ordinary try according to the fallible-access rules.

Reading users[id] never inserts a missing entry.

Map Indexed Assignment

Map insertion and replacement use indexed assignment:

try users[id] = user

Semantics:

existing key:
    replace the stored value

missing key:
    insert a new key/value entry

Because inserting a missing key may require structural growth or resources, the operation may be fallible.

Collection-facing structural failure uses the collection error contract.

The assignment does not use :=. := remains declaration/initialization syntax.

Where an explicit ownership move is required and permitted:

try users[id] <- user

follows the ordinary move-assignment rules.

Sets Are Not Indexed

A set[T] stores unique values but does not define positional or key-to-value indexing.

Use membership, insertion, removal and iteration operations instead.

This is not set access syntax:

activeUsers[0]

A set's iteration order is unspecified, so exposing a positional index would create semantics the base set contract deliberately does not provide.

Shaped Indexing

vector, matrix, tensor and tensor_view use shaped indexing rules.

Unlike nested ordinary arrays, multidimensional shaped types use one bracket expression with one selector per source axis.

matrix[row, column]
tensor[channel, y, x]

A selector may be a scalar index or a range selector.

One Selector per Axis

For a rank-three tensor, structurally valid forms include:

value[i, j, k]
value[i, .., k]
value[.., .., ..]

Sec requires exactly one selector per source axis.

It does not implicitly append omitted trailing .. selectors.

Core shaped slicing has no ellipsis selector.

Thus this style is not used:

value[i, ...]

Shaped Scalar Selectors

A scalar selector removes one axis from the result.

If every selector is scalar:

let element := value[i, j, k]

the result is an element Place[T].

Sec does not create a rank-zero tensor merely to represent a fully scalar-indexed element.

The ordinary place rules then determine read, borrow, mutable borrow or replacement.

Shaped Range Selectors

A range selector preserves its axis.

Examples:

matrix[2, ..]
matrix[.., 2]
tensor[1, .., 2]
tensor[1..<3, .., 4..<10]

When at least one axis remains, the result is a borrowed shaped view:

ref tensor_view[T, ResultRank]

or, when mutable authority and mapping rules permit:

ref mut tensor_view[T, ResultRank]

Shaped slicing:

• does not allocate;
• does not copy elements;
• preserves backing identity;
• preserves memory-space identity;
• derives new shape and strides;
• recomputes contiguity.

Shaped Range step

Shaped range selectors support Sec's existing step syntax:

value[.. step 2]
value[10..<90 step 2]
value[.. step -1]

Positive step creates a forward strided view. Negative step creates a reverse strided view.

step 0 is invalid.

This is deliberately different from ordinary one-dimensional slice creation, whose standard slice range is contiguous and non-descending.

Shaped views can express non-unit and negative strides because the shaped view model explicitly carries stride semantics.

Shaped Bounds and Range Checks

Shaped indexing follows the same static-proof-first model.

Statically invalid examples are compile-time errors:

• out-of-bounds scalar index;
• invalid static range;
• wrong number of axis selectors;
• known step 0;
• invalid static axis index.

Runtime-dependent scalar indexing uses IndexError on the fallible path.

Runtime-dependent shaped ranges use RangeError on the fallible path.

The compiler may eliminate checks after proving shape and index facts.

Raw Pointers Do Not Use Safe Collection Indexing

RawPtr[T] is an unchecked address value, not a bounded Sec sequence.

The raw-pointer model therefore does not gain ordinary safe pointer[index] collection semantics.

Pointer traversal uses explicit unsafe operations such as:

pointer.Offset(elements)
pointer.Read()
pointer.Write(value)

A raw pointer carries no implicit bounds merely because its pointee type is known.

If bounded safe access is desired, establish a valid safe reference or slice under the raw-to-safe construction rules and use the resulting safe abstraction.

unsafe Does Not Disable Bounds Checks

Safe array, slice, list and shaped indexing retain their normal bounds semantics inside unsafe.

unsafe {
    let value := values[index]
}

remains an ordinary checked safe index operation.

unsafe accepts proof obligations for operations that are defined as unsafe; it does not reinterpret safe indexing as unchecked memory access.

Truly unchecked traversal belongs to raw-pointer operations.

Ownership, Borrowing and Lifetime Interaction

Indexed places participate in the same ownership model as named fields and other places.

The compiler tracks:

• whether the source is available;
• whether the element type is copyable or move-only;
• shared and exclusive borrows of the selected place;
• possible aliasing between runtime indexes;
• storage identity and backing generation;
• structural mutations that may invalidate indexed borrows;
• destruction of replaced owned elements.

An indexed borrow into a relocatable dynamic collection remains tied to the current backing incarnation.

A later operation that may relocate or invalidate that backing conflicts with the live borrow.

Evaluation Order

Indexing follows Sec's ordinary expression evaluation order.

For:

GetValues()[NextIndex()] = BuildReplacement()

the compiler must preserve source-visible evaluation and side effects.

It may not duplicate:

• the target expression;
• the index expression;
• the replacement expression.

The bounds decision and ownership checks occur at the semantic access boundary before a destructive replacement commits.

Optimization may eliminate redundant checks or address calculations only when the observable behavior remains unchanged.

Diagnostics

Important indexing diagnostics include:

• target type is not indexable;
• invalid index type;
• negative constant index;
• constant index equal to or beyond the sequence length;
• runtime bounds failure on the fallible path;
• assignment through an immutable element place;
• replacement type mismatch;
• conflicting borrow of the indexed element;
• attempted move of a move-only element through ordinary indexing;
• use of a unit-bearing value as a logical index when incompatible;
• string indexed as though it were an array;
• set indexed as though it were an ordered sequence;
• map key type mismatch;
• map lookup missing key on a checked access path;
• map indexed assignment structural/resource failure;
• wrong selector count for a shaped value;
• invalid shaped scalar index;
• invalid shaped range;
• shaped step 0;
• safe indexing incorrectly assumed unchecked inside unsafe.

A constant bounds diagnostic should be direct:

array index 4 is out of bounds for int[4]

valid indexes are 0..<4

A move-only diagnostic should explain the ownership alternative:

cannot move Resource out through ordinary indexing

help: borrow the element with `ref resources[index]`
help: use an explicit owning extraction operation when the collection provides one

Tooling should show proven index ranges where useful and may explain why a runtime bounds check was removed or remains necessary.

Best Practices

• Use direct indexing when the access naturally refers to one logical position.
• Use try target[index] when a runtime out-of-bounds condition must be handled without panic.
• Prefer branch/range facts that let the compiler prove indexes safe rather than switching to unsafe access.
• Borrow move-only elements instead of trying to extract them through ordinary indexing.
• Use collection-specific removal operations when ownership extraction is the real intent.
• Use ref mut target[index] only when exclusive element mutation is required.
• Do not assume two runtime indexes are disjoint without a proof.
• Remember that slice indexes are relative to the slice origin.
• Use chained indexing for nested ordinary arrays.
• Use comma-separated axis selectors for shaped values.
• Do not index string as an array; use the string API or explicit byte/rune conversions.
• Do not assume sets have positional indexing.
• Use explicit raw-pointer operations for genuinely unchecked memory traversal.

Summary

• Linear sequence indexing uses target[index].
• For linear sequences, indexing produces an element Place.
• The use context determines read, shared borrow, mutable borrow or replacement.
• Valid linear index types include signed integers, unsigned integers and compatible named integer types.
• Float, decimal, bool and string are not ordinary linear index types.
• Incompatible unit-bearing numeric values are not logical indexes.
• Linear sequence indexing is zero-based.
• Negative signed indexes are out of bounds and do not mean “from the end”.
• Fixed-array bounds are 0 <= index < N.
• Dynamic-array, slice and list bounds are 0 <= index < Len.
• A statically proven invalid access is a compile-time error.
• A statically proven valid access may require no runtime bounds check.
• A runtime-dependent ordinary access is checked and may carry a panic effect.
• try target[index] selects the panic-free fallible access path.
• Fallible ordinary bounds access produces IndexError.OutOfBounds.
• The compiler may eliminate bounds checks using range, branch, loop and specialization proofs.
• A copyable indexed element may be read by value.
• An indexed element may be borrowed with ref.
• A mutable element place may be borrowed with ref mut.
• Indexed assignment requires mutable authority, a compatible replacement and no conflicting borrow.
• The replacement is fully evaluated before the old owned element is destroyed.
• Ordinary indexing never silently moves a move-only value out of an owning collection.
• Dynamic-array RemoveAt is an explicit owning extraction operation.
• A slice never transfers ownership through indexing.
• Fixed arrays often permit complete compile-time index validation because length is part of the type.
• Dynamic-array indexes are bounded by live Len, not hidden capacity.
• Slice indexes are relative to the slice's logical origin.
• list[T] uses the same linear indexing model.
• Nested ordinary arrays use chained indexing such as matrix[1][2].
• string is not implicitly indexable as byte, char or rune storage.
• Map bracket syntax performs key lookup rather than positional indexing.
• A successful map lookup produces the stored value Place.
• A missing map key is a checked key-access failure and does not insert.
• Map indexed assignment performs replacement or insertion.
• Potentially structural map assignment uses explicit fallible syntax such as try users[id] = user.
• Sets have no positional indexing.
• Multidimensional shaped indexing supplies exactly one selector per source axis.
• A shaped scalar selector removes one axis.
• Full scalar shaped indexing yields Place[T], not a rank-zero tensor.
• A shaped range selector preserves an axis and yields a tensor view when at least one axis remains.
• Shaped ranges may use positive or negative step; step 0 is invalid.
• Runtime shaped scalar access uses IndexError on the fallible path.
• Runtime shaped range access uses RangeError on the fallible path.
• RawPtr[T] does not gain safe collection indexing or implicit bounds.
• Raw traversal uses explicit unsafe operations such as Offset, Read and Write.
• unsafe does not disable bounds checks on otherwise safe indexing operations.
• Indexed references remain subject to ordinary ownership, borrow, lifetime and backing-invalidation rules.