Function check_transitions 

pub fn check_transitions(
    transitions: &[Transition],
    state_ty: TyId,
    agent_name: &str,
    input: &ResolvedCommons,
    expr_types: &mut HashMap<ExprId, TypedExpr>,
    errors: &mut Vec<CompileError>,
    refs: &mut RefSink,
    hints: &mut HintSink,
    locals: &mut LocalsSink,
    requirements: &mut RequirementSink,
    callees: &mut HashMap<ExprId, Callee>,
    tys: &Types,
)

Check an agent’s step invariants (v0.116 §, testing track slice 4). A transition is the invariant predicate widened to the step (ADR 0144 — one predicate surface): a pure Bool predicate over the old/new state pair, each bound to the agent’s synthetic state record (state_ty), so old.status / new.status resolve like any record field. The pass enforces, mirroring check_invariants:

• bynk.transition.duplicate_name — two transitions share a name (the name rides the InvariantViolation failure report).
• bynk.transition.impure_predicate — a predicate uses an effectful or test-only construct.
• bynk.transition.no_step_reference — a predicate references neither old nor new; it is a snapshot claim misfiled as a step (use invariant).
• bynk.transition.not_bool — a predicate does not type to Bool.

Placement is enforced structurally by the grammar (a transition is an agent-body-only declaration), so there is no “transition on a non-agent” diagnostic to raise here.