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:

flowchart LR
    Source[".str source"] --> Check["strata check"]
    Check --> Build["strata build"]
    Build --> Artifact[".mta artifact"]
    Artifact --> Run["mantle run"]

The runnable gates 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
cargo +stable install mdbook-mermaid --version 0.17.0 --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, mdbook, and mdbook-mermaid 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, mdbook --version, and mdbook-mermaid --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:

just build

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

Check A Strata Program

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

just 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.

just strata-build examples/hello.str

Expected result:

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

Run The Program

Mantle validates and executes the generated artifact:

just mantle-run target/strata/hello.mta

Expected output includes:

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

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

Inspect Local Spawn Authority

For programs that declare local spawn authority, the optional inspection commands show the checked source authority surface and the admitted artifact authority tables without changing the normal build or run path:

just strata-authority-summary examples/actor_emit_spawn_send.str
just strata-build examples/actor_emit_spawn_send.str
just mantle-inspect-authority target/strata/actor_emit_spawn_send.mta

Pass json as the final recipe argument when CI or audit tooling needs deterministic machine-readable output.

For checked component composition, the source-side report emits the admitted composition graph, admitted binding facts, and endpoint authority edges without changing the Mantle artifact:

just strata-composition-report examples/component_composition_main.str json
just strata-build examples/component_composition_main.str
just strata-composition-build examples/component_composition_main.str
just strata-composition-admit target/strata/component_composition_main.component-composition.json json
just strata-composition-bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  target/strata/component_composition_main.deployment-composition.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json
just strata-target-requirements examples/component_composition_main.str json
just mantle-feature-declaration json
just mantle-admit target/strata/component_composition_main.mta json

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 bounded/property assurance smoke tests:

just bounded-assurance-smoke

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.

flowchart TB
    subgraph Source["Strata source surface"]
        Records["records and enums"]
        Functions["pure functions"]
        Processes["process declarations"]
        Effects["declared effects"]
    end

    subgraph Runtime["Mantle runtime surface"]
        Instances["process instances"]
        Mailboxes["bounded mailboxes"]
        Ids["loaded typed IDs"]
        Events["runtime events"]
    end

    Source -->|"checked and lowered"| Runtime
    Records -. diagnostics .-> Events
    Processes -. trace metadata .-> Events
    Ids --> Events

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 process-local functions;
• 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:

authority spawn_worker: Cap<Spawn<Worker>>;

let worker: ProcessRef<Worker> = spawn Worker;

The authority declaration is process-local, exact for the target process, and must be used by a local spawn site. 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 functions at module level and inside processes. Functions are checked and expanded before lowering; Mantle does not dispatch by function 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 functions are immutable value producers. They perform no statements, use ! [] ~ [] @det, and return whole values. A process-local function can encapsulate non-message-handling value construction for init, step results, and send payloads.

Payload-bearing enum constructors are source values too. A function 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. For spawn, the effect list is separate from the typed Cap<Spawn<Target>> authority descriptor.

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.

Effectful local sends can also be bound as immutable typed outcomes:

let sent: Result<Unit,SendError<WorkerMsg>> = send worker Ping;

The outcome is a source-visible value, not an exception path. Mantle commits an accepted message and returns Ok(Unit). If local delivery fails before acceptance, the SendError<WorkerMsg> value preserves the original message. Local spawn outcomes use Result<ProcessRef<TargetProcess>,SpawnError<Unit>>; accepted spawns return the committed process reference as step-local authority.

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:

flowchart LR
    Source[".str source"] --> Parse["parse"]
    Parse --> Check["check"]
    Check --> Lower["lower"]
    Lower --> Artifact[".mta artifact"]
    Artifact --> Admit["admit"]
    Admit --> Run["run"]
    Run --> Trace["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 implementation. It is an authoring reference for .str programs, not a description of Mantle artifact internals.

Source Surface

The module declaration names a source unit. Explicit imports connect source units before checking and lowering and define direct cross-unit scope. They do not create packages, libraries, re-exports, visibility modifiers, or runtime boundaries.

Source Unit

A Strata source file starts with a module declaration:

module hello;

After the module declaration, zero or more imports may appear before protocols, ports, components, compositions, records, enums, source functions, and processes. See Tutorial: Hello for the minimal complete source shape.

Imports use the narrow form import module_name;. The CLI resolves module_name to a sibling module_name.str file from the importing source unit, then builds a typed source-unit dependency graph. The graph must be acyclic, module identities must be unique, and unqualified top-level type, function, and process names must not be ambiguous across reachable source units. Cross-unit function names and enum constructor names also share one unqualified callable namespace so flattening cannot turn a transitive source unit into a later call-site ambiguity. Each source unit may use only its own declarations and declarations from its direct imports; transitive imports are not re-exported. Declarations from the reachable graph are checked together in a deterministic dependency-first order. Mantle receives only the lowered target artifact; it does not resolve imports or execute by source-unit names.

Protocol, Port, And Component Boundaries

The current boundary form declares typed protocols, ports, and component exports before lowering. send target via Port Message; proves the target process, protocol message enum, and process-local Cap<PortConnect<Port>> authority, then lowers typed boundary IDs into Mantle. Details are in Boundary Contracts.

Components may declare imported ports with component MainComponent exports MainPort imports WorkerPort requires ...;. A local composition is an implementation-local source admission input for component instances and typed port binding edges, such as bind main imports WorkerPort -> worker exports WorkerPort;.

The checker admits this local input only when instances name visible components, each import is bound once, exports belong to exporters, ports share one protocol, and the binding preserves exact current Cap<PortConnect<Port>> authority. strata composition build <path.str> renders the Strata-owned checked-subset strata.checked_component_composition artifact for that checked local composition graph under target/strata/<stem>.component-composition.json by default, and strata composition admit <path.json> validates the artifact fail-closed before it can be used as checked-subset validation evidence. The artifact is not .mta and is not read directly by Mantle; runtime composition correlation requires a separate explicit mantle.runtime_composition_binding artifact from strata composition bind-runtime. Source names inside it are provenance, diagnostics, and debug metadata only; component-instance IDs, port-binding IDs, port IDs, protocol IDs, and authority descriptor IDs carry the checked meaning. Binding classes outside the current source subset are present as empty fail-closed arrays rather than inferred facts. The older strata composition-report command remains review evidence, not the artifact.

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, authority, bind, bounded, child, component, composition, else, emit, enum, exports, fn, for, if, import, imports, in, instance, let, local, mailbox, match, module, mut, one_for_one, permanent, port, proc, protocol, record, requires, return, security, send, spawn, supervise, target, temporary, transient, type, var, and via are reserved everywhere identifiers are accepted. ProcResult, ProcessRef, Cap, Spawn, ProtocolBoundary, PortConnect, ComponentExport, List, Map, String, Bytes, Unit, Option, Result, SendError, SpawnError, U8, U16, U32, U64, I8, I16, I32, and I64 are reserved type names because they name built-in transition, process-reference, capability descriptor, collection, primitive data, effect outcome, and scalar value 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 function instead, it is expanded as a function call; constructor and function names cannot collide silently.

Scalar Integer Values

Scalar integer source values are fixed-width and explicitly typed. The accepted types are U8, U16, U32, U64, I8, I16, I32, and I64. Numeric value literals require suffixes:

0_u8
10_u32
-1_i16

Unsuffixed numeric value expressions are rejected. Capacity and mailbox-bound numbers remain separate syntax and do not use scalar literal suffixes.

Scalar arithmetic supports +, -, *, /, and % over matching integer types only. Ordering supports <, <=, >, and >= over matching integer types and produces Bool. Equality supports scalar operands with the same integer type. There is no implicit widening, narrowing, signed/unsigned mixing, or string coercion.

Fully concrete scalar expressions fold during checking. Overflow, underflow, statically known division by zero, statically known modulo by zero, out-of-range literals, and malformed suffixes fail before lowering. Runtime-bound scalar expressions lower as typed Mantle value templates with scalar type metadata and fail-closed runtime evaluation. They do not lower as source strings, binding names, or function names.

Scalars are ordinary source values when they do not carry authority: they can be used in source function parameters and returns, source-local bindings, process local pure functions, record fields, message payloads, list/map values, and runtime if predicates through Bool.

Built-In Values

The buildable value surface includes Bool, String, Bytes, Unit, Option<T>, Result<T,E>, SendError<M>, and SpawnError<A>. String and Bytes are reserved immutable data primitives, not dispatch keys or authority carriers. Literals use canonical "..." and b"..." forms with only the escapes documented in the syntax reference; lowering emits typed primitive shapes/templates and lowercase-hex labels such as String(7265616479) and Bytes(010262696e). Payload-bearing enum constructors named String or Bytes are rejected; exact equality requires matching primitive types and adds no dynamic string operations, coercions, structural equality, or authority-in-data.

Bool has the fieldless core values False and True. Bool, False, and True are always available to Strata source and cannot be redeclared by user code or reused as source declaration names, including records, record fields, enums, variants, functions, processes, component instances, process authorities, supervisor children, or boundary declarations. The checker resolves them to core typed IDs, lowering emits the canonical Mantle fieldless enum shape, and Mantle admits and executes only the typed artifact value shape rather than dispatching on source strings. This core surface does not introduce a general prelude, standard library, floats, dynamic string operations, or implicit truthiness.

Unit has the single value Unit. Option<T> has None and Some(T). Result<T,E> has Ok(T) and Err(E). Local send outcomes use Result<Unit,SendError<MessageType>>; local spawn outcomes use Result<ProcessRef<TargetProcess>,SpawnError<Unit>>.

let send_result: Result<Unit,SendError<WorkerMsg>> = send worker Work;
let spawn_result: Result<ProcessRef<Worker>,SpawnError<Unit>> = spawn Worker;

Outcome bindings are immutable and scoped to the step body. They may feed whole-value state transitions when the checker can admit the finite runtime outcome values into the process state table. Spawn successes carry process references, so they remain step-local authority values rather than storable source state. Outcomes may also drive follow-up effects through immutable if conditions such as send_result == Ok(Unit) or spawn_result != Err(Exhausted(Unit)); those tests compare typed built-in variant shape, not process-reference identity. Top-level pre-state effect bindings are declaration ordered: an outcome is usable only after its let statement, and outcome bindings must appear before ordinary non-prefix effects that would otherwise cross the commit-or-return boundary. SendError<M> preserves the original message for pre-acceptance failures, including direct ProcessRef<T> payload metadata; that authority remains a send/message boundary value, not ordinary process state. Admitted variants are Full(M), Stopped(M), Crashed(M), and MailboxClosed(M). Mantle produces Full for capacity preflight, Stopped for normally terminated targets when that cause remains observable, Crashed for failed targets, and MailboxClosed for explicit mailbox closure, supervisor-driven shutdown, or indistinguishable closed-state rejection. A denied admitted port_connect policy is an authority failure rather than a mailbox lifecycle cause, so typed-port send outcomes fail closed before source-visible binding on policy denial. Ordinary source-created Panic(...) still records no-replay evidence and fails before a later sender can recover the target as a source-visible outcome. SpawnError<A> admits Denied(A), Exhausted(A), and BackendUnavailable(A). Mantle produces Denied for denied declared spawn authority, Exhausted for exhausted local process capacity, and BackendUnavailable when the local spawn backend is explicitly unavailable before acceptance; none of those failures admits or executes the rejected child.

Bare statement send and spawn remain fail-closed runtime effects: Mantle rejects pre-acceptance delivery and process-limit failures instead of silently dropping them. Outcome-form send returns the typed failure before acceptance and commits only on Ok(Unit). These outcomes add no source-visible mutation, source-name runtime dispatch, hidden retries, silent drops, or implicit authority grants; Mantle executes the lowered typed artifact templates.

Local Spawn Authority

A process that dynamically creates another local process must declare an exact typed spawn capability:

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

    authority spawn_worker: Cap<Spawn<Worker>>;

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

Cap<Spawn<Worker>> authorizes only dynamic local creation of Worker. A capability for another process, a duplicate or unused descriptor, a malformed descriptor, a self-targeting capability, or a capability targeting the entry process is rejected. The ! [spawn] effect remains exact effect usage; it does not prove spawn authority by itself. After checking, authority declarations lower to typed authority IDs and spawn-site IDs. Source names remain syntax, diagnostics, and trace metadata.

Local Port Authority

authority connect_worker: Cap<PortConnect<WorkerPort>>; authorizes only send ... via WorkerPort from that process. Mismatched, duplicate, or unused port authorities are rejected; ! [send] is effect usage, not authority proof.

Local Supervision

supervise local one_for_one(max_restarts: 2_u32, within_ms: 1000_u64) { child worker: Worker = spawn Worker as permanent; } declares static lexical child processes owned by a process, separate from dynamic Cap<Spawn<Target>> authority. The current surface supports local one_for_one supervisors only. Child names are unique, restart intensity is explicit, modes are permanent, transient, or temporary, and child graphs must be acyclic. send worker Work; resolves worker to typed supervisor and child IDs.

Collections

Lists and maps are immutable source values with explicit numeric capacities. They can be used as source function 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 part of the buildable surface. Repeated canonical map keys are 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 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 may contain fewer entries because bounded list values may be shorter than capacity.

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 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 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; dynamic-key dictionaries remain deferred. Scalar keys are allowed when they are static source values. 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 uses only listed static keys.

Record field and map entry order are preserved in authored values, artifact values, labels, and traces. Projection still addresses map entries by key, and the language exposes no 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 represented 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 process-local 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.

An init function returns one immutable whole state value. It may use a whole-body match or a pure return match over one fieldless enum constructor when the checker can select one arm before lowering:

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

This is not runtime dispatch. The checker proves the fieldless enum scrutinee, checks exhaustiveness and arm shapes, and emits the selected initial state as the existing typed state ID. init return match arms must be statement-free and must return whole state values; nested return matches and payload-binding materialization into the initial state are rejected.

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 function is visible only inside that process. A module function is visible throughout the module. Recursive function call cycles are rejected.

Source function block bodies may introduce sequential immutable source-local values before the terminal return:

fn route(work: Work) -> Phase ! [] ~ [] @det {
    let current: Phase = status(work);
    let selected: Phase = if (current == Active) { Active } else { Idle };
    return selected;
}

Each binding uses let name: Type = value_expr;. The annotated type must be a declared source value type without process-reference authority: String, Bytes, a scalar integer type, a record, enum, List<T,N>, or Map<K,V,N> whose contained types are also source values. A message enum that carries a direct ProcessRef<T> payload is valid as a message type, but it is not a pure source value type. The right-hand side is a pure source value expression and may refer to parameters, pattern bindings, earlier source-local bindings, source function calls, source-time conditionals, return-match values, record/list/map constructors, and Bool/equality predicates. Bindings are immutable and cannot be reassigned.

Source-local bindings may not shadow parameters, pattern bindings, earlier local bindings, constructors, types, processes, or visible source functions. They cannot use ProcessRef<T>, spawn, send, emit, runtime for, mutation, or runtime-only state/payload forms. The checker resolves these names during source function expansion; lowering emits only typed values, templates, typed IDs, and validated artifact data. Source-local binding names do not become Mantle dispatch keys or executable runtime bindings.

Source-function pattern bindings use the same immutable checker namespace. They must not shadow source functions or process-reference bindings introduced by the owning process.

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 function 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 function 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 function 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 function 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 function matches and function return-match expressions may split one top-level constructor when nested typed enum predicates are provably disjoint. The split remains checker-time source dispatch before lowering:

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

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

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

Whole-body function matches can destructure exact list patterns, suffix-only list rest, exact map patterns, and map subset/rest patterns. A wildcard arm may provide fallback:

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 function 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 function whole-body matches and return-match expressions may repeat a top-level constructor only when nested typed enum predicates are provably disjoint; identical predicates, unguarded constructor arms, and unproven overlaps are rejected. Signature groups still keep one clause per top-level constructor. Record body/return matches use one record pattern arm for the matched record type. Collection patterns match exact list length or exact map keys unless they use ..tail, .., or ..rest; _ remains available as a collection fallback. Payload-bearing source function patterns and record/list/map destructuring patterns bind immutable source values. A function call must provide a concrete enum constructor value for signature-pattern, whole-body match, or function return-match dispatch. Record and collection destructuring functions require a concrete value argument after source function expansion. Functions are still expanded before lowering and do not become runtime dispatch entries.

Pure Conditionals

Source functions and pure value expressions can use a source-time value-level conditional:

fn readiness(flag: Bool) -> Readiness ! [] ~ [] @det {
    return if (flag) { WarmReady } else { ColdReady };
}

The equivalent braced pure return form is also supported in source functions. The condition type is exactly core Bool; user declarations of Bool, True, or False are rejected. Both expression-form branches are source value expressions checked against the same expected return, field, state, or payload type. Braced source function return-if branches may contain immutable source-local bindings before the terminal pure return. Branches cannot perform emit, send, spawn, runtime for, branch-local process-reference binding, mutation, or any other runtime statement.

Concrete conditionals are selected during source checking and source function expansion, so lowering sees only the selected value. Runtime-bound value conditionals over Bool lower as typed Mantle value templates containing the condition template and both typed branch value templates. Mantle does not receive a conditional runtime dispatch entry, a source function name, or a source-string branch key.

Typed Equality Predicates

The equality surface is == and != over these operand families:

• core Bool with fieldless False and True values;
• fixed-width scalar integer values with matching scalar types;
• immutable String values and immutable Bytes values with matching primitive types;
• fieldless values of the same payload-free enum type;
• built-in Option, Result, SendError, and SpawnError values only when one side is a safe built-in variant pattern such as None, Ok(Unit), or Err(Exhausted(Unit)).

Both operands must have the same checked type. Concrete source operands fold during checking, so lowering sees only the selected True or False value. Runtime-dependent operands lower as typed Mantle value templates and Mantle evaluates them from typed values. Equality does not dispatch through source names, function names, debug labels, or parser strings.

Structural record/list/map equality, payload enum equality, process-reference equality, direct equality between two spawn outcomes, dynamic string predicates, and matching a preserved message payload by equality are not part of the buildable equality surface.

Boolean Predicate Composition

Bool-producing predicates can be composed with grouping, unary !, binary &&, and binary ||:

if ((flag == True) && !(status == Done)) {
    emit "still active";
} else {
    emit "complete";
}

Every composed operand must produce core Bool. The supported operands are direct Bool values or templates, typed equality predicates, typed scalar-ordering predicates, and nested Boolean predicate composition. Fully concrete source predicates fold during checking. Runtime-dependent predicates lower into typed Mantle value templates; Mantle validates the typed tree, validates all operands, evaluates it from typed runtime values, and records the selected branch through the existing branch_selected trace event.

Predicate composition does not add floats, dynamic string operations, structural equality, payload enum equality, process-reference equality, assignment, mutation, or authority.

Runtime branching, runtime iteration, statements, effects, step patterns, state transitions, and limits are documented in Runtime Reference.

Boundary Contracts

Boundary declarations give source-visible communication an explicit typed contract before it reaches Mantle.

protocol WorkerProtocol message WorkerMsg requires Cap<ProtocolBoundary<WorkerProtocol>>;
port WorkerPort protocol WorkerProtocol target Worker requires Cap<PortConnect<WorkerPort>>;
component WorkerComponent exports WorkerPort requires Cap<ComponentExport<WorkerComponent>>;

WorkerMsg must be a named enum. WorkerPort must target a declared process whose type Msg is WorkerMsg. WorkerComponent exports that port. The required capability descriptors must point back to the declaration being defined; mismatched descriptors are rejected.

Components can also declare imported ports and a local composition can bind component instances through typed port edges:

component MainComponent exports MainPort imports WorkerPort requires Cap<ComponentExport<MainComponent>>;

composition AppComposition {
    instance main component MainComponent;
    instance worker component WorkerComponent;
    bind main imports WorkerPort -> worker exports WorkerPort;
}

The checker builds typed component-instance IDs and typed port-binding edges before lowering. A composition is admitted only when every component import is bound exactly once, both instances are declared, the importing component actually imports the port, the exporting component actually exports the port, and the two ports share one protocol. Direct source-unit imports still control which components and ports are visible; transitive-only component or port access is rejected.

A typed boundary send uses the optional via clause:

authority connect_worker: Cap<PortConnect<WorkerPort>>;

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

Checking proves all of these facts before lowering:

• the send target is a typed ProcessRef<Worker>;
• WorkerPort targets Worker;
• WorkerProtocol uses WorkerMsg;
• Work is a variant of WorkerMsg;
• the sending process declares and uses exact Cap<PortConnect<WorkerPort>> authority.

After checking, boundary references are typed IDs. Lowering emits Mantle protocol, port, component, composition, authority, and action tables with those IDs. Mantle admits the tables before ArtifactLoaded and runtime dispatch uses admitted process, message, and port IDs. Protocol, port, component, component instance, process, and message names are metadata for diagnostics and traces only.

Invalid boundary shapes fail closed at the earliest layer that can see them. A source program with an undeclared port, mismatched protocol message type, missing port authority, duplicate boundary name, ambiguous direct import, unbound component import, duplicate component import binding, unimported-port binding, protocol-mismatched or port-authority-mismatched composition edge, or reserved descriptor type name fails checking. A hand-authored artifact with mismatched boundary table IDs, unimported-port composition binding, missing port authority, malformed composition edge, port-authority mismatch, or unbound component import fails admission before runtime events begin.

Typed boundary sends emit boundary_send_checked runtime trace events before mailbox acceptance. Accepted sends continue to message acceptance; admitted authority-policy denials record boundary_result=denied and stop before target message side effects. Invalid boundary shapes are still admission diagnostics, not runtime trace events, because they do not enter runtime dispatch or produce ArtifactLoaded.

Run the source-to-runtime example with:

just run-example boundary_contracts_main
just run-example component_composition_main

Current implementation limits: the source composition form is a local typed graph admission input for component instances and port bindings. strata composition build checks that graph and emits the Strata-owned checked-subset strata.checked_component_composition validation artifact; it is not .mta, is not Mantle runtime input, and it does not add remote send, distributed transport, capability binding syntax, deployment manifests, package resolution, hot upgrade, or generated port stubs. Runtime composition correlation requires the separate explicit strata composition bind-runtime bridge, which validates admitted checked composition evidence against a matching .mta and emits mantle.runtime_composition_binding for mantle run --composition-binding. Binding classes outside the current source subset are emitted as empty arrays and fail closed if forged non-empty. Use just strata-composition-report examples/component_composition_main.str json for review evidence, and just strata-build examples/component_composition_main.str plus just strata-composition-build examples/component_composition_main.str plus just strata-composition-admit target/strata/component_composition_main.component-composition.json json plus just strata-composition-bind-runtime target/strata/component_composition_main.component-composition.json target/strata/component_composition_main.mta target/strata/component_composition_main.deployment-composition.json when CI needs fail-closed Strata-owned checked-subset validation evidence and the explicit runtime-correlation binding. Use just strata-target-requirements examples/component_composition_main.str json to inspect the typed Mantle runtime features Strata requires for the checked program. strata authority-summary ... --format json also reports the checked component-boundary authority edge summary for the same checked IR. Mantle admits the lowered .mta by comparing embedded typed requirements against mantle feature-declaration; it does not consume source-side reports or composition validation artifacts.

Runtime Reference

This page documents Strata source forms that lower to typed Mantle runtime behavior. It continues the authoring reference from Language Reference.

Runtime Feature Declaration And Target Binding

Every lowered .mta artifact carries a typed target_requirements block. For Strata, the block is derived from checked IR and lowering facts: local execution, bounded mailboxes, trace support, local spawn/send/effect use, runtime branches and loops, typed value templates, typed effect outcomes, boundary tables, and component-composition metadata where those surfaces are present.

Mantle publishes its own runtime feature declaration for the current local-only target profile, mantle.local_only.v1:

just mantle-feature-declaration json

Admission compares the artifact identity and typed requirements against that profile-backed declaration and reports the admitted runtime_profile:

just strata-target-requirements examples/component_composition_main.str json
just mantle-admit target/strata/component_composition_main.mta json

Current implementation limits are runtime implementation limits, not Strata language law. The admitted profile is single-host local runtime execution with explicit local host sinks, no ambient network authority, no transport authority, no cluster membership, and no admitted remote operation policy. Remote send, remote spawn, distributed transport, cluster membership, package management, hot upgrade, generated stubs, native output, and serialized execution-plan bytecode remain unsupported. Mantle may compile an admitted LoadedProgram into internal executable plans for dispatch and value-template evaluation, but .mta remains the language-neutral boundary. Strata does not emit bytecode or executable template programs. Unsupported required features, malformed source-language metadata, or invalid loaded template references fail before ArtifactLoaded and runtime side effects. Mantle treats source language as opaque artifact metadata and never dispatches on source names.

Mantle execution is host-boundary explicit: after artifact admission and loaded runtime-table construction, the runtime core records events, program stdout, monotonic clock reads, and final flushes through a RuntimeHost. mantle run is the filesystem/stdout host adapter that writes *.observability.jsonl and program output; in-memory execution uses the same admitted runtime core with in-memory sinks. Program-output trace events are written before stdout so failed stdout sinks still leave audit evidence; mandatory host sink setup, write, or flush failures fail closed before the CLI prints a successful run report.

Admitted Authority/Effect Binding

Authority/effect facts cross through .authority-effect.json; typed policy decisions cross through .authority-policy.json; Strata binds both with a matching .mta into .authority-effect-binding.json. Mantle consumes only --authority-effect-binding, validating schema/source namespace, .mta identity, typed descriptors/effects, and the closed policy table before side effects. Raw checked sidecars are never valid Mantle runtime input.

Runtime Branching

Step bodies can use a final-position runtime if whose condition is a checked Bool value template, or a statement-level runtime if whose branches run effects and then continue to the enclosing final return:

fn step(state: WorkerState, Branch(flag: Bool)) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    if (flag == True) {
        emit "worker took warm branch";
        return Stop(WarmReady);
    } else {
        emit "worker took cold branch";
        return Stop(ColdReady);
    }
}

fn step(state: WorkerState, Branch(flag: Bool)) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    if (flag != False) {
        emit "worker handled true";
    } else {
        emit "worker handled false";
    }
    return Continue(state);
}

Statement-level runtime branches also support guard/no-op shapes:

fn step(state: WorkerState, Check(flag: Bool)) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    if (flag == True) {
        emit "guard saw true";
    }
    if (!(flag == False)) {
        emit "guard enabled";
    } else {
    }
    if (flag == True) {
    } else {
        emit "guard saw false";
    }
    return Continue(state);
}

This is ordinary runtime branching. If the condition depends on the received payload or current state payload, Strata lowers the checked condition, branch actions, and any branch next states into the Mantle artifact. Mantle validates the typed condition, validates both branches, executes only the selected branch, and records branch_selected trace events with a stable artifact branch_path. Branch effects must be declared by the step effect list. Statement-level runtime branches may contain one direct nested statement-level runtime branch action; deeper direct branch nesting is rejected at source checking, artifact admission, and loaded-runtime admission. Runtime branch statement prefixes cannot bind source-local values or process references. Branches may contain bounded runtime for statements, including effect-only loop prefixes before the terminal return in final-position runtime branches. Each loop body remains the same runtime-loop body surface. Final-position branch prefixes may also contain one direct statement-level runtime if action; deeper direct branch-action nesting remains rejected. A final-position runtime branch may end in one direct nested final-position runtime if, which lowers as a bounded nested NextState::IfElse; third-level terminal runtime branches remain rejected at source checking, artifact admission, and loaded-runtime admission. An omitted statement-level else lowers as an explicit empty branch. Empty statement-level branches perform no effects, no state change, no authority acquisition, and no hidden work; branch selection is still observable through branch_selected. One branch may be empty when the sibling branch contains at least one action. Both branches empty are rejected at source checking, artifact admission, and loaded-runtime admission. Final-position runtime branches must return the same step result from both branches. Statement-level runtime branches cannot return; state changes still occur only through the enclosing immutable whole-value Continue, Stop, or Panic return.

Scalar ordering, scalar equality, and checked scalar arithmetic are supported over matching fixed-width integer types. Exact String and Bytes equality is supported over matching primitive types. Runtime-bound scalar/primitive predicates and pure value conditionals lower as typed Mantle templates; Mantle admission and runtime evaluation validate those templates in admitted value-template positions. Unbounded loops, Mantle-side import resolution, floats, dynamic string operations, structural collection comparison, and a standard library remain outside the buildable runtime surface.

Runtime Iteration

Step bodies can use a bounded runtime for loop over an immutable typed list binding:

authority spawn_worker: Cap<Spawn<Worker>>;

fn step(state: BatchState, Batch(items: List<Bool,2>)) -> ProcResult<BatchState> ! [spawn, send] ~ [] @det {
    let worker: ProcessRef<Worker> = spawn Worker;
    for item in items {
        send worker Branch(item);
    }
    return Stop(state);
}

This is ordinary runtime iteration. The collection source must be an identifier binding that checks as List<Element,N> and remains runtime-bound, such as a message payload binding. Strata lowers the checked collection template, typed loop element ID, immutable element binding, maximum item count, and body actions into the Mantle artifact. Mantle validates the loop structure and body, executes the body once per runtime element in collection order, enforces the collection length and runtime fuel limits, and records loop_started, loop_iteration, and loop_completed trace events.

The loop element is immutable and may be used only as a typed value template in the loop body. A loop item may also use a record pattern over the element type, for example for Job { phase: routed_phase } in jobs { ... }. That binds an immutable projected field value for the loop body; lowering emits a typed record field projection from the active loop element, not an executable source binding name. Loop bodies may use statement-level runtime if over the active loop element, a projected loop-element field, or another checked Bool template, including the same one-sided no-op branch shapes supported outside loops. Mantle selects the branch during execution and records branch_selected inside the loop trace with the active loop element ID and iteration index. Bounded loops may also appear inside statement-level runtime branches, allowing a guard to select or skip a whole loop. If the selected branch is empty, Mantle records only the outer branch_selected event and emits no loop events. If the selected branch contains the loop, trace order is branch_selected, loop_started, ordered loop_iteration body effects, and loop_completed.

The loop body is intentionally narrow: no nested loops, no spawn, no return, no assignment, and no process-reference element type. A loop body may contain the statement-level runtime if / no-op shape, including one direct nested statement-level runtime branch and including when the loop is itself inside a selected guard branch. Deeper direct branch nesting remains rejected. Send targets may be process references bound before the loop or direct ProcessRef<T> payloads received by the current step. Declare every body effect in the enclosing step effect list.

Statements

The accepted statements are:

emit "text";
let worker: ProcessRef<Worker> = spawn Worker;
send worker Ping;
if (flag == True) { emit "true"; } else { emit "false"; }
if (flag == True) { emit "true"; }
if (flag == True) {} else { emit "false"; }
for item in items { send worker Branch(item); }
for item in items { if ((item != False) && !(item == False)) { send worker Branch(item); } }
for Job { phase: routed_phase } in jobs { send worker AssignPhase(routed_phase); }
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.

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 checked target process ID. Source names remain diagnostics and trace metadata.

Received references can also be used as send targets inside statement-level branches and bounded loop bodies. This does not make process references general source values: they remain direct message payload authority, and lowering emits typed received-payload send targets rather than source binding names.

Current process-reference boundaries:

Patterns are source-level syntax for typed value decomposition. The current runnable surface supports constructor patterns, constructor payload bindings, nested constructor and record/list/map payload destructuring, function return-match expressions, and wildcards. Normal source functions 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. Whole-body match msg arms and step parameter patterns may split one top-level message constructor by exact nested typed payload predicates when those predicates are provably disjoint over discovered concrete payload cases. Checking resolves each arm into typed message-keyed transitions, typed payload guards when needed, and typed projection templates before lowering. Mantle still dispatches by typed message IDs, current state IDs when a transition is state-specific, payload type IDs, exact typed payload identity, 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 typed message ID plus checked current state ID, and runtime selection fails closed if the current state is not in the loaded state table.

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 exact source-level effect usage for each step clause. It must exactly match the clause actions. For a match msg, match state, or step return match step, the one effect list applies to every generated transition. Match-body arms must use exactly those effects. A return-match uniform prefix lowers the same actions onto each selected transition, and selected-arm prefixes must still leave every generated transition with exactly the declared effects. Missing, duplicate, and unused declared effects are rejected before lowering.

Dynamic local process creation also requires a process-local typed authority declaration such as authority spawn_worker: Cap<Spawn<Worker>>;. The ! [spawn] effect proves that the transition uses spawning; it does not prove which process may be spawned.

Lexical local supervisor children are a separate authority path. Mantle starts static children declared by supervise local one_for_one(...) in declaration order, stops them in reverse declaration order when the owning process stops, and routes send child_name Message; through admitted supervisor and child IDs. Source checking, artifact validation, and loaded-runtime admission reject cyclic local supervisor child graphs before startup. Restarted children receive fresh runtime process IDs and rerun init; Mantle does not replay accepted messages, effects, or previous state after a crash. permanent children restart after normal stop or panic, transient children restart after panic only, and temporary children are not restarted. Restart intensity is enforced per supervisor plan. If restart intensity, runtime process capacity, or the default same-monotonic-tick throttle denies a restart, Mantle fails the supervisor scope and reports the scope failure in the runtime trace. Forced child-tree stops are reported with supervisor-specific stop reasons, not as source-level normal termination.

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

Authority Inspection

Authority inspection is an optional tooling surface. It does not run during normal check, build, or run commands, and it does not write a report file.

The source-side command checks Strata source and prints the checked process authorities and spawn-site classifications before lowering:

just strata-authority-summary examples/actor_emit_spawn_send.str
just strata-authority-summary examples/actor_emit_spawn_send.str json

The artifact-side command admits a Mantle Target Artifact and prints the artifact authority and spawn-site tables without executing the program:

just strata-build examples/actor_emit_spawn_send.str
just mantle-inspect-authority target/strata/actor_emit_spawn_send.mta
just mantle-inspect-authority target/strata/actor_emit_spawn_send.mta json

Text output is intended for local review. JSON output is deterministic and uses typed process IDs, authority IDs, capability descriptors, spawn-site IDs, supervisor IDs, supervisor child IDs, child modes, and restart-intensity fields so CI and audit tooling can compare the source-side and artifact-side authority surfaces. Process, authority, and child labels are included only as metadata.

Composition admission reporting and component-composition artifact admission stay Strata-side. Runtime correlation requires a separate explicit binding step:

just strata-composition-report examples/component_composition_main.str
just strata-composition-report examples/component_composition_main.str json
just strata-build examples/component_composition_main.str
just strata-composition-build examples/component_composition_main.str
just strata-composition-admit target/strata/component_composition_main.component-composition.json json
just strata-composition-bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  target/strata/component_composition_main.deployment-composition.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json

The report is emitted from checked Strata composition facts and a diagnostic FNV-1a source fingerprint. It records typed component-instance IDs, typed component import/export port obligations, typed port-binding IDs, admitted binding results, empty unsatisfied imports for admitted compositions, component export authority surfaces, endpoint port authority requirements, and cross-component authority edges. The component-composition artifact is the durable JSON form of that source-side checked-subset validation evidence and self-identifies as strata.checked_component_composition. It is not .mta and is not read by Mantle. strata composition bind-runtime validates an admitted checked composition artifact against a matching .mta and emits the separate mantle.runtime_composition_binding JSON artifact. Mantle accepts that binding only when supplied with --composition-binding; without it, Mantle executes the .mta normally and emits no composition/deployment correlation fields.

just strata-target-requirements examples/actor_ping.str
just strata-target-requirements examples/actor_ping.str json
just mantle-feature-declaration
just mantle-feature-declaration json

strata target-requirements checks and lowers source, then prints the runtime feature IDs embedded in the generated artifact. mantle feature-declaration prints the current mantle.feature_declaration.v6 metadata: artifact format, schema version, source-language metadata policy, local containment and mailbox models, conservative message-observation fields, allocation fields, validity-window defaults, component/spawn observability fields, supported runtime features, and unsupported implementation limits. Mantle admission derives the minimum feature set required by the .mta tables and requires the embedded target requirements to cover that set. The reports do not execute source names or alter runtime state.

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 rejected; use the constructor pattern without destructuring when the payload is ignored. Multiple parameter-pattern or state-match step clauses may share one top-level message constructor only when exact nested typed payload predicates are provably disjoint. For state-match clauses, each accepted payload case expands across the checked current-state cases from the match state body, and lowering emits typed transitions keyed by message ID, current state ID, and exact typed payload guard. A wildcard step pattern may cover discovered concrete payload cases not matched by explicit payload-sensitive step-signature or state-match clauses. The fallback lowers to exact typed payload-guarded transitions for those discovered cases; it is not an open-ended runtime catch-all for future payload values. State-match fallback cases additionally expand across the checked current-state cases from the fallback match state body before lowering.

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, or every discovered concrete payload case inside a payload-sensitive split, must resolve to exactly one generated transition. Explicit constructor clauses handle their named variants. One wildcard clause may cover variants that do not have explicit clauses. When payload-sensitive step-signature or state-match splitting is active for a variant, the same wildcard may cover only discovered concrete payload cases not matched by explicit payload predicates. Duplicate explicit clauses, overlapping payload predicates, missing coverage, duplicate wildcard clauses, missing variant 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, current state ID when a transition is state-specific, and exact typed payload identity when a payload guard exists. Payload-bearing variants keep one stable typed 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);

A step body may also use return match over a concrete enum source value binding when the checker can reduce the match to one typed transition before lowering. Statements before the return match are a uniform action prefix; the checker lowers that same typed action list onto every generated transition. The selected arm may then perform its own typed action-block prefix, including emit, direct in-scope send, statement-level runtime if, and bounded runtime for actions, before the terminal whole-value result:

fn step(state: WorkerState, Envelope(Assign(phase: Phase))) -> ProcResult<WorkerState> ! [emit] ~ [] @det {
    emit "return-match prefix";
    return match phase {
        Ready => {
            emit "ready arm prefix";
            return Continue(SawReady);
        }
        Done => {
            emit "done arm prefix";
            return Stop(Done);
        }
    };
}

This form is not runtime dispatch. The checker requires an immutable enum source binding with a concrete value proven during step clause or state-match expansion, checks every arm as a ProcResult<StateType>, selects the matching arm, and lowers the selected arm to the existing typed transition shape. Uniform prefix effects occur before the selected arm prefix in source program order and remain committed runtime actions. Selected arm prefixes use the same statement-level action sequencing as a step body: local emit, in-scope direct send, statement-level runtime if, and bounded runtime for over checked runtime List<T,N> bindings. The checker still validates every arm template fail-closed before selected actions lower as typed Mantle artifact actions. Arm-local spawn, process-reference binding, nested runtime for statements, final-position runtime if, nested return matches, matching state, matching non-enum values, and dynamic payload catch-all dispatch are rejected.

Typed Effect Outcomes

Local send and spawn operations can bind typed immutable outcomes in step bodies:

let spawn_result: Result<ProcessRef<Worker>,SpawnError<Unit>> = spawn Worker;
let send_result: Result<Unit,SendError<WorkerMsg>> = send worker Work;
return Stop(MainState { sent: send_result });

These bindings lower to typed Mantle effect-outcome IDs and typed value templates. Source binding names are not runtime dispatch keys. When an outcome template is used as a next-state value, the checker admits the finite outcome states required by that transition before artifact execution. Spawn outcome successes carry process references, so they are kept as step-local authority values and are not admitted as ordinary source state.

The source checker enforces declaration order for outcome bindings. An outcome is visible only after its binding statement, and outcome bindings must precede ordinary effect statements. Process-reference spawns in that prefix are executed before state resolution so outcome sends can target them. Process-reference spawns after ordinary effects execute in ordinary source order and cannot be used by later outcome bindings.

For local send outcomes, Mantle checks target process, lifecycle mailbox state, and mailbox capacity before accepting the message. Accepted sends commit and return Ok(Unit); pre-acceptance failures return Err(Full(message)), Err(Stopped(message)), Err(Crashed(message)), or Err(MailboxClosed(message)) with the original message preserved. Stopped is produced for normally terminated targets when that cause remains observable. MailboxClosed is reserved for explicit mailbox closure, supervisor-driven shutdown, or indistinguishable closed-state rejection. A denied admitted port_connect policy is a typed authority failure rather than a mailbox lifecycle cause; both bare typed-port sends and typed-port send outcomes fail closed as runtime errors before delivery after recording boundary_send_checked denial evidence. Ordinary source-created Panic(...) still records no-replay evidence and fails before a later sender can recover the target; direct ProcessRef<T> message metadata remains send/message-boundary authority and does not become storable source state.

For local spawn outcomes, accepted spawns commit the new process and return Ok(process_ref) with a typed ProcessRef<TargetProcess> payload. If process authority is denied by the admitted runtime policy before acceptance, Mantle returns Err(Denied(Unit)); if process capacity is exhausted before acceptance, Mantle returns Err(Exhausted(Unit)); if Mantle has no available local spawn backend for this run, it returns Err(BackendUnavailable(Unit)) before acceptance. Bare statement send and spawn still fail closed: pre-acceptance failure is reported as a runtime error instead of being silently dropped.

The mantle run CLI accepts --max-runtime-processes N for bounded local execution and rejects missing, zero, non-integer, and overflowed values before execution. With --max-runtime-processes 1, the exhausted-spawn example observes Err(Exhausted(Unit)) after the entry process consumes capacity; no Worker is admitted or executed. The CLI also accepts --disable-local-spawn-backend for bounded local backend-unavailable testing; outcome-form spawn returns Err(BackendUnavailable(Unit)), while bare spawn and lexical supervisor child startup fail closed before binding or admitting a child process. Mantle records each typed outcome binding as effect_outcome_bound trace evidence with the numeric outcome_id, outcome action, target process ID, and closed result category. The event proves whether a source-visible outcome came from accepted runtime work, denied spawn authority, exhausted process capacity, or a pre-acceptance send failure without using source binding names as runtime dispatch keys.

Outcome values can also drive follow-up effects through ordinary immutable branching:

if (spawn_result != Err(Exhausted(Unit))) {
    emit "spawn accepted";
} else {
    emit "spawn rejected";
}

if (send_result == Ok(Unit)) {
    emit "send accepted";
} else {
    emit "send not accepted";
}

These conditions branch on a typed built-in variant pattern. They do not add structural equality for preserved message payloads, and they do not compare process-reference identities from Ok(process_ref) spawn outcomes.

examples/effect_outcome_mailbox_full.str, examples/effect_outcome_stopped_target.str, examples/process_ref_stale_lifecycle.str, and examples/local_supervision_inactive_crashed_send_outcome.str exercise source-to-runtime pre-acceptance send failure outcomes; the stale lifecycle gate keeps a newer same-definition worker running while a transported old PID returns Err(Stopped(message)) instead of retargeting. The denied-, exhausted-, and backend-unavailable spawn examples check/build the same typed local spawn outcome shape, then run Mantle with denied admission, an exhausted process limit, or a disabled local spawn backend. Each rejected spawn outcome records typed trace evidence and admits no child process.

Current pattern-matching closure boundaries:

State changes are immutable whole-value transitions. There is no assignment statement, no source-visible field mutation, and no payload rewrite inside an existing process state.

Limits

The buildable language surface enforces bounded sizes:

These limits are part of the 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 import_decl* top_level_decl*
module_decl =
    "module" ident ";"
import_decl =
    "import" ident ";"
top_level_decl =
    record_decl
  | enum_decl
  | protocol_decl
  | port_decl
  | component_decl
  | composition_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.

Imports must appear immediately after the module declaration and before any top-level declaration. The current import form admits one source-unit module identifier and resolves it from the importing source unit’s directory; aliases, wildcards, re-exports, packages, and path strings are not accepted.

Protocols, Ports, And Components

protocol_decl =
    "protocol" ident "message" ident "requires" type_ref ";"
port_decl =
    "port" ident "protocol" ident "target" ident "requires" type_ref ";"
component_decl =
    "component" ident "exports" ident component_imports? "requires" type_ref ";"
component_imports =
    "imports" ident ("," ident)*
composition_decl =
    "composition" ident "{" composition_item* "}"
composition_item =
    component_instance
  | port_binding
component_instance =
    "instance" ident "component" ident ";"
port_binding =
    "bind" ident "imports" ident "->" ident "exports" ident ";"

A protocol names one enum message type, a port binds that protocol to one target process, and a component exports one port with zero or more imported ports. A composition declares local component instances and port binding edges from an imported port on one instance to an exported port on another instance. This is the current implementation’s local source admission input. strata composition build emits Strata-owned checked-subset evidence (strata.checked_component_composition), not .mta or direct Mantle input. Runtime correlation requires a separate explicit mantle.runtime_composition_binding artifact from strata composition bind-runtime. Source names are metadata only; typed component-instance, import/export port, port-binding, port, protocol, and authority descriptor IDs carry meaning. Unsupported binding classes stay empty fail-closed arrays; strata composition-report remains Strata-owned review evidence. The required authority annotations must be exact: Cap<ProtocolBoundary<ProtocolName>>, Cap<PortConnect<PortName>>, and Cap<ComponentExport<ComponentName>>. See Boundary Contracts for the checked and lowered contract. Capability bindings, remote bindings, package manifests, and port stubs are not part of this implementation surface.

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
  | authority_decl
  | supervisor_decl
  | init_function
  | step_function
  | source_function
state_alias =
    "type" "State" "=" type_ref ";"
message_alias =
    "type" "Msg" "=" type_ref ";"
authority_decl =
    "authority" ident ":" process_authority_type ";"
process_authority_type =
    "Cap" "<" "Spawn" "<" ident ">" ">"
  | "Cap" "<" "PortConnect" "<" ident ">" ">"
supervisor_decl =
    "supervise" "local" "one_for_one" "(" "max_restarts" ":" number "_u32" "," "within_ms" ":" number "_u64" ")" "{" supervisor_child+ "}"
supervisor_child =
    "child" ident ":" ident "=" "spawn" ident "as" ("permanent" | "transient" | "temporary") ";"

The aliases, authority declarations, supervisor declarations, and functions may appear in any order. State, Msg, and init must each appear exactly once. Cap<Spawn<ProcessName>> and Cap<PortConnect<PortName>> authorities must target declared objects and be used by matching local actions. Non-init/step functions are process-local source functions. A local supervisor declares static lexical children and does not grant dynamic spawn authority. Each concrete message case must resolve to one generated transition through an explicit constructor pattern, one wildcard pattern, one match msg body, or a state-match step for a constructor or wildcard message pattern. Parameter-pattern, state-match, and whole-body match msg dispatch may split same-constructor clauses by exact typed payload guard when nested predicates are disjoint over discovered payload cases. A process cannot mix parameter-pattern/state-match forms with a match msg step body. 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 "(" constructor_payload_pattern ")"
  | ident "{" record_pattern_fields "}"
  | "List" list_type_args? "[" list_pattern_items? "]"
  | "Map" map_type_args? "[" map_pattern_entries? "]"
  | "_"
constructor_payload_pattern =
    ident ":" type_ref
  | ident
  | ident "(" constructor_payload_pattern ")"
  | ident "{" record_pattern_fields "}"
  | "List" list_type_args? "[" list_pattern_items? "]"
  | "Map" map_type_args? "[" map_pattern_entries? "]"
  | "_"
record_pattern_fields =
    record_pattern_field ("," record_pattern_field)* ","?
record_pattern_field =
    ident
  | ident ":" ident
list_type_args =
    "<" type_ref "," number ">"
map_type_args =
    "<" type_ref "," type_ref "," number ">"

list_pattern_items =
    collection_pattern_binding ("," collection_pattern_binding)* ("," ".." ident ","? | ","?)

map_pattern_entries =
    ".." ident? ","?
  | value_expr "=>" collection_pattern_binding
    ("," value_expr "=>" collection_pattern_binding)*
    ("," ".." ident? ","? | ","?)

collection_pattern_binding =
    nested_collection_pattern
  | ident
  | "_"

nested_collection_pattern =
    ident "(" constructor_payload_pattern ")"
  | ident "{" record_pattern_fields "}"
  | "List" list_type_args? "[" list_pattern_items? "]"
  | "Map" map_type_args? "[" map_pattern_entries? "]"

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

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

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

determinism =
    "@det" | "@nondet"

Collection pattern bindings that begin with an identifier are nested patterns only when the identifier is followed by ( or {, or when List/Map is followed by optional type arguments and [. Otherwise the identifier is an immutable binding name.

Buildable source accepts bodies for init, step, module functions, and process-local functions. It requires deterministic functions and empty may-behavior lists. Normal source functions are pure: they use ! [], allow only source value expressions, immutable source-local bindings, and pure braced return branches, perform no runtime statements, and are expanded before lowering.

Function Bodies

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

block_body =
    block_statement* (return_statement | return_if_else)

block_statement =
    source_function_statement
  | runtime_statement

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

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

Patterns are source-level binding and decomposition syntax. Strata supports constructor patterns, constructor payload bindings/destructuring, record destructuring patterns, list/map collection patterns, and _ wildcards. Buildable semantic consumers are normal source function signatures and match bodies, function return-match expressions, fieldless enum init matches, actor step dispatch, message-specific match state step bodies, and step return-match expressions with optional uniform action prefixes. Record/list/map destructuring patterns are accepted in those payload-capable positions when the payload has the matching type. These forms may split a top-level constructor by disjoint exact nested typed payload predicates. Source function calls still expand before lowering; enum pattern dispatch requires a concrete enum constructor value and record/list/map destructuring requires a concrete value.

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 "(" constructor_payload_pattern ")" | "_") ")"
    "->" "ProcResult" "<" type_ref ">"
    "!" effect_list "~" "[]" "@det"
    "{" block_body "}"

The first type_ref names the process state type. The message pattern is a constructor, payload constructor, or _. Patterns bind immutable transition locals, may destructure concrete records/lists/maps and nested constructors, and use fieldless nested enum constructors as typed shape predicates. List rest is suffix-only after at least one fixed element. Map patterns are exact unless they end in .. or ..rest; ..rest binds the remaining immutable map.

Multiple parameter-pattern step clauses may share one top-level message constructor only when exact nested typed payload predicates are provably disjoint. A wildcard fallback may cover only discovered concrete payload cases not matched by explicit payload-sensitive clauses. The fallback lowers to exact typed payload-guarded transitions for those discovered cases; it is not a runtime catch-all for future payload values.

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 constructor or wildcard pattern syntax. Constructor payload patterns may bind or destructure nested constructor, record, list, and map payloads. Arms that share one top-level message constructor may split by exact typed payload guard when their nested predicates are provably disjoint. 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 "(" constructor_payload_pattern ")" | "_") ")"
    "->" "ProcResult" "<" type_ref ">"
    "!" effect_list "~" "[]" "@det"
    "{" "match" "state" "{" match_arm+ "}" "}"

State-match arms resolve against the declared process state enum. Payload variants may bind the whole payload or destructure concrete record/list/map and nested constructor payloads. Bindings are immutable and transition-local. Each generated transition is keyed by message ID and checked current state ID, with an exact typed payload guard when payload-sensitive clauses split. State changes still occur only by returning a whole value through Continue(...), Stop(...), or Panic(...).

In a block-bodied step, the return expression may be a match over a transition-local enum source binding whose concrete value is already proven by step clause or state-match expansion. Any statements before the return match are a uniform action prefix for every selected lowered transition:

step_return_match =
    "return" "match" ident "{" match_arm+ "}" ";"

Every arm body may use local emit, in-scope direct send, statement-level runtime if, and bounded runtime for before the terminal result. The checker validates each arm fail-closed, selects the concrete arm before lowering, and emits the same typed transition metadata as a direct step return. Arm-local spawn, process-reference binding, nested runtime for, final-position runtime if, nested return matches, catch-all dispatch, source-string selectors, and source-function or init arm statements remain rejected.

In a pure block-bodied init, the return expression may be a match over one fieldless enum constructor:

init_return_match =
    "return" "match" ident "{" match_arm+ "}" ";"

Every arm body must be statement-free and must return one whole state value. The checker selects the concrete arm before lowering and emits the selected initial state as the existing typed state ID. This syntax does not allow effect statements before the return match, nested return matches in arms, dynamic dispatch, or source-string selectors.

A normal source function 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 "}")

Function block bodies must not contain effect statements, process-reference bindings, sends, or runtime loops. They may contain zero or more immutable source-local value bindings before the terminal return:

source_local_binding =
    "let" ident ":" type_ref "=" value_expr ";"

The binding type must be a source value type without process-reference authority, and the value expression must be pure. Message enums that carry direct ProcessRef<T> payloads are message authority surfaces, not source-local value types. Source-local bindings are distinct from ProcessRef<T> spawn bindings and are rejected in init, step, statement-level runtime branches, or runtime loop bodies.

Function match bodies match the function’s typed binding parameter. A function block may also return a match over an in-scope source value binding, or use braced pure return branches:

fn readiness(flag: Bool) -> Readiness ! [] ~ [] @det {
    if (flag) {
        return WarmReady;
    } else {
        return ColdReady;
    }
}

The braced form is pure control flow for returned values. Each branch may contain immutable source-local bindings before its terminal return. Concrete conditions select one branch during source function expansion. Function return-match arms are exhaustive, duplicate-free, immutable, and still expand before lowering. Function 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 function is expanded in init, step result values, and send payload values. Recursive function call cycles are rejected.

Statements

source_function_statement =
    source_local_binding

runtime_statement =
    emit_statement
  | process_ref_statement
  | spawn_outcome_statement
  | send_statement
  | send_outcome_statement
  | if_statement
  | for_statement

source_local_binding =
    "let" ident ":" type_ref "=" value_expr ";"

emit_statement =
    "emit" string_literal ";"

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

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

spawn_outcome_statement =
    "let" ident ":" "Result" "<" process_ref_type "," "SpawnError" "<" "Unit" ">" ">"
    "=" "spawn" ident ";"

send_statement =
    "send" ident ("via" ident)? ident payload_arg? ";"

send_outcome_statement =
    "let" ident ":" "Result" "<" "Unit" "," "SendError" "<" type_ref ">" ">"
    "=" "send" ident ("via" ident)? ident payload_arg? ";"

payload_arg =
    "(" value_expr ")"

if_statement =
    "if" "(" value_expr ")" "{" branch_statement* "}"
    ("else" "{" branch_statement* "}")?

branch_statement =
    emit_statement
  | send_statement
  | nested_if_statement
  | for_statement

nested_if_statement =
    "if" "(" value_expr ")" "{" nested_branch_statement* "}"
    ("else" "{" nested_branch_statement* "}")?

nested_branch_statement =
    emit_statement
  | send_statement
  | for_statement

for_statement =
    "for" for_item "in" ident "{" loop_statement* "}"

loop_statement =
    emit_statement
  | send_statement
  | if_statement

for_item =
    ident
  | ident "{" record_pattern_fields "}"

return_statement =
    "return" return_expr ";"

return_if_else =
    "if" "(" value_expr ")" "{" block_body "}"
    "else" "{" block_body "}"

Statement admission is contextual. Pure source function blocks admit only source_function_statement; init and step runtime blocks admit runtime_statement. Runtime branches and loop bodies use the narrower branch_statement, nested_branch_statement, and loop_statement sets above.

The identifier in process_ref_statement 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.

spawn_outcome_statement binds Result<ProcessRef<TargetProcess>,SpawnError<Unit>> as an immutable step-local value. The Ok branch carries the committed process reference; it is authority data and is not valid source state. A top-level outcome binding is visible only to later statements and return values.

The first send identifier is a local process reference or direct ProcessRef<T> payload binding. Optional via PortName must name a declared port matching the target process and message type, with a used local Cap<PortConnect<PortName>> authority. Payload variants require one payload value; unit variants reject payload values.

send_outcome_statement binds a typed local send result. The annotation must be Result<Unit,SendError<TargetMessageType>> so pre-acceptance failure variants can preserve the original message value. Top-level send and spawn outcome bindings must precede ordinary non-prefix effect statements in the same step body. A top-level process-reference spawn can remain in that pre-state prefix so later outcome sends can target the spawned process reference.

The for collection source is an identifier binding with runtime-bound List<T,N> type. The element item is an immutable element binding or record pattern over the element type. Loop bodies support statement-level runtime if, but reject nested loops, return, spawn, branch-local source or process reference bindings, and branch nesting beyond one direct nested layer.

Types

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

type_arg =
    type_ref
  | number

Checking accepts ProcResult<StateType> for step, ProcessRef<ProcessName> for direct process authority surfaces, Cap<Spawn<ProcessName>> and Cap<PortConnect<PortName>> in process authorities, and List<T,N> / Map<K,V,N> over source value types. String, Bytes, Unit, Option<T>, Result<T,E>, SendError<M>, and SpawnError<A> are built-in value shapes for primitive data, explicit domain failure, and typed effect outcomes.

Values

return_expr =
    value_expr
  | match_body

value_expr =
    value_or_expr

value_or_expr =
    value_and_expr
  | value_or_expr "||" value_and_expr

value_and_expr =
    value_equality_expr
  | value_and_expr "&&" value_equality_expr

value_equality_expr =
    value_ordering_expr
  | value_ordering_expr equality_op value_ordering_expr

equality_op =
    "=="
  | "!="

value_ordering_expr =
    value_additive_expr
  | value_additive_expr ordering_op value_additive_expr

ordering_op =
    "<"
  | "<="
  | ">"
  | ">="

value_additive_expr =
    value_multiplicative_expr
  | value_additive_expr additive_op value_multiplicative_expr

additive_op =
    "+"
  | "-"

value_multiplicative_expr =
    value_unary_expr
  | value_multiplicative_expr multiplicative_op value_unary_expr

multiplicative_op =
    "*"
  | "/"
  | "%"

value_unary_expr =
    value_primary_expr
  | "!" value_unary_expr
  | "-" suffixed_integer_literal

value_primary_expr =
    ident
  | string_literal
  | bytes_literal
  | suffixed_integer_literal
  | ident "(" value_expr ")"
  | ident "{" record_value_field ("," record_value_field)* ","? "}"
  | "List" list_type_args? "[" value_expr_list? "]"
  | "Map" map_type_args? "[" map_value_entries? "]"
  | "(" value_expr ")"
  | "if" "(" value_expr ")" "{" value_expr "}" "else" "{" value_expr "}"

record_value_field =
    ident ":" value_expr

value_expr_list =
    value_expr ("," value_expr)* ","?

map_value_entries =
    value_expr "=>" value_expr
    ("," value_expr "=>" value_expr)* ","?

suffixed_integer_literal =
    number scalar_suffix

string_literal = '"' (string_literal_char | string_escape)* '"'
bytes_literal = 'b"' (bytes_literal_char | bytes_escape)* '"'
string_literal_char = printable character except '"' or '\\'
bytes_literal_char = printable ASCII byte except '"' or '\\'
string_escape = '\\"' | '\\\\' | '\\n' | '\\r' | '\\t' | '\\u{' hex{1,6} '}'
bytes_escape = '\\"' | '\\\\' | '\\n' | '\\r' | '\\t' | '\\x' hex hex
hex = ASCII hex digit

scalar_suffix =
    "_u8" | "_u16" | "_u32" | "_u64"
  | "_i8" | "_i16" | "_i32" | "_i64"

Parenthesized value expressions group any value expression without changing its type. ident(value) is a function call when ident names a visible source function and a payload-bearing enum value when it names a constructor of the expected enum type.

List and map constructors are explicit. Optional type and capacity arguments are accepted for readability; the checker still validates each value against the expected bounded source value type.

Typed equality predicates are deliberately narrow. left == right and left != right require operands with the same checked type: Bool, String, Bytes, a scalar integer type, or a payload-free enum. Fully concrete source equality folds during checking. Runtime-bound equality lowers as a typed Mantle value template; operands are not runtime dispatch strings. Structural record/list/map equality, dynamic string predicates, process-reference equality, and payload enum equality remain unsupported.

Scalar literals require explicit suffixes in value positions. Arithmetic uses +, -, *, /, and %; ordering uses <, <=, >, and >=. Scalar operators require matching integer types and perform checked arithmetic. Fully concrete overflow, underflow, division by zero, and modulo by zero fail during checking. Runtime-bound scalar operators lower as typed Mantle value templates and fail closed during runtime evaluation.

Boolean predicate composition is also narrow. !, &&, and || are supported only over Bool values, typed equality or scalar-ordering predicates, or nested composed predicates. ! binds tighter than &&, and && binds tighter than ||; use parentheses for explicit grouping. Fully concrete predicates fold during checking. Runtime-bound predicates lower as typed Mantle value templates over typed Bool-producing operands, not as source strings or function names.

Pure conditionals require core Bool, whose fieldless False and True values are always available and cannot be redeclared. Both branches are value expressions checked against the same expected type. Concrete conditions select one branch before lowering. Runtime-bound expression-form conditionals lower as typed Mantle value templates. Expression branch bodies cannot contain statements or effects.

Final-position return_if_else is runtime control flow in step bodies. The condition must produce core Bool, but it may depend on received payload or current-state payload bindings. Each branch is a block body with its own statements and terminal return. Branch statement prefixes are limited to emit, send, bounded for actions, and one direct statement-level if_statement action. A bounded for prefix keeps the ordinary loop-body surface, including the loop-body branch action. Strata lowers the checked condition, branch action prefixes, and branch next states to Mantle control flow; Mantle executes only the selected branch and traces the branch choice. Deeper direct branch-action nesting remains rejected at source checking, artifact admission, and loaded-runtime admission.

Statement-level if_statement is runtime control flow for effects before the enclosing return. Branches may contain emit, send, and bounded for statements, plus one direct nested statement-level if_statement. The else branch may be omitted, and one branch body may be empty when the sibling branch has at least one effect statement, nested branch action, or bounded-loop action; both branches empty are rejected. An omitted else lowers as an explicit empty branch in the typed Mantle artifact. Branches cannot bind source-local values or process references, return, contain nested loops, or exceed the one direct nested branch-action layer. Inside for, the condition may use the immutable loop element binding or an immutable field projected from a loop-element record pattern; lowering emits typed Mantle templates over the loop element ID, not the source binding name. Loop-body branch bodies follow the same direct nested branch-action bound.

init returns a state value or a pure return match that the checker reduces to one state value before lowering. step returns Continue(value), Stop(value), Panic(value), a final-position runtime if, or a return match that the checker reduces to one of those result forms before lowering while preserving any uniform action prefix as typed transition actions. A final-position runtime if branch may end in one direct nested final-position runtime if; third-level terminal runtime branches remain rejected.

Literals

The literal surface is intentionally narrow:

• decimal numbers are accepted for mailbox bounds;
• suffixed integer literals are accepted for scalar source values;
• string literals are accepted as immutable String values and for emit text, with only \", \\, \n, \r, \t, and valid one-to-six-digit \u{HEX} escapes;
• bytes literals are accepted as immutable Bytes values, with printable ASCII plus \", \\, \n, \r, \t, and \xNN escapes;
• newline and carriage return characters are not allowed raw inside string or bytes literals.

Identifiers

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

_, as, authority, bind, bounded, child, component, composition, else, emit, enum, exports, fn, for, if, import, imports, in, instance, let, local, mailbox, match, module, mut, one_for_one, permanent, port, proc, protocol, record, requires, return, security, send, spawn, supervise, target, temporary, transient, type, var, and via are reserved everywhere identifiers are accepted. The single _ token is reserved for wildcard patterns. Bool, ProcResult, ProcessRef, Cap, Spawn, ProtocolBoundary, PortConnect, ComponentExport, List, Map, Unit, Option, Result, SendError, SpawnError, String, Bytes, U8, U16, U32, U64, I8, I16, I32, and I64 are reserved type names because they name built-in truth, transition, process-reference, capability descriptor, collection, primitive data, effect outcome, and scalar value 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. This example does not import another source unit 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

just run-example hello

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:

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

    authority spawn_worker: Cap<Spawn<Worker>>;

    fn step(state: MainState, Start) -> ProcResult<MainState> ! [spawn, send] ~ [] @det {
        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

just build

just run-example actor_ping

just run-example actor_sequence

just run-example actor_match

just run-example actor_instances

just run-example actor_payloads

just run-example actor_reply

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:

just 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.

Trace Schema

Every event includes Mantle-owned trace schema metadata:

• trace_schema, currently mantle-runtime-observability;
• trace_schema_version, currently 1.

These fields describe the JSONL observability contract only. They do not identify a .mta artifact schema, carry executable bindings, select runtime behavior, or move runtime semantics into Strata.

When mantle run receives an admitted explicit runtime composition binding with --composition-binding, each trace event also carries deployment_id and composition_id, and events associated with a mapped runtime process carry component_instance_id. The current binding schema uses singleton deployment_id=0; it is a stable correlation namespace, not a unique deployment allocator. These fields are observability correlation only. They are emitted from the validated mantle.runtime_composition_binding artifact, not from source names and not from .component-composition.json. Deployment, composition, and component-instance trace fields appear only when that binding is supplied; absent binding input means Mantle fabricates no deployment, composition, or component-instance IDs. Trace validation requires deployment and composition identity to stay stable for the whole bound trace. Once a mapped process emits component_instance_id, later events for the same process_id must keep the same component-instance correlation; adding it after an earlier uncorrelated event for that process or omitting it later fails closed. Binding admission requires every runtime process to map to one checked component instance, so process-scoped events in bound traces carry component_instance_id. Non-process-scoped events carry only the bound deployment_id/composition_id namespace. These fields are observability-only and are never used for dispatch or source-name lookup.

Mantle validates traces with a read-only schema check when repository tests ask for trace evidence. Validation checks event kind support, required fields, string-vs-number field shapes, exact per-event field sets, payload and loop context field grouping, strict unsigned integer syntax, numeric branch-path segments that match Mantle’s emitted branch-path encoding, schema identity, artifact_loaded first/no-repeat ordering, closed runtime enum value domains, u32 artifact typed-ID width, u16 branch-path segment width, branch-path length, artifact process-ID bounds from process_count, Mantle-contiguous spawned PID sequencing, non-entry spawn parent evidence, runtime PID-to-process-ID correlation, optional deployment/composition/component-instance correlation field grouping plus whole-trace identity stability, bound component-instance table bounds, one-to-one process/component-instance correlation, supervisor-child slot causality for child starts and restart decisions, restart-window numeric bounds and decision coupling, and process lifecycle causality boundaries after terminal stop/fail events. It never dispatches from trace data and never turns labels, source names, or debug strings into runtime inputs.

The validator fails closed under explicit byte, event-count, and runtime-process limits. The default validation limits match Mantle’s default 8 MiB trace-byte budget, cap validation at 100,000 events, and cap spawned runtime process correlation at 10,000 process IDs; callers that expose trace validation outside the repository gates can pass caller-specific positive limits. Limits bound validation work only. They do not make trace JSON executable, trusted source semantics, or an artifact boundary.

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;
• outcome_id, the admitted effect-outcome binding ID for a pre-state outcome action;
• 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":"6","source_language":"strata","module":"actor_sequence","entry_process_id":0,"entry_process":"Main","entry_message_id":0,"process_count":2,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

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,"trace_schema":"mantle-runtime-observability","trace_schema_version":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. When present, the spawning PID must still be live; a stopped or failed process cannot create a later runtime process.

Spawn Authority Checked

Example shape:

{"event":"spawn_authority_checked","pid":1,"process_id":0,"process":"Main","target_process_id":1,"spawn_site_id":0,"authority_id":0,"authority_policy_decision_id":0,"spawn_kind":"dynamic_local","authority_result":"accepted","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

spawn_site_id and authority_id are admitted typed table IDs. authority_policy_decision_id is the admitted typed policy row, or null for runs without an authority/effect binding. spawn_kind currently records dynamic_local. authority_result is accepted or denied; a denied spawn outcome returns Err(Denied(Unit)) before the target process is accepted.

Boundary Send Checked

Example shape:

{"event":"boundary_send_checked","pid":1,"process_id":0,"process":"Main","port_id":0,"port":"WorkerPort","protocol_id":0,"protocol":"WorkerProtocol","authority_id":1,"authority_policy_decision_id":1,"target_process_id":1,"target_process":"Worker","message_id":0,"message":"Work","boundary_result":"accepted","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

port_id, protocol_id, authority_id, target_process_id, and message_id are admitted typed IDs. authority_policy_decision_id is the admitted typed policy row, or null for runs without an authority/effect binding. Labels are diagnostics and trace metadata only. A boundary_result of accepted is emitted only for typed-port sends that proceed on the same runtime path as mailbox acceptance; a policy denied result is emitted before mailbox acceptance and before target-side message side effects. A typed send outcome that returns Full, Stopped, Crashed, or MailboxClosed before mailbox acceptance does not emit an accepted boundary event; a denied typed-port send outcome fails closed before any effect_outcome_bound event. Invalid boundary shapes still fail artifact or loaded-program admission before runtime dispatch.

Effect Outcome Bound

Example shapes:

{"event":"effect_outcome_bound","pid":1,"process_id":0,"process":"Main","outcome_id":0,"action":"spawn","target_process_id":1,"spawn_site_id":0,"outcome_result":"backend_unavailable","trace_schema":"mantle-runtime-observability","trace_schema_version":1}
{"event":"effect_outcome_bound","pid":1,"process_id":0,"process":"Main","outcome_id":1,"action":"send","target_process_id":1,"message_id":0,"outcome_result":"mailbox_closed","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

outcome_id, target_process_id, spawn_site_id, message_id, and port_id are admitted typed IDs. action is spawn or send. outcome_result is a closed Mantle result category: ok, denied, exhausted, or backend_unavailable for spawn outcomes, and ok, full, stopped, crashed, or mailbox_closed for send outcomes. Authority-policy denial of a typed-port send outcome is not represented as a send outcome result; it fails closed before source-visible binding. Spawn outcome events require spawn_site_id and do not carry a message or port ID. Send outcome events require message_id and may carry port_id when the outcome action was tied to an admitted typed port.

This event records the Mantle-owned cause of the immutable source-visible Result value. It does not add executable source bindings, does not dispatch from labels, and does not turn trace JSON into a Strata or .mta input.

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,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}
{"event":"message_dequeued","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"First","queue_depth":0,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

message_accepted records mailbox admission. message_dequeued records the message selected for the next transition. When sender_pid is present, it must reference a live runtime process at the admission event; payload process references remain typed evidence and are not executable dispatch handles.

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,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

Runtime dispatch always uses the numeric message_id; labels are trace metadata. For transitions without payload guards, payload values are recorded only as trace data. Payload-sensitive dispatch, when present, uses the admitted payload type ID and exact typed payload value identity, not source strings or debug labels. 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,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

Branch Selected

Example shape:

{"event":"branch_selected","pid":2,"process_id":1,"process":"Worker","message_id":0,"message":"Branch","branch":"then","scope":"action","branch_path":[0],"condition_type_id":0,"condition":"True","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

branch is then or else. scope is action for action-level branch execution, including statement-level branches and branch action prefixes lowered from final-position runtime if, and next_state for branch selection used to resolve the transition result state. branch_path is a stable numeric path assigned from the admitted runtime artifact structure; it is trace identity, not source syntax. Its segments must be values the Mantle runtime encoder can emit: action indexes, selected branch action indexes, selected loop-body action indexes, or selected next-state branch sentinels. condition_type_id is the admitted artifact type ID for the checked Bool condition, and condition is trace metadata for the evaluated value. Runtime branch selection uses the admitted typed condition, not source strings, function names, or debug labels. For composed predicates, this metadata is still only the final evaluated Bool value; the branch path remains the trace identity for the admitted artifact node. Statement-level branches record this event even when the selected branch is an admitted no-op branch with no actions. When a selected statement-level branch contains the single admitted nested runtime branch action, the nested branch records its own branch_selected event with a child branch_path derived from the admitted outer branch path and selected branch action index. When a statement-level branch guards a bounded runtime loop, the outer branch_selected event is recorded before any loop events. If the selected branch is empty, no loop_started, loop_iteration, or loop_completed event is emitted for that branch.

When a branch runs inside a bounded runtime loop body, branch_selected appears after that iteration’s loop_iteration event and before the selected branch effects. The event also includes loop_element_id and loop_index so the selected branch is tied directly to the active immutable loop element binding. The condition may be the evaluated active loop element value.

Runtime Loop Events

Example shape:

{"event":"loop_started","pid":2,"process_id":1,"process":"BatchWorker","message_id":0,"message":"Batch","element_id":0,"collection_type_id":0,"max_items":2,"item_count":2,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}
{"event":"loop_iteration","pid":2,"process_id":1,"process":"BatchWorker","message_id":0,"message":"Batch","element_id":0,"index":0,"element_type_id":1,"element":"True","trace_schema":"mantle-runtime-observability","trace_schema_version":1}
{"event":"loop_completed","pid":2,"process_id":1,"process":"BatchWorker","message_id":0,"message":"Batch","element_id":0,"iteration_count":2,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

element_id, collection_type_id, and element_type_id are admitted artifact IDs. index, item_count, and iteration_count record the bounded runtime execution. element is trace metadata for the evaluated element value. Runtime loop execution uses the admitted typed collection template and loop element ID, not the source binding name.

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","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

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","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

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","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

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","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

The stop reason is normal for source-level Stop(...) termination, supervisor_shutdown when a running supervisor stops its child tree during orderly shutdown, and supervisor_failure when a failed supervisor or failed supervised process forces its child tree to stop.

Process Failed

Example shape:

{"event":"process_failed","pid":2,"process_id":1,"process":"Worker","state_id":1,"state":"Failed","reason":"panic","trace_schema":"mantle-runtime-observability","trace_schema_version":1}

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. Supervisor-scope failures also use process_failed; current supervisor failure reasons are supervisor_restart_intensity_exceeded, supervisor_restart_capacity_exceeded, and supervisor_restart_throttled. These process_failed.reason values are detailed failure-class metadata. For supervisor restart causality, every process_failed terminal event has the supervisor exit class panic.

Supervisor Lifecycle Events

Example shapes:

{"event":"supervisor_child_started","supervisor_pid":1,"supervisor_process_id":0,"supervisor_process":"Main","supervisor_id":0,"child_id":0,"child":"worker","child_pid":2,"child_process_id":1,"child_process":"Worker","spawn_site_id":0,"spawn_kind":"lexical_supervisor_child","trace_schema":"mantle-runtime-observability","trace_schema_version":1}
{"event":"supervisor_restart_decision","supervisor_pid":1,"supervisor_process_id":0,"supervisor_process":"Main","supervisor_id":0,"child_id":0,"child":"worker","child_pid":2,"child_process_id":1,"child_process":"Worker","reason":"panic","decision":"restarted","restart_time_ms":0,"restart_window_count":1,"restart_window_limit":3,"restart_window_ms":1000,"new_child_pid":3,"trace_schema":"mantle-runtime-observability","trace_schema_version":1}

supervisor_id, child_id, and spawn_site_id are admitted typed IDs. spawn_kind records the lexical supervisor-child classification. child, supervisor_process, and child_process are trace labels only. restart_time_ms is the sampled monotonic runtime time for restart-window decisions. restarted and denied decisions carry numeric restart time; not_restarted records null because no restart-window sample is needed. The restart window fields record the observed count and configured limit/window after stale entries are pruned. The configured limit and window duration must be greater than zero, and the observed count must not exceed the configured limit. restarted records a nonzero observed count; not_restarted records zero because no restart was attempted. Only a restarted decision carries a numeric new_child_pid; not_restarted and denied decisions set new_child_pid to null. Supervisor lifecycle events must be caused by a live supervisor PID. Child-start events require a live child PID that was spawned by the supervisor. Restart decisions require prior supervisor_child_started evidence for the same typed supervisor/child slot, require child_pid to be that slot’s current child, require a prior process_stopped/process_failed event whose terminal exit class matches the restart decision reason (process_stopped normal matches normal; any process_failed matches panic), and for restarted decisions require a distinct live new_child_pid spawned by the supervisor. A denied restart fails the supervisor scope when intensity, capacity, or the default same-monotonic-tick throttle prevents a restart. Runtime supervision uses admitted supervisor tables and typed child IDs, not labels.

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 validated execution failures.

Reading A Diagnostic

Run:

just 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 Artifact And Runtime Errors

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:

just strata-check path/to/program.str
just strata-build path/to/program.str

Then run Mantle:

just 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. init_return_match.str for pure init return-match expressions.
7. function_match.str for module functions, process-local functions, and pattern matching outside actor dispatch.
8. function_payload_match.str for payload-bearing enum construction and matching in normal source functions.
9. function_if_else.str for pure value-level conditionals selected before lowering. See also function_local_bindings.str for sequential immutable source-local computation in normal source functions.
10. function_collection_match.str for immutable list/map source values and collection patterns in normal source functions.
11. function_return_match.str for function return-match expressions.
12. process_return_match.str for process step return-match expressions with uniform effect prefixes.
13. process_return_match_arm_prefix.str for selected step return-match arm action prefixes.
14. process_return_match_arm_runtime_if_prefix.str for selected step return-match arm-local runtime branch prefixes.
15. process_return_match_arm_for_prefix.str for selected step return-match arm-local bounded runtime loop prefixes.
16. process_return_match_arm_for_if_prefix.str for selected step return-match arm-local bounded runtime loop prefixes with loop-body runtime branch actions.
17. process_return_match_arm_if_for_prefix.str for selected step return-match arm-local runtime branch prefixes with bounded runtime loop branch actions.
18. process_return_match_arm_action_block.str for selected step return-match arms using ordinary action-block sequencing with multiple runtime branches and bounded loops.
19. function_record_pattern.str for source function record destructuring patterns.
20. function_record_return_match.str for function return-match record destructuring.
21. function_record_body_match.str for whole-body function match record destructuring.
22. state_payload_enum.str for payload-bearing process state enum transitions.
23. collection_state.str for immutable collection state and payload-dependent collection next-state templates.
24. state_payload_match.str for matching immutable current process state payloads.
25. actor_instances.str for multiple runtime instances of one process definition.
26. actor_payloads.str for typed message payloads and immutable payload bindings in actor step parameter patterns.
27. runtime_if_else.str for Mantle-backed runtime branching over a message payload.
28. runtime_scalar_priority.str for typed scalar payload computation, runtime-bound value conditionals, and Mantle-backed scalar branch selection.
29. source_contract_data_primitives.str for immutable String and Bytes data in records, messages, functions, collections, exact equality, and Mantle typed primitive runtime values.
30. runtime_payload_projection_if.str for Mantle-backed runtime branching over a projected field from an immutable received record payload.
31. runtime_payload_projection_next_state.str for Mantle-backed runtime next-state branching over a projected field from an immutable received record payload.
32. runtime_state_payload_projection_if.str for Mantle-backed runtime branching over a projected field from an immutable current-state record payload.
33. runtime_state_payload_projection_next_state.str for Mantle-backed runtime next-state branching over a projected field from an immutable current-state record payload.
34. runtime_nested_if_actions.str for one bounded layer of nested statement-level runtime branch actions.
35. runtime_final_if_guarded_loop.str for bounded loop action prefixes inside final-position runtime branches.
36. runtime_final_if_nested_if_actions.str for one direct nested statement-level runtime branch action inside final-position runtime branches.
37. runtime_final_if_nested_terminal_if.str for one direct nested terminal final-position runtime branch inside final-position runtime branches.
38. runtime_guard_noop.str for omitted else and explicit no-op runtime branch behavior.
39. runtime_for_each.str for Mantle-backed bounded runtime iteration over a typed list payload.
40. runtime_for_each_empty.str for the zero-iteration runtime collection case.
41. runtime_for_each_if.str for Mantle-backed runtime branch selection inside bounded loop bodies.
42. runtime_for_each_nested_if_actions.str for one bounded nested runtime branch inside a bounded loop-body branch.
43. runtime_guarded_for_each.str for guarding a whole bounded runtime loop.
44. runtime_guarded_ref_loop.str for routing a guarded bounded loop through a received direct process reference.
45. runtime_guarded_ref_loop_jobs.str for routing ordinary immutable Job values through a guarded loop and received direct process reference.
46. runtime_loop_element_projection.str for projecting immutable record fields from guarded runtime loop elements.
47. actor_payload_match.str for the same payload binding through a whole-body match msg.
48. actor_payload_split_match.str for payload-sensitive same-message splitting inside a whole-body match msg.
49. actor_payload_split_signature.str for payload-sensitive same-message splitting across step parameter patterns.
50. actor_payload_split_signature_wildcard.str for payload-sensitive step-signature wildcard fallback over discovered concrete payload cases.
51. actor_payload_state_match_split.str for payload-sensitive same-message splitting across state-match step clauses.
52. actor_payload_state_match_wildcard.str for payload-sensitive state-match wildcard fallback over discovered concrete payload cases.
53. nested_patterns.str for nested immutable constructor, record, list, and map payload destructuring.
54. actor_reply.str for transporting typed process references through message payloads.
55. process_ref_stale_lifecycle.str for a transported old runtime PID returning Err(Stopped(message)) without retargeting to a newer worker.
56. actor_emit_spawn_send.str for one transition with declared emit, spawn, and send authority.
57. imports_main.str, with imports_types.str and imports_worker.str, for source-unit imports checked and lowered from one root source path.
58. boundary_contracts_main.str, with boundary_contracts_worker.str, for typed protocol, port, and component boundary contracts.
59. component_composition_main.str, with component_composition_worker.str, for checked local component-instance and port-binding composition admission.
60. effect_outcomes.str for immutable typed local send/spawn outcomes, commit-or-return state evidence, and the typed send-error contract shape.
61. effect_outcome_mailbox_full.str for a source-visible Full send outcome.
62. effect_outcome_stopped_target.str for a source-visible Stopped send outcome after a normally terminated target.
63. effect_outcome_crashed_target.str for the fail-closed boundary where a source-created Panic(...) prevents a later observer from recovering the crash as a source-visible send outcome.
64. effect_outcome_spawn_denied.str for source-visible local spawn authority denial before process acceptance.
65. effect_outcome_spawn_exhausted.str for source-visible local spawn capacity exhaustion before process acceptance under --max-runtime-processes 1.
66. effect_outcome_spawn_backend_unavailable.str for source-visible local spawn backend unavailability before process acceptance under --disable-local-spawn-backend.
67. actor_panic_no_replay.str for fail-closed actor failure and no replay after message dequeue.
68. local_supervision_restart.str, local_supervision_permanent_stop.str, local_supervision_temporary.str, local_supervision_transient_restart.str, local_supervision_transient.str, and local_supervision_inactive_send_outcome.str for local one_for_one supervision, lexical child sends, restart modes, stopped-child send outcomes, and restart observability.
69. local_supervision_inactive_crashed_send_outcome.str for source-visible Err(Crashed(message)) when an inactive temporary supervised child failed before the send was accepted.

Detailed notes are grouped by topic:

• Basic examples
• Function and return-match examples
• Runtime and actor examples
• Import, boundary, and failure examples

Basic Examples

These examples cover the first source-to-runtime programs and initial process dispatch forms.

Hello

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

just build
just run-example hello

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.

just run-example actor_ping

Key source ideas:

• Main declares authority spawn_worker: Cap<Spawn<Worker>>;, then 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(...).

just run-example actor_sequence

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.

just run-example actor_match

Key source ideas:

• fn step(state: WorkerState, msg: WorkerMsg) declares a typed message parameter.
• match msg must be the whole function body.
• 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.

just run-example init_match

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.

Init Return Match

examples/init_return_match.str exercises a pure return match expression in init. The checker resolves the fieldless enum scrutinee, proves the arms are exhaustive, selects one whole initial state value, and lowers that state through the existing typed artifact state table.

just run-example init_return_match

Key source ideas:

• return match Warm { ... }; is accepted only because Warm is a fieldless enum constructor.
• Each arm is statement-free and returns one immutable whole MainState value.
• Mantle receives the selected typed initial state ID; it does not dispatch on the source match arm names.

Function And Return-Match Examples

These examples cover pure source functions, immutable source-local computation, source patterns, and checked return-match forms.

Function Match

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

just run-example function_match

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 functions for state construction.
• send worker Assign(ready_job(Ready)) proves function calls are expanded for message payload discovery and lowering.
• Mantle sees typed state IDs, message IDs, and payload templates, not source function dispatch names.

Function Payload Match

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

just run-example function_payload_match

Key source ideas:

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

Function If Else

examples/function_if_else.str uses pure source-time conditionals in normal source functions. The checker resolves the core Bool condition and selects one immutable branch before lowering. The example includes both expression-form return if (...) { value } else { value }; and braced pure return branches.

just run-example function_if_else

Key source ideas:

• Bool, False, and True are core built-ins for conditionals and cannot be redeclared.
• if (flag) { WarmReady } else { ColdReady } is a pure value expression, not a statement block.
• if (flag) { return WarmReady; } else { return ColdReady; } is an equivalent pure source-function return branch shape, not a runtime branch.
• Both branches are checked against the same expected type.
• Mantle receives selected typed state values, not a conditional branch key or source function dispatch name.

Function Local Bindings

examples/function_local_bindings.str uses sequential immutable bindings in normal source functions and process-local pure functions. The checker resolves each typed source-local value before lowering.

just run-example function_local_bindings

Key source ideas:

• let current_local: Phase = status(work); binds an immutable source value, not a runtime action.
• Later source-local bindings can use earlier bindings in source function calls, pure conditionals, scalar arithmetic and ordering, record/list/map constructors, and equality predicates.
• Braced pure return-if branches can introduce branch-local immutable values before their terminal return.
• Function return-match arms can use source-local bindings before their terminal pure return.
• Process-local pure functions use the same source-local binding rules.
• Runtime-bound pure value if expressions over Bool lower as typed Mantle value templates, not source strings or source function dispatch names.
• Message enums that carry direct ProcessRef<T> payloads remain authority surfaces and are rejected as source-local binding types.
• Mantle receives typed values and templates, not source-local binding names or source function dispatch names.

Function Collection Match

examples/function_collection_match.str uses immutable List<T,N> and Map<K,V,N> source values in normal source functions.

just run-example function_collection_match

Key source ideas:

• List<Phase,2>[Ready, Done] and Map<Phase,Phase,2>[Ready => Done, Unknown => Unknown] are typed, bounded immutable collection values.
• fn first(List<Phase,2>[phase, _]) dispatches on exact list length and binds one immutable element.
• Function body and return matches can use exact list patterns, list rest patterns such as List[_, ..tail], exact map patterns, and subset map patterns such as Map[Ready => selected, ..rest] with _ fallback arms.
• Function expansion leaves Mantle with a resolved MainState value, not source function dispatch names.

Function Return Match

examples/function_return_match.str uses a function return match expression to select an immutable result from an in-scope source value binding.

just run-example function_return_match

Key source ideas:

• return match work { ... }; is checked as a pure function return expression.
• The selected arm binds enum payloads immutably before function expansion.
• Mantle receives the resolved MainState{status:Active(Job{phase:Ready})} state value, not source function dispatch.

Process Return Match

examples/process_return_match.str uses a process step return match over a concrete enum payload binding after a uniform emit prefix.

just run-example process_return_match

Key source ideas:

• Envelope(Assign(phase: Phase)) binds an immutable enum payload whose concrete value is already proven by payload-sensitive dispatch.
• emit "process return match uniform prefix"; lowers as the same typed action prefix on every selected transition.
• return match phase { ... }; is checked and reduced to a typed Continue(...) or Stop(...) transition before lowering.
• Mantle executes the emitted typed transition IDs and payload guards; it does not dispatch on source strings or function names.

Process Return Match Arm Prefix

examples/process_return_match_arm_prefix.str extends step return match with selected arm-local emit and typed send prefixes before the terminal result.

just run-example process_return_match_arm_prefix

Key source ideas:

• The checker still selects one concrete return-match arm before lowering.
• The uniform prefix lowers onto every selected transition before the arm-local prefix.
• Only the selected arm’s typed actions lower onto that transition; the arm-local send prefixes also seed the receiver’s payload-sensitive transitions before lowering.
• Arm labels and source binding names are not executable runtime dispatch keys.
• Arm-local spawn, process-reference binding, final-position runtime if, nested return matches, and mutable source state changes remain rejected.

Process Return Match Arm Runtime If Prefix

examples/process_return_match_arm_runtime_if_prefix.str extends selected step return match arm prefixes with statement-level runtime if actions.

just run-example process_return_match_arm_runtime_if_prefix

Key source ideas:

• The checker still source-selects one concrete return-match arm before lowering.
• The checked arm-local runtime branch lowers as a typed Mantle action inside that selected arm prefix, after any uniform prefix actions and before the terminal Continue(...) or Stop(...).
• This example keeps branch bodies action-only with local emit and in-scope direct send; process_return_match_arm_if_for_prefix.str also covers bounded runtime for actions inside selected runtime branches.
• Branch-local spawn, process-reference binding, branch returns, final-position runtime if, and runtime branch nesting beyond the artifact bound remain rejected.
• Mantle selects the runtime branch from typed artifact templates; source arm labels and source binding names are not executable dispatch keys.

Process Return Match Arm For Prefix

examples/process_return_match_arm_for_prefix.str extends selected step return match arm prefixes with bounded runtime for over a checked runtime List<T,N> binding.

just run-example process_return_match_arm_for_prefix

Key source ideas:

• The checker still source-selects one concrete return-match arm before lowering.
• The selected arm loop lowers as a typed Mantle for_each action after any uniform and arm-local checked action prefixes, before the terminal Continue(...) or Stop(...).
• Loop collections must be checked runtime List<T,N> bindings. Loop element projections lower as typed templates, not source-name dispatch.
• Loop bodies remain action-only: local emit and in-scope direct send actions are supported, while spawn, process-reference binding, nested loops, and branch-local process-reference binding remain rejected.

Process Return Match Arm For-If Prefix

examples/process_return_match_arm_for_if_prefix.str extends selected step return match arm-local bounded loops with loop-body runtime if actions.

just run-example process_return_match_arm_for_if_prefix

Key source ideas:

• The checker still source-selects one concrete return-match arm before lowering.
• The selected arm loop lowers as a typed Mantle for_each action, and the direct loop-body runtime branch lowers as a typed Mantle branch action inside that loop body.
• The branch condition and branch sends project from typed immutable loop element bindings, not source aliases or debug strings.
• Loop-body branches remain action-only: local emit and in-scope direct send actions are supported, while branch returns, branch-local spawn, process-reference binding, nested runtime for, and runtime branch nesting beyond the artifact bound remain rejected.

Process Return Match Arm If-For Prefix

examples/process_return_match_arm_if_for_prefix.str extends selected step return match arm-local runtime branches with bounded runtime for actions inside branches.

just run-example process_return_match_arm_if_for_prefix

Key source ideas:

• The checker still source-selects one concrete return-match arm before lowering.
• The selected arm runtime branch lowers as a typed Mantle branch action, and a selected branch may contain bounded typed for_each actions.
• Loop collections remain checked runtime List<T,N> bindings, and loop element projections lower through typed templates rather than source aliases.
• Branch-local loops remain action-only and bounded: local emit, in-scope direct send, and loop-body runtime branch actions are accepted; branch returns, branch-local spawn, process-reference binding, nested runtime for, and runtime branch nesting beyond the artifact bound remain rejected.

Process Return Match Arm Action Block

examples/process_return_match_arm_action_block.str exercises selected step return match arms as ordinary typed step action blocks before their terminal result.

just run-example process_return_match_arm_action_block

Key source ideas:

• Each selected arm contains multiple statement-level runtime if actions and multiple sibling bounded runtime for actions in source order.
• Nested statement-level runtime branches are supported only up to the shared artifact/runtime branch-action bound.
• Runtime loops remain bounded over checked List<T,N> bindings, and nested runtime loops remain rejected.
• Arm-local spawn, branch-local process-reference binding, final-position runtime if, nested return matches, mutation, and source-string dispatch remain rejected.

Function Record Pattern

examples/function_record_pattern.str destructures an immutable record value in a normal source function signature.

just run-example function_record_pattern

Key source ideas:

• fn phase_of(Job { phase }) binds the phase field as an immutable source value.
• field: binding may rename a record field binding in the function signature.
• The function expands before lowering; Mantle receives the resolved MainState{phase:Ready} state value.

Function Record Return Match

examples/function_record_return_match.str destructures an immutable record value inside a function return match expression.

just run-example function_record_return_match

Key source ideas:

• return match job { Job { phase } => { return phase; } }; binds the phase field as an immutable source value inside the selected arm.
• Record return-match destructuring requires the scrutinee to be an in-scope source binding with a concrete record value.
• The function expands before lowering; Mantle receives the resolved MainState{phase:Ready} state value.

Function Record Body Match

examples/function_record_body_match.str destructures an immutable record value inside a whole-body source function match.

just run-example function_record_body_match

Key source ideas:

• match job { Job { phase } => { return phase; } } binds the phase field as an immutable source value inside the selected arm.
• Record body-match destructuring requires one record pattern arm over the function parameter’s concrete record value.
• The function expands before lowering; Mantle receives the resolved MainState{phase:Ready} state value.

Runtime And Actor Examples

These examples cover runtime state transitions, branching, loops, payload dispatch, process references, and failure behavior.

Runtime Scalar Priority

examples/runtime_scalar_priority.str sends a typed U32 payload to a worker, computes an immutable scalar priority in process-local pure functions, and lets Mantle select the runtime branch and the runtime-bound priority value from typed scalar templates.

just run-example runtime_scalar_priority

Key source ideas:

• Assign(U32) is a typed scalar message payload, not a string payload.
• compute_level uses immutable U32 source-local bindings and checked scalar arithmetic.
• compute_level(weight) >= 10_u32 lowers into typed Mantle scalar templates; high_priority(weight) is the pure Bool function used by the runtime branch.
• classify(weight) returns if (urgent) { High } else { Normal }; when urgent depends on the message payload, lowering emits a typed Mantle value-if template for the selected state field.
• The selected branch emits scalar priority high, proving Mantle executed the scalar branch path.

State Payload Enum

examples/state_payload_enum.str shows 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 }).

just run-example state_payload_enum

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 resolves the resulting Working(Job{phase:Ready}) only because it is present in the typed state table.

Collection State

examples/collection_state.str shows immutable List<Phase,1> and Map<Phase,Phase,2> process states and lowers received payloads, including list rest and subset map payload projections, into collection next-state templates.

just run-example collection_state

Key source ideas:

• type State = List<Phase,1>; and type State = Map<Phase,Phase,2>; make worker states collection values rather than records or enums.
• return Stop(tail); and return Stop(Map<Phase,Phase,2>[Ready => next, Done => Ready]); create new immutable whole collection states from received payload bindings.
• Mantle receives typed list-rest and map value templates and evaluates them during runtime execution.

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.

just run-example state_payload_match

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 typed message ID plus checked 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.

just run-example actor_instances

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.

just run-example actor_payloads

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.

Component Composition

examples/component_composition_main.str imports examples/component_composition_worker.str, declares a MainComponent that imports WorkerPort, and admits a local AppComposition binding the import to the worker component export. The binding is checked as a typed graph edge before lowering; Mantle admits typed component-instance and port IDs as metadata/admission data, while runtime send dispatch still uses loaded typed process, message, and port IDs.

strata check examples/component_composition_main.str
strata build examples/component_composition_main.str
strata composition build examples/component_composition_main.str
strata composition admit target/strata/component_composition_main.component-composition.json --format json
strata composition bind-runtime target/strata/component_composition_main.component-composition.json target/strata/component_composition_main.mta --output target/strata/component_composition_main.deployment-composition.json
mantle run target/strata/component_composition_main.mta --composition-binding target/strata/component_composition_main.deployment-composition.json

The component-composition.json output is Strata-owned checked-subset evidence (strata.checked_component_composition), not .mta or Mantle runtime input. strata composition bind-runtime emits the separate deployment-composition.json binding (mantle.runtime_composition_binding), which Mantle admits only with --composition-binding and a matching .mta. Source names remain metadata; typed IDs carry binding, authority-flow, and trace correlation. Unsupported binding classes stay empty fail-closed arrays.

Typed Effect Outcomes

examples/effect_outcomes.str binds local spawn and send results as immutable Result values, branches on typed outcome variant patterns, and stores the finite send result in the next state as whole-value data.

just run-example effect_outcomes

Key source ideas:

• let spawn_result: Result<ProcessRef<Worker>,SpawnError<Unit>> = spawn Worker; returns the committed process reference on accepted local spawn.
• let send_result: Result<Unit,SendError<WorkerMsg>> = send worker Work; returns Ok(Unit) after Mantle accepts the message, or typed SendError<WorkerMsg> before acceptance.
• Outcome branches such as spawn_result != Err(Exhausted(Unit)) and send_result == Ok(Unit) use immutable typed variants, not process-reference identity comparisons.
• The next state stores send_result; spawn_result stays step-local because success carries process-reference authority rather than ordinary source state.
• The artifact uses typed outcome IDs and value templates, not source binding names, for runtime meaning.
• effect_outcome_mailbox_full, effect_outcome_stopped_target, and effect_outcome_crashed_target cover pre-acceptance capacity failure, normally stopped targets, and source-created panic fail-closed behavior.
• process_ref_stale_lifecycle proves a transported old runtime PID returns Err(Stopped(message)) without retargeting to a newer same-definition worker.
• effect_outcome_spawn_denied covers denied admitted spawn authority before a Worker instance is accepted.
• effect_outcome_spawn_exhausted covers process-capacity exhaustion before a Worker is accepted under --max-runtime-processes 1; the exhausted branch emits without admitting or executing the child. The runtime trace records effect_outcome_bound with outcome_result:"exhausted".
• effect_outcome_spawn_backend_unavailable covers a disabled local spawn backend under --disable-local-spawn-backend; the backend-unavailable branch emits without binding a process reference, admitting a child, or dispatching from source names.
• The local supervision examples cover lexical child sends, explicit restart intensity, child modes, stopped- and crashed-child send outcomes, and restart traces without replaying consumed messages; crashed-child send outcomes record effect_outcome_bound with outcome_result:"crashed".

Runtime If Else

examples/runtime_if_else.str branches inside Worker.step over a received Bool payload. The branch is not selected by Strata during checking; it lowers as typed Mantle control flow and executes when each worker handles its message.

just run-example runtime_if_else

Key source ideas:

• Branch(True) and Branch(False) send two different runtime payloads.
• if (flag == True) { ... } else { ... } lowers to Mantle branch control flow through a typed equality template.
• Each branch emits its own declared output and returns a whole immutable state.
• The runtime trace records branch_selected for both then and else paths.

Runtime Payload Projection If

examples/runtime_payload_projection_if.str branches inside Worker.step over a field destructured from a received Job record payload. The source binding is immutable step-local syntax; the runtime branch lowers through a typed Mantle record-field projection over the received payload.

just run-example runtime_payload_projection_if

Key source ideas:

• Assign(Job { phase: assigned_phase }) destructures the received record payload without introducing mutation.
• if (assigned_phase == Ready) { ... } else { ... } lowers as typed Mantle branch control through ReceivedPayload<Job>, RecordField("phase"), and a Phase equality predicate.
• Only the ready payload emits output; the done payload takes the empty branch.

Runtime Payload Projection Next State

examples/runtime_payload_projection_next_state.str branches inside Worker.step over a field destructured from a received Job record payload. The branch controls the final next-state result, and the state change remains a whole immutable value returned through Continue.

just run-example runtime_payload_projection_next_state

Key source ideas:

• Assign(Job { phase: assigned_phase }) is source syntax for an immutable payload destructuring binding.
• The final-position if (assigned_phase == Ready) { ... } else { ... } lowers to Mantle NextState::IfElse through ReceivedPayload<Job>, RecordField("phase"), and a Phase equality predicate.
• Both branches return whole WorkerState enum values; the artifact does not use the source alias as an executable runtime path.

Runtime State Payload Projection If

examples/runtime_state_payload_projection_if.str stores immutable Job records in process state, later destructures the current state payload, and uses the projected field to select a statement-level runtime branch action inside Mantle.

just run-example runtime_state_payload_projection_if

Key source ideas:

• Assign(job: Job) stores the whole received job as Holding(job).
• Holding(Job { phase: held_phase }) destructures the immutable current-state payload for the selected Decide transition arm.
• The statement-level if (held_phase == Ready) { ... } else { ... } lowers to Mantle ArtifactAction::IfElse through CurrentStatePayload<Job>, RecordField("phase"), and a Phase equality predicate.
• Both branches emit from typed runtime action selection, then return Continue(state) as a whole-value continuation; the artifact does not use the source alias as an executable runtime path.

Runtime State Payload Projection Next State

examples/runtime_state_payload_projection_next_state.str stores immutable Job records in process state, later destructures the current state payload, and uses the projected field to choose a final next state inside Mantle.

just run-example runtime_state_payload_projection_next_state

Key source ideas:

• Assign(job: Job) stores the whole received job as Holding(job).
• Holding(Job { phase: held_phase }) destructures the immutable current-state payload for the selected Decide transition arm.
• The final-position if (held_phase == Ready) { ... } else { ... } lowers to Mantle NextState::IfElse through CurrentStatePayload<Job>, RecordField("phase"), and a Phase equality predicate.
• Both branches return whole WorkerState enum values; the artifact does not use the source alias as an executable runtime path.

Runtime Nested If Actions

examples/runtime_nested_if_actions.str sends immutable CheckFlags record payloads to three workers and uses one nested statement-level runtime branch to choose effect-only action output inside Mantle.

just run-example runtime_nested_if_actions

Key source ideas:

• Check(CheckFlags { outer_flag: primary, inner_flag: secondary }) destructures the received record payload into immutable source bindings.
• The outer and inner if conditions lower through typed RecordField(ReceivedPayload<CheckFlags>, ...) Bool equality templates.
• The nested branch is an typed Mantle action with a stable nested branch_path; source aliases such as primary and secondary are not executable dispatch paths.
• State remains a whole-value Continue(state) after the effect-only nested branch action; branch-local spawn, process-reference binding, return, nested loops, and deeper direct branch nesting remain rejected.

Runtime Final If Guarded Loop

examples/runtime_final_if_guarded_loop.str sends immutable CheckFlags record payloads to three workers and uses a bounded loop action prefix inside a final-position runtime branch before returning the whole-value step result.

just run-example runtime_final_if_guarded_loop

Key source ideas:

• The final-position if (enabled == True) { ... } else { ... } lowers both branch action prefixes and branch next states through typed Mantle control flow.
• The selected enabled branch records branch_selected, runs the bounded loop, and then returns Continue(state).
• The selected disabled branch emits worker disabled, returns the same whole-value step result shape, and does not execute loop actions.
• Loop element access lowers through the typed loop element ID; source aliases such as item are not executable runtime dispatch paths.
• Branch-local spawn, branch-local process-reference binding, nested loops, deeper direct branch-action nesting, and mutable state updates remain rejected.

Runtime Final If Nested If Actions

examples/runtime_final_if_nested_if_actions.str sends immutable CheckFlags record payloads to four workers and uses one direct nested statement-level runtime branch action as an action prefix inside each selected final-position runtime branch. Each outer final-position branch still ends in the same whole-value Continue(state) result.

just run-example runtime_final_if_nested_if_actions

Key source ideas:

• The final-position if (outer == True) { ... } else { ... } lowers both branch action prefixes and branch next states through typed Mantle control flow.
• The direct nested if (inner == True) { ... } else { ... } in each selected final-position branch lowers as a typed Mantle ArtifactAction::IfElse.
• Nested branch sends use the declared reporter: ProcessRef<Reporter> binding created before the final-position branch and typed ReceivedPayload record field templates for the immutable inner_flag value.
• Runtime execution records the final-position branch selection, nested branch selection, selected emit/send effects, and final whole-value result behavior in order.
• Third-level runtime branch actions, nested loops, branch-local spawn, branch-local process-reference binding, statement-branch return, and mutable state updates remain rejected.

Runtime Final If Nested Terminal If

examples/runtime_final_if_nested_terminal_if.str sends immutable CheckFlags record payloads to four workers and uses one direct nested final-position runtime branch as the terminal return inside each selected final-position runtime branch. Each nested leaf returns a whole-value Continue(...) state.

just run-example runtime_final_if_nested_terminal_if

Key source ideas:

• The outer if (outer == True) { ... } else { ... } lowers to a typed Mantle NextState::IfElse.
• The terminal nested if (inner == True) { ... } else { ... } in each selected branch lowers to a direct nested typed Mantle NextState::IfElse.
• Branch conditions lower through typed ReceivedPayload record-field templates for immutable outer_flag and inner_flag, not source aliases.
• Runtime execution records outer and nested next_state branch selections, selected output effects, and the final whole-value state transition in order.
• Third-level terminal runtime branches, deeper branch actions, nested loops, branch-local spawn, branch-local process-reference binding, statement-branch return, and mutable state updates remain rejected.

Runtime Guard Noop

examples/runtime_guard_noop.str shows statement-level runtime branches where one selected branch intentionally performs no effects. The conditions are still checked Bool predicates and lower into typed Mantle branch actions.

just run-example runtime_guard_noop

Key source ideas:

• if (flag == True) { ... } lowers an omitted else as an explicit empty Mantle branch.
• else {} is an explicit no-op branch; {} on one side is allowed when the sibling branch has an declared effect.
• Empty selected branches do not emit, send, acquire authority, or change state, but they still record branch_selected.
• Both branches empty are rejected before runtime execution.

Runtime For Each

examples/runtime_for_each.str iterates inside BatchWorker.step over a received List<Bool,2> payload. The loop is not unrolled or selected by Strata during checking; it lowers as typed Mantle loop control flow and executes once per runtime element.

just run-example runtime_for_each

examples/runtime_for_each_empty.str uses the same shape with List<Bool,0>[] and proves that Mantle records loop start/completion without executing the body.

just run-example runtime_for_each_empty

Key source ideas:

• for item in items { ... } requires items to be a typed runtime list binding.
• item is an immutable per-iteration value binding lowered to a typed loop element ID.
• The loop body sends Branch(item) in collection order.
• The runtime trace records loop_started, one loop_iteration per item, and loop_completed.

examples/runtime_for_each_if.str extends the same runtime loop with statement-level branch control inside the loop body.

just run-example runtime_for_each_if

Key source ideas:

• if ((item != False) && !(item == False)) { ... } else { ... } runs in Mantle for each loop iteration through typed Boolean predicate templates.
• The branch condition uses the typed loop element ID; branch payloads remain typed loop element values.
• One branch may be empty when the sibling branch has declared effects. Branches can emit and send, and may contain one direct nested statement-level branch. They cannot return, spawn, loop, or nest more deeply.
• The runtime trace records loop_iteration, branch_selected, branch effects, and loop_completed in deterministic collection order.

examples/runtime_for_each_nested_if_actions.str projects immutable fields from each CheckFlags loop element and selects one direct nested statement-level runtime branch inside the selected outer loop-body branch.

just run-example runtime_for_each_nested_if_actions

Key source ideas:

• The loop item record pattern binds immutable outer and inner field values.
• Lowering emits typed RecordField(LoopElement(...), "...") templates for the outer condition, nested condition, and send payload.
• Runtime execution records the loop iteration, outer branch selection, nested branch selection, and selected branch effects in order.
• Third-level runtime branch actions, nested loops, branch-local spawn, and branch-local process-reference binding remain rejected.

examples/runtime_guarded_for_each.str guards a whole bounded runtime loop with a statement-level branch.

just run-example runtime_guarded_for_each

Key source ideas:

• if (enabled == True) { for item in items { ... } } else {} lowers as a typed Mantle branch whose selected then branch contains a bounded loop.
• The disabled selected branch records branch_selected but emits no loop events and performs no branch-local work.
• The enabled selected branch records branch_selected, then loop_started, ordered loop_iteration body effects, and loop_completed.
• The guarded branch and loop body keep the same restrictions: no nested loops, no spawn, no return, no assignment, and no process-reference loop element type. Statement-level branch nesting still cannot exceed the single nested layer.

examples/runtime_guarded_ref_loop.str routes that guarded-loop send through a direct ProcessRef<Worker> received as the current message payload.

just run-example runtime_guarded_ref_loop

Key source ideas:

• BatchWorker stores only value data in state. The worker reference remains a direct message payload on Route(ProcessRef<Worker>).
• The selected enabled branch sends Branch(item) through the received reference from inside the guarded loop body.
• The disabled branch records only branch_selected; it emits no loop events and performs no branch-local or loop-local authority acquisition.
• Lowering emits a typed received-payload send target. Runtime dispatch uses the transported runtime process ID plus checked target process ID, not the source payload binding name.

Runtime Guarded Ref Loop Jobs

examples/runtime_guarded_ref_loop_jobs.str keeps the same received direct ProcessRef<Worker> routing shape, but the guarded loop iterates over ordinary immutable Job record values.

just run-example runtime_guarded_ref_loop_jobs

Key source ideas:

• The guard remains a Bool predicate over current BatchRequest state.
• The loop collection is List<Job,2>, and Job is plain value data.
• The worker reference remains direct message authority on Route(ProcessRef<Worker>); it is not stored in state or nested inside the job list.
• Lowering emits the jobs projection as a current-state value template, the loop element as Job, and the send target as a typed received-payload process reference.

Runtime Loop Element Projection

examples/runtime_loop_element_projection.str projects immutable Job.phase data from each loop element, branches on the typed Phase, and sends only the Ready phase through the received direct ProcessRef<Worker>.

just run-example runtime_loop_element_projection

Key source ideas:

• The loop item uses a record pattern, Job { phase: routed_phase }, to bind an immutable field value inside the loop body.
• Lowering emits RecordField(LoopElement(...), "phase") typed templates for the inner branch condition and send payload.
• Runtime execution uses typed loop element IDs, type IDs, and received process-ref payload targets. The source binding alias is not executable dispatch metadata.

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.

just run-example actor_payload_match

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 typed message IDs and payload type IDs.

Actor Payload Split Match

examples/actor_payload_split_match.str proves that one top-level message variant can be split inside a whole-body match msg by disjoint nested typed payload predicates.

just run-example actor_payload_split_match

Key source ideas:

• Envelope(Assign(Ready)) and Envelope(Assign(Done)) share the same top-level message constructor and differ only by nested payload identity.
• The checker accepts the split only because the nested typed predicates are provably disjoint over discovered concrete payload cases.
• Lowering emits exact typed payload guards in Mantle transition records.
• Runtime dispatch uses typed message IDs, current state IDs when applicable, and exact typed payload identity, not source strings or debug labels.

Actor Payload Split Signature

examples/actor_payload_split_signature.str proves the same payload-sensitive same-message split through step parameter patterns rather than a whole-body match msg.

just run-example actor_payload_split_signature

Key source ideas:

• Multiple fn step(state, Envelope(Assign(...))) clauses can share one top-level message constructor when the nested typed predicates are provably disjoint.
• Envelope(Assign(Ready)) and Envelope(Assign(Done)) lower to two typed payload-guarded Mantle transitions for the same typed message ID.
• Mantle selects the transition by typed message ID, current state ID when applicable, and exact typed payload identity.
• actor_payload_split_match.str exercises the equivalent whole-body match msg authoring form.

Actor Payload Split Signature Wildcard

examples/actor_payload_split_signature_wildcard.str proves that a payload-sensitive step-signature split can use _ as fallback for discovered concrete payload cases not handled by explicit nested predicates.

just run-example actor_payload_split_signature_wildcard

Key source ideas:

• Envelope(Assign(Ready)) handles the explicitly guarded payload case.
• _ handles the discovered Envelope(Assign(Done)) case, and lowering emits a typed payload guard for Assign(Done) rather than an open runtime catch-all.
• The fallback remains bounded to discovered concrete payload cases discovered by checking.
• Runtime dispatch still uses typed message IDs and exact typed payload identity, not source strings or debug labels.

Actor Payload State-Match Split

examples/actor_payload_state_match_split.str proves that state-match step clauses can share one top-level message constructor by disjoint nested typed payload predicates.

just run-example actor_payload_state_match_split

Key source ideas:

• Envelope(Assign(Ready)) and Envelope(Assign(Done)) are explicit, discovered payload cases for the same message constructor.
• Each payload case expands across the checked Idle, SawReady, and Done current-state cases from match state.
• Lowering emits typed Mantle transitions keyed by message ID, current state ID, and exact typed payload guard.
• State changes remain immutable whole-value returns through Continue(...) or Stop(...); runtime dispatch does not use source strings or debug labels.

Actor Payload State-Match Wildcard

examples/actor_payload_state_match_wildcard.str proves that a payload-sensitive state-match split can use _ as fallback for discovered concrete payload cases not handled by explicit state-match clauses.

just run-example actor_payload_state_match_wildcard

Key source ideas:

• Envelope(Assign(Ready)) handles the explicitly guarded payload case.
• The wildcard state-match step handles the discovered Envelope(Assign(Done)) case; lowering emits Assign(Done) as an exact typed payload guard rather than an unguarded payload catch-all.
• Each explicit and fallback payload case expands across the checked Idle, SawReady, and Done current-state cases from its match state body.
• State changes remain immutable whole-value returns through Continue(...) or Stop(...); runtime dispatch does not use source strings or debug labels.

Nested Patterns

examples/nested_patterns.str composes immutable destructuring across constructor payloads, records, list elements/rest, and map values/rest.

just run-example nested_patterns

Key source ideas:

• AssignEnvelope(Assign(Job { phase })) binds a nested record field from a constructor payload through typed projection paths.
• HoldEnvelope(Hold(List[Job { phase }, ..tail])) binds an immutable list suffix whole value, not a mutable view.
• LookupEnvelope(Lookup(Map[Ready => Job { phase }, ..rest])) keeps map matching on static keys while binding nested values and an immutable rest map.
• Lowering emits typed Mantle value templates; runtime execution does not use source strings as executable references.

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.

just run-example actor_reply

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 checked target process ID, not by source labels.

Actor Emit Spawn Send

examples/actor_emit_spawn_send.str combines emit, spawn, and send in one checked transition. Main declares each effect and exact Cap<Spawn<Worker>> authority, spawns Worker, sends Ping through the typed process reference, and stops with a whole replacement state.

just run-example actor_emit_spawn_send

Key source ideas:

• authority spawn_worker: Cap<Spawn<Worker>>; declares the exact local spawn capability.
• fn step(...) -> ProcResult<MainState> ! [emit, spawn, send] declares the exact effects used by the body.
• let worker: ProcessRef<Worker> = spawn Worker; creates a typed process reference.
• send worker Ping; dispatches by the checked process-reference target and message ID after lowering, not by source text.
• return Stop(MainState { phase: Done }); preserves immutable whole-state transition semantics.

Import, Boundary, And Failure Examples

This page covers runnable examples where source-unit visibility, boundary contracts, or fail-closed runtime behavior are the primary evidence.

Source-Unit Imports

examples/imports_main.str imports imports_types.str and imports_worker.str. The root owns Main, the type unit owns Job, Phase, and complete, and the worker unit owns Worker. Strata resolves that graph before checking and lowering.

just run-example imports_main

The graph is checked in deterministic dependency-first order, direct imports authorize visible declarations, and Mantle runs target/strata/imports_main.mta without loading .str files or resolving import names at runtime.

Boundary Contracts

examples/boundary_contracts_main.str runs the checked boundary surface in Boundary Contracts:

Run it with just run-example boundary_contracts_main.

Actor Panic No Replay

examples/actor_panic_no_replay.str shows an abnormal transition that consumes one queued Ping, returns Panic(Failed), records failure evidence, and does not replay the consumed message.

just run-example actor_panic_no_replay

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

File Types

This repository uses these first-class file identities:

• .str for Strata source.
• .mta for Mantle Target Artifacts.
• .component-composition.json for Strata-owned checked-subset component-composition validation artifacts generated under target/strata/ by default.
• .authority-effect.json for Strata-owned checked authority/effect fact artifacts generated under target/strata/ by default.
• .authority-policy.json for Strata-owned typed authority policy decision artifacts generated under target/strata/ by default from admitted authority/effect facts.
• .deployment-composition.json for explicit runtime composition binding artifacts generated under target/strata/ by default when a checked composition artifact is bound to a matching .mta.
• .authority-effect-binding.json for explicit Mantle runtime authority/effect binding artifacts generated under target/strata/ by default when checked authority/effect facts are bound to a matching .mta.

.str

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

A root .str file may import sibling source units with import module_name;. Those imports are resolved by Strata before checking and lowering. They do not make .mta files import-aware, and Mantle does not load .str files or resolve Strata imports at runtime.

Expected MIME type:

text/x-strata

.component-composition.json

.component-composition.json files are Strata checked-subset component-composition validation artifacts. They are generated by strata composition build <path.str> and validated by strata composition admit <path.json>. They are not .mta, not Mantle runtime inputs, not runtime composition bindings, and not executable dispatch data.

The artifact self-identifies internally with schema_id=strata.checked_component_composition, schema_version_major=1, schema_version_minor=0, artifact_kind=checked_component_composition, hash_alg=fnv1a64-diagnostic, and source_language=strata. It records source provenance, a composition ID, component instances with import/export port obligations, empty arrays for binding classes the current source subset cannot express, port bindings, binding admission results, unsatisfied imports, cross-component authority-flow edges, nullable policy/diagnostic hash slots, an empty extensions map, and a global admission result. Admitted artifacts must bind every declared component import exactly once, have empty unsatisfied_imports, no rejected binding results, and no rejection evidence. Rejected artifacts must carry bounded rejection evidence and must list any unbound declared import once. strata composition admit also requires source_fingerprint to be the canonical 16-character lowercase hexadecimal value for the declared source_fingerprint_algorithm. It may inspect rejected artifacts, but as a checked-subset validation gate it exits non-zero unless the artifact is globally admitted.

Source names in the JSON are metadata for diagnostics, provenance, and review. Executable meaning is carried by typed component-instance IDs, port-binding IDs, component IDs, port IDs, protocol IDs, and validated authority descriptors. A hand-edited artifact may rename metadata labels without changing typed admission, but one that drops typed IDs, strips binding evidence, duplicates an import binding, references unknown instances, makes an authority descriptor inconsistent with its typed ID, uses an unsupported schema, or marks unsatisfied imports as admitted fails closed. The admission command validates the artifact schema and internal typed-ID consistency; it is not a source re-check or tamperproof attestation for a coherently rewritten JSON file.

.authority-effect.json

.authority-effect.json files are Strata-owned checked authority/effect fact artifacts. They are generated by strata authority-effects build <path.str> and validated by strata authority-effects admit <path.json>. They are not .mta, not Mantle runtime inputs, not policy grants, and not executable dispatch data.

The artifact self-identifies internally with schema_id=strata.checked_authority_effects, schema_version_major=1, schema_version_minor=0, artifact_kind=checked_authority_effects, hash_alg=fnv1a64-diagnostic, and source_language=strata. It records source provenance, each checked process by typed process ID, per-process state/message counts, checked protocol/port/component table counts, process-local authority IDs with exact authority descriptors, typed spawn-site IDs, supervisor-child spawn proof facts for lexical supervisor spawn sites, typed transition IDs with exact message, current-state, and declared-effect IDs, typed component authority surfaces with declared import-port counts, nullable policy/diagnostic hash slots, an empty policy_inputs array, an empty extensions map, and admission_result=admitted.

Source names and labels in the JSON are metadata for diagnostics, provenance, and review. Runtime-affecting meaning is carried by typed process IDs, authority IDs, spawn-site IDs, transition IDs, component IDs, port IDs, protocol IDs, and exact effect IDs. Admission rejects malformed schema identity, unsupported versions, noncanonical typed-ID ordering, duplicate exact effects, unknown referenced process/authority/message/state/protocol/port/component IDs, lexical supervisor-child spawn facts without matching supervisor/child backlinks, declared table-count/import-count mismatches, inconsistent component/port authority descriptors, noncanonical source fingerprints, non-empty unsupported policy inputs, and non-empty extensions. It validates the checked fact artifact shape; it does not re-check source and does not make hand-edited JSON a trust or integrity attestation. The fnv1a64-diagnostic fingerprint is provenance correlation metadata, not a cryptographic authenticity proof.

.deployment-composition.json

.deployment-composition.json files are explicit runtime composition binding artifacts. They are generated by strata composition bind-runtime <component-composition.json> <artifact.mta> --output <path.json> after the checked composition artifact admits and the .mta has been built from matching source. They self-identify with schema_id=mantle.runtime_composition_binding, schema_version_major=1, schema_version_minor=0, artifact_kind=runtime_composition_binding, source_language=strata, matching .mta format/schema/module/source-hash fields, the exact strata.checked_component_composition checked-composition schema, matching checked-composition version/composition ID fields, canonical component-instance-to-runtime-process correlations, canonical port binding IDs, singleton deployment_id=0 correlation namespace, admission_result=admitted, and an empty extensions map.

This binding artifact is not Strata source, not .mta, not a package manifest, and not executable dispatch data. It is the only file Mantle accepts for runtime composition correlation, and only when supplied explicitly with mantle run <artifact.mta> --composition-binding <deployment-composition.json>. Mantle does not read .component-composition.json, does not infer composition identity from source names, and does not verify Strata composition safety itself. If no binding is supplied, Mantle emits no deployment, composition, or component-instance trace correlation fields.

Mantle validates runtime bindings fail-closed before execution: malformed schema or version fields, non-admitted bindings, mismatched checked-composition schema, mismatched source fingerprint or .mta identity, mismatched component instance or port-binding IDs, duplicate component instance IDs, duplicate process correlations, and forged non-empty unsupported fields are rejected before ArtifactLoaded or host-visible runtime side effects. Labels and source names remain diagnostics/provenance metadata; typed IDs and loaded runtime process IDs carry meaning.

.authority-policy.json

.authority-policy.json files are Strata-owned typed authority policy decision artifacts. They are generated by strata authority-effects policy build <authority-effect.json> and validated by strata authority-effects policy admit <authority-policy.json> <authority-effect.json>. They are not .mta, not raw runtime input, not a policy DSL, and not source re-check evidence.

The artifact self-identifies with schema_id=strata.authority_policy_decisions, schema_version_major=1, schema_version_minor=0, artifact_kind=authority_policy_decisions, matching source identity fields, matching checked authority/effect schema identity/version, admission_result=admitted, and an empty extensions map. Its decisions array is a closed, canonical table over the checked process-authority set. Each entry carries only typed decision_id, process_id, authority_id, an exact descriptor, and a decision of admit or deny.

Admission fails closed when the policy is malformed, missing a checked authority, has duplicate or out-of-order typed IDs, references unknown process/authority IDs, mismatches a descriptor, carries source-label spoofing fields, mismatches the checked facts’ source identity, uses unsupported decisions, or has non-empty extensions. Source names and debug labels are not accepted as authority lookup keys.

.authority-effect-binding.json

.authority-effect-binding.json files are explicit Mantle runtime authority/effect binding artifacts. They are generated by strata authority-effects bind-runtime <authority-effect.json> <authority-policy.json> <artifact.mta> --output <path.json> after the checked authority/effect artifact and authority policy artifact admit and the .mta has been built from matching source. They self-identify with schema_id=mantle.runtime_authority_effect_binding, schema_version_major=1, schema_version_minor=0, artifact_kind=runtime_authority_effect_binding, singleton deployment_id=0, matching .mta format/schema/module/source-hash fields, the matching checked authority/effect schema identity/version, matching authority policy schema identity/version, canonical typed process authority, spawn-site, transition-effect, component-surface facts, canonical typed policy_decisions, admission_result=admitted, and an empty extensions map.

This binding artifact is not Strata source, not .mta, not a source report, and not executable dispatch data. It is the only authority/effect sidecar Mantle accepts, and only when supplied explicitly with mantle run <artifact.mta> --authority-effect-binding <authority-effect-binding.json>. Mantle validates the binding against the loaded .mta before ArtifactLoaded or host-visible runtime side effects. Forged source fingerprints, mismatched .mta identity, altered authority descriptors, altered spawn-site facts, altered exact-effect facts, missing or conflicting policy decisions, unsupported policy values, source-label injection, noncanonical typed IDs, and non-empty unsupported fields fail closed.

The binding intentionally strips Strata source labels and debug names from runtime-authoritative structures. Policy dispatch is by typed process and authority IDs only: admitted decisions can accept or deny dynamic spawn authority and boundary port-connect authority while preserving typed trace evidence. Mantle does not read .authority-effect.json or .authority-policy.json directly at runtime and does not infer authority from source labels, debug names, report text, or command-line widening flags.

.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=6
source_language=strata
target_requirements.source_language=strata
target_requirements.feature_count=...
target_requirements.feature.0=bounded_mailbox

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, 6 is the single admitted artifact schema baseline. Unsupported schema versions are rejected; artifact producers must emit the admitted schema.

The target_requirements.* block is a typed frontend-to-runtime binding surface. Strata emits it from checked IR and lowering facts; Mantle admits it only when the artifact format and schema version match the admitted artifact baseline, source_language is valid metadata and matches target_requirements.source_language, and every required runtime feature is supported by the current Mantle runtime feature declaration. The current Mantle runtime declaration treats source language as opaque artifact metadata rather than an executable dispatch key or language whitelist. Requirement entries are canonical runtime feature IDs such as local_execution, bounded_mailbox, local_send, local_spawn, typed_boundary_tables, and component_composition_metadata. They are not source names and are never executable dispatch strings.

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, an optional exact typed payload guard, and exact effect usage for their actions. Validation requires each message to have either a transition base with no current-state guard or one transition base for every admitted current-state ID. Within each message/current-state base, validation admits either one payload-unguarded transition or a payload-specific set where every transition carries an exact typed payload guard. Payload-specific sets enumerate admitted concrete payload cases; they do not encode source-payload algebra. Runtime selection indexes the admitted transition table by typed message ID, typed current state ID when a state guard is present, and exact typed payload identity when a payload 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, ordered value label, and optional typed payload metadata for each admitted state. The label must match the rendering of the typed value, preserving record field and map entry order from the admitted value. 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. Preserved order is visible in labels and traces, but runtime projection uses admitted typed IDs: record fields use record-field IDs into the admitted record shape, and map projections use typed static keys. Labels remain trace and diagnostic metadata, not runtime dispatch keys.

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.

Local spawn authority is encoded as per-process authority tables and spawn-site tables. A spawn action references a spawn-site ID, which references an authority ID with a typed Spawn descriptor for the same target process. Authority names remain metadata; admission and runtime checks use typed IDs and descriptors.

Protocol, port, component, and composition boundary data is encoded as typed tables. Component imports and composition bindings use port and component-instance IDs; names remain metadata for diagnostics and traces. Mantle validates complete composition binding and protocol compatibility before runtime execution, but it does not resolve Strata component names, import names, or source strings at runtime.

Local supervisor children are encoded as per-process supervisor plans with typed supervisor IDs, child IDs, child modes, restart intensity, and lexical supervisor-child spawn-site classifications. A lexical child spawn site carries supervisor and child IDs instead of a dynamic authority ID.

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 and, for payload-specific transitions, admitted typed payload identity, not payload text, source strings, or debug 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:

flowchart LR
    Source[".str source"]
    Check["strata check"]
    Build["strata build"]
    Artifact[".mta artifact"]
    Run["mantle run"]
    Trace["observability trace"]

    Source --> Check --> Build --> Artifact --> Run --> Trace

For fail-closed runtime behavior, the source must check and build, and mantle run must fail only after Mantle validates 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 is the root integration harness, with focused gate families under crates/strata-mantle-acceptance/tests/source_to_runtime_gates/.
• docs/src/examples.md owns the curated list of runnable examples. The grouped example pages document the behavior each example 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 in the grouped example pages.

The language surface proof substrate checks that the agreed current-surface proof domains map to declared features and that those features point at the required parser, checker, lowering, boundary, artifact, runtime, diagnostics, example, test, fuzz, and bounded/property evidence classes where those classes apply. It also checks that each proof domain declares the proof obligations implied by those features. That substrate supports implementation claims; it does not replace this executable gate shape.

Representative Commands

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

just run-example hello

A richer state/payload gate follows the same shape:

just run-example state_payload_match

The source-unit import gate starts at a root source file and proves that Strata, not Mantle, resolves the reachable dependency graph before lowering:

just run-example imports_main

The source contract data primitive gate proves immutable String and Bytes values survive source checking, lowering, Mantle artifact admission, runtime execution, and observability as typed primitive data rather than string dispatch:

just run-example source_contract_data_primitives

BDD scenario: Given immutable String and Bytes state/message values in a checked .str program, when Strata builds the typed .mta and Mantle runs it, then the trace and output show typed primitive data survived checking, lowering, admission, runtime branch evaluation, and process termination without source string dispatch.

The typed boundary contract gate proves protocol, port, component, and process-local PortConnect declarations check before lowering and run through Mantle-admitted typed IDs:

just run-example boundary_contracts_main

The component composition gate proves source-unit reachability plus typed component import binding before lowering, then runs the admitted artifact without runtime source-name resolution:

strata check examples/component_composition_main.str
strata build examples/component_composition_main.str
strata composition build examples/component_composition_main.str
strata composition admit target/strata/component_composition_main.component-composition.json --format json
strata composition bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.deployment-composition.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json
strata target-requirements examples/component_composition_main.str --format json
mantle feature-declaration --format json
mantle admit target/strata/component_composition_main.mta --format json

This target-binding gate keeps the boundary explicit. Strata reports the typed runtime features required by the checked program, emits and admits the Strata-owned strata.checked_component_composition JSON artifact as checked-subset component-composition validation evidence, and then emits an explicit mantle.runtime_composition_binding deployment binding for the matching .mta. Mantle separately reports the typed features it currently supports, admits the .mta requirements before execution, and emits deployment, composition, and component-instance trace correlation only when the explicit binding is supplied. The checked composition artifact is not Mantle input; Mantle does not infer source composition, verify Strata composition safety, or dispatch from source names. Source imports, component names, authority labels, composition artifacts, deployment bindings, and report data remain diagnostics, provenance, review records, admission evidence, or observability correlation evidence; they are not runtime dispatch inputs.

The authority/effect admission-binding gate proves checked authority and exact effect facts cross the Strata/Mantle boundary as admitted typed artifacts and a matching runtime binding. The dynamic-local branch exercises effect_outcome_spawn_denied:

strata check examples/effect_outcome_spawn_denied.str
strata build examples/effect_outcome_spawn_denied.str
strata authority-effects build examples/effect_outcome_spawn_denied.str
strata authority-effects admit target/strata/effect_outcome_spawn_denied.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --output target/strata/effect_outcome_spawn_denied.authority-policy.json
strata authority-effects policy admit \
  target/strata/effect_outcome_spawn_denied.authority-policy.json \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  target/strata/effect_outcome_spawn_denied.authority-policy.json \
  target/strata/effect_outcome_spawn_denied.mta \
  --output target/strata/effect_outcome_spawn_denied.authority-effect-binding.json
mantle run target/strata/effect_outcome_spawn_denied.mta \
  --authority-effect-binding target/strata/effect_outcome_spawn_denied.authority-effect-binding.json
strata authority-effects policy build \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --deny-spawn-authority \
  --output target/strata/effect_outcome_spawn_denied.authority-deny-policy.json
strata authority-effects policy admit \
  target/strata/effect_outcome_spawn_denied.authority-deny-policy.json \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/effect_outcome_spawn_denied.authority-effect.json \
  target/strata/effect_outcome_spawn_denied.authority-deny-policy.json \
  target/strata/effect_outcome_spawn_denied.mta \
  --output target/strata/effect_outcome_spawn_denied.authority-effect-deny-binding.json
mantle run target/strata/effect_outcome_spawn_denied.mta \
  --authority-effect-binding target/strata/effect_outcome_spawn_denied.authority-effect-deny-binding.json

The same gate also exercises the lexical supervisor-child branch:

strata check examples/local_supervision_restart.str
strata build examples/local_supervision_restart.str
strata authority-effects build examples/local_supervision_restart.str
strata authority-effects admit target/strata/local_supervision_restart.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/local_supervision_restart.authority-effect.json \
  --output target/strata/local_supervision_restart.authority-policy.json
strata authority-effects policy admit \
  target/strata/local_supervision_restart.authority-policy.json \
  target/strata/local_supervision_restart.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/local_supervision_restart.authority-effect.json \
  target/strata/local_supervision_restart.authority-policy.json \
  target/strata/local_supervision_restart.mta \
  --output target/strata/local_supervision_restart.authority-effect-binding.json
mantle run target/strata/local_supervision_restart.mta \
  --authority-effect-binding target/strata/local_supervision_restart.authority-effect-binding.json

The same gate also exercises component authority surfaces with both explicit runtime sidecars supplied to Mantle:

strata check examples/component_composition_main.str
strata build examples/component_composition_main.str
strata composition build examples/component_composition_main.str
strata composition admit target/strata/component_composition_main.component-composition.json --format json
strata composition bind-runtime \
  target/strata/component_composition_main.component-composition.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.deployment-composition.json
strata authority-effects build examples/component_composition_main.str
strata authority-effects admit target/strata/component_composition_main.authority-effect.json --format json
strata authority-effects policy build \
  target/strata/component_composition_main.authority-effect.json \
  --output target/strata/component_composition_main.authority-policy.json
strata authority-effects policy admit \
  target/strata/component_composition_main.authority-policy.json \
  target/strata/component_composition_main.authority-effect.json \
  --format json
strata authority-effects bind-runtime \
  target/strata/component_composition_main.authority-effect.json \
  target/strata/component_composition_main.authority-policy.json \
  target/strata/component_composition_main.mta \
  --output target/strata/component_composition_main.authority-effect-binding.json
mantle run target/strata/component_composition_main.mta \
  --composition-binding target/strata/component_composition_main.deployment-composition.json \
  --authority-effect-binding target/strata/component_composition_main.authority-effect-binding.json

This gate keeps the ownership split explicit. Strata emits and admits strata.checked_authority_effects facts from checked IR; Strata emits and admits the closed strata.authority_policy_decisions table over typed process authority IDs; the runtime binding then correlates those facts and decisions with a matching .mta. Mantle consumes only mantle.runtime_authority_effect_binding, only when supplied through --authority-effect-binding, and validates the binding before ArtifactLoaded or runtime side effects. Dynamic spawn and boundary port-connect decisions are enforced by typed IDs and traced with authority_policy_decision_id. Source labels, authority names, report text, and debug names remain diagnostics/provenance metadata and cannot retarget authority, policy, or effect facts.

An immutable source computation gate proves sequential source-local bindings are resolved before lowering while Mantle executes only typed artifact data:

just run-example function_local_bindings

A scalar computation gate proves typed scalar payloads, immutable process-local scalar functions, runtime scalar predicates, runtime-bound value conditionals, and Mantle execution of typed scalar templates:

just run-example runtime_scalar_priority

A selected return-match arm-prefix gate proves source-selected dispatch before Mantle executes typed runtime arm actions:

just run-example process_return_match_arm_runtime_if_prefix
just run-example process_return_match_arm_for_prefix
just run-example process_return_match_arm_for_if_prefix
just run-example process_return_match_arm_if_for_prefix

A runtime control-flow gate checks, builds, validates, runs, and traces typed Mantle execution:

just run-example runtime_guard_noop
just run-example runtime_scalar_priority
just run-example runtime_nested_if_actions
just run-example runtime_final_if_guarded_loop
just run-example runtime_final_if_nested_if_actions
just run-example runtime_final_if_nested_terminal_if
just run-example runtime_for_each
just run-example runtime_for_each_empty
just run-example runtime_for_each_if
just run-example runtime_for_each_nested_if_actions
just run-example runtime_guarded_for_each
just run-example runtime_guarded_ref_loop
just run-example runtime_guarded_ref_loop_jobs
just run-example runtime_loop_element_projection
just run-example effect_outcomes
just run-example effect_outcome_mailbox_full
just run-example effect_outcome_stopped_target
just run-example process_ref_stale_lifecycle
# Default-limit acceptance only; the exhausted/backend-unavailable branches use dedicated gates below.
just run-example effect_outcome_spawn_exhausted
just run-example effect_outcome_spawn_backend_unavailable
just run-example local_supervision_restart
just run-example local_supervision_permanent_stop
just run-example local_supervision_temporary
just run-example local_supervision_transient_restart
just run-example local_supervision_transient
just run-example local_supervision_inactive_send_outcome
just run-example local_supervision_inactive_crashed_send_outcome

just process-ref-lifecycle-gates runs process_ref_stale_lifecycle plus the trace-level assertion that a transported old runtime PID stops instead of retargeting to a newer same-definition worker.

run-example uses default runtime limits and policies. For effect_outcome_spawn_exhausted and effect_outcome_spawn_backend_unavailable, it proves the checked source still runs with available local spawn capacity/backend; the source-visible failure branches use the dedicated commands below.

The local spawn authority denial gate uses the same check/build path and then runs Mantle with a direct denial runtime limit. The authority/effect binding gate above is the product path for typed admitted spawn-authority policy:

just strata-check examples/effect_outcome_spawn_denied.str
just strata-build examples/effect_outcome_spawn_denied.str
just mantle-run-deny-spawn-authority target/strata/effect_outcome_spawn_denied.mta

The local spawn capacity exhaustion gate uses the same check/build path and then runs Mantle with a deliberately exhausted process limit:

just strata-check examples/effect_outcome_spawn_exhausted.str
just strata-build examples/effect_outcome_spawn_exhausted.str
just mantle-run-max-runtime-processes target/strata/effect_outcome_spawn_exhausted.mta 1

The local spawn backend-unavailable gate uses the same check/build path and then runs Mantle with the bounded local backend disabled before acceptance:

just strata-check examples/effect_outcome_spawn_backend_unavailable.str
just strata-build examples/effect_outcome_spawn_backend_unavailable.str
just mantle-run-disable-local-spawn-backend target/strata/effect_outcome_spawn_backend_unavailable.mta

The exhausted-spawn, backend-unavailable-spawn, stopped-target send, stale-process-ref send, and inactive-crashed-child send gates also assert effect_outcome_bound trace events. The denied-port-policy send-outcome gate instead proves fail-closed authority denial before source-visible outcome binding or delivery; runtime-unit and trace-validation coverage separately exercise closed-mailbox runtime causes. These trace events carry the numeric outcome_id, the spawn or send action kind, and the closed outcome_result category so the branch result is attributable to Mantle runtime cause rather than inferred only from output text. For stale process references, the proof combines the received payload_pid, the later stopped send outcome, and the absence of delivery to the newer runtime PID.

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

just strata-check examples/failures/effect_authority_missing.str
just strata-check examples/failures/source_local_binding_process_ref_carrier_enum.str
just strata-check examples/failures/scalar_overflow.str
just strata-check examples/failures/scalar_type_mismatch.str
just strata-check examples/failures/scalar_divide_by_zero.str
just strata-check examples/failures/scalar_runtime_divide_by_zero.str
just strata-check examples/failures/scalar_runtime_modulo_by_zero.str
just strata-check examples/failures/scalar_unsuffixed_literal.str

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

just run-example actor_panic_no_replay

Each successful mantle run command must validate 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. Acceptance tests that read trace evidence validate the Mantle-owned JSONL trace schema before trusting the trace summary. That validation checks schema identity, exact per-event field sets, required fields, typed ID field shapes, grouped payload/loop fields, artifact_loaded first/no-repeat ordering, Mantle-contiguous spawned PID sequencing, u32 artifact typed-ID width, u16 branch path segments and bounded path length, non-entry spawn parent evidence, runtime PID-to-process-ID correlation, supervisor-child restart causality, and restart-window numeric bounds/coupling only; it does not make trace JSON an artifact boundary or a source semantics input.

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.

Language Surface Proof Substrate

The current language surface proof substrate is an executable, machine-readable model of the implemented Strata and Mantle surface. It maps the agreed proof domains for the current language surface to declared feature entries, maps those entries to typed proof obligations, and maps those obligations to the evidence classes required for that feature: parser coverage, checker/static validation, checked IR and lowering coverage, Strata/Mantle boundary preservation, Mantle artifact admission, runtime execution, diagnostics, examples, positive and negative tests, source-to-runtime gates, fuzz seeds, and bounded or property coverage where that evidence applies. Typed scalar values and value operators are part of the runtime-bearing surface: their source syntax, checked folding, typed lowering, Mantle artifact admission, typed value-if templates, runtime evaluation, and fail-closed diagnostics are all recorded in the inventory. Source contract data primitives are recorded as a runtime-bearing typed data surface: immutable String and Bytes literal syntax, exact primitive equality, checked primitive value shapes, lowercase-hex artifact labels, Mantle artifact admission, runtime typed-value execution, observability evidence, source-to- runtime gates, fuzz seeds, bounded/property coverage, performance-smoke profiles, diagnostics, and docs are tracked together. Source strings, labels, and primitive payload bytes remain data or metadata and never become executable runtime dispatch inputs. Typed effect outcomes are also runtime-bearing: source-visible send/spawn Result bindings, checked outcome templates, Mantle artifact admission, runtime commit-or-return behavior, spawn success process-reference evidence, source-to-runtime success plus Full pre-acceptance capacity, stopped-target Stopped, runtime-unit MailboxClosed supervisor-closure, inactive-child Crashed, denied/exhausted/backend-unavailable spawn failure evidence, parse/check/lower, artifact-decode, and runtime-from-source fuzz seeds, bounded state-admission evidence, and diagnostics are recorded together. Local spawn authority is recorded as a runtime-bearing boundary feature: process-local Cap<Spawn<Target>> declarations, exact checked target matching, typed authority IDs, typed spawn-site IDs, Mantle artifact and loaded-runtime admission, overbroad-authority rejection, spawn_authority_checked trace evidence, Err(Denied(Unit)) runtime denial before acceptance, source-to-runtime gates, fuzz seeds, bounded authority-model evidence, diagnostics, and docs are tracked together.

Authority policy decisions are recorded as a runtime-bearing Strata/Mantle boundary feature: checked authority IDs, spawn-site IDs, transition message/current-state/effect IDs, component authority surfaces with declared import-port counts, and exact effect facts are rendered as the Strata-owned strata.checked_authority_effects artifact, admitted before policy admission, covered by a closed strata.authority_policy_decisions typed decision table, correlated with the matching .mta, and rendered as the Mantle-facing mantle.runtime_authority_effect_binding artifact. Mantle admits the runtime binding by typed IDs and descriptor/effect equivalence before execution. The dynamic-local branch applies admitted policy decisions before spawn side effects and records typed spawn_authority_checked evidence; boundary sends apply the typed port_connect decision before message acceptance; both bare sends and typed send outcomes fail closed on denial without binding a source-visible mailbox outcome while recording boundary_send_checked evidence with authority_policy_decision_id; the lexical supervisor-child branch records typed supervisor_child_started and supervisor_restart_decision evidence instead of inventing dynamic authority. Source labels, debug names, diagnostics, and report text remain metadata; they cannot retarget authorities, spawn sites, ports, components, effects, or policy decisions. source_path is slash-normalized provenance metadata, and the checked schema namespace is frontend-owned as <source_language>.checked_authority_effects. Mantle rejects raw .authority-effect.json and .authority-policy.json files supplied as runtime bindings before trace creation. Source-to-runtime gates for admitted and denied dynamic-local spawn authority, denied boundary port authority, denied port-authority send outcomes, lexical supervisor-child spawning, and component authority surfaces; forged-binding negative tests; authority/effect, authority-policy, dynamic-local, lexical supervisor-child, and component runtime-binding fuzz seeds; performance-smoke profiles; diagnostics; and docs are tracked together.

Local supervision is recorded as a runtime-bearing boundary feature: local one_for_one supervisor declarations, lexical child IDs, child restart modes, explicit restart intensity, lexical spawn-site classification, Mantle artifact and loaded-runtime admission, acyclic child-graph validation, restart trace evidence, no message replay after panic, source-to-runtime gates, fuzz seeds, diagnostics, and docs are tracked together.

Source-unit imports are recorded as a Strata-owned composition feature: import module_name; syntax, root source loading, typed source-unit IDs, an acyclic dependency graph, deterministic dependency-first checking, duplicate and ambiguous-name rejection, direct-import symbol validation, source-to-runtime execution from a multi-file program, fuzz seeds, diagnostics, and docs are tracked together. Mantle import resolution is not part of the surface; module names in artifacts remain metadata.

Typed protocol, port, and component boundaries are recorded as a runtime-bearing boundary feature: source declarations, optional send ... via Port syntax, process-local Cap<PortConnect<Port>> authority, checked protocol/port/component IDs, direct-import validation, deterministic lowering into Mantle boundary tables, artifact and loaded-runtime admission, accepted boundary_send_checked trace evidence, fail-closed admission diagnostics for denied boundary shapes, source-to-runtime execution, fuzz seeds, bounded deterministic lowering evidence, diagnostics, and docs are tracked together. Mantle does not resolve protocol, port, component, or import names at runtime; those names remain metadata.

Checked local component port-binding composition admission is recorded as a runtime-bearing boundary feature: component import lists, local composition declarations, implementation-local source admission input, typed component-instance IDs, typed port-binding edges, direct-import validation, duplicate and unbound import rejection, unimported-port binding rejection, protocol mismatch rejection, deterministic graph lowering, Mantle composition-table admission, Strata-owned composition admission report emission, Strata-owned strata.checked_component_composition artifact build/admit coverage, source-to-runtime execution, fuzz seeds, performance-smoke evidence, diagnostics, and docs are tracked together. The report and the durable artifact record the diagnostic FNV-1a source fingerprint, typed component-instance IDs, component import/export port obligations, typed port-binding IDs, admitted binding results, empty unsatisfied imports for admitted compositions, endpoint port authority requirements, and cross-component authority edges for review/admission. The artifact is emitted as target/strata/<stem>.component-composition.json, self-identifies with schema ID/version/source-language fields, and fails closed when typed IDs are missing, duplicated, malformed, stripped of required binding evidence, internally inconsistent with authority descriptors, or inconsistent with admission results. It validates the artifact schema and internal typed-ID consistency; it is not a source re-check, not a tamperproof attestation for a coherently rewritten JSON file, and not directly executable Mantle input. strata composition bind-runtime adds the explicit deployment-admission bridge by validating an admitted checked composition artifact against a matching .mta and rendering the separate mantle.runtime_composition_binding JSON artifact. That binding must match the .mta module, source fingerprint, composition ID, component instances, runtime process IDs, and port bindings before Mantle can use it for observability correlation. The checked composition artifact remains Strata-owned and not .mta; checked IR lowering, Mantle artifact admission, and explicit runtime binding admission remain separate evidence classes. Mantle admits typed composition metadata inside .mta but does not resolve source component names, source-unit imports, source strings, Strata composition artifacts, or report data at runtime.

Runtime feature declaration and target binding are recorded as a runtime-bearing boundary feature: Strata derives canonical typed target requirements from checked IR and lowering facts, embeds them in the .mta, renders them through strata target-requirements, Mantle renders its own typed mantle.feature_declaration.v6 declaration, and Mantle admission compares the artifact’s format, schema version, source language, declared runtime features, and artifact-derived minimum required features before execution. The runtime declaration includes conservative message-observation fields and explicit validity-window defaults without claiming distributed transport support. Mismatched or malformed source-language metadata, unsupported runtime features, underdeclared requirements, malformed requirement fields, remote send/spawn, and distributed transport remain fail-closed implementation limits. The evidence includes unit, negative, bounded determinism, source-to-runtime, acceptance, fuzz-seed, performance-smoke, docs, and assurance matrix coverage; it does not claim theorem-prover coverage.

Remote/distributed runtime capabilities are recorded as a future/non-admitted boundary: Strata lowering must not emit remote_send, remote_spawn, or distributed_transport, and Mantle’s mantle.local_only.v1 target profile must reject forged artifacts requiring those canonical feature IDs before admission, ArtifactLoaded, host sinks, or runtime side effects. The focused remote / distributed boundary gate checks current .str entry examples against the local-only profile and separately forges remote/distributed artifact requirements to prove fail-closed admission. This preserves the local-runtime boundary until a real distributed Mantle design exists.

Mantle executable-plan construction is recorded as an internal runtime implementation feature: Mantle validates a loaded .mta, builds typed dispatch/action tables and a Mantle-owned executable template program from the admitted LoadedProgram, and executes from those pre-resolved plan references. The evidence covers plan construction, deterministic transition ordering, typed action tables, executable next-state/send/for-each template refs, source-name/debug-label retargeting attempts, invalid loaded-template reference rejection before ArtifactLoaded, runtime execution equivalence, source-to-runtime gates, performance-smoke coverage, and docs. This evidence does not add a serialized bytecode format, a Strata lowering target, new source semantics, new fuzz decoder seeds, or new unsafe indexing assumptions; it remains bounded machine-checked assurance.

Runtime trace observability is recorded as a Mantle-owned runtime feature: runtime events are strongly typed before rendering, JSONL output carries the mantle-runtime-observability schema ID and version, and the validator checks required fields, exact per-event field sets, grouped payload/loop fields, typed ID fields, strict unsigned integer syntax, u16 branch path segments plus bounded path length, closed runtime enum value domains, u32 artifact typed-ID width, artifact process-ID bounds, artifact_loaded first/no-repeat ordering, Mantle-contiguous spawned PID sequencing, non-entry spawn parent evidence, runtime PID-to-process-ID correlation, optional runtime-composition correlation field grouping plus whole-trace composition identity stability, supervisor-child restart causality, and restart-window numeric bounds/coupling using borrowed line scans over already-read trace text. Deployment, composition, and component-instance trace fields appear only when Mantle was explicitly launched with an admitted mantle.runtime_composition_binding artifact; absent binding input leaves those fields absent and forbids fabricated IDs. Validation is capped by explicit trace-byte, event-count, and runtime-process limits before trace evidence is used by a gate. The evidence includes unit and negative schema tests, source-to-runtime trace validation, fuzz seeds for malformed traces, bounded rendered-all-event contract evidence for metadata-vs-typed-ID separation, JSONL performance-smoke coverage, docs, and assurance matrix coverage. No new unsafe code, arena indexing assumption, or unchecked correlation path is introduced by the trace validator, so this slice does not add a new Miri-specific target beyond the existing just miri-ci disposition. The trace contract remains observability evidence only; it is not an artifact format, Strata lowering target, source semantic surface, or executable dispatch input.

Run it with:

just language-surface-assurance

The machine-readable inventory is rooted in:

crates/strata-mantle-acceptance/tests/language_surface_assurance.rs

The proof-domain declarations and feature declarations are split by surface under:

crates/strata-mantle-acceptance/tests/language_surface_assurance/

The gate fails when a declared proof domain is missing, when a declared language surface feature is not included in a proof domain, when a domain omits a proof obligation implied by its features, when an obligation has no supporting evidence class, when a feature is missing one of its required evidence classes, when an evidence path disappears, or when the recorded marker no longer exists in the cited file. Source-to-runtime evidence must point at the active Justfile check/build/run commands for the cited source example. The inventory also fails if an evidence class is incompatible with the feature’s declared surface layer, so source-only, checker/lowering, artifact-admission, runtime, docs/example, and future/non-admitted classifications remain distinct.

This gate is the current-language-surface proof substrate for implementation claims. It is not a full theorem-prover proof of every semantic rule, and it does not replace runnable source-to-runtime behavior:

flowchart LR
    Source[".str source"] --> Check["strata check"]
    Check --> Build["strata build"]
    Build --> Run["mantle run"]
    Run --> Trace["trace"]

Runtime-bearing features still need source-to-runtime evidence. Trace labels, source names, and documentation text remain metadata and diagnostics surfaces; executable behavior must cross the Strata/Mantle boundary as checked IR, typed IDs, typed value templates, and admitted Mantle artifacts. Record field projection is represented as admitted record-field IDs; source field names remain labels, diagnostics, and trace metadata.

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.

flowchart LR
    Source["Strata source names"]
    Checked["checked symbols and IDs"]
    Artifact["artifact typed tables"]
    Runtime["loaded runtime IDs"]
    Trace["trace labels"]

    Source --> Checked --> Artifact --> Runtime
    Source -. metadata .-> Trace
    Artifact -. labels .-> Trace
    Runtime --> Trace

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.

Artifact source_hash_fnv1a64 is a non-authoritative diagnostic fingerprint for correlating a lowered artifact with source text during local inspection. It is not an integrity, provenance, authority, or trust decision input; artifact admission must rely on explicit format/schema validation and typed structures.

Target requirements are checked/lowered facts embedded in the artifact. Strata emits target_requirements.source_language and a sorted set of canonical runtime feature IDs such as bounded_mailbox, local_execution, local_send, local_spawn, emit_effect, and typed_boundary_tables. Mantle compares those requirements with its mantle.local_only.v1 runtime target profile before ArtifactLoaded or executing runtime side effects; an unsupported feature fails closed with a diagnostic such as target runtime feature remote_spawn is not supported.

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;
• typed target requirements, including target source language and canonical runtime feature IDs;
• 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;
• unique typed authority descriptors, referenced authority IDs, and spawn-site table entries per process;
• typed protocol, port, and component boundary tables, including exact required-authority descriptors and port target process/message compatibility;
• typed component composition tables, including declared component instances, imported port bindings, protocol compatibility, and complete binding of every component import;
• either one unguarded transition per accepted message or one state-specific transition for each admitted state value;
• exact transition effect usage for emitted, spawned, and sent actions;
• transition references to known messages, state values, type IDs, process references, authority IDs, spawn-site IDs, outputs, and process IDs.

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

Mantle also publishes a typed mantle.feature_declaration.v6 runtime feature declaration. The current declaration names the artifact format and schema version it admits, its opaque source-language metadata policy, local runtime feature support, target-profile identity, host/network/transport/cluster authority policy, non-progress containment class, message-count mailbox model, conservative message-observation support, allocation model, component/spawn observability support, validity-window defaults, backend identity, and explicit implementation limits such as remote send, remote spawn, and distributed transport. Admission derives the minimum runtime feature set required by the decoded .mta tables and requires the artifact’s typed target_requirements block to cover that set before ArtifactLoaded or any runtime side effect. Unsupported schema versions, unsupported required features, underdeclared requirements, unsorted or duplicate requirement entries, mismatched source-language metadata, and malformed requirement fields fail closed.

Strata owns requirement derivation. It derives requirements from checked IR and lowering facts such as local execution, bounded mailboxes, emitted effects, local spawn/send, typed effect outcomes, scalar value templates, runtime branching, bounded runtime loops, typed boundary tables, and component composition metadata. Mantle owns only the declaration and comparison; it does not infer Strata source composition, imports, source names, authority widening, or deployment safety.

Internal Executable Plan

After a .mta decodes into a LoadedProgram, Mantle validates loaded admission and then constructs an internal executable plan for runtime dispatch. The plan pre-resolves transition dispatch, action blocks, process-reference targets, spawn-site authority references, branch bodies, loop bodies, and value-template program references into typed runtime structures. Runtime value templates are compiled into Mantle-owned ExecutableTemplateProgram entries and runtime actions/next-state plans carry ExecutableValueTemplate references rather than walking recursive loaded artifact templates on the hot path. Process and message labels may be borrowed for reports and traces, but they are not executable dispatch keys.

The executable plan and executable template program are not serialized bytecode, not Strata lowering targets, and not replacements for artifact validation. Constructing them cannot grant authority or bypass feature, artifact, or loaded-program admission. Invalid loaded references fail before ArtifactLoaded and before host-visible runtime side effects. Source names, process debug names, message labels, template labels, and other display strings remain diagnostics and trace metadata; runtime dispatch and template execution use admitted typed IDs and executable-plan references. Canonical type, variant, and field labels are materialized only when Mantle constructs the bounded RuntimeValue representation for payload/state data or trace/report rendering; executable template plans carry typed IDs, not string selectors.

Host Path Handling

Artifact and trace paths are validated before host IO. On Unix targets, Mantle opens artifact and trace paths with descriptor-relative parent traversal and O_NOFOLLOW so symlink parents and final symlink leaves fail closed at open time. On Windows targets, Mantle opens final artifact and trace paths with reparse-point traversal disabled, rejects reparse-point path components, and validates the opened handle against the canonical path with stable Windows file metadata. Other targets fail closed unless they provide equivalent secure path support.

Execution

Mantle executes from the admitted executable plan. Before emitting ArtifactLoaded or executing runtime side effects, Mantle validates loaded entry metadata, state tables, transition state targets and templates, outputs, record field projections, and all plan-resolved action references. Record field projection and record construction templates carry typed record-field IDs into admitted record type shapes; record field names remain metadata for value labels, diagnostics, and traces. Process references, sends, payload templates, and transition effect usage are validated as typed IDs or admitted templates before execution. Loaded authority tables and spawn-site tables are validated before any runtime side effect. A spawn action references a typed spawn-site ID; that site references a typed authority ID whose descriptor must be an exact local Spawn capability for the same target process. A typed boundary send through a loaded PortId requires an exact process-local PortConnect authority for that same port. Loaded authorities that are not referenced by any spawn site or typed-port send are rejected as overbroad. Authority debug names and source labels are metadata, not dispatch inputs. 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.

Typed boundary sends carry an optional admitted PortId. Mantle validates that the port targets the same process as the send, that the port protocol message type matches the target process message enum, and that the process authority table admits the same port ID. Runtime dispatch still uses the loaded process and message IDs; protocol, port, and component names are trace metadata only. Invalid or denied boundary shapes fail artifact or loaded-program admission before ArtifactLoaded; accepted typed boundary sends emit boundary_send_checked during runtime dispatch.

Component composition metadata carries component-instance IDs and port IDs. It is admitted as a typed graph: every instance must point at a component table entry, every imported port edge must target a declared instance, the importing component must declare that imported port, the exporting component must export the bound port, protocols must match, and every component import on every instance must be bound. Runtime dispatch does not look up component names or source import names; the composition graph is metadata/admission data for the already lowered typed IDs. The checked composition admission report is a Strata-owned inspection surface derived before Mantle execution. It records the diagnostic FNV-1a source fingerprint, typed component-instance IDs, typed port-binding IDs, admitted binding results, empty unsatisfied imports for admitted compositions, and endpoint authority edges for review, but it is not an executable artifact and Mantle does not read it.

The component-composition validation artifact is also Strata-owned and is emitted by strata composition build as target/strata/<stem>.component-composition.json by default. It self-identifies as the checked-subset strata.checked_component_composition schema version 1.0 with hash_alg=fnv1a64-diagnostic, carries source provenance as metadata whose diagnostic source fingerprint must have the declared canonical lowercase hexadecimal shape, and admits or rejects the checked local composition graph with typed component-instance, component import/export port, port-binding, port, protocol, and authority descriptor IDs. It is deliberately not .mta and Mantle does not read it as runtime input. Binding classes that the current source subset cannot express are present as empty arrays and fail closed if forged non-empty, keeping the Strata-owned source evidence boundary explicit without inventing capability, interface, runtime-feature, archive-format, crypto-policy, policy-hash, or diagnostic-set facts.

strata composition bind-runtime is the explicit deployment-admission bridge from admitted checked composition evidence to Mantle observability correlation. It validates that the checked artifact is globally admitted and matches a specific .mta source language, module, diagnostic source hash, composition ID, component-instance table, runtime process correlation, and port-binding table, then emits target/strata/<stem>.deployment-composition.json with schema_id=mantle.runtime_composition_binding and composition_schema_id=strata.checked_component_composition. Mantle accepts that artifact only when the operator supplies mantle run <artifact.mta> --composition-binding <deployment-composition.json>, validates the exact binding and checked-composition schema identities again before ArtifactLoaded, and uses it only to render singleton deployment_id=0, composition_id, and optional component_instance_id trace correlation. Without the binding argument, Mantle runs the .mta without composition correlation fields; it does not infer composition identity from source names, does not verify Strata composition safety itself, and does not dispatch from composition metadata.

The authority/effect fact artifact is a separate Strata-owned boundary surface emitted by strata authority-effects build as target/strata/<stem>.authority-effect.json by default. It self-identifies as the checked strata.checked_authority_effects schema version 1.0 with hash_alg=fnv1a64-diagnostic, records checked process IDs, process-local state/message counts, checked protocol/port/component table counts, authority IDs, spawn-site IDs, transition IDs, transition message/current-state references, exact effect IDs, supervisor-child spawn proof facts for lexical supervisor spawn sites, component/port authority-surface IDs, declared import-port counts, and source provenance metadata, and fails closed when typed IDs are noncanonical, duplicated, outside declared table counts, unknown, internally inconsistent, missing a supervisor-child backlink, or paired with unsupported non-empty future fields. It is not .mta, not runtime input, and not a policy grant. Its source_path field is slash-normalized diagnostic metadata for review/provenance only; neither Strata lowering nor Mantle execution uses that path as an executable binding.

strata authority-effects policy build turns admitted checked authority/effect facts into the separate strata.authority_policy_decisions artifact. Policy admission validates a closed, canonical decision table over typed process-authority IDs and exact descriptors. Missing, duplicated, out-of-order, unknown, unsupported, label-spoofed, stale, or descriptor-mismatched decisions fail closed; source names and debug labels are metadata only.

strata authority-effects bind-runtime is the explicit runtime-admission bridge from admitted checked authority/effect facts plus an admitted typed authority policy artifact to Mantle policy input and observability evidence. It validates the admitted .authority-effect.json and .authority-policy.json against each other and against a specific .mta source language, module, source hash, process table, authority table, spawn-site table, transition effect table, and component authority-surface table, then emits target/strata/<stem>.authority-effect-binding.json with schema_id=mantle.runtime_authority_effect_binding. The checked authority/effect schema name is a frontend-owned namespace, <source_language>.checked_authority_effects; Strata emits strata.checked_authority_effects, and Mantle validates a binding language-neutrally against the loaded artifact’s source_language plus that suffix rather than hardcoding Strata ownership. Mantle accepts the runtime binding only when the operator supplies mantle run <artifact.mta> --authority-effect-binding <authority-effect-binding.json>, validates the binding, checked-fact schema identity, and authority-policy schema identity again before ArtifactLoaded, and uses admitted policy_decisions only to accept or deny already-declared runtime-enforceable authorities by typed process and authority IDs. Dynamic spawn and boundary port-connect decisions are enforced before runtime side effects and recorded with authority_policy_decision_id. Source labels, debug names, report text, and authority names are metadata and cannot grant, widen, strip, or retarget runtime authority.

Transition effect metadata is admitted with the artifact, loaded as runtime effect usage, and must exactly match the action effects that execute. Runtime if conditions are admitted as typed Bool value templates. Strata lowers core Bool to the canonical Mantle fieldless enum/value IDs, and Mantle validates the typed artifact shape instead of dispatching through source names. Mantle validates both branch bodies before execution, executes only the selected branch, admits one direct nested runtime branch action layer, rejects deeper direct branch nesting, rejects branch-local process-reference binding, and records branch selection in the runtime trace. Runtime branch bodies may contain admitted bounded loop actions; Mantle validates loop bodies before execution and still rejects nested loops. Equality conditions are admitted as typed value templates over Bool or payload-free enum operands; Mantle evaluates admitted typed values, not source strings or debug labels. Boolean predicate composition is admitted as a typed Bool value-template tree built from !, &&, ||, direct Bool templates, and typed equality templates.

The action set covers:

• emitting declared output;
• spawning a declared process through a process reference and admitted spawn authority;
• binding typed spawn and send effect outcomes in the pre-state action prefix;
• sending a declared message through a bound process reference;
• selecting a typed runtime branch over admitted action blocks;
• iterating over an admitted bounded list template with a typed active loop element binding.

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. Every emitted event also carries the Mantle-owned trace schema ID mantle-runtime-observability and schema version 1. The schema identifies the observability contract only; it is not a .mta schema, serialized bytecode, source semantic surface, retargeting input, or dispatch table. Trace validators may check required fields, typed ID field shapes, artifact_loaded first/no-repeat ordering, Mantle-contiguous spawned PID sequencing, and runtime PID-to-process-ID correlation. Repository validation rejects fields outside the per-event trace contract and checks grouped payload/loop fields, strict unsigned integer syntax, u32 artifact typed-ID width, u16 branch-path segment width, branch-path length, renderer-valid branch-path segment encoding, non-entry spawn parent evidence, closed runtime enum value domains, process lifecycle causality boundaries after terminal stop/fail events, and artifact process-ID bounds. Lifecycle causality validation requires active parent/sender/supervisor PIDs for events that imply runtime action. Supervisor restart validation also requires prior child-start evidence for the same typed supervisor/child slot, a terminal event for the current child PID, and a distinct active replacement PID spawned by the supervisor for restarted decisions. It also rejects impossible restart-window evidence such as zero limits/windows, observed counts above the configured limit, restarted decisions with zero count, and non-restarted decisions with nonzero count, while still allowing typed evidence to reference the terminated child when reporting a supervisor decision. Validators apply explicit byte, event, and runtime-process limits, remain read-only, and never turn labels, source names, process names, message labels, or debug strings into executable meaning.

mantle inspect-authority is a read-only inspection command for admitted artifacts. It validates the .mta through the same artifact reader used before execution, then prints the typed authority and spawn-site tables. It does not dispatch by source names, execute runtime actions, or generate a mandatory report; JSON output is available only when explicitly requested by the caller. The source-side composition report is emitted by strata composition-report. The durable checked-subset source-side component-composition artifact is emitted by strata composition build and validated by strata composition admit. Both are separate from mantle inspect-authority, canonical deployment-composition artifacts, and .mta admission.

Target binding inspection is split along the same boundary:

• strata target-requirements <path.str> checks and lowers the source, then renders the typed requirements Strata would place in the .mta.
• mantle feature-declaration renders the current Mantle runtime feature declaration.
• mantle admit <path.mta> decodes and validates the .mta, compares typed target requirements against the Mantle declaration, and returns before executing runtime behavior.

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

flowchart LR
    Source["source text"]
    Lexer["lexer"]
    Parser["parser"]
    Ast["AST"]
    Checker["semantic checker"]
    Checked["checked IR"]
    Lowering["lowering"]
    Artifact["Mantle Target Artifact"]

    Source --> Lexer --> Parser --> Ast --> Checker --> Checked --> Lowering --> 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

flowchart LR
    Artifact["artifact text"]
    Decode["decode"]
    Validate["validate"]
    Load["load typed runtime tables"]
    Plan["build executable plan"]
    Spawn["spawn Main"]
    Deliver["deliver entry message"]
    Dispatch["dispatch by message ID"]
    Execute["execute typed actions"]
    Host["explicit runtime host"]
    Trace["JSONL trace sink"]
    Output["program output sink"]

    Artifact --> Decode --> Validate --> Load --> Plan --> Spawn --> Deliver --> Dispatch --> Execute --> Host
    Host --> Trace
    Host --> Output

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. The executable plan is an internal Mantle structure built from the admitted LoadedProgram; it pre-resolves typed dispatch, action, and executable value template references but is not serialized bytecode and is not emitted by Strata lowering. Strata still emits typed .mta value templates at the boundary; Mantle owns only the internal executable template program derived from admitted artifact data. Runtime execution emits events, program output, monotonic time queries, and final flushes through an explicit RuntimeHost; the CLI is a filesystem/stdout host adapter over that admitted core, while in-memory callers use the same runtime path with in-memory sinks.

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;
• host-mediated runtime events, output, clocks, and 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.

flowchart LR
    subgraph Strata["Strata frontend"]
        Syntax["source syntax"]
        Check["semantic checking"]
        Ir["checked IR"]
    end

    subgraph Lower["Lowering boundary"]
        Map["typed ID mapping"]
        Mta["Mantle Target Artifact"]
    end

    subgraph Mantle["Mantle runtime"]
        Admit["artifact admission"]
        Tables["loaded typed tables"]
        Plan["internal executable plan"]
        Exec["runtime execution"]
        Obs["observability"]
    end

    Syntax --> Check --> Ir --> Map --> Mta --> Admit --> Tables --> Plan --> Exec --> Obs

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/init_return_match.str;
• examples/function_match.str;
• examples/function_payload_match.str;
• examples/function_if_else.str;
• examples/function_collection_match.str;
• examples/function_return_match.str;
• examples/process_return_match.str;
• examples/process_return_match_arm_prefix.str;
• examples/process_return_match_arm_runtime_if_prefix.str;
• examples/process_return_match_arm_for_prefix.str;
• examples/process_return_match_arm_for_if_prefix.str;
• examples/process_return_match_arm_if_for_prefix.str;
• examples/function_record_pattern.str;
• examples/function_record_return_match.str;
• examples/function_record_body_match.str;
• examples/state_payload_enum.str;
• examples/collection_state.str;
• examples/state_payload_match.str;
• examples/actor_instances.str;
• examples/actor_payloads.str;
• examples/runtime_if_else.str;
• examples/runtime_payload_projection_if.str;
• examples/runtime_payload_projection_next_state.str;
• examples/runtime_state_payload_projection_if.str;
• examples/runtime_state_payload_projection_next_state.str;
• examples/runtime_nested_if_actions.str;
• examples/runtime_final_if_guarded_loop.str;
• examples/runtime_final_if_nested_if_actions.str;
• examples/runtime_final_if_nested_terminal_if.str;
• examples/runtime_guard_noop.str;
• examples/runtime_for_each.str;
• examples/runtime_for_each_empty.str;
• examples/runtime_for_each_if.str;
• examples/runtime_for_each_nested_if_actions.str;
• examples/runtime_guarded_for_each.str;
• examples/runtime_guarded_ref_loop.str;
• examples/runtime_guarded_ref_loop_jobs.str;
• examples/runtime_loop_element_projection.str;
• examples/actor_payload_match.str;
• examples/actor_payload_split_match.str;
• examples/actor_payload_split_signature.str;
• examples/actor_payload_split_signature_wildcard.str;
• examples/actor_payload_state_match_split.str;
• examples/actor_payload_state_match_wildcard.str;
• examples/nested_patterns.str;
• examples/actor_reply.str;
• examples/actor_emit_spawn_send.str;
• examples/effect_outcome_spawn_denied.str;
• examples/actor_panic_no_replay.str.

The integration tests rooted at crates/strata-mantle-acceptance/tests/source_to_runtime_gates.rs, with focused gate families under crates/strata-mantle-acceptance/tests/source_to_runtime_gates/, mirror the same source check, artifact build, and runtime execution sequence:

just run-example hello

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.

The quality bundle includes just cfg-check, which typechecks the workspace for representative Linux, macOS, and Windows Rust targets through the repository recipe. This keeps platform-specific and test-only #[cfg] paths covered by real compiler evidence without changing source visibility or suppressing rust-analyzer’s weak inactive-code hints. If a target is missing locally, install the reported target with rustup target add --toolchain stable .... Windows cfg-check coverage includes the Windows source-loading, artifact IO, and trace path implementations that use reparse-point rejection and stable opened-file metadata checks.

Runtime host/sink boundary changes must prove both the in-memory host and the CLI filesystem/stdout host adapter. Focused coverage should include trace sink, program-output sink, trace-first program-output audit evidence, and flush failure paths, plus a CLI assertion that mandatory host failures return before any successful run report is printed.

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

The success gates include the typed target-binding path for the component composition example: strata target-requirements, mantle feature-declaration, mantle admit, and mantle run. That path proves requirement extraction, mantle.feature_declaration.v6 rendering, requirements-vs-declaration admission before runtime execution, and Mantle’s artifact-derived check that declared requirements cover the decoded runtime feature surface. just remote-distributed-boundary-gates is part of the broader source-to-runtime gate and keeps the local-only runtime target profile explicit: checked Strata entry examples must not lower remote/distributed target requirements, and forged artifacts requiring remote send, remote spawn, or distributed transport must fail before runtime admission. They also include authority/effect admission-binding paths for dynamic local spawn authority in examples/effect_outcome_spawn_denied.str and lexical supervisor-child spawning in examples/local_supervision_restart.str: strata authority-effects build, strata authority-effects admit, strata authority-effects policy build, strata authority-effects policy admit, strata authority-effects bind-runtime, and mantle run --authority-effect-binding. Those paths prove checked authority/effect facts and closed typed policy decisions are emitted as separate Strata-owned artifacts, admitted before binding, correlated with the matching .mta, and consumed by Mantle as typed runtime policy/observability input rather than source labels or report text. Trace-reading acceptance gates also validate the Mantle-owned JSONL trace schema before using trace evidence. That validation is limited to observability metadata, exact per-event field sets, required field shapes, grouped payload/loop fields, artifact_loaded first/no-repeat ordering, Mantle-contiguous spawned PID sequencing, u32 artifact typed-ID width, u16 branch path segments and bounded path length, non-entry spawn parent evidence, runtime PID-to-process-ID correlation, supervisor-child restart causality, and restart-window numeric bounds/coupling; executable behavior still comes from checked IR, admitted .mta tables, and Mantle runtime dispatch.

Language Surface Proof Substrate

just language-surface-assurance runs the executable current-language-surface proof substrate. The inventory maps agreed proof domains to declared Strata/Mantle features, maps those features to typed proof obligations, maps those obligations to required evidence classes, and verifies that each evidence pointer still names live repository content. Source-to-runtime evidence must name active executable check/build/run gate coverage. This gate does not add language behavior and does not replace .str source-to-runtime execution.

just language-surface-assurance

Bounded Assurance

just bounded-assurance-smoke runs the focused bounded assurance surface for the current bounded language surfaces. It covers immutable source-local binding chains, bounded scalar expression trees, binding-expanded scalar equivalents, scalar values in records, lists, and maps, and pure source value/return if selection. It also covers selected step return match action blocks. The gate compares checked IR shapes with lowered Mantle artifact shapes, validates the artifact boundary, verifies typed send IDs, checks terminal Continue / Stop / Panic lowering, runs an explicit smaller bounded runtime execution generator through Mantle, and runs bypass-mutation rejection tests for malformed artifact equivalents.

This is machine-checked bounded exhaustiveness for the named surface. It is not a theorem-prover proof of the whole language surface.

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, native and cross-target checks, tests, clippy, performance smoke checks, build, tool metadata validation, toolchain policy validation, mdBook, the language surface proof substrate, source-to-runtime gates, and diff hygiene. The docs tool install path pins both mdbook and the Mermaid preprocessor, so Mermaid diagrams are built by the same just docs command locally, in quality CI, and in the Pages workflow.

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

Focused Component-Composition Artifact Gate

Run the focused Strata-owned composition artifact gate when changing checked composition artifact generation or admission:

just composition-artifact-gates

It checks and builds examples/component_composition_main.str, writes the default target/strata/component_composition_main.component-composition.json checked-subset validation artifact, validates it with strata composition admit --format json, binds that admitted evidence to the matching .mta through strata composition bind-runtime, and runs Mantle with the resulting target/strata/component_composition_main.deployment-composition.json. This proves the explicit Strata/deployment-to-Mantle observability bridge while still keeping .component-composition.json out of Mantle runtime input.

Focused Authority/Effect Artifact Gate

Run the focused authority/effect artifact gate when changing checked authority/effect rendering, admission, runtime binding, or Mantle authority policy admission:

just authority-effect-artifact-gates

It checks and builds examples/effect_outcome_spawn_denied.str, writes the default target/strata/effect_outcome_spawn_denied.authority-effect.json checked authority/effect artifact, validates it with strata authority-effects admit --format json, builds and admits target/strata/effect_outcome_spawn_denied.authority-policy.json, binds the admitted facts and typed policy decisions to the matching .mta, and runs Mantle with the accepted-policy target/strata/effect_outcome_spawn_denied.authority-effect-binding.json. It then builds an explicit deny-spawn target/strata/effect_outcome_spawn_denied.authority-deny-policy.json, admits it, binds it, and runs Mantle with target/strata/effect_outcome_spawn_denied.authority-effect-deny-binding.json. Next, it repeats the build/admit/bind/run chain for examples/local_supervision_restart.str so lexical supervisor-child facts are proven through the same explicit runtime binding bridge. Finally, it checks and builds examples/component_composition_main.str, emits and admits both the component-composition, authority/effect, and authority-policy artifacts, binds both runtime sidecars, and runs Mantle with both explicit bindings. This proves the explicit Strata-to-Mantle authority/effect bridge across dynamic-local authority, lexical supervisor-child facts, and component/port authority surfaces while keeping source labels, debug names, report text, and the Strata-owned .authority-effect.json artifact non-executable inside Mantle.

Performance Smoke

just performance-smoke runs stable source-to-runtime resource smoke profiles over examples/collection_state.str, the multi-file source-unit import example, the typed boundary-contract example, the checked component-composition example, and the local supervision restart example. It measures repeated Strata checking and lowering for collection state, source-unit imports, boundary contracts, and component composition; repeated checked composition report rendering, Strata-owned composition artifact build/rendering, Strata-owned composition artifact admission/validation, target requirement rendering from a prechecked composition input, and repeated Mantle runs with an explicit runtime composition binding; authority/effect artifact build/rendering, authority/effect artifact admission, authority-policy artifact build/rendering and admission, authority/effect runtime-binding admission for the denied-spawn and component authority-surface examples, and repeated Mantle runs with the explicit authority/effect binding for the denied-spawn example; Mantle admission comparison through the runtime profiles; Mantle artifact encode/decode; repeated Mantle in-memory execution of the collection-state and boundary-contract artifacts; repeated Mantle JSONL-trace execution of the collection-state artifact; and repeated Mantle in-memory execution of the supervision artifact. The Mantle runtime profiles exercise artifact admission, loaded-program validation, internal executable-plan construction, typed dispatch, and host execution together; they do not benchmark a serialized bytecode path.

The smoke output reports wall time, allocation/deallocation counts, allocated and deallocated bytes, interval-relative live-byte metrics, process CPU time when the platform exposes it, and resident memory. Allocation metrics come from a test-only global allocator wrapper around std::alloc::System; the wrapper does not change allocation policy and only records atomic counters. The live metrics are relative to the start of each measured profile: net live-byte delta is the signed end-of-interval live byte change, and peak live over interval start is the highest live byte count above that start baseline. The net live-byte delta budget is an upper bound; negative deltas remain valid. Linux CI reports process CPU from /proc/self/stat and current/peak RSS through /proc; macOS and BSD local runs report current RSS through ps. RSS budgets are enforced against current RSS for each measured profile; process-lifetime peak RSS is reported as context when available. Unlike allocation metrics, ordinary smoke RSS is whole-test-process resident memory, so use it as a budget signal rather than per-profile attribution.

The gate uses enforced resource ceilings with CI headroom for scheduler noise. It is meant to catch meaningful regressions in compilation, runtime, CPU, or memory paths without treating every small local timing fluctuation as a failure.

Reviewed reference values and enforced budget ceilings live in benchmarks/performance-smoke.baseline. Local and CI runs print current measurements to their logs; git tracks reviewed baseline changes, not every noisy raw run. The baseline file uses strict key=value entries with nanosecond, KiB, byte, and count units.

For RSS attribution, use the fresh-process comparison harness instead of the ordinary smoke run. just performance-rss-compare <base-worktree> <current-worktree> installs a temporary probe test into both worktrees, runs one named profile per test process, repeats each profile, and reports median, minimum, maximum, and p90 current-RSS deltas in KiB. This keeps profile-order, test-binary, and allocator-retained-page effects separate from the ordinary multi-profile smoke gate.

The default RSS comparison profiles cover collection-state checking/lowering, collection-state in-memory runtime execution, and boundary-contract in-memory runtime execution. To attribute local-supervision RSS, pass local_supervision_restart.in_memory_runtime explicitly after the two worktrees; both worktrees must contain examples/local_supervision_restart.str.

For review-grade memory evidence, use just performance-memory-review <base-worktree> <current-worktree>. It runs both the fresh-process test-profile RSS comparison and the product CLI footprint comparison. Treat allocator metrics as the strict code-path signal. Treat RSS as a repeated median/p90 comparison signal because operating systems and allocators can keep freed pages resident outside the measured source path.

For product-footprint attribution, use just performance-cli-footprint-compare <base-worktree> <current-worktree>. It builds the release Strata and Mantle CLI binaries in both worktrees, compares release binary file sizes, then repeats fresh-process product commands for strata check, strata build, and mantle run over examples/collection_state.str under a minimal environment. The reported CLI RSS values come from the operating system process for each command; they are closer to product footprint than test-harness RSS, but they still are not per-Mantle-actor memory. The harness also writes metadata with the compared worktrees, HEADs, platform, run count, and clean-environment policy.

For Linux /proc-based memory evidence from a macOS checkout, run the same review through local act with two mounted worktrees:

just performance-memory-review-act /tmp/strata-base .

The act recipe uses the performance-memory workflow and mounts the base and current worktrees into an Ubuntu container. It is an optional review tool, not a replacement for just quality. The same workflow can also be started manually in GitHub with a base ref when local worktree mounts are not available.

Useful local command:

just performance-smoke

Useful RSS comparison command:

just performance-rss-compare /tmp/strata-base .

Useful product CLI footprint command:

just performance-cli-footprint-compare /tmp/strata-base .

Useful full memory review command:

just performance-memory-review /tmp/strata-base .

Fuzzing

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

• parsing, checking, and lowering arbitrary UTF-8 source;
• parsing, checking, and lowering delimited multi-source Strata source programs;
• admitting Strata-owned checked component-composition artifacts;
• admitting Strata-owned checked authority/effect artifacts;
• decoding and re-encoding arbitrary UTF-8 artifact text;
• running valid lowered artifacts through the in-memory runtime host;
• admitting Mantle runtime composition bindings;
• admitting Mantle runtime authority/effect bindings;
• validating Mantle-owned runtime trace JSONL without trusting trace strings as executable meaning.

Committed seed corpora under fuzz/seeds/ keep the smoke runs exercising valid collection, template, and source-to-runtime examples even before mutation finds those forms from random input. The smoke recipe copies those seeds into ignored fuzz/corpus/ directories before running cargo-fuzz, so mutation output does not touch tracked seed fixtures.

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. It includes targeted immutable source-local binding check/lower coverage for the source resolution path, composition_artifact coverage for the pure component-composition artifact renderer/admission validator, representative authority/effect artifact render/admit and closest component-import negative coverage, and focused Mantle runtime composition- and authority/effect-binding admission checks, including component authority-surface and negative forged-field authority/effect-binding checks. Filesystem-specific CLI behavior remains covered by unit and acceptance tests instead.

Useful local commands:

just install-miri-tools
just miri-ci

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