Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Diagnostics

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

Reading A Diagnostic

Run:

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

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

Common Source Errors

Diagnostic ContainsLikely CauseFix
expected record, enum, function, or proc declarationA top-level item is not accepted.Use record, enum, fn, or proc after module.
entry process Main is not declaredThe program has no Main process.Add proc Main ....
uses reserved prefix __strata_checked_A source type name collides with internal checked type metadata.Rename the source type without the reserved prefix.
checked type_count exceeds Mantle artifact limitThe checked program needs more distinct artifact types than Mantle admits.Reduce the number of distinct state, message, payload, and process-reference types.
process ... must declare type StateA process is missing its state alias.Add type State = StateType;.
process ... must declare type MsgA process is missing its message alias.Add type Msg = MessageEnum;.
init must declare no parametersinit has parameters.Use fn init() -> StateType ....
init body must not perform statementsinit uses emit, spawn, or send.Return only the initial state.
step must declare state parameter and message patternstep has the wrong parameter count.Use state: StateType, MessageConstructor or state: StateType, _.
step second parameter must be a message constructor pattern or wildcard patternThe second step parameter is a typed binding instead of a message pattern.Replace msg: MsgType with a message constructor or _, or use a whole-body match msg.
step returns ..., expected ProcResult<...>step return type is wrong.Return ProcResult<StateType>.
step body must return Stop..., Continue..., or Panic...A step returns a bare state value or an unsupported result form.Return one whole state value inside Continue(...), Stop(...), or Panic(...).
step may-behaviors must be emptyThe ~ [...] list is not empty.Use ~ [].
step must be deterministicstep uses @nondet.Use @det.
uses effect ... but does not declare itThe body performs emit, spawn, or send without matching effect authority.Add the exact used effect to ! [...] or remove the statement.
declares effect ... but does not use itThe effect list is wider than the body.Remove the unused effect.
declares duplicate effectThe effect list repeats one authority.Keep each effect at most once.

Source Function Errors

Diagnostic ContainsLikely CauseFix
function ... conflicts with a declared type or value constructorA source function name collides with a type or enum constructor.Choose a distinct function name.
function ... must declare exactly one parameterA normal source function uses an arity outside the current buildable call form.Use one typed binding parameter or one pattern parameter clause.
function ... must use a declared record or enum typeA source function parameter or return type names something outside the source value type set.Use a declared record or enum type.
function ... must not declare effects / function ... must not perform statementsA normal source function tries to perform runtime behavior.Keep normal functions pure; perform emit, spawn, and send only in step.
function ... may-behaviors must be empty / function ... must be deterministicA normal source function is not in the deterministic buildable subset.Use ~ [] @det.
function ... is not declaredA value expression calls an unknown function.Declare a module function or process-local helper with that name.
function ... returns ..., expected ...The function return type does not match the value position where it is called.Call a function returning the expected type or change the annotation.
source function call cycle ... is not supportedSource helper calls are recursive, but helpers are expanded before lowering and have no recursion model.Remove the cycle; pass whole values through non-recursive helpers.
function ... declares duplicate pattern for variant ...More than one source function clause handles the same constructor.Keep one clause per constructor.
function ... must handle variant ...A source function signature pattern group or match body is non-exhaustive.Add the missing constructor clause/arm or one _ fallback.
function ... wildcard pattern is unreachableExplicit source function clauses already cover every variant.Remove the wildcard clause or remove the explicit clauses it should cover.
payload ... has type ..., expected ...A source helper or step payload binding annotation does not match the constructor payload type.Use the declared payload type.
match payload binding ... conflicts with an existing source value bindingA source helper match arm reuses the helper parameter name for a payload binding.Use a distinct immutable payload binding name.
value ... is not a variant of enum ...A payload-constructor expression names a constructor outside the expected enum.Use a constructor from the expected enum or call a declared helper.
enum variant ... requires a payload / does not accept a payloadA payload-bearing constructor was used as a fieldless value, or a fieldless constructor was called with a payload.Match the constructor’s declared payload shape.

Message Handling Errors

Diagnostic ContainsLikely CauseFix
step pattern message ... is not acceptedA step pattern names a message constructor outside the process message enum.Use a declared message constructor.
duplicate step pattern for messageA message variant has more than one explicit step clause.Keep one explicit clause per variant.
duplicate wildcard step patternMore than one step clause uses _.Keep one wildcard clause.
wildcard step pattern is unreachableExplicit clauses already cover every accepted message variant.Remove the wildcard clause or remove an explicit clause that it should cover.
must declare step pattern for messageA message variant is not covered by an explicit or wildcard step clause.Add a step clause for the missing message or add one _ clause.
match body must be the whole function bodyA match msg appears after another statement or has trailing body statements.Use one whole-body match msg form or step parameter patterns.
match step must declare a typed message parameterA match step uses a parameter pattern instead of msg: MsgType.Use fn step(state: StateType, msg: MsgType).
match scrutinee ... must be the step message parameterThe match scrutinee is not the typed message parameter.Match the declared message parameter, usually match msg.
state match step must use a match bodyA match state step was parsed in a non-match body shape.Make match state { ... } the whole step body.
state match pattern ... requires a payload bindingA payload-bearing state variant is matched without binding its payload.Write the arm as Variant(name: PayloadType).
state match pattern ... does not carry a payloadA fieldless state variant was matched with a payload binding.Remove the binding from the fieldless variant arm.
state match payload ... has type ..., expected ...A state payload binding annotation does not match the state variant payload type.Use the declared state variant payload type.
state payload binding ... conflicts with message payload bindingA match state arm reuses the enclosing message payload binding name.Give the state payload binding its own transition-local name.
message parameter ... has type ..., expected ...The typed message parameter is not the process Msg type.Use the process message type in the second parameter.
cannot mix match step bodies with step parameter patternsOne process mixes match msg dispatch with parameter-pattern or state-match dispatch.Use either parameter-pattern/state-match clauses or one match msg body for the process.
sends message ... not accepted by ...The target process message enum has no such variant.Send a declared target message variant.
message ... requires a payloadA send omits the payload for a payload variant.Pass one value with send worker Variant(value);.
message ... does not accept a payloadA send passes a payload to a unit variant.Remove the payload argument or send a payload variant.
payload type ... must be a named record, enum, or process reference typeA payload variant uses an unsupported applied/generic type.Declare a named record or enum type, or use ProcessRef<TargetProcess>.
step pattern payload ... has type ... expected ...A step payload binding annotation does not match the variant payload type.Use the declared payload type in the parameter pattern.
payload binding ... conflicts / process reference ... conflicts with payload bindingA local immutable binding shadows state, a process, a type, a value constructor, or another local binding in the same transition.Use distinct immutable binding names.
payload has type ..., expected ...A runtime envelope or artifact payload template carries the wrong value type.Match the payload value type to the target message variant.
payload ... exceeds maximum lengthA payload value label is too large for the artifact or runtime trace boundary.Use a smaller payload value or split the payload into smaller fields/messages.
payload ... is not a bound process referenceA ProcessRef<T> payload send uses a value that is not a process reference.Pass an immutable process reference binding or received ProcessRef<T> payload.
process references must be direct message payloads / process reference template must be a direct message payloadA process reference payload is nested inside a record, enum, or next-state template.Send ProcessRef<T> only as the direct payload of a message that declares ProcessRef<T>.

Match Errors

Diagnostic ContainsLikely CauseFix
match scrutinee ... is not a fieldless enum variantAn init match uses a scrutinee that is not a fieldless enum constructor in this source slice.Match a declared fieldless enum constructor.
match pattern ... is not a variant of enum ...A match arm names a constructor outside the scrutinee enum.Use a constructor from the matched enum.
init match must handle variantAn init match is non-exhaustive.Add an arm for the missing variant or one _ arm.
init match declares duplicate patternMore than one arm handles the same constructor.Keep one arm per constructor.
init match wildcard pattern is unreachableExplicit arms already cover the matched enum.Remove the wildcard arm or remove the explicit arms it should cover.
init match pattern ... does not carry a payloadA fieldless constructor pattern tries to bind a payload.Remove the binding.
init match arm cannot use payload binding ... in returned stateAn init match arm tries to materialize a payload binding even though init matches lower to a static initial state.Return a concrete whole state value from each init match arm.

State Errors

Diagnostic ContainsLikely CauseFix
value ... is not a variant of enum ...A returned enum value does not belong to the expected enum.Return a variant from the process state enum.
record constructor ... does not match expected record ...A record value constructor does not match the expected state type.Construct the expected record type.
record value fields use ':'A record value used assignment syntax.Use field: value, not field = value.
process reference payloads are not valid state values / process reference templates are not valid next-state valuesA state value or next-state template tries to embed runtime process authority.Keep process references in direct message payloads; process states must be immutable data values.
state value state conflictsA state enum variant is named state.Rename the variant.
current state payload template requires a payload-bearing stateAn artifact or checked transition uses a state-payload template without a payload-bearing current state guard.Ensure the transition is keyed by an admitted payload-bearing state value.
current_state id ... is not a valid state value / is not a loaded state valueAn artifact transition references a current state outside the admitted state table.Emit only admitted state IDs from lowering; reject or regenerate invalid artifacts.

Process And Mailbox Errors

Diagnostic ContainsLikely CauseFix
spawns itselfA process tries to spawn itself.Spawn another declared process.
conflicts with a process declarationA process reference uses the same name as a process definition.Use a distinct reference name.
undeclared process referenceA send references a name that is never spawned in the process.Add a matching let worker: ProcessRef<Worker> = spawn Worker; statement.
send target ... is not a process reference payloadA send target names a payload binding whose type is not ProcessRef<T>.Send through a process reference binding or a received ProcessRef<T> payload.
unbound process referenceA transition sends through a reference before it is bound.Spawn the reference before sending through it.
duplicates process reference idA transition binds the same reference twice.Use two distinct references or bind once.
mailbox would exceed boundA send would overflow the target mailbox.Increase the mailbox bound or send fewer messages before the target runs.
would retain ... unhandled messageA process can stop while messages remain in its mailbox.Continue until queued messages are handled or avoid queuing them.
mailbox_bound must be no greater thanThe mailbox bound exceeds the admitted limit.Lower the bound.

Runtime Errors

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

Use the source gate first:

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

Then run Mantle:

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

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