Module agent_state 

#2220: the agent state model lives in bynk-check, shared with the checker; re-exported here so existing paths keep working. #2195: the agent state model — each agent’s state machine, derived from its handlers (agent-state-views track, slice 1; retired-track summary in design/archive/retired-tracks.md, §3.1, §3.3, §3.7).

The language leaves an agent’s machine implicit: a store Cell of a user sum type (enum { … } or pipe form) is the machine, match/is read it and := moves it. This query recovers, for every such field, the edges the handlers can produce — (from-set, handler, guards, target, outcome, span) — and the set of states reachable from the initialiser.

A dataflow pass, not path enumeration (§3.3 step 1). Each handler body is walked over a set of abstract paths. A path carries the states it can have started in (the from-set), the field’s current value, the last write, its opaque guards, and — once it reaches a tail — its outcome:

• Before the first write, a match <field> arm or an is/== test narrows the from-set. After a known write the same test is decided statically (a read after a write sees the staged value — ADR 0125 D4), pruning infeasible branches. After a computed write it narrows nothing and becomes an opaque guard.
• Any other condition is an opaque guard, labelled with its source text.
• At each join, paths that agree on from-set, current value, last write and outcome merge; their guards combine.
• The last write on a path wins, since writes commit together at return. A domain Err is a value, so a write before it still makes an edge.
• Past PATH_BUDGET live paths a handler is truncated: its edges become one Target::Unknown edge from every state, which keeps reachability (and slice 3’s overlay) sound.

Reachability treats an Target::Unknown edge as reaching every state — a sound over-approximation, so a state outside StateMachine::reachable is truly unreachable from the handlers.

Placement (§3.7; #2220). A pure function of an [AgentDecl] and the type table, taking no LSP or checker-internal type. It lives in bynk-check so the state view (bynk-ide, bynk-lsp) and a checker diagnostic read one model; bynk-ide re-exports it as bynk_ide::agent_state.

Fault paths (a failing expect or <-) persist nothing and are not modelled as edges: the walk follows the success path of every statement.

Out of scope, as in the sequence diagram (ADR 0259): control flow and writes nested inside an argument expression (Ok(if c { … } else { … }), a field.update(f) that is not the top of its expression) or a lambda. This costs guard and outcome precision, never edges: a := is a statement, and a field.update(f) only runs when it is awaited (<-, do) or returned as a tail — an Effect buried in an argument is a value that never executes.

Structs

AgentStateModel

The state machines of one agent — one per state field.

Edge

One way a handler can leave the field.

NotEvaluated

#2197: a transition on the field outside the evaluated fragment.

StateMachine

One state field’s machine.

Violation

#2197: an edge a transition would refuse at commit (InvariantViolation).

Enums

Certainty

Target

Constants

PATH_BUDGET

The most live abstract paths one handler may carry before it is truncated (#2195 DECISION C) — a backstop against a pathological handler in a live view, far above anything in the corpus.

Functions

agent_state_model

Derive every state machine of agent. types is the unit’s combined type table (ContextBoundaryInfo::types); a state field whose type doesn’t resolve to a sum in it is skipped, not guessed (#2195 DECISION A).

combine_guards

The guards of two merged paths: either side holding is enough, so an unconditional side makes the merge unconditional, and two different conjunctions become one disjunction label.

handler_commits

Whether handler commits: whether its body writes any of agent’s store fields anywhere, the emitter’s condition for wrapping it in the commit that checks transitions. This recomputes bynk_lower::body_writes_state syntactically; bynk-lower’s tests pin the two together (#2220).

may_violate_diagnostics

#2221: bynk.transition.may_violate — a warning for each move a handler can make that a transition refuses at commit (track §3.2–§3.5).