axon/session_runtime/
mod.rs

1//! §Fase 41.d — the **runtime** of a session-typed dialogue.
2//!
3//! `axon-frontend::session` (§41.a/b/c) gives the static algebra: the
4//! `SessionType` grammar, the duality involution, the regular-coinductive
5//! equality, and the Presburger-decidable credit-refined backpressure
6//! index `!ⁿA.S`. This crate's `session_runtime` module is the dynamic
7//! counterpart — the operational state machine that *runs* a session
8//! type over a network carrier.
9//!
10//! Layering:
11//! - [`state::SessionRuntime`] is **transport-agnostic**: it owns a
12//!   cursor (the residual session type after the trace so far), a
13//!   [`state::CreditWindow`] (the runtime witness of `!ⁿA.S`), and one
14//!   method per operational rule (`try_send` / `try_recv` / `try_select`
15//!   / `try_offer` / `try_end`). The same runtime would plug into a
16//!   QUIC stream, an in-process channel, or unit-test scaffolding.
17//! - [`wire::Frame`] is the **closed-catalog JSON envelope** carried by
18//!   one WebSocket text message per operational step. Versioned (`v:1`)
19//!   first key, `kind` discriminator, fully `serde`-checked.
20//! - [`ws`] is the **RFC 6455 carrier**: an axum upgrade-handler-shaped
21//!   driver that reads peer frames, routes them onto the runtime, emits
22//!   our outgoing frames in turn, and closes with `1000 normal closure`
23//!   on `end` or `1002 protocol error` on a [`error::ProtocolError`].
24//!
25//! The carrier in 41.d is WebSocket; future fases extend the same
26//! `SessionRuntime` over:
27//! - 41.f: the enterprise axum server (multi-tenant + RLS + audit per
28//!   utterance — the Kivi single-image unblock);
29//! - 41.g: typed reconnection via `cognitive_states` (the §41.a residual
30//!   type sealed at disconnect resumes from the same cursor);
31//! - 41.h: multiparty projection (the global-type `G` projected to each
32//!   role `G⌐r`, each running its own `SessionRuntime`).
33
34pub mod error;
35pub mod sse;
36pub mod state;
37pub mod wire;
38pub mod ws;
39
40pub use error::ProtocolError;
41pub use sse::drive_sse_producer;
42pub use state::{CreditWindow, ResumeError, SealedRuntime, SessionRuntime, SEALED_RUNTIME_VERSION};
43pub use wire::{Frame, AXON_WIRE_VERSION};
44pub use ws::{drive, PeerRole};
axon/session_runtime/mod.rs

axon/session_runtime/
mod.rs
