State Machines

Wire formats alone are not enough to implement a protocol correctly. A parser can decode every individual packet perfectly and still allow illegal sequences — sending data on a closed connection, retransmitting after a handshake that never completed, or abandoning a path that was never active. wirespec makes state machines a first-class language primitive: they are declared in the same .wspec file as the wire formats they describe, compiled to verifiable C dispatch code, and subject to the same type-checking rules as the rest of the language.

Basic Structure

A state machine begins with state machine Name { ... }. Inside, you declare states, the initial state, and transitions.

state machine PathState {
    state Init       { path_id: VarInt }
    state Validating { path_id: VarInt, challenge: bytes[8] }
    state Active     { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
    state Standby    { path_id: VarInt }
    state Closing    { path_id: VarInt, error_code: VarInt }
    state Closed [terminal]

    initial Init
    ...
}

Each state carries associated data declared as typed fields in braces. Fields may have default values (rtt: u64 = 0). States with no associated data need no braces (state Idle).

The [terminal] marker means the state machine cannot leave that state. Sending an event to a terminal state (other than a wildcard transition defined to absorb it) returns WIRESPEC_ERR_INVALID_STATE.

initial Name designates which state the machine starts in.

Transitions

A transition moves the machine from one state to another in response to an event.

transition Validating -> Active {
    on recv_path_response(r: bytes[8])
    guard r == src.challenge
    action { dst.path_id = src.path_id; }
}

The three optional clauses inside a transition are:

Clause	Role
on event(params)	The event that triggers this transition (required)
guard expr	Boolean condition; transition is skipped if false (optional)
action { ... }	Assignments that initialize the destination state (optional)

src and dst

• src holds the current state's data — read-only
• dst holds the next state's data — write-only
• guard may only read src
• action reads src, writes dst

Assignments inside action are separated by semicolons:

action {
    dst.path_id = src.path_id;
    dst.error_code = code;
}

A trailing semicolon after the last assignment is allowed but not required.

Complete Initialization

The compiler enforces that every dst field without a default value is assigned somewhere in the action block. Leaving a field unassigned is a compile error — there is no zero-initialization or implicit copying.

transition Active -> Closing {
    on send_path_abandon(code: VarInt)
    action {
        dst.path_id = src.path_id;    # required: Closing has path_id (no default)
        dst.error_code = code;         # required: Closing has error_code (no default)
    }
}

Fields that have defaults (rtt: u64 = 0) do not need to be assigned; they receive their default value automatically if omitted.

Wildcard Transitions

transition * -> State matches from any source state. This is how you express "this event always terminates the connection regardless of where we are":

transition * -> Closed { on connection_closed }

Concrete transitions always take priority over wildcard transitions. If both a concrete A -> B { on ev } and * -> Closed { on ev } are defined, and the machine is in state A, the concrete one wins.

State Constructors

When you need to create a state value as a literal — for example, when initializing an array element — use the state constructor syntax:

PathState::Active(path_id, 0, 0)

Arguments are positional, in the order fields are declared. Fields with defaults may be omitted from the right end:

# Active has: path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0
PathState::Active(pid)          # equivalent to PathState::Active(pid, 0, 0)
PathState::Active(pid, 10)      # equivalent to PathState::Active(pid, 10, 0)

Terminal states with no fields require no parentheses:

PathState::Closed               # not PathState::Closed()

fill() for Arrays

State fields can be arrays of other state machines. To initialize every element of an array to the same value, use the built-in fill() expression:

dst.paths = fill(PathState::Closed, 4)   # set all 4 slots to Closed

fill(value, count) is a built-in — it is not a function call and cannot be passed as a value.

Array Subscript and +=

Individual array elements can be read and assigned:

action {
    dst.paths = src.paths;
    dst.paths[src.active_path_count] = PathState::Init(path_id);
    dst.active_path_count = src.active_path_count + 1;
}

The += shorthand is available for incrementing counters:

action {
    dst.paths = src.paths;
    dst.paths[src.active_path_count] = PathState::Init(path_id);
    dst.active_path_count += 1;
}

Putting It Together: PathState

Here is the complete PathState machine from examples/mpquic/path.wspec:

module mpquic.path

import quic.varint.VarInt

state machine PathState {
    state Init       { path_id: VarInt }
    state Validating { path_id: VarInt, challenge: bytes[8] }
    state Active     { path_id: VarInt, rtt: u64 = 0, cwnd: u64 = 0 }
    state Standby    { path_id: VarInt }
    state Closing    { path_id: VarInt, error_code: VarInt }
    state Closed [terminal]

    initial Init

    transition Init -> Validating {
        on send_path_challenge(c: bytes[8])
        action { dst.path_id = src.path_id; dst.challenge = c; }
    }
    transition Validating -> Active {
        on recv_path_response(r: bytes[8])
        guard r == src.challenge
        action { dst.path_id = src.path_id; }
    }
    transition Validating -> Closed { on validation_timeout }
    transition Active -> Standby {
        on recv_path_standby
        action { dst.path_id = src.path_id; }
    }
    transition Standby -> Active {
        on recv_path_available
        action { dst.path_id = src.path_id; }
    }
    transition Active -> Closing {
        on send_path_abandon(code: VarInt)
        action { dst.path_id = src.path_id; dst.error_code = code; }
    }
    transition Standby -> Closing {
        on send_path_abandon(code: VarInt)
        action { dst.path_id = src.path_id; dst.error_code = code; }
    }
    transition Closing -> Closed { on closing_complete }
    transition * -> Closed { on connection_closed }
}

The Active <-> Standby transitions demonstrate that the same event names can appear on multiple transitions from different source states. The * -> Closed at the bottom ensures connection_closed terminates the path cleanly from any state.

delegate for Hierarchical State Machines

A state machine can hold another state machine as a field. The parent forwards events to the child using delegate:

module mpquic.connection

state machine ChildProcess {
    state Running { value: u8 }
    state Stopped [terminal]
    initial Running
    transition Running -> Stopped { on halt }
    transition * -> Stopped { on force_stop }
}

state machine SimpleDelegateExample {
    state Active { child: ChildProcess, data: u64 }
    state Closed [terminal]

    initial Active

    transition Active -> Active {
        on child_event(ev: u8)
        delegate src.child <- ev
    }

    transition Active -> Closed { on disconnect }
    transition * -> Closed { on error }
}

The delegate src.child <- ev clause in SimpleDelegateExample forwards the ev event to src.child (the ChildProcess sub-machine).

Rules for delegate:

• Only valid on self-transitions (the source and destination state must be the same, here Active -> Active)
• A transition with delegate cannot also have an explicit action block
• The target of delegate must be a field whose type is another state machine

Automatic dst initialization

When a transition uses delegate, the compiler automatically copies src into dst before forwarding the event to the child. You do not need to write dst.data = src.data yourself. The child update then happens in-place on the already-copied dst.

child_state_changed

After a delegate transition forwards an event and the child's state actually changes, the runtime fires an internal event called child_state_changed back at the parent. The parent can define a transition to react:

transition Connected -> Draining {
    on child_state_changed
    guard all(src.paths[0..src.active_path_count], in_state(Closed))
}

child_state_changed is the one event that is silently discarded when no matching transition (or no matching guard) exists. Every other unhandled event returns WIRESPEC_ERR_INVALID_STATE. This makes child_state_changed safe to fire frequently — the parent only reacts when it has something meaningful to do.

child_state_changed is a reserved identifier; you cannot define a user event with that name.

all() Quantifier and in_state()

all(collection, predicate) checks that every element of a collection satisfies a predicate:

guard all(src.paths[0..src.active_path_count], in_state(Closed))

• The collection is a slice expression (see below)
• The predicate must be in_state(StateName) — this is the only supported predicate form in v1.0
• all() is a built-in special form, not a general higher-order function

in_state(S) checks that an element is currently in state S. It is only meaningful when applied to a field or array element whose type is a state machine.

Slice Expressions

A slice collection[start..end] selects elements from index start up to (but not including) index end — a half-open range, matching Rust's .. convention:

src.paths[0..src.active_path_count]   # first active_path_count elements
src.paths[1..4]                        # elements at indices 1, 2, 3

Slices appear in:

• all(slice, predicate) — check a subset of an array
• exists i in 0..N: ... — iterate over a range of indices (in verify properties)

verify Declarations

State machines may include verify declarations:

verify NoDeadlock
verify AllReachClosed
verify property AbandonIsFinal:
    in_state(Closing) -> [] not in_state(Active)

verify NoDeadlock and verify AllReachClosed are named built-in properties that the compiler knows how to check. verify property Name: formula attaches a named temporal-logic property using the same expression language as guards, extended with temporal operators ([] always, <> eventually, ~> leads-to).

TLA+ generation not yet implemented

verify declarations are parsed and type-checked in the current release. The TLA+ model generation that exercises these properties is planned for Phase 3. Defining them now has no runtime effect but makes the intent explicit and will be automatically picked up when the TLA+ backend ships.

Generated C

The compiler generates a double-switch dispatch function for each state machine. Given a machine named FooState:

wirespec_result_t foo_state_dispatch(
    foo_state_t *sm,
    foo_state_event_t event,
    const void *event_data);

The generated body looks like:

switch (sm->tag) {
    case FOO_STATE_ACTIVE:
        switch (event) {
            case FOO_STATE_EVENT_TIMEOUT:
                /* evaluate guard, then action */
                ...
                return WIRESPEC_OK;
            default:
                return WIRESPEC_ERR_INVALID_STATE;
        }
    case FOO_STATE_CLOSED:
        return WIRESPEC_ERR_INVALID_STATE;   /* terminal */
    ...
}

The outer switch selects the current state; the inner switch dispatches the event. The compiler statically verifies that all non-wildcard transitions are covered and that no (state, event) pair has two conflicting concrete transitions.

State data is represented as a tagged union:

typedef struct {
    foo_state_tag_t tag;
    union {
        foo_state_active_t active;
        foo_state_validating_t validating;
        /* ... */
    } data;
} foo_state_t;

Next Steps

• Modules & Imports — Split your protocol definitions across multiple .wspec files
• Language Tour — Wire format primitives, frames, capsules, and expressions
• C API Reference — Full reference for the generated parse/serialize/dispatch functions