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
34/// §Fase 111.i — the SessionType compiler: `IRSession` → [`crate::session::SessionType`].
35///
36/// The declarations reached the IR all along; nothing read them. The type-checker
37/// lowered the roles to prove duality and dropped the result, and the enterprise
38/// server — which *does* serve the wire — substituted a hardcoded chat schema for
39/// every deployed socket. So a protocol could be *proven* dual at compile time and
40/// a **different one** enforced at runtime. This module closes that gap.
41pub mod compile;
42pub mod error;
43pub mod sse;
44pub mod state;
45pub mod wire;
46pub mod ws;
47
48pub use error::ProtocolError;
49pub use sse::drive_sse_producer;
50pub use state::{
51    CreditWindow, ParkedContinuation, ResumeError, SealedRuntime, SessionRuntime,
52    SEALED_RUNTIME_VERSION,
53};
54pub use compile::{credit_for_socket, schema_for_socket, server_schema, session_type_of_role};
55pub use wire::{Frame, AXON_WIRE_VERSION};
56pub use ws::{drive, PeerRole};
axon/session_runtime/mod.rs

axon/session_runtime/
mod.rs
