axon/session_runtime/error.rs
1//! Operational protocol errors raised by the §Fase 41.d session-typed
2//! WebSocket runtime — every variant is a runtime witness of a static
3//! discipline that the connection must respect on every transition.
4//!
5//! When the static type checker (`axon-frontend`, §41.b/c) has already
6//! validated the bound `session` + `socket { credit }`, a [`ProtocolError`]
7//! at runtime can only fire because the **peer** sent a frame that diverges
8//! from the conformant trace (or because a malformed frame entered the
9//! decoder). The carrier (WebSocket) closes with code `1002 protocol error`
10//! when one of these is observed; the error is recorded verbatim in the
11//! close-reason payload so the peer can diagnose the divergence.
12
13use std::fmt;
14
15use axon_frontend::session::Payload;
16
17/// Runtime protocol violation — the peer's next frame is inconsistent with
18/// the session-type cursor or with the credit window.
19#[derive(Debug, Clone, PartialEq, Eq)]
20pub enum ProtocolError {
21 /// The cursor expected a `send`/`recv` of payload `expected` but the
22 /// peer's frame announced payload `got`. The static type discipline is
23 /// violated — at runtime this means the peer is not running the dual
24 /// of our declared role.
25 PayloadMismatch { expected: Payload, got: Payload },
26 /// The cursor expected an operation of one kind (e.g. `recv`) but the
27 /// peer's frame announced another (e.g. `select`). The connection state
28 /// machine has no transition rule for the observed input.
29 UnexpectedFrame {
30 cursor_kind: &'static str,
31 frame_kind: &'static str,
32 },
33 /// The cursor is at an internal/external choice and the peer's label is
34 /// not in the type's arm set. Lists the declared labels so the peer can
35 /// recover.
36 UnknownLabel { label: String, expected: Vec<String> },
37 /// A `send` was attempted at zero available credit — the §Fase 41.c
38 /// "no rule at `n = 0`" axiom (paper §4.2) projected onto the runtime.
39 /// Static analysis (`credit_analyse`) catches this at compile time
40 /// when the declared protocol demands more than `k` sends in a burst;
41 /// at runtime it is the dynamic-safety net for an off-spec peer.
42 CreditExhausted { payload: Payload, budget: u64 },
43 /// The cursor has reached `end` but the peer sent more data, or the
44 /// peer requested an action while we already closed our half.
45 AlreadyComplete { frame_kind: &'static str },
46 /// The frame did not parse as a well-formed AXON session-typed
47 /// envelope (malformed JSON, unknown `kind`, missing required field).
48 /// Carries the raw payload for diagnostics.
49 MalformedFrame(String),
50 /// The transport (WebSocket) returned an I/O error or was closed
51 /// abruptly mid-dialogue.
52 Transport(String),
53 /// §Fase 79.d — a `signal` fired but no interruptible region is armed
54 /// (the cursor is not inside an `interrupt { … }` body).
55 NoInterruptArmed,
56 /// §Fase 79.d — the fired signal's cause does not match the armed
57 /// region's declared `on <Signal>`.
58 SignalMismatch { expected: Payload, got: Payload },
59 /// §Fase 79.d — the fail-closed WCET watchdog (D79.5): the reaction path
60 /// (signal → cancellation-acknowledged) took more transitions than the
61 /// statically-declared bound. A breach never silently degrades — it trips
62 /// this fault, which the carrier audits.
63 WatchdogBreach { bound: u32, actual: u32 },
64 /// §Fase 79.d — `resume` invoked on an already-consumed (or never
65 /// captured) one-shot continuation — the linear-type violation of D79.1,
66 /// caught at runtime even if it somehow slipped the static check.
67 DoubleResume,
68}
69
70impl fmt::Display for ProtocolError {
71 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
72 match self {
73 ProtocolError::PayloadMismatch { expected, got } => write!(
74 f,
75 "payload mismatch: cursor expected `{expected}`, peer sent `{got}` \
76 (the connection is not dual to the declared role)"
77 ),
78 ProtocolError::UnexpectedFrame { cursor_kind, frame_kind } => write!(
79 f,
80 "unexpected frame: cursor is at `{cursor_kind}`, peer sent `{frame_kind}` \
81 — the state machine has no transition for this input"
82 ),
83 ProtocolError::UnknownLabel { label, expected } => write!(
84 f,
85 "unknown choice label `{label}` — declared labels: {}",
86 expected.join(", ")
87 ),
88 ProtocolError::CreditExhausted { payload, budget } => write!(
89 f,
90 "credit exhausted on `send {payload}` at window n = 0 \
91 (budget = {budget}, §Fase 41.c, paper §4.2)"
92 ),
93 ProtocolError::AlreadyComplete { frame_kind } => write!(
94 f,
95 "dialogue already at `end`; peer sent `{frame_kind}` post-termination"
96 ),
97 ProtocolError::MalformedFrame(detail) => write!(f, "malformed frame: {detail}"),
98 ProtocolError::Transport(detail) => write!(f, "transport error: {detail}"),
99 ProtocolError::NoInterruptArmed => write!(
100 f,
101 "signal fired but no interruptible region is armed (cursor not inside \
102 an `interrupt` body, §Fase 79.d)"
103 ),
104 ProtocolError::SignalMismatch { expected, got } => write!(
105 f,
106 "interrupt signal mismatch: region declares `on {expected}`, got `{got}`"
107 ),
108 ProtocolError::WatchdogBreach { bound, actual } => write!(
109 f,
110 "WCET watchdog breach: reaction path took {actual} transitions, declared \
111 bound is {bound} (fail-closed, §Fase 79.d / D79.5)"
112 ),
113 ProtocolError::DoubleResume => write!(
114 f,
115 "`resume` on an already-consumed one-shot continuation \
116 (linear-type violation, §Fase 79 D79.1)"
117 ),
118 }
119 }
120}
121
122impl std::error::Error for ProtocolError {}
123
124impl ProtocolError {
125 /// A compact identifier suitable for the WebSocket close-frame reason
126 /// payload (RFC 6455 §5.5.1 caps the reason at 123 bytes UTF-8 — keep
127 /// these stable, short and machine-readable).
128 pub fn code(&self) -> &'static str {
129 match self {
130 ProtocolError::PayloadMismatch { .. } => "payload_mismatch",
131 ProtocolError::UnexpectedFrame { .. } => "unexpected_frame",
132 ProtocolError::UnknownLabel { .. } => "unknown_label",
133 ProtocolError::CreditExhausted { .. } => "credit_exhausted",
134 ProtocolError::AlreadyComplete { .. } => "already_complete",
135 ProtocolError::MalformedFrame(_) => "malformed_frame",
136 ProtocolError::Transport(_) => "transport",
137 ProtocolError::NoInterruptArmed => "no_interrupt_armed",
138 ProtocolError::SignalMismatch { .. } => "signal_mismatch",
139 ProtocolError::WatchdogBreach { .. } => "watchdog_breach",
140 ProtocolError::DoubleResume => "double_resume",
141 }
142 }
143}