Module session_runtime 

§Fase 41.d — the runtime of a session-typed dialogue. The static algebra (axon_frontend::session: duality, regular-coinductive equality, credit-refined backpressure index !ⁿA.S) gets a dynamic counterpart here: an operational state machine (SessionRuntime) with one method per algebra rule, a wire envelope (Frame), and an RFC 6455 WebSocket carrier (ws::drive) that runs a session type against a peer. Carrier-agnostic core; the WS layer is one binding. §Fase 41.d — the runtime of a session-typed dialogue.

axon-frontend::session (§41.a/b/c) gives the static algebra: the SessionType grammar, the duality involution, the regular-coinductive equality, and the Presburger-decidable credit-refined backpressure index !ⁿA.S. This crate’s session_runtime module is the dynamic counterpart — the operational state machine that runs a session type over a network carrier.

Layering:

• [state::SessionRuntime] is transport-agnostic: it owns a cursor (the residual session type after the trace so far), a [state::CreditWindow] (the runtime witness of !ⁿA.S), and one method per operational rule (try_send / try_recv / try_select / try_offer / try_end). The same runtime would plug into a QUIC stream, an in-process channel, or unit-test scaffolding.
• [wire::Frame] is the closed-catalog JSON envelope carried by one WebSocket text message per operational step. Versioned (v:1) first key, kind discriminator, fully serde-checked.
• [ws] is the RFC 6455 carrier: an axum upgrade-handler-shaped driver that reads peer frames, routes them onto the runtime, emits our outgoing frames in turn, and closes with 1000 normal closure on end or 1002 protocol error on a [error::ProtocolError].

The carrier in 41.d is WebSocket; future fases extend the same SessionRuntime over:

• 41.f: the enterprise axum server (multi-tenant + RLS + audit per utterance — the Kivi single-image unblock);
• 41.g: typed reconnection via cognitive_states (the §41.a residual type sealed at disconnect resumes from the same cursor);
• 41.h: multiparty projection (the global-type G projected to each role G⌐r, each running its own SessionRuntime).

Re-exports

pub use error::ProtocolError;

pub use sse::drive_sse_producer;

pub use state::CreditWindow;

pub use state::ResumeError;

pub use state::SealedRuntime;

pub use state::SessionRuntime;

pub use state::SEALED_RUNTIME_VERSION;

pub use wire::Frame;

pub use wire::AXON_WIRE_VERSION;

pub use ws::drive;

pub use ws::PeerRole;

Modules

error

Operational protocol errors raised by the §Fase 41.d session-typed WebSocket runtime — every variant is a runtime witness of a static discipline that the connection must respect on every transition.

sse

§Fase 41.e — Server-Sent Events carrier for the single-polarity fragment of a session type. The paper’s §4.4 identity S_SSE = Π↓(S_WS) makes SSE not a parallel protocol but the downstream projection of the WebSocket dialogue: when a session type satisfies [SessionType::projects_to_sse] (only End / Send / internal-Select / Rec / Var — no client input, no offered choice), the same SessionRuntime that runs over a WebSocket can be driven onto an SSE response stream byte-for-byte compatible with Fase 33’s W3C SSE framing.

state

The operational state machine for a single session-typed dialogue.

wire

Wire format for the §Fase 41.d session-typed WebSocket dialogue.

ws

WebSocket carrier for the session-typed dialogue runtime.