language-reference.md

Language Reference

This page documents the Strata source surface accepted by the buildable slice. It is an authoring reference for .str programs, not a description of Mantle artifact internals.

Source Surface

Area	Accepted Surface
Source unit	One module name; declaration per file.
Top-level declarations	record, enum, fn, and proc.
Classes	Not available.
Methods	Not available.
Top-level functions	Pure deterministic one-argument source helpers.
Process functions	init, step, and pure deterministic one-argument process-local helpers.
Imports	Not available.
Standard library	Not available.
Effects	emit, spawn, and send.
Process references	let worker: ProcessRef<Worker> = spawn Worker;, send worker Ping;, and send reply_to Done; for received typed references.
Collections	Immutable List<T,N> and Map<K,V,N> source values with explicit List[...] and Map[key => value] constructors.
Patterns	Constructor patterns, constructor payload bindings, nested constructor and record/list/map payload destructuring in helpers and step/state matches, helper return-match expressions, and _ wildcards.
Message payloads	enum WorkerMsg { Assign(Job) }, enum WorkerMsg { Work(ProcessRef<Sink>) }, collection payloads, payload sends, and payload-binding step patterns.
Pattern dispatch	Function signature patterns, source function match bodies, helper return-match expressions, fieldless enum matches in init, step parameter patterns, wildcard step patterns, one whole-body match msg step form per process, and whole-body match state inside message-specific step clauses.
Transition result	ProcResult<T> with Continue(value), Stop(value), and Panic(value).

The module declaration names a source unit. It does not create an import namespace, package, library, or visibility boundary.

Source Unit

A Strata source file starts with a module declaration:

module hello;

After the module declaration, the accepted top-level declarations are records, enums, source functions, and processes.

module example;

record MainState;
enum MainMsg { Start }

fn identity_state(state: MainState) -> MainState ! [] ~ [] @det {
    return state;
}

proc Main mailbox bounded(1) {
    type State = MainState;
    type Msg = MainMsg;

    fn init() -> MainState ! [] ~ [] @det {
        return MainState;
    }

    fn step(state: MainState, Start) -> ProcResult<MainState> ! [] ~ [] @det {
        return Stop(state);
    }
}

Every buildable program must declare a Main process. Mantle starts Main and delivers the first message variant of Main's message enum as the entry message.

Identifiers

Identifiers must start with an ASCII letter or _, then contain only ASCII letters, ASCII digits, or _. The single _ token is reserved for wildcard patterns and cannot be used as an identifier.

Valid examples:

Main
Worker_1
_InternalState

Invalid examples:

1Main
worker-name
_

as, let, mut, and var are reserved everywhere identifiers are accepted. ProcResult, ProcessRef, List, and Map are reserved type names because they name built-in transition, process-reference, and collection types. Type names beginning with __strata_checked_ are reserved for checked IR and artifact metadata. Checked process-reference artifact labels under that prefix are keyed by resolved process IDs, not source process names.

Records

Records define structured state values. A fieldless record uses a semicolon:

record MainState;

A record with fields uses braces and does not take a semicolon after the closing brace:

enum Phase { Idle, Done }

record WorkerState {
    phase: Phase,
}

Record fields are immutable. mut and var field declarations are rejected.

Record values use constructor syntax:

WorkerState { phase: Idle }

Fieldless record values are written as the record name:

MainState

Record value fields use :, not =. A braced record value must provide every declared field exactly once; missing, duplicate, or unknown fields are rejected.

Payload-bearing enum values use constructor syntax with one immutable payload value:

Assigned(Job { phase: Ready })

The checker resolves this form against the expected enum type. If the identifier names a source helper instead, it is expanded as a helper call; constructor and helper names cannot collide silently.

Collections

Lists and maps are immutable source values with explicit numeric capacities. They can be used as source helper parameters and return values, record fields, process state types, and message payloads when their element, key, and value types are source value types.

List<Phase,2>[Ready, Done]
Map<Phase,Phase,1>[Ready => Done]

Collection constructors are explicit. Bare [Ready, Done] and { Ready: Done } forms are not admitted in this slice. Map keys are canonical source values; a map value or map pattern that repeats a canonical key is rejected. List and map patterns are exact by default. List rest patterns are suffix-only:

List[first, second] // exact list length
List[first, ..tail] // first must exist; tail is the unmatched suffix

..tail binds an immutable whole list containing entries after the fixed prefix. If the matched value has type List<T,N> and the pattern lists M fixed prefix elements, the tail binding has type List<T,N-M>. The actual tail value may contain fewer entries because bounded list values may be shorter than capacity. Arbitrary prefix/rest/suffix matching remains deferred.

A trailing .. marker makes a map pattern a subset pattern over the listed static keys:

Map[Ready => selected]     // exact key set
Map[Ready => selected, ..] // Ready must exist; extra keys are allowed
Map[Ready => selected, ..rest] // rest binds a map without Ready

Map ..rest binds an immutable whole map containing entries except the listed static keys. If the matched value has type Map<K,V,N> and the pattern lists M distinct static keys, the rest binding has type Map<K,V,N-M>. The actual rest value may contain fewer entries because subset patterns still match maps that omit unlisted keys.

Overlapping exact and subset map patterns are rejected instead of relying on source order or specificity. Subset overlap is capacity-aware: two subset patterns overlap when one bounded map can contain both required key sets. Runtime-bound map value keys must be static source values in this slice; dynamic-key dictionaries remain deferred. Rest binding does not expose collection iteration, order-dependent dispatch, mutation, dynamic keys, or mutable views.

Collection pattern element and map-value positions may contain nested structural patterns, such as List[Job { phase }, ..tail] or Map[Ready => Job { phase }, ..rest]. Map nesting still uses only the listed static keys; dynamic-key map dispatch remains outside this source slice.

Record field order and map entry order are preserved in source-authored values, emitted artifact values, labels, and traces. Projection still addresses map entries by key, and this slice does not expose source-level map iteration or order-dependent dispatch.

Enums

Enums define named variants:

enum MainMsg {
    Start,
}

enum WorkerState {
    Idle,
    Handled,
}

enum WorkerMsg {
    Assign(Job),
    Stop,
}

Enums used as process state or message types must declare at least one variant. Duplicate variants are rejected. Payload variants are accepted for process state and message enums. Process state payloads remain immutable whole-state values admitted through typed state IDs.

Processes

A process declares a mailbox bound, a state type, a message type, an init function, and one step clause for each accepted message:

proc Worker mailbox bounded(1) {
    type State = WorkerState;
    type Msg = WorkerMsg;

    fn init() -> WorkerState ! [] ~ [] @det {
        return Idle;
    }

    fn step(state: WorkerState, Ping) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
        emit "worker handled Ping";
        return Stop(Handled);
    }
}

Only the aliases State and Msg are accepted inside a process. Processes may also declare pure deterministic helper functions alongside init and step. Each message variant must resolve to exactly one step clause, selected by an explicit constructor pattern, by one wildcard pattern, or by one whole-body match msg. A message-specific step clause can also dispatch over current state with a whole-body match state. A process cannot mix parameter-pattern or state-match step clauses with a match msg step body in this slice.

Function Signatures

The accepted function signature shape is:

fn name(params...) -> ReturnType ! [effects] ~ [may_behaviors] @det {
    ...
}

Buildable source requires:

Function	Required Shape
init	No parameters, returns the process state type, uses ! [] ~ [] @det.
parameter-pattern step	Parameters exactly state: StateType, MessagePattern, returns ProcResult<StateType>, uses ~ [] @det.
match step	Parameters exactly state: StateType, msg: MsgType, returns ProcResult<StateType>, uses ~ [] @det, and has a whole-body match msg.
state-match step	Parameters exactly state: StateType, MessagePattern, returns ProcResult<StateType>, uses ~ [] @det, and has a whole-body match state.
source helper	One binding parameter or one pattern parameter, returns a source value type, uses ! [] ~ [] @det, and has no runtime statements.

The parser recognizes @nondet, but buildable source rejects it. The may-behavior list after ~ must be empty.

Normal source functions are checked before lowering and expanded into the value positions where they are called. They do not become Mantle runtime dispatch entries and cannot perform runtime effects. A process-local helper is visible only inside that process. A module helper is visible throughout the module. Recursive helper call cycles are rejected in this source slice.

Function signature patterns can author enum dispatch:

fn readiness(Cold) -> Readiness ! [] ~ [] @det {
    return ColdReady;
}

fn readiness(Warm) -> Readiness ! [] ~ [] @det {
    return WarmReady;
}

fn status(Assigned(job: Job)) -> WorkStatus ! [] ~ [] @det {
    return Active(job);
}

A source helper signature may also destructure fields from an immutable record value:

fn phase_of(Job { phase }) -> JobPhase ! [] ~ [] @det {
    return phase;
}

fn renamed_phase(Job { phase: current }) -> JobPhase ! [] ~ [] @det {
    return current;
}

Source helper signatures may also dispatch on exact immutable collection shapes:

fn first(List<Phase,2>[phase, _]) -> Phase ! [] ~ [] @det {
    return phase;
}

fn lookup(Map<Phase,Phase,1>[Ready => selected]) -> Phase ! [] ~ [] @det {
    return selected;
}

Nested helper patterns compose constructor payloads, records, and collection element/value projections:

fn routed_phase(Assign(Job { phase })) -> Phase ! [] ~ [] @det {
    return phase;
}

fn listed_phase(List<Routed,1>[Assign(Job { phase })]) -> Phase ! [] ~ [] @det {
    return phase;
}

A helper may also use a whole-body match over its typed binding parameter:

fn readiness_body(mode: StartupMode) -> Readiness ! [] ~ [] @det {
    match mode {
        Cold => {
            return ColdReady;
        }
        Warm => {
            return WarmReady;
        }
    }
}

Whole-body helper matches and helper return-match expressions may split one top-level constructor when nested typed enum predicates are provably disjoint. The split remains checker-time source dispatch; helper expansion resolves the concrete source value before lowering:

fn route(packet: Packet) -> Phase ! [] ~ [] @det {
    match packet {
        Envelope(Assign(Ready)) => {
            return Ready;
        }
        Envelope(Assign(Done)) => {
            return Done;
        }
    }
}

Whole-body helper matches may also destructure a concrete record binding:

fn phase_of(job: Job) -> JobPhase ! [] ~ [] @det {
    match job {
        Job { phase } => {
            return phase;
        }
    }
}

Whole-body helper matches can destructure exact list patterns, suffix-only list rest patterns, exact map patterns, and map subset/rest patterns. A wildcard arm may provide a fallback for collection shapes that are not listed:

fn first_or_unknown(items: List<Phase,1>) -> Phase ! [] ~ [] @det {
    match items {
        List[phase] => {
            return phase;
        }
        _ => {
            return Unknown;
        }
    }
}

Or a block body may return a match over an in-scope source value binding:

fn status(work: Work) -> WorkStatus ! [] ~ [] @det {
    return match work {
        Empty => {
            return Idle;
        }
        Assigned(job: Job) => {
            return Active(job);
        }
    };
}

The same helper return-match form may destructure a concrete record binding:

fn phase_of(job: Job) -> JobPhase ! [] ~ [] @det {
    return match job {
        Job { phase } => {
            return phase;
        }
    };
}

Collection return matches use the same collection patterns:

fn ready_value(items: Map<Phase,Phase,2>) -> Phase ! [] ~ [] @det {
    return match items {
        Map[Ready => selected, ..rest] => {
            return selected;
        }
        _ => {
            return Unknown;
        }
    };
}

Enum matches are exhaustive and immutable. Source helper whole-body matches and helper return-match expressions may repeat a top-level constructor only when the nested typed enum predicates are provably disjoint; identical predicates, unguarded constructor arms, and unproven overlaps are rejected. Source helper signature groups still keep one clause per top-level constructor. Record body matches and return matches use one record pattern arm for the matched record type. Collection patterns match exact list length unless they use the trailing ..tail suffix rest binding. Map patterns match exact key sets unless they use the trailing .. subset or rest marker. _ remains available as a collection fallback in helper match bodies and return matches. Payload-bearing source helper patterns and record/list/map destructuring patterns bind immutable source values. A helper call must provide a concrete enum constructor value for signature-pattern, whole-body match, or enum helper return-match dispatch. Record and collection destructuring helpers require a concrete value argument after source helper expansion. Helpers are still expanded before lowering and do not become runtime dispatch entries.

Statements

The accepted statements are:

emit "text";
let worker: ProcessRef<Worker> = spawn Worker;
send worker Ping;
return Stop(state);
return Continue(next_state);
return Panic(failed_state);

emit records and prints an output literal. Output literals must be non-empty, must not contain control characters, and do not support string escapes in this slice.

spawn starts another declared process and returns an immutable typed process reference. The reference binding is local to the transition and must be typed as ProcessRef<TargetProcess>.

send queues a message through a process reference spawned in the same transition or through a received ProcessRef<T> payload binding. The message must be accepted by the reference target's process message enum. Static validation rejects self-spawn, spawning the already-started entry process, duplicate process-reference binding in one transition, sends before the reference is bound, mailbox overflow, and messages left unhandled after a target stops normally.

Payload messages use the variant constructor at the send site:

send worker Assign(Job { phase: Ready });

The payload value is checked against the target message variant's payload type. Unit message variants reject payload arguments, and payload variants require one payload argument.

Process references can be payloads when the message variant declares a typed reference:

enum WorkerMsg { Work(ProcessRef<Sink>) }
send worker Work(sink);

The received reference is immutable and can be used as a send target:

fn step(state: WorkerState, Work(reply_to: ProcessRef<Sink>)) -> ProcResult<WorkerState> ! [send] ~ [] @det {
    send reply_to Done;
    return Stop(state);
}

Runtime dispatch uses the transported runtime process ID and admitted target process ID. Source names remain diagnostics and trace metadata.

Patterns are source-level syntax for typed value decomposition. The current runnable subset admits constructor patterns, constructor payload bindings, nested constructor and record/list/map payload destructuring, helper return-match expressions, and wildcards. Normal source helpers may match concrete enum values or destructure concrete record/list/map values, init may use one whole-body match over a fieldless enum constructor to select the initial state, and actor message dispatch may use one whole-body match over the typed message parameter:

fn step(state: WorkerState, msg: WorkerMsg) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    match msg {
        First => {
            emit "worker matched First";
            return Continue(SawFirst);
        }
        Second => {
            emit "worker matched Second";
            return Stop(Done);
        }
    }
}

Step match is an authoring form for the same semantics as step parameter patterns, including typed payload bindings and nested record/list/map payload destructuring. Checking resolves each arm into typed message-keyed transitions and typed projection templates before lowering. Mantle still dispatches by admitted message IDs, payload type IDs, and loaded template structure, not by source strings. In this buildable step subset the match scrutinee must be the typed message parameter, and match arms are block-delimited without comma separators.

A message-specific step may instead match the current state parameter when the process state type is an enum:

fn step(state: WorkerState, Complete) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    match state {
        Idle => {
            emit "worker had no job";
            return Stop(Idle);
        }
        Working(job: Job) => {
            emit "worker completed job";
            return Stop(Done(job));
        }
        Done(job: Job) => {
            emit "worker already done";
            return Stop(Done(job));
        }
    }
}

State-match arms resolve against the declared process state enum and are exhaustive over its variants. Payload-bearing state variants may bind the whole payload with the declared payload type or destructure a concrete record/list/map payload. Each binding is immutable and local to that transition arm. Lowering emits typed Mantle transitions keyed by admitted message ID plus admitted current state ID, and runtime selection fails closed if the current state is not admitted.

An init match is checked against the enum that owns the scrutinee constructor. It must be exhaustive, duplicate-free, and statement-free; each arm returns an immutable whole state value. Payload-bearing enum variants can be covered by explicit patterns or _, but init arms cannot materialize payload bindings in the returned state because the initial state lowers to one static state ID.

Effects

The ! [...] effect list is source-level authority for the runtime effects used by each step clause. It must exactly match the clause actions. For a match msg or match state step, the one effect list applies to every generated transition, so each arm must use exactly those effects. Missing, duplicate, and unused declared effects are rejected before lowering.

Effect	Statement
emit	emit "text";
spawn	let worker: ProcessRef<Worker> = spawn Worker;
send	send worker Ping; or send reply_to Done;

init cannot perform statements in the buildable slice and therefore uses an empty effect list.

Step Patterns

A step parameter pattern handles one message constructor:

fn step(state: MainState, Start) -> ProcResult<MainState> ! [emit] ~ [] @det {
    emit "hello from Strata";
    return Stop(state);
}

Payload constructors can bind the received payload in a step parameter pattern or a whole-body match msg arm:

fn step(state: WorkerState, Assign(job: Job)) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Stop(WorkerState { job: job });
}

fn step(state: WorkerState, msg: WorkerMsg) -> ProcResult<WorkerState> ! [] ~ [] @det {
    match msg {
        Assign(job: Job) => {
            return Stop(WorkerState { job: job });
        }
    }
}

The binding is immutable and local to that transition. It can be used where a value of the bound payload type is expected, including whole-value state returns, record fields, downstream message payload sends, and send targets when the payload type is ProcessRef<T>. Payload bindings cannot shadow the state parameter, process declarations, type names, or value constructors. Process-reference bindings in the same transition cannot shadow a payload binding.

Record, list, and map payloads can also be destructured directly in step parameter patterns, match msg arms, and match state arms:

fn step(state: WorkerState, Assign(Job { phase })) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Continue(WorkerState { seen: phase });
}

fn step(state: WorkerState, Items(List[phase, ..tail])) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Continue(WorkerState { seen: phase });
}

fn step(state: WorkerState, Lookup(Map[Ready => phase, ..rest])) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Continue(WorkerState { seen: phase });
}

fn step(state: WorkerState, Envelope(Assign(Job { phase }))) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Continue(WorkerState { seen: phase });
}

fn step(state: WorkerState, Holding(List[Job { phase }, ..tail])) -> ProcResult<WorkerState> ! [] ~ [] @det {
    return Continue(WorkerState { tail: tail });
}

These bindings are immutable projections of the concrete payload value. A constructor payload, record field, list element, list rest, map value, or map rest can be used in whole-value state returns and downstream payloads, but process references still remain valid only as direct message payload bindings. Fieldless nested enum constructors such as Envelope(Assign(Ready)) are accepted as typed shape predicates; they do not introduce bindings. Shape-only collection payload patterns such as Items(List[_]), Lookup(Map[Ready => _]), or Lookup(Map[..]) are not admitted in this slice; use the constructor pattern without destructuring when the payload is ignored.

If a process accepts more than one message, it can declare explicit clauses for specific constructors and one wildcard clause for the remaining variants:

fn step(state: WorkerState, First) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    emit "worker handled First";
    return Continue(SawFirst);
}

fn step(state: WorkerState, _) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    emit "worker handled Second";
    return Stop(Done);
}

Every accepted message variant must resolve to exactly one clause. Explicit constructor clauses handle their named variants. One wildcard clause may cover variants that do not have explicit clauses. Duplicate explicit clauses, duplicate wildcard clauses, missing coverage, and unreachable wildcard clauses are rejected. Parameter patterns are compile-time dispatch only: Mantle dequeues one message at a time and dispatches by typed message ID. Payload-bearing variants keep one stable admitted message case, and their immutable values travel in runtime message envelopes.

State Transitions

step returns ProcResult<StateType>:

return Continue(next_state);
return Stop(final_state);
return Panic(failed_state);

Continue(value) replaces the process state and keeps the process running. Stop(value) replaces the process state and terminates the process normally. Panic(value) replaces the process state, marks the process failed, records failure trace evidence, and fails the run without replaying the consumed message.

Passing the state parameter preserves the supplied state:

return Stop(state);

Passing a record value, enum variant, list, or map creates an explicit whole-value state replacement:

return Continue(WorkerState { phase: Idle });
return Continue(Working(Job { phase: Ready }));
return Continue(List<Phase,2>[Ready, Done]);
return Continue(Map<Phase,Phase,1>[Ready => Done]);
return Stop(Handled);
return Panic(Failed);

State changes are immutable whole-value transitions. There is no assignment statement and no source-visible field mutation.

Payload-bearing process states can be observed only through checked immutable state patterns such as Working(job: Job). Returning Done(job) creates a new whole state value; it does not rewrite the payload inside the existing state.

Limits

The buildable source slice enforces bounded sizes:

Limit	Value
Source bytes	1 MiB
Identifier bytes	128
Distinct checked artifact types	4096
Output literal bytes	16 KiB
Processes	256
State values per process	1024
Message variants per process	1024
Static process-reference bindings per process definition	4096
Distinct output literals	4096
Actions per process	4096
Mailbox bound	65,536
Type nesting	32
Value nesting	32

These limits are part of the admitted artifact and runtime boundary.