Checked state machines

A MACHINE defines pure functions over explicit instance and event data. Use it for payment lifecycles, approval policies, connection protocols and other finite sets of guarded transitions. Calling STEP proposes a next instance; ordinary formulas, reducers and rules decide what to retain.

CHOICE OrderEvent = Pay | Ship

order = MACHINE
  STATE pending, paid, shipped
  EVENT OrderEvent
  INITIAL pending
  FINAL shipped
  MATCH UNIQUE
  UNHANDLED ERROR

  TRANSITION payment: pending ON OrderEvent.Pay() -> paid
  TRANSITION dispatch: paid ON OrderEvent.Ship() -> shipped
END

initial = order.INITIAL()
attempt = order.STEP(initial, OrderEvent.Pay())
report = order.REPORT(initial, OrderEvent.Pay())

MACHINE order ... END is the equivalent declaration spelling. The definition binds INITIAL, STEP, REPORT, CHECK, RESTORE, REPLAY and TRACE. It creates no instance, actor, worker, timer or event subscription. These members use the existing compiled execution path and can be imported, aliased, or passed as ordinary callables. Local declarations also work in DO blocks, including named function bodies.

Context, events and transitions

EVENT names an algebraic CHOICE; nullary constructors use parentheses in patterns and values. Payload fields use ordinary types. Concrete generic CHOICE applications use the existing nominal type system. CONTEXT declares a closed record of fields; omitting it gives an empty context and a zero-argument INITIAL. EMITS optionally names the CHOICE family of emitted values.

CHOICE PaymentEvent = Pay(amount: number) | Cancel(reason: string)
CHOICE PaymentNotice = Recorded(amount: number) | Cancelled(reason: string)

payment = MACHINE
  STATE pending, paid, cancelled
  EVENT PaymentEvent
  CONTEXT {total: number, received: number}
  EMITS PaymentNotice
  INITIAL pending
  FINAL paid, cancelled
  MATCH UNIQUE
  UNHANDLED ERROR
  INVARIANT positive_total: context.total > 0
  INVARIANT valid_received: context.received >= 0 AND context.received <= context.total

  TRANSITION partial: pending ON PaymentEvent.Pay(amount)
    WHEN amount > 0 AND context.received + amount < context.total -> pending
    WITH {received: context.received + amount}
    EMIT PaymentNotice.Recorded(amount)

  TRANSITION settle: pending ON PaymentEvent.Pay(amount)
    WHEN amount > 0 AND context.received + amount = context.total -> paid
    WITH {received: context.received + amount}
    EMIT PaymentNotice.Recorded(amount)

  TRANSITION cancel: pending ON PaymentEvent.Cancel(reason) -> cancelled
    EMIT PaymentNotice.Cancelled(reason)
END

initial = payment.INITIAL({total: 120, received: 0})
attempt = payment.STEP(initial, PaymentEvent.Pay(40))

Declarations precede transitions. State names and transition/invariant labels must be unique within their respective namespaces, ignoring case. Every source, target, INITIAL and FINAL name must exist. A transition cannot leave a FINAL state. Structurally unreachable states produce an advisory diagnostic; guards are not treated as proof of reachability. * as a source matches every non-final state; _ as the event pattern matches every admitted event. Constructor payload patterns bind names or discard fields with _.

Guards and patches see context, state, event, and their pattern bindings. Emission expressions additionally see next_context and next_state. Invariants see only context and state. Pattern bindings cannot shadow these contextual names. Varying data belongs in context or the event. Referenced constants and helpers must be immutable, deterministic, pure and acyclic; a local declaration cannot capture changing enclosing function arguments into its definition.

WITH is a literal field patch. Every right-hand side reads the old context, so {a: context.b, b: context.a} exchanges two values atomically. Unmentioned fields retain their values. Arbitrary nested expressions, including DO, use their ordinary expression grammar.

Evaluation order and failure

Every STEP follows this order:

1. Validate the instance identity, state, complete context and event payload.
2. Check incoming invariants.
3. Evaluate eligible guards in authored order. FIRST stops at its first true guard. UNIQUE evaluates all eligible guards, then rejects multiple matches.
4. Evaluate the selected patch against the old context and validate its fields.
5. Check invariants against the proposed state and context.
6. Evaluate emissions in clause order, then return the complete Step.

A guard or invariant must return a boolean. An absent guard is true. A false guard is a non-match; an error is a rejection. No update or emission runs before UNIQUE ambiguity has been resolved. A failed update, invariant or emission returns no proposed next instance and no successful emission prefix.

UNHANDLED ERROR rejects an event with no matching transition. UNHANDLED IGNORE returns the unchanged instance and an empty emitted List. This policy also applies in final states. Invalid input and failed incoming invariants are rejected under both policies. A successful self-loop is a transition, even when the context is unchanged.

EMIT value contributes one correctly typed value. EMIT EACH values requires a native List, for example VECTOR(Notice.Recorded(1), Notice.Recorded(2)). Arrays, wrong families, invalid payloads and oversized lists are refused. Emissions are data; delivery remains an explicit operation of their consumer.

Values and reports

Operation	Value
m.INITIAL(context)	Validated {definition, state, context} or a Grid error
m.INITIAL() without CONTEXT	The same instance shape with an empty context
m.STEP(instance, event)	Native Result<Step, MachineError>
m.REPORT(instance, event)	A report containing the same Result and its trace
m.CHECK(value)	Result<Instance, MachineError> without taking an event
m.RESTORE(state, context)	Checked reconstruction for the current definition
m.REPLAY(instance, events, policy)	Result<Replay, MachineError> with progress and ordered emissions
m.TRACE(instance, events, policy)	The same replay result, also retaining step reports

Known argument shapes and types are checked during compilation, including extra context fields. Dynamic inputs are checked again when the operation runs. These checks remain active in both loose and strict models.

A Step contains next, status and a native List emitted. Status is :transitioned or :ignored. A MachineError contains text code and message, a symbol phase, Option-valued transition and invariant labels, and a bounded Option-valued cause retaining an underlying error's code and message.

REPORT has schema grid.machine.report.v1, definition, symbol status, outcome, evaluated_transitions, matched_transitions, Option-valued selected_transition, and boolean matching_complete. It performs one step attempt. The evaluated list contains only structurally eligible guards actually visited. A guard error leaves matching incomplete and no transition selected. STEP does not construct these report lists.

Use ordinary native-result matching to choose a rejection policy:

next = MATCH(attempt,
  OK(step) -> step.next,
  ERR(problem) -> initial
)

Checking, restoring and migrating an instance

m.CHECK(value) returns OK(instance) or ERR(MachineError) without taking an event. It checks bounded data, exact instance shape, definition identity, declared state, complete context types and incoming invariants. Its input accepts unknown data, so it is also useful at a deserialization boundary. Empty replay applies the same checks.

m.RESTORE(state, context) constructs an instance for this definition and runs the same validation. Without a CONTEXT declaration, use m.RESTORE(state). Declared final and structurally unreachable states can be restored. Unknown states and invalid context are refused.

Restoration makes migration explicit:

admitted = current.CHECK(saved)
migrated = current.RESTORE(saved.state, {
  total: saved.context.total,
  received: saved.context.paid
})

CHECK never accepts an old definition identity automatically. RESTORE deliberately adopts the current definition after the caller chooses the new state and context. Neither operation loads storage, commits state or emits notices.

Bounded replay and trace

Use m.REPLAY(instance, events, policy) to apply a native List of events, and m.TRACE(instance, events, policy) when the individual reports are useful. Both return a native Result and require an explicit :stop or :continue policy.

attempts = VECTOR(PaymentEvent.Pay(40), PaymentEvent.Pay(100), PaymentEvent.Pay(80))
replay = payment.REPLAY(initial, attempts, :continue)
trace = payment.TRACE(initial, attempts, :stop)

A successful replay result contains:

Field	Meaning
next	Last successfully accepted instance
status	:stopped when :stop encounters a rejection, otherwise :complete
processed	Number of attempts, including rejected events
remaining	Number of events left unattempted
rejected	Number of rejected attempts
emitted	Accepted emissions in event order, then clause order
failures	Ordered {index, error} records; indexes start at one
reports	TRACE only: one REPORT for each attempted event

With :stop, a semantic rejection returns OK with status: :stopped, the accepted prefix and the failing attempt, even when that was the last event. With :continue, the instance remains unchanged for that attempt and subsequent events are processed. An ignored event counts as a successful attempt. A completed replay can therefore have failures; inspect rejected or failures when success of every event is required.

Invalid starting instances, invalid policies, malformed sequence data and budget exhaustion return top-level ERR. They never return a truncated prefix as a successful result. Event type errors follow the chosen rejection policy. Replay is pure: returning its final instance does not commit it or deliver emissions. Ordinary REDUCE and SCAN remain available for custom policies.

Replay accepts at most 4,096 events. Each STEP retains its existing limits. The complete retained prefix must fit the normal 1 MiB data budget, depth/work bounds and a 65,536-element bound on each accumulated List. TRACE retains reports as well as emissions, so it can exhaust the data budget earlier. The stopped suffix does not execute STEP or REPORT; bounded input validation still inspects the supplied sequence.

Conservative predicate diagnostics

Admission warns about proven FIRST shadowing, witnessed UNIQUE overlaps and uncovered non-final state/event cases. Incoming invariants constrain witnesses; wildcard and constructor-specific transitions retain their authored priority. Warnings do not change execution or make partial machines invalid.

Analysis shares the bounded predicate machinery used by Decisions. It recognizes boolean predicates, finite numeric comparisons and supported boolean composition. Equivalent supported predicates can also prove FIRST shadowing; payload-binding renames do not hide that equivalence. Unused context and payload fields do not expand the case space. Unsupported helper calls, complex data and numeric representations stay unknown. Unknown predicates participate conservatively in shadow proofs and cannot establish an overlap or coverage witness. Uninterpreted primitive fields can supply a type witness when the guard and invariants are proven independently of their values. Analysis never evaluates user code. It considers at most 4,096 cases per state/event combination and one million work units per definition, retains at most 16 notices, and reports analysis exhaustion. Absence of warnings is not a proof of total coverage or reachability.

State ownership and replacement

For local reactive ownership, a single STATE record can retain an instance and its latest report. This rule keeps the instance after rejection:

input incoming = PaymentEvent.Pay(40)
STATE current = {
  instance: payment.INITIAL({total: 120, received: 0}),
  last: NONE()
}

WHEN incoming THEN
  current = DO
    report = payment.REPORT(current.instance, incoming)
    next = MATCH(report.outcome,
      OK(step) -> step.next,
      ERR(problem) -> current.instance
    )
    {instance: next, last: SOME(report)}
  END
END

The ordinary rule owns the commit. Its latest report is not a durable event log. Finite replay uses REPLAY or TRACE with an explicit policy. Ordinary REDUCE and SCAN support custom accumulation and retention policies.

Instances carry a semantic definition identity computed during compilation. Formatting, comments and unrelated model edits do not change it; state/type contracts, policies, transition order and referenced helper semantics do. A different definition rejects an old instance with MACHINE_DEFINITION_MISMATCH. Reset or migrate explicitly. Equal identity never bypasses validation of restored data.

Hierarchy, parallel regions, implicit internal-event queues, timed durable instances and delivery guarantees are separate extensions. Ordinary workflow, transaction and scheduler owners remain responsible for those operations.

Bounds and implementation

A definition admits at most 256 states, 256 event constructors, 256 context fields, 256 invariants and 4,096 transitions. A transition admits at most 64 emission clauses; a successful step emits at most 1,024 elements. Selected data admission is bounded to 1 MiB, depth 64 and one million inspected nodes, with at most 4,096 compiled type nodes. Compilation also bounds candidate expansion to 262,144 entries and generated expressions to 262,144 nodes / 64 MiB. The complete Step and report each fit the data byte bound; oversized reports return MACHINE_REPORT_BUDGET. Existing expression and operation limits also apply. Exceeding a bound fails closed and never truncates a successful List.

The compiler builds state/event candidate lists and generates ordinary compiled callables, lexical bindings, records and Results. Machines and decisions share the ordered guard selector. Closed data contracts are static metadata operands; validation does not deserialize a definition, hash it at each step, or create a runtime registry. Type, invariant and identity checks are part of the selected operation's cost. Legacy CHOICE interfaces retain the ordinary compiler's gradual static representation; their complete event and payload contracts are still checked at the machine boundary. Concrete nominal CHOICE applications retain their static family types.

Canonical examples: payment, approval, and connection protocol.