Overview

Strata is an experimental systems language for explicit authority, typed concurrency, and runtime-visible execution. Mantle is the runtime target for Strata programs.

The source-to-runtime boundary is executable behavior:

.str source -> strata check -> strata build -> .mta artifact -> mantle run

The runnable slices carry real .str programs through checking, Mantle Target Artifact build, Mantle admission, execution, and runtime observability.

If you are new to Strata, start with Getting Started, then Language Concepts, then the Hello tutorial. Use the Language Reference and Syntax Reference as the source-authoring contract.

The documentation in this book tracks accepted behavior, file identities, runtime boundaries, and the development gates that must stay green as the language and runtime grow.

Reading Paths

For a first working program:

1. Read Getting Started.
2. Build and run examples/hello.str.
3. Read Tutorial: Hello.
4. Read Tutorial: Actors And Messages.

For precise source behavior:

1. Read Language Reference.
2. Read Syntax Reference.
3. Check Diagnostics when a command rejects a program.

For runtime and contributor work:

1. Read Runtime Traces.
2. Read Artifact And Runtime Boundary.
3. Read Implementation Architecture.
4. Use Development Gates before closing changes.

Getting Started

This guide takes a clean checkout to a checked, built, and executed Strata program.

Prerequisites

Install stable Rust 1.85 or newer with Cargo. The workspace uses Rust Edition 2024. Standard repository gates select stable explicitly; nightly is reserved for fuzz and Miri recipes that opt into it per command.

Useful local tools:

rustup toolchain install stable --profile minimal --component rustfmt,clippy
cargo +stable install just --version 1.50.0 --locked
cargo +stable install mdbook --version 0.5.2 --locked

The 1.50.0 value above is the pinned just command runner version, not the Rust compiler version.

The standard just quality gate runs documentation and metadata checks on every local platform. Install jq, xmllint, and mdbook before using that bundle. Ubuntu-based environments can install the metadata tools with:

sudo apt-get install jq libxml2-utils

macOS systems with Homebrew can install the metadata tools with:

brew install jq libxml2

Windows systems should install jq and an xmllint provider such as libxml2 with their package manager, or run the full just quality bundle in a WSL Ubuntu environment. Confirm the tools are on PATH with jq --version, xmllint --version, and mdbook --version.

Do not set a repository-wide nightly Rust override. Use just install-fuzz-tools and just install-miri-tools only when running the nightly fuzz or Miri gates.

Build The Binaries

From the repository root:

cargo build

This builds the Strata CLI and Mantle runtime CLI. The executable filenames are platform-specific, so the commands below use Cargo to run the right binary on the local platform.

Check A Strata Program

strata check parses and semantically checks source without writing an artifact.

cargo run -p strata --bin strata -- check examples/hello.str

Expected result:

strata: checked examples/hello.str (module hello, entry Main)

Build A Mantle Artifact

strata build checks the source and writes a Mantle Target Artifact under target/strata/ by default.

cargo run -p strata --bin strata -- build examples/hello.str

Expected result:

strata: built examples/hello.str -> target/strata/hello.mta

Run The Program

Mantle admits and executes the generated artifact:

cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

Expected output includes:

mantle: loaded target/strata/hello.mta
mantle: spawned Main pid=1
mantle: delivered Start to Main
hello from Strata
mantle: stopped Main normally
mantle: trace target/strata/hello.observability.jsonl

The trace path is important. It records what Mantle actually admitted and executed.

Run The Standard Gate

After editing source, examples, runtime behavior, artifacts, or docs, use the central automation:

just quality

For the source-to-runtime acceptance examples only:

just source-to-runtime-gates

For the docs only:

just docs

What To Read Next

Read Language Concepts for the core ideas, then Tutorial: Hello for a guided walkthrough of the smallest accepted program.

Language Concepts

Strata is a source language for explicit state, explicit effects, typed messages, and runtime-observable process execution.

The implementation is intentionally small. The .str source surface declares source-level records, enums, pure source functions, processes, message types, state types, and process transitions. Mantle executes the admitted artifact produced from that source.

Source Versus Runtime

Strata source is where author-visible meaning lives:

• names;
• records;
• enums;
• source functions;
• process declarations;
• message declarations;
• state transition expressions;
• declared effects.

Mantle runtime is where admitted execution lives:

• process instances;
• process references;
• mailboxes;
• loaded typed IDs;
• transition tables;
• runtime events;
• trace output.

The two surfaces are related, but not interchangeable. Source labels are useful for diagnostics and traces. Runtime dispatch uses loaded typed IDs.

Processes

A Strata program is organized around processes. A process declares:

• a bounded mailbox;
• a state type;
• a message type;
• an init function that creates the initial state;
• optional pure helper functions local to the process;
• a step function that handles messages and returns a transition result.

The entry process is named Main. Mantle starts Main and delivers its first message variant as the entry message.

Spawning a process creates a runtime process instance and binds it to an immutable typed process reference value:

let worker: ProcessRef<Worker> = spawn Worker;

The reference is local to the transition that spawned it. Multiple references may target the same process definition, which creates multiple runtime instances.

Messages

A process message type is an enum. Each variant is a message the process can accept.

enum WorkerMsg {
    Ping,
    Assign(Job),
}

Sends are statically checked against the target process message enum:

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

Payload variants carry one immutable value. Actor step parameter patterns can bind that payload, and whole-body match msg arms can bind the same payload:

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

Source Functions

Strata accepts pure source helper functions at module level and inside processes. Helpers are checked and expanded before lowering; Mantle does not dispatch by helper names at runtime.

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

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

Source helpers are immutable value producers. They perform no statements, use ! [] ~ [] @det, and return whole values. A process-local helper can encapsulate non-message-handling value construction for init, step results, and send payloads.

Payload-bearing enum constructors are source values too. A helper may match Assigned(job: Job) in a signature pattern or whole-body match, and the payload binding is an immutable value scoped to that clause or arm.

State

Process state is immutable at the source level. A transition returns a whole replacement state or the supplied state.

return Continue(SawFirst);
return Stop(state);
return Panic(Failed);

Panic(value) is an abnormal terminal result: Mantle records the replacement state and failure evidence, fails the run, and does not replay the consumed message.

There is no assignment statement and no field update expression. Record state is constructed as a new whole value:

return Continue(WorkerState { phase: Idle });

Effects

Effects must be visible in the function signature. The effects are:

• emit;
• spawn;
• send.

The declared effect list must exactly match the effects used by each step clause.

fn step(state: MainState, Start) -> ProcResult<MainState> ! [spawn, send] ~ [] @det {
    let worker: ProcessRef<Worker> = spawn Worker;
    send worker Ping;
    return Stop(state);
}

This is deliberately stricter than “allow anything in the list.” A declared but unused effect is rejected.

Determinism And May-Behaviors

Function signatures include determinism and may-behavior positions:

! [effects] ~ [may_behaviors] @det

Buildable source requires ~ [] @det. The parser recognizes @nondet, but accepted buildable programs are deterministic.

Execution Shape

The source-to-runtime path is:

.str source -> parse -> check -> lower -> .mta artifact -> admit -> run -> trace

Each phase has a different responsibility. Parser success alone does not mean a program is accepted. A program must also pass semantic checking, artifact validation, and runtime admission.

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

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 and ProcessRef are reserved type names because they name built-in transition and process-reference 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 =.

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.

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:

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 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;
        }
    }
}

These matches are exhaustive, duplicate-free, and immutable. Payload-bearing source helper patterns bind payloads as immutable values. A helper call must provide a concrete enum constructor value for signature-pattern or whole-body match dispatch; 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, and wildcards. Normal source helpers may match concrete enum 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. Checking resolves each arm into typed message-keyed transitions before lowering. Mantle still dispatches by admitted message IDs and payload type IDs, 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 must bind their payload with the declared payload type. The 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.

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.

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 or enum variant creates an explicit whole-value state replacement:

return Continue(WorkerState { phase: Idle });
return Continue(Working(Job { phase: Ready }));
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:

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

Syntax Reference

This page gives a compact grammar-style view of the accepted source syntax. The Language Reference explains the same surface in prose.

The notation is informal:

• quoted text is literal syntax;
• ? means optional;
• * means zero or more;
• + means one or more;
• | means choice.

Source File

source_file =
    module_decl top_level_decl*

module_decl =
    "module" ident ";"

top_level_decl =
    record_decl
  | enum_decl
  | function
  | process_decl

Records

record_decl =
    "record" ident ";"
  | "record" ident "{" record_field ("," record_field)* ","? "}"

record_field =
    ident ":" type_ref

Fieldless records use the semicolon form. Braced records must declare at least one field.

Enums

enum_decl =
    "enum" ident "{" enum_variant_list? "}"

enum_variant_list =
    enum_variant ("," enum_variant)* ","?

enum_variant =
    ident
  | ident "(" type_ref ")"

Enums used as process state or message types must have at least one variant. Payload variants are accepted for process state and message enums. State enum payload constructors create immutable whole-state values.

Processes

process_decl =
    "proc" ident "mailbox" "bounded" "(" number ")" "{"
        process_member*
    "}"

process_member =
    state_alias
  | message_alias
  | init_function
  | step_function
  | source_function

state_alias =
    "type" "State" "=" type_ref ";"

message_alias =
    "type" "Msg" "=" type_ref ";"

The aliases and functions may appear in any order. State, Msg, and init must each appear exactly once. Non-init/step functions are process-local source helpers. Each message variant must resolve to exactly one step clause, either through an explicit constructor pattern, through one wildcard pattern, through one match msg step body, or through a state-match step for a specific message pattern. A process cannot mix parameter-pattern/state-match step forms with a match msg step body in this slice. Other process members are rejected.

Functions

function =
    "fn" ident "(" params? ")" "->" type_ref
    "!" effect_list
    "~" ident_list
    determinism
    function_body

params =
    function_param ("," function_param)* ","?

function_param =
    param_binding
  | pattern

param_binding =
    ident ":" type_ref

pattern =
    ident
  | ident "(" ident ":" type_ref ")"
  | "_"

effect_list =
    "[" (effect ("," effect)* ","?)? "]"

effect =
    "emit" | "spawn" | "send"

ident_list =
    "[" (ident ("," ident)* ","?)? "]"

determinism =
    "@det" | "@nondet"

Buildable source accepts bodies for init, step, module helpers, and process-local helpers. It requires deterministic functions and empty may-behavior lists. Normal source helpers are pure: they use ! [], perform no statements, and are expanded before lowering.

Function Bodies

function_body =
    ";"
  | "{" block_body "}"
  | "{" match_body "}"

block_body =
    statement* return_statement

match_body =
    "match" ident "{" match_arm+ "}"

match_arm =
    pattern "=>" "{" block_body "}"

Patterns are source-level binding and decomposition syntax. This source slice admits constructor patterns, constructor payload bindings, and _ wildcards. Buildable semantic consumers are normal source function signatures and match bodies, fieldless enum init matches, and actor step message dispatch. Actor step bodies may also match the current process state parameter when the process state type is an enum. Normal source helpers, actor step dispatch, and current-state matches accept constructor payload bindings. Source helper calls still expand before lowering; they require a concrete enum constructor value for pattern selection.

Buildable source requires bodies. init uses no parameters. Each parameter-pattern step uses state: StateType followed by one message constructor or wildcard pattern:

parameter_pattern_step_function =
    "fn" "step" "(" "state" ":" type_ref ","
        (ident | ident "(" ident ":" type_ref ")" | "_") ")"
    "->" "ProcResult" "<" type_ref ">"
    "!" effect_list "~" "[]" "@det"
    "{" block_body "}"

The first type_ref must name the process state type. An ident after the comma is a message constructor accepted by the process message type. A payload pattern such as Assign(job: Job) binds the received payload as an immutable transition-local value. _ is a wildcard pattern that covers accepted variants without explicit clauses.

A match step uses a typed message parameter and a whole-body match over that parameter:

match_step_function =
    "fn" "step" "(" "state" ":" type_ref "," ident ":" type_ref ")"
    "->" "ProcResult" "<" type_ref ">"
    "!" effect_list "~" "[]" "@det"
    "{" match_body "}"

Each match arm uses the same pattern syntax as parameter-pattern dispatch. The match scrutinee must be the typed message parameter in the current buildable step subset. Match arms are block-delimited and do not use comma separators. The step effect list applies to every generated transition, so each arm must use exactly the declared effects.

A state-match step uses the normal state parameter plus a message constructor or wildcard pattern, then uses a whole-body match state:

state_match_step_function =
    "fn" "step" "(" "state" ":" type_ref ","
        (ident | ident "(" ident ":" type_ref ")" | "_") ")"
    "->" "ProcResult" "<" type_ref ">"
    "!" effect_list "~" "[]" "@det"
    "{" "match" "state" "{" match_arm+ "}" "}"

State-match arms resolve against the declared process state enum. Payload variants must bind their payload with an explicit type, such as Working(job: Job). Fieldless variants must not bind a payload. Bindings are immutable and transition-local. Each generated transition is keyed by the message ID and the admitted current state ID; state changes still occur only by returning a whole state value through Continue(...), Stop(...), or Panic(...).

A normal source helper is a module-level function or a process-local function whose name is not init or step:

source_function =
    "fn" ident "(" (param_binding | pattern) ")"
    "->" type_ref
    "!" "[]" "~" "[]" "@det"
    ("{" block_body "}" | "{" match_body "}")

Helper block bodies must not contain statements. Helper match bodies match the function’s typed binding parameter. Helper calls and payload-bearing enum values share the same surface syntax:

call_or_payload_constructor =
    ident "(" value_expr ")"

The checker resolves that form against the expected type. A declared enum constructor becomes an immutable enum value; a declared helper is expanded in init, step result values, and send payload values. Recursive helper call cycles are rejected.

Statements

statement =
    emit_statement
  | process_ref_statement
  | send_statement

emit_statement =
    "emit" string_literal ";"

process_ref_statement =
    "let" ident ":" process_ref_type "=" "spawn" ident ";"

process_ref_type =
    "ProcessRef" "<" ident ">"

send_statement =
    "send" ident ident payload_arg? ";"

payload_arg =
    "(" value_expr ")"

return_statement =
    "return" return_expr ";"

The identifier after let names an immutable process reference value. The identifier after spawn is the process definition name. The ProcessRef<T> annotation must name the same process definition.

The first identifier in send is a local process reference or a received payload binding whose type is ProcessRef<T>. The second identifier is the message variant to send. Payload variants require one payload value. Unit variants reject payload values.

Types

type_ref =
    ident
  | ident "<" type_ref ("," type_ref)* ","? ">"

The built-in generic types accepted by checking are ProcResult<StateType> as a step return type and ProcessRef<ProcessName> in spawn bindings, message payload declarations, and payload-binding step patterns.

Values

return_expr =
    value_expr
  | ident "(" value_expr ")"

value_expr =
    ident
  | ident "(" value_expr ")"
  | ident "{" record_value_field ("," record_value_field)* ","? "}"

record_value_field =
    ident ":" value_expr

The parenthesized value expression is typed during checking. It is a helper call when ident names a visible source helper and a payload-bearing enum value when ident names a constructor of the expected enum type.

init returns a state value. step returns Continue(value), Stop(value), or Panic(value).

Literals

The literal surface is intentionally narrow:

• decimal numbers are accepted for mailbox bounds;
• string literals are accepted for emit;
• string escapes are not supported;
• newline and carriage return characters are not allowed inside string literals.

Identifiers

ident =
    (ASCII letter | "_") (ASCII letter | ASCII digit | "_")*

as, let, mut, and var are reserved everywhere identifiers are accepted. The single _ token is reserved for wildcard patterns. ProcResult and ProcessRef are reserved type names because they name built-in transition and process-reference types.

Tutorial: Hello

This tutorial walks through the smallest Strata program accepted by the source-to-runtime gate.

The complete source is examples/hello.str.

Module

module hello;

The module declaration names the source unit. It does not import anything and does not create a package boundary.

State And Message Types

record MainState;
enum MainMsg {
    Start,
}

MainState is a fieldless record. It gives the process a concrete state type without carrying data.

MainMsg declares the messages accepted by Main. Start is the first variant, so it is the entry message delivered to Main when Mantle starts the program.

Main Process

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

Every runnable program needs a Main process. The mailbox bound limits how many messages can wait in the process mailbox.

The State alias points to the process state type. The Msg alias points to the process message enum.

Initial State

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

init takes no parameters and returns the initial state. It uses no effects, has no may-behaviors, and is deterministic.

Step Function

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

step receives the process state and handles the Start message named in its parameter pattern.

The body emits text and then returns Stop(state). Passing state preserves the supplied state while stopping normally.

The effect list is [emit] because the body uses exactly one effect.

Run It

cargo build
cargo run -p strata --bin strata -- check examples/hello.str
cargo run -p strata --bin strata -- build examples/hello.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

The program prints:

hello from Strata

Mantle also writes:

target/strata/hello.observability.jsonl

That trace should contain artifact_loaded, process_spawned, message_accepted, message_dequeued, program_output, and process_stopped events.

Common Edits

If you remove emit "hello from Strata";, also change the effect list from [emit] to []. Declaring an unused effect is rejected.

If you add a second message variant to MainMsg, add a step clause for that variant or use one _ clause for variants without explicit clauses. Each accepted message must resolve to exactly one clause.

Tutorial: Actors And Messages

This tutorial introduces multiple processes, message sends, and message-keyed state transitions.

Read Tutorial: Hello first if the basic Main process shape is unfamiliar.

Process Roles

examples/actor_ping.str has two processes:

• Main, the entry process;
• Worker, a process spawned by Main.

Main starts the worker, sends Ping, and stops. Worker receives Ping, emits output, transitions to Handled, and stops.

Worker Message Type

enum WorkerMsg {
    Ping,
}

This says Worker accepts one message: Ping.

Main can send that message after spawning Worker:

let worker: ProcessRef<Worker> = spawn Worker;
send worker Ping;
return Stop(state);

worker is an immutable process reference for the spawned runtime instance. The order matters in this source surface. Sending through a reference before it is bound is rejected.

Worker State Type

enum WorkerState {
    Idle,
    Handled,
}

Worker starts in Idle:

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

After handling Ping, it stops in Handled:

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

The transition is a whole state replacement. Handled is the new state value.

Multiple Messages

examples/actor_sequence.str extends the pattern with two worker messages:

enum WorkerMsg {
    First,
    Second,
}

When a process accepts multiple messages, each message must resolve to one step clause. Explicit patterns handle named variants, and _ handles the remaining accepted 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);
}

Missing coverage, duplicate explicit patterns, duplicate wildcard patterns, and wildcards that cannot cover any remaining message are rejected.

Continue Versus Stop

Continue(SawFirst) means:

• replace the worker state with SawFirst;
• keep the worker running;
• allow later queued messages to be handled.

Stop(Done) means:

• replace the worker state with Done;
• terminate the worker normally.

The runtime trace records both steps with message IDs and state IDs.

Message Payloads

examples/actor_payloads.str adds a typed payload to a worker message:

record Job {
    phase: JobPhase,
}

enum WorkerMsg {
    Assign(Job),
}

The sender constructs one immutable payload value:

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

The receiver binds that value in a step parameter pattern:

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

The payload binding is immutable and local to the transition. Mantle executes typed message IDs; payload values travel in runtime message envelopes and appear in traces as payload metadata on the stable Assign message label.

Process references can also travel as typed payloads:

enum WorkerMsg {
    Work(ProcessRef<Sink>),
}

send worker Work(sink);

The receiver can use the immutable payload binding as a send target:

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

Mantle routes that send by the transported runtime process ID and admitted target process ID. The source binding name is trace and diagnostic metadata, not the runtime dispatch key.

Multiple Instances

examples/actor_instances.str spawns two runtime instances of the same process definition:

let first: ProcessRef<Worker> = spawn Worker;
let second: ProcessRef<Worker> = spawn Worker;
send first Ping;
send second Ping;

first and second are separate process references. Mantle assigns each spawned worker a different runtime pid, and the trace records both messages and both worker steps with the same process definition ID but different process instance IDs.

Run The Actor Examples

cargo build

cargo run -p strata --bin strata -- check examples/actor_ping.str
cargo run -p strata --bin strata -- build examples/actor_ping.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_ping.mta

cargo run -p strata --bin strata -- check examples/actor_sequence.str
cargo run -p strata --bin strata -- build examples/actor_sequence.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_sequence.mta

cargo run -p strata --bin strata -- check examples/actor_match.str
cargo run -p strata --bin strata -- build examples/actor_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_match.mta

cargo run -p strata --bin strata -- check examples/actor_instances.str
cargo run -p strata --bin strata -- build examples/actor_instances.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_instances.mta

cargo run -p strata --bin strata -- check examples/actor_payloads.str
cargo run -p strata --bin strata -- build examples/actor_payloads.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_payloads.mta

cargo run -p strata --bin strata -- check examples/actor_reply.str
cargo run -p strata --bin strata -- build examples/actor_reply.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_reply.mta

For actor_sequence, the trace should show Worker dequeuing First, stepping with Continue, then later dequeuing Second and stepping with Stop. actor_match should show the same typed transition behavior from the whole-body match msg authoring form.

Runtime Traces

Mantle writes runtime traces as line-delimited JSON. Each line is one runtime event.

By default, running:

cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_sequence.mta

writes:

target/strata/actor_sequence.observability.jsonl

The trace is evidence that Mantle admitted and executed the artifact. It is not a substitute for running the source-to-runtime gate.

Identity Fields

Trace events include both labels and numeric IDs.

Labels are for reading:

• process;
• message;
• state;
• text.

IDs are for stable runtime identity:

• pid, the runtime process instance ID;
• process_id, the admitted process definition ID;
• message_id, the admitted message case ID;
• state_id, the admitted typed state value ID;
• payload_type_id, the admitted artifact type ID when a payload is present;
• output_id, the admitted output literal ID.

Do not treat labels as runtime dispatch keys. Runtime execution uses admitted typed IDs and typed state value identities.

When multiple runtime instances are spawned from one process definition, the instances share process_id and label metadata but have different pid values. examples/actor_instances.str exercises that shape.

Event Types

Artifact Loaded

Example shape:

{"event":"artifact_loaded","format":"mantle-target-artifact","schema_version":"1","source_language":"strata","module":"actor_sequence","entry_process_id":0,"entry_process":"Main","entry_message_id":0,"process_count":2}

Important fields:

• format and schema_version identify the artifact schema;
• source_language identifies the frontend that produced the artifact;
• entry_process_id and entry_message_id identify the runtime entrypoint.

Process Spawned

Example shape:

{"event":"process_spawned","pid":2,"process_id":1,"process":"Worker","state_id":0,"state":"Waiting","mailbox_bound":2,"spawned_by_pid":1}

pid is the runtime process instance. process_id is the admitted process definition. spawned_by_pid is present when another process spawned this one.

Message Accepted And Dequeued

Example shape:

{"event":"message_accepted","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"First","queue_depth":1,"sender_pid":1}
{"event":"message_dequeued","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"First","queue_depth":1}

message_accepted records mailbox admission. message_dequeued records the message selected for the next transition.

Payload-bearing messages keep the stable admitted message label and add payload_type_id plus payload fields:

{"event":"message_accepted","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"Assign","payload_type_id":2,"payload":"Job{phase:Ready}","queue_depth":1,"sender_pid":1}

Runtime dispatch uses the numeric message_id; labels and payload values are trace metadata. Payload type identity is the numeric ID from the admitted artifact type table, not a source type string.

For state-specific transitions produced by match state, runtime dispatch uses the current admitted state_id together with the admitted message_id. The trace continues to record the resulting state ID and label; labels are not used to select the transition.

When a payload is a transported process reference, the trace also includes the admitted target process ID and runtime process ID:

{"event":"message_accepted","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"Work","payload_type_id":2,"payload":"type2#3","payload_process_id":2,"payload_pid":3,"queue_depth":1,"sender_pid":1}

Process Stepped

Example shape:

{"event":"process_stepped","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"First","result":"Continue","state_id":1,"state":"SawFirst"}

result is Continue, Stop, or Panic. state_id and state are the transition target state. Payload-bearing steps include the same payload_type_id and payload fields as mailbox events.

State Updated

Example shape:

{"event":"state_updated","pid":2,"process_id":1,"process":"Worker","from_state_id":0,"from":"Waiting","to_state_id":1,"to":"SawFirst"}

State updates are whole-value replacements. The trace records the previous and new admitted state values, including payload-bearing enum state values such as Working(Job{phase:Ready}).

Program Output

Example shape:

{"event":"program_output","pid":2,"process_id":1,"process":"Worker","stream":"stdout","output_id":0,"text":"worker handled First"}

output_id identifies the admitted output literal. text is the readable output.

Process Stopped

Example shape:

{"event":"process_stopped","pid":2,"process_id":1,"process":"Worker","reason":"normal"}

The stop reason is normal.

Process Failed

Example shape:

{"event":"process_failed","pid":2,"process_id":1,"process":"Worker","state_id":1,"state":"Failed","reason":"panic"}

Panic(value) records a process_stepped event with result:"Panic", then a process_failed event. The dequeued message is already consumed and is not replayed. The failure reason is panic.

Diagnostics

Strata diagnostics are intended to reject invalid source close to the layer that can explain it. Parser errors describe source shape. Checker errors describe semantic rules. Runtime errors describe admitted execution failures.

Reading A Diagnostic

Run:

cargo run -p strata --bin strata -- check examples/hello.str

If checking fails, fix the first reported error first. Later errors may be a result of the first invalid shape.

Common Source Errors

Source Function Errors

Message Handling Errors

Match Errors

State Errors

Process And Mailbox Errors

Runtime Errors

Runtime errors are emitted by Mantle after artifact admission starts. Common causes include invalid artifacts, blocked trace paths, mailbox exhaustion, explicit Panic(...) transition results, trace size exhaustion, and dispatch budget exhaustion.

Use the source gate first:

cargo run -p strata --bin strata -- check path/to/program.str
cargo run -p strata --bin strata -- build path/to/program.str

Then run Mantle:

cargo run -p mantle-runtime --bin mantle -- run target/strata/program.mta

If source checking passes but Mantle rejects an artifact, inspect the artifact and runtime boundary docs before changing runtime behavior.

Examples

Runnable Strata examples live under examples/.

Read them in this order:

1. hello.str for the minimum source-to-runtime program.
2. actor_ping.str for spawning, sending, and a single worker transition.
3. actor_sequence.str for multiple messages and message-keyed transitions.
4. actor_match.str for whole-body match authoring that checks into typed message-keyed transitions.
5. init_match.str for whole-body match authoring in init.
6. function_match.str for module functions, process-local helpers, and pattern matching outside actor dispatch.
7. function_payload_match.str for payload-bearing enum construction and matching in normal source helpers.
8. state_payload_enum.str for payload-bearing process state enum transitions.
9. state_payload_match.str for matching immutable current process state payloads.
10. actor_instances.str for multiple runtime instances of one process definition.
11. actor_payloads.str for typed message payloads and immutable payload bindings in actor step parameter patterns.
12. actor_payload_match.str for the same payload binding through a whole-body match msg.
13. actor_reply.str for transporting typed process references through message payloads.
14. actor_panic_no_replay.str for fail-closed actor failure and no replay after message dequeue.

Hello

examples/hello.str is the first source-to-runtime gate. It checks, builds, runs, emits hello from Strata, and records an observability trace.

cargo build
cargo run -p strata --bin strata -- check examples/hello.str
cargo run -p strata --bin strata -- build examples/hello.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

Key source ideas:

• Main is the entry process.
• MainMsg.Start is the entry message.
• emit is declared in the step effect list.
• Stop(state) terminates normally without changing state.

Actor Ping

examples/actor_ping.str is the first actor/runtime gate. It spawns a worker, sends a message, handles that message, updates state, terminates normally, and records the runtime trace.

cargo run -p strata --bin strata -- check examples/actor_ping.str
cargo run -p strata --bin strata -- build examples/actor_ping.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_ping.mta

Key source ideas:

• Main uses let worker: ProcessRef<Worker> = spawn Worker; before send worker Ping;.
• WorkerMsg.Ping is checked against Worker’s message type.
• Worker replaces Idle with Handled.
• Both processes stop normally.

Actor Sequence

examples/actor_sequence.str exercises message-keyed process transitions. The worker handles First, returns a whole replacement state with Continue(...), then handles Second through the wildcard clause and returns a whole replacement state with Stop(...).

cargo run -p strata --bin strata -- check examples/actor_sequence.str
cargo run -p strata --bin strata -- build examples/actor_sequence.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_sequence.mta

Key source ideas:

• WorkerMsg has two variants, and each variant resolves to exactly one step clause.
• The explicit First clause handles First; _ covers the remaining accepted message variants.
• Continue(SawFirst) keeps the worker alive for the next queued message.
• Stop(Done) terminates the worker normally.

The runtime trace records process, message, state, and output IDs alongside labels so that behavior can be checked without treating labels as executable bindings.

Actor Match

examples/actor_match.str exercises the whole-body match msg authoring form. The checker resolves each arm into the same typed transition table used by step parameter patterns.

cargo run -p strata --bin strata -- check examples/actor_match.str
cargo run -p strata --bin strata -- build examples/actor_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_match.mta

Key source ideas:

• fn step(state: WorkerState, msg: WorkerMsg) declares a typed message parameter.
• match msg must be the whole function body in this source slice.
• Each arm returns a whole replacement state through Continue(...) or Stop(...).
• The generated Mantle artifact still dispatches by typed message IDs.

Init Match

examples/init_match.str exercises a non-step whole-body match in init. The checker resolves the fieldless enum scrutinee, proves the arms are exhaustive, and selects the typed initial state before lowering.

cargo run -p strata --bin strata -- check examples/init_match.str
cargo run -p strata --bin strata -- build examples/init_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/init_match.mta

Key source ideas:

• match Warm is checked against StartupMode.
• Both Cold and Warm arms return immutable whole MainState record values.
• The Mantle trace starts Main in MainState{readiness:WarmReady}, proving the selected initial state reached runtime admission.

Function Match

examples/function_match.str exercises normal source functions outside actor dispatch. It uses module-level functions and process-local helpers, including signature-pattern dispatch and a whole-body match helper.

cargo run -p strata --bin strata -- check examples/function_match.str
cargo run -p strata --bin strata -- build examples/function_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/function_match.mta

Key source ideas:

• readiness_sig(Cold) and readiness_sig(Warm) are module-level function clauses selected by typed signature patterns.
• readiness_body(mode: StartupMode) uses a whole-body match mode outside an actor step.
• Main and Worker declare process-local helper functions for state construction.
• send worker Assign(ready_job(Ready)) proves helper calls are expanded for message payload discovery and lowering.
• Mantle sees typed state IDs, message IDs, and payload templates, not source helper dispatch names.

Function Payload Match

examples/function_payload_match.str extends normal source helpers to payload-bearing enum values. It constructs source-visible enum payload values, matches them through signature patterns and whole-body helper matches, and lowers a received actor payload through a process-local helper into an enum payload state template.

cargo run -p strata --bin strata -- check examples/function_payload_match.str
cargo run -p strata --bin strata -- build examples/function_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/function_payload_match.mta

Key source ideas:

• Assigned(Job { phase: Ready }) is resolved as a typed enum value, not a helper call.
• status_sig(Assigned(job: Job)) binds the enum payload immutably in a normal source helper signature pattern.
• status_body(work: Work) matches the typed helper parameter and binds the payload inside the selected arm.
• state_for(Assigned(job)) proves a process-local helper can wrap a received immutable payload into a source enum value before lowering.

State Payload Enum

examples/state_payload_enum.str admits payload-bearing process state enum values. It starts a worker in fieldless Idle, receives an immutable Job payload, and transitions to Working(Job { phase: Ready }).

cargo run -p strata --bin strata -- check examples/state_payload_enum.str
cargo run -p strata --bin strata -- build examples/state_payload_enum.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/state_payload_enum.mta

Key source ideas:

• enum WorkerState { Idle, Working(Job) } declares a payload-bearing state variant.
• return Stop(Working(job)); constructs a whole replacement state from an immutable received payload.
• Mantle receives a next-state value template and admits the resulting Working(Job{phase:Ready}) only because it is present in the typed state table.

State Payload Match

examples/state_payload_match.str matches the current process state as typed immutable data. The worker first enters Working(Job { phase: Ready }); a later Complete message dispatches over the current state and binds job inside the selected state arm.

cargo run -p strata --bin strata -- check examples/state_payload_match.str
cargo run -p strata --bin strata -- build examples/state_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/state_payload_match.mta

Key source ideas:

• fn step(state: WorkerState, Complete) can use a whole-body match state.
• Working(job: Job) binds the state enum payload immutably for that transition arm only.
• return Stop(Done(job)); returns a whole replacement state; it does not mutate the current state in place.
• The Mantle artifact carries state-specific transitions keyed by admitted message ID plus admitted current state ID, and the payload-derived next state uses a typed current-state payload template.

Actor Instances

examples/actor_instances.str proves process references and instance-aware sends. Main spawns the Worker process definition twice, binds each runtime instance to a different process reference, and sends Ping through both references.

cargo run -p strata --bin strata -- check examples/actor_instances.str
cargo run -p strata --bin strata -- build examples/actor_instances.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_instances.mta

Key source ideas:

• let first: ProcessRef<Worker> = spawn Worker; and let second: ProcessRef<Worker> = spawn Worker; create two runtime worker instances.
• send first Ping; and send second Ping; dispatch by reference, not by process definition label.
• The runtime trace records two different pid values with the same process_id for Worker.

Actor Payloads

examples/actor_payloads.str sends a typed payload from Main to Worker. Worker binds that payload with a step parameter pattern and returns a whole replacement state containing the immutable payload value.

cargo run -p strata --bin strata -- check examples/actor_payloads.str
cargo run -p strata --bin strata -- build examples/actor_payloads.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_payloads.mta

Key source ideas:

• enum WorkerMsg { Assign(Job) } declares a payload-bearing message variant.
• send worker Assign(Job { phase: Ready }); sends one checked payload value.
• Assign(job: Job) binds the received payload as an immutable step-local value.
• WorkerState { job: job } constructs the next state as a whole value.

Actor Payload Match

examples/actor_payload_match.str proves the same immutable payload binding works from a whole-body match msg arm, not only from a step signature.

cargo run -p strata --bin strata -- check examples/actor_payload_match.str
cargo run -p strata --bin strata -- build examples/actor_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_payload_match.mta

Key source ideas:

• fn step(state: WorkerState, msg: WorkerMsg) binds the message parameter.
• match msg dispatches through the same typed pattern validation used by signature patterns.
• Assign(job: Job) binds the received payload immutably inside the match arm.
• Runtime still dispatches by admitted message IDs and payload type IDs.

Actor Reply References

examples/actor_reply.str passes a ProcessRef<Sink> as a typed immutable message payload. Worker receives that reference and sends Done through it.

cargo run -p strata --bin strata -- check examples/actor_reply.str
cargo run -p strata --bin strata -- build examples/actor_reply.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_reply.mta

Key source ideas:

• enum WorkerMsg { Work(ProcessRef<Sink>) } declares a typed reference payload.
• send worker Work(sink); transports the spawned Sink reference to Worker.
• Work(reply_to: ProcessRef<Sink>) binds the received reference immutably.
• send reply_to Done; routes by the transported runtime process ID and admitted target process ID, not by source labels.

Actor Panic No Replay

examples/actor_panic_no_replay.str admits an explicit abnormal transition. Main queues two Ping messages to Worker; Worker dequeues one message, returns Panic(Failed), records failure evidence, and the consumed message is not replayed.

cargo run -p strata --bin strata -- check examples/actor_panic_no_replay.str
cargo run -p strata --bin strata -- build examples/actor_panic_no_replay.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_panic_no_replay.mta

The final command is expected to return non-zero. The runtime trace should show two accepted Ping messages, one message_dequeued for Worker, one process_stepped event with result:"Panic", and one process_failed event.

File Types

This repository uses two first-class file extensions:

• .str for Strata source.
• .mta for Mantle Target Artifacts.

.str

.str files are Strata source files. They are the user-authored program surface and should be UTF-8 text with LF line endings.

Expected MIME type:

text/x-strata

.mta

.mta files are Mantle Target Artifacts. They are executable inputs to Mantle, not Strata source and not proof or evidence artifacts.

The extension is intentionally language-neutral. Strata can emit .mta; other frontends can emit .mta too. Mantle must decide whether an artifact is admissible from its internal header and validation data, not from the filename.

Minimum artifact identity fields:

format=mantle-target-artifact
schema_version=1
source_language=strata

The schema version identifies the admitted .mta encoding shape. It is not a Strata language release, a migration counter, or a stability guarantee. In the current greenfield implementation, 1 is the single admitted artifact schema baseline.

Executable references, type identity, and state transitions inside .mta use validated table IDs and typed transition forms. Process transition records are encoded by transition index and carry a message ID field, an optional current_state ID guard, and exact effect authority for their actions. Validation requires either one unguarded transition for a message or a complete set of state-specific transitions over the admitted state table. Runtime selection indexes the admitted transition table by typed message ID plus typed current state ID when a state guard is present.

Artifact type identity is carried by a Mantle type table. Process state_type_id, message_type_id, message payload_type_id, payload template type_id, state value type_id, and received-payload send-target target_payload_type_id fields refer to that table by numeric TypeId. Type labels are metadata only; Mantle does not parse source type strings such as process-reference spellings to decide runtime behavior.

State value tables carry a type ID, typed value identity, display label, and optional typed payload metadata for each admitted state. Mantle admission and runtime next-state resolution use the type ID and value identity. State-match payload templates use the admitted current state’s typed payload metadata. Labels remain trace and diagnostic metadata.

Process references are encoded as per-process reference tables. A spawn action binds a process-reference ID to a runtime process instance for the transition. A send action targets either a process-reference ID or a received typed process-reference payload plus a message ID. Reference debug names remain metadata; runtime delivery uses admitted IDs and runtime process instance IDs.

Message variants may carry an optional payload type ID. Send actions may carry an immutable payload value template, and Mantle delivers the evaluated value in a runtime message envelope. Process-reference payloads carry the admitted target process ID and runtime process ID. Message dispatch uses admitted typed IDs, not payload text or source labels.

Each transition’s action_count is bounded during decode before allocation. Validation also caps the aggregate action count across all transitions for a process as an admitted process resource budget.

Names are retained for diagnostics, traces, and metadata. Mantle execution must load and run resolved IDs rather than dispatching by source text.

Generated .mta files should normally remain under target/. Checked-in .mta files are allowed only as explicitly labeled fixtures or specimens and must not be used as a substitute for a successful strata build and mantle run.

Expected MIME type:

application/vnd.mantle.target-artifact

Source-To-Runtime Gates

A runtime-bearing milestone is not complete until the command a user would run succeeds. Documentation and generated artifacts do not replace executable source-to-runtime behavior.

The normal gate shape is:

.str source -> strata check -> strata build -> mantle run -> trace

For fail-closed runtime behavior, the source must check and build, and mantle run must fail only after Mantle admits the artifact and emits trace evidence for the failure. Source-level rejection gates are different: they must fail before build/lowering and must not leave a target artifact behind.

Canonical Gates

The canonical user-facing gate is:

just source-to-runtime-gates

The split entrypoints are available when only one side of the gate is needed:

just source-to-runtime-success-gates
just source-to-runtime-failure-gates

The maintained command list belongs in the executable gate definitions:

• Justfile owns the commands a user or CI runner executes.
• crates/strata-mantle-acceptance/tests/source_to_runtime_gates.rs mirrors the same source-to-runtime contract as integration tests.
• docs/src/examples.md owns the curated list of runnable examples and the behavior each one demonstrates.

This page intentionally does not enumerate every runtime gate. When a new user-visible language or runtime behavior needs source-to-runtime proof, update the executable gate and document the example on the examples page.

Representative Commands

The minimum success gate checks, builds, runs, and traces hello.str:

cargo run -p strata --bin strata -- check examples/hello.str
cargo run -p strata --bin strata -- build examples/hello.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

A richer state/payload gate follows the same shape:

cargo run -p strata --bin strata -- check examples/state_payload_match.str
cargo run -p strata --bin strata -- build examples/state_payload_match.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/state_payload_match.mta

A source rejection gate must fail during checking and must not create a target artifact:

cargo run -p strata --bin strata -- check examples/failures/effect_authority_missing.str

A runtime fail-closed gate checks and builds successfully, then returns non-zero from Mantle after writing trace evidence:

cargo run -p strata --bin strata -- check examples/actor_panic_no_replay.str
cargo run -p strata --bin strata -- build examples/actor_panic_no_replay.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/actor_panic_no_replay.mta

Each successful mantle run command must admit the generated .mta, execute it, and emit an observability trace under target/strata/. Expected-failure gates must return non-zero with source diagnostics or runtime failure evidence at the layer being tested.

When adding a new user-visible language or runtime behavior, add or update an example that follows this shape. A passing unit test is useful, but it does not replace a runnable source-to-runtime command when the behavior is user-facing.

Artifact And Runtime Boundary

Strata owns source syntax, diagnostics, semantic checking, checked IR, and source-visible meaning. Lowering owns conversion from checked Strata IR into Mantle Target Artifacts. Mantle owns artifact admission, runtime execution, process and mailbox state, host boundaries, and observability.

This separation keeps names, metadata, and runtime identity from collapsing into one surface. Source names are useful for diagnostics and traces, but executable runtime dispatch must use loaded typed IDs.

Mantle crates are structurally language-neutral. They may carry source_language as opaque artifact metadata, but they must not own Strata source constants, Strata output-directory defaults, .str examples, or source-to-runtime gates. Strata-owned defaults live in crates/strata; cross-boundary gates live in crates/strata-mantle-acceptance.

Artifact type identity is structural in Mantle. Lowering emits a Mantle type table and artifact records refer to entries by TypeId; Mantle admission and runtime execution do not parse source type spellings or ProcessRef<...> text to decide behavior. Type labels remain diagnostics and trace metadata only.

Admission

Mantle admits artifacts through validation, not filename trust. Before execution, the artifact decoder and validator check:

• artifact magic, format, schema version, and source language;
• bounded process, message, state, output, transition, and action counts;
• bounded type table entries and type-kind targets;
• unique process debug names;
• unique typed state value identities per process;
• unique process reference names per process;
• either one unguarded transition per accepted message or one state-specific transition for each admitted state value;
• exact transition effect authority for emitted, spawned, and sent actions;
• transition references to known messages, state values, type IDs, process references, outputs, and process IDs.

Decode-time bounds must happen before allocation when counts come from the artifact body.

Execution

Mantle loads admitted transitions into indexed runtime tables. Before emitting ArtifactLoaded or executing runtime side effects, Mantle validates loaded entry metadata, state tables, transition state targets and templates, outputs, process references, sends, payload templates, and transition effect authority. A dequeued message selects the transition by typed message ID, and by admitted current state ID when the transition table is state-specific. Dynamic next-state templates resolve to an admitted state ID by typed state value identity, not by display label text.

Transition effect metadata is admitted with the artifact, loaded as runtime effect authority, and must exactly match the action effects that execute.

The action set covers:

• emitting declared output;
• spawning a declared process through a process reference;
• sending a declared message through a bound process reference.

The runtime fails closed on invalid sends, unbound process references, duplicate process-reference bindings, mailbox exhaustion, runtime process instance budget exhaustion, dispatch budget exhaustion, emitted-output budget exhaustion, and trace budget exhaustion.

Observability

Runtime traces are line-delimited JSON. They include labels for readability and numeric IDs for process, message, state, payload type, and output identity. A trace is evidence of runtime execution, not a substitute for running the source-to-runtime gate.

Implementation Architecture

This page maps the source-to-runtime implementation for contributors. It is not required for writing simple Strata programs.

Crate Layout

Source Path

source text
  -> lexer
  -> parser
  -> AST
  -> semantic checker
  -> checked IR
  -> lowering
  -> Mantle Target Artifact

The parser accepts source shape. The checker assigns source-visible meaning, resolves names, validates process/message/state rules, and produces checked IR. It resolves process reference names and source type references into checked IDs, including checked type identities for value and process-reference payloads. Lowering converts checked IR into Mantle artifact tables by mapping checked process, message, state, output, and type IDs to artifact IDs.

Runtime Path

artifact text
  -> decode
  -> validate
  -> load typed runtime tables
  -> spawn Main
  -> deliver entry message
  -> dispatch by message ID
  -> execute actions by typed process references and IDs
  -> write JSONL trace

Mantle must validate artifacts before execution. Runtime dispatch uses loaded typed IDs, not source strings. Payload and state type identity is admitted through Mantle type-table IDs; source type labels are metadata only.

Important Boundaries

Strata owns:

• source syntax;
• diagnostics;
• AST;
• semantic checking;
• checked IR;
• source-visible meaning.

Lowering owns:

• conversion from checked Strata IR into Mantle artifact records;
• mapping checked process, message, state, type, and output IDs to artifact IDs.

Mantle owns:

• artifact decoding and validation;
• admitted runtime tables;
• process instances and mailboxes;
• action execution;
• runtime traces.

Workspace source-to-runtime acceptance gates own the cross-boundary proof that a Strata program can be checked, lowered, admitted by Mantle, executed, and traced.

Do not move source-only assumptions into Mantle as trusted runtime behavior. Do not make Mantle dispatch through labels that exist only for diagnostics or trace readability. Do not move Strata source constants, default output paths, examples, or source-to-runtime gates into Mantle-owned crates.

Adding A Language Feature

A source-facing feature usually needs changes across several layers:

• parser;
• AST;
• checker;
• checked IR;
• lowering;
• artifact schema or validation, when runtime representation changes;
• runtime execution, when behavior changes;
• diagnostics;
• examples;
• docs;
• positive tests;
• negative tests;
• source-to-runtime gates, when user-visible execution changes.

Parser acceptance alone is not enough. If another layer can construct or admit the same invalid state, that layer needs its own validation.

Existing Source-To-Runtime Gates

The runnable examples are:

• examples/hello.str;
• examples/actor_ping.str;
• examples/actor_sequence.str;
• examples/actor_match.str;
• examples/init_match.str;
• examples/function_match.str;
• examples/function_payload_match.str;
• examples/state_payload_enum.str;
• examples/state_payload_match.str;
• examples/actor_instances.str;
• examples/actor_payloads.str;
• examples/actor_payload_match.str;
• examples/actor_reply.str;
• examples/actor_emit_spawn_send.str;
• examples/actor_panic_no_replay.str.

The integration tests in crates/strata-mantle-acceptance/tests/source_to_runtime_gates.rs mirror the same source check, artifact build, and runtime execution sequence:

cargo run -p strata --bin strata -- check examples/hello.str
cargo run -p strata --bin strata -- build examples/hello.str
cargo run -p mantle-runtime --bin mantle -- run target/strata/hello.mta

The same pattern applies to the actor examples. Fail-closed examples check and build, but their runtime gate expects mantle run to return non-zero after emitting trace evidence.

Closure Rule

A change that affects source syntax, artifact schema, runtime behavior, diagnostics, examples, or gates should update this book and pass:

just quality

Docs explain the contract; runnable gates prove the behavior.

Development Gates

Repository automation is centralized in Justfile. GitHub Actions and lefthook delegate to the same recipes used locally.

The standard local verification bundle is:

just quality

This bundle selects stable Rust explicitly through the Justfile. The workspace requires Rust 1.85 or newer for Edition 2024. The bundle also runs just toolchain-policy-check, which rejects repository instructions or workflow steps that switch the whole checkout to nightly Rust. Nightly-only tools must be invoked per command with +nightly.

Run the source-to-runtime gates after changes that affect syntax, checking, lowering, artifacts, runtime behavior, diagnostics, examples, or acceptance criteria.

just source-to-runtime-gates

Continuous Integration

The standard CI workflow installs just and calls just ci-rust on Linux, macOS, and Windows. The Linux quality job calls just ci-quality, which runs formatting, check, tests, clippy, build, tool metadata validation, toolchain policy validation, mdBook, source-to-runtime gates, and diff hygiene.

CI uses GitHub-owned, SHA-pinned checkout and cache actions. The cache stores Cargo registry/git data and per-job build target directories. It does not cache installed executable tools directly; tool installs remain version-pinned and reuse the cached Cargo target directory where possible.

For local Linux CI parity through act:

just ci-local

Fuzzing

The fuzz harnesses live under fuzz/ and run with cargo-fuzz on nightly Rust. They cover three initial boundaries:

• parsing, checking, and lowering arbitrary UTF-8 source;
• decoding and re-encoding arbitrary UTF-8 artifact text;
• running valid lowered artifacts through the in-memory runtime host.

Useful local commands:

just install-fuzz-tools
just fuzz-ci

Miri

Miri runs on nightly Rust. The Miri gate is a smoke suite focused on pure or in-memory paths rather than filesystem-specific CLI behavior.

Useful local commands:

just install-miri-tools
just miri-ci

Every slice that changes user-facing syntax, artifact schema, runtime behavior, diagnostics, examples, or acceptance gates should update this book and pass mdbook build docs.