Function lower_service_handler_ir 

pub fn lower_service_handler_ir(
    h: &Handler,
    protocol: &ServiceProtocol,
    program: &CheckedProgram,
) -> IrHandler

P6.11’s real service-handler IrHandler constructor ([DECISION E], #1171) — the sibling to lower_handler_ir, not a widening of it. lower_fn_body_ir’s own doc comment already states the governing rule (“a free fn/method and an agent handler seed genuinely different scopes … that would otherwise have to coexist behind one signature for no shared benefit”); the same reasoning gives the same answer here, more strongly:

• The two scopes are disjoint, not overlapping — an agent handler body seeds self/store_cells; a service handler body seeds params/ binder only. Not one of store_cells/state_ty/invariants/ transitions means anything for a service.
• lower_handler_ir asserts h.by_clause.is_none() — an explicit “agent-only by contract” guard. Widening would delete the one thing that today catches a service handler reaching the wrong entry point.

protocol is a parameter solely to disambiguate HandlerKind::Message — the same literal AST variant is a queue consumer under ServiceProtocol::Queue and a WebSocket inbound frame under ServiceProtocol::WebSocket (HandlerKind::Close’s own doc comment says so), and the checker itself dispatches on exactly this (kind, protocol) pair (context_checks.rs:1938-1945) — without protocol here, the ConnectionBinder derivation below would wrongly capture every queue consumer in the language too.

binder is read back, not threaded in as a parameter — the deliberate inverse of lower_handler_ir’s own [DECISION E] (store_cells/state_ty/invariants/transitions are parameters because no persisted table survives check_agent_decls’s own transient scope). Here the opposite premise holds: #1170 persisted exactly this pair into TypedCommons::actor_bindings, so the opposite choice follows. None is a legitimate outcome, not an error — a binder-less by <Actor>, no by clause at all, or a binder that shadowed a param and was suppressed (context_checks.rs:2050-2055) all resolve to None here exactly as they do in handler_actor_binding itself; this function does not, and must not, assert binder.is_some() from h.by_clause.is_some().

commit passes empty invariants/transitions slices to lower_commit_shape_ir — [DECISION F]’s own predicted service call site, real for the first time. CommitShape::Transactional is structurally unreachable here, not merely unproduced by convention: a service declares no store fields for body_writes_state to find a write against. No is_service flag is added anywhere — Decision F’s whole point is that none is needed.

The websocket lifecycle case, closed (P6.13, [DECISION G], #1179). A from websocket service’s on open/on message/on close handler receives the synthetic leading connection: Connection[out] binding the checker injects into its own params_for_check only (open_connection_param, context_checks.rs:2020-2032, injected at :1944-1954) — never into h.params, so params/given above stay derived from h.params alone, exactly mirroring the checker’s own asymmetry (handler.params itself is never mutated either). This function re-derives the same Connection[out] type via cx.resolve_type_ref over a freshly-built TypeRef::Connection, the same construction open_connection_param performs, since that function is private to bynk-check and there is no persisted TypedCommons table to read it back from (contrast binder, below, which #1170 did persist). borrowed mirrors the checker’s own borrowed_held distinction (context_checks.rs:1955-1963): false for on open (a fresh owned socket, disposed via transfer to an agent), true for on message/on close (the borrowed firing socket). The resulting ConnectionBinder is threaded into lower_service_handler_body_ir so connection.… reads resolve via cx.lookup like any other bound name, and carried on IrHandler itself for any consumer that needs the owned/borrowed distinction without re-deriving it from kind/protocol.