socket

Attested. A fixture written in AXON is compiled and executed by a gate in the test suite, so this page describes behaviour a test exercises.

Since v2.3.0 · Top-level declaration

Grammar

socket <Name> {
    protocol: <SessionRef>            # required — must reference a declared `session`
    backpressure: credit(<n>)          # optional — Presburger-decidable index, n ≥ 1
    reconnect: cognitive_state         # optional — enables AAD-bound resume
    legal_basis: <basis> # optional — v2.0.0 legal-basis tag
}

The socket primitive binds a declared session (the bidirectional dialogue protocol) to a WebSocket transport (RFC 6455). Shipped in v2.3.0; the v2.3.0–c algebra proves the two endpoints are duals at compile time and discharges the credit-refined backpressure constraint in Presburger arithmetic.

Surface

socket is a top-level declaration. It is not nested inside a flow, a daemon, or a session. It references a session by name.

session Chat {
    client: [
        loop,
        select { ask: [send Utterance, branch { token: [receive Token, loop],
                                                done:  [end] }],
                 cancel: [end] }
    ]
    server: [
        loop,
        branch { ask: [receive Utterance, select { token: [send Token, loop],
                                                   done:  [end] }],
                 cancel: [end] }
    ]
}

socket ChatWS {
    protocol: Chat
    backpressure: credit(8)
    reconnect: cognitive_state
    legal_basis: legitimate_interest
}

Fields

protocol: (required)

Must reference a declared session. The compiler:

1. Resolves the name in the symbol table.
2. Lowers both roles into the v2.3.0 SessionType algebra (with loop becoming μX.…).
3. Verifies the connection law peer ≡ self⊥ via regular-coinductive equality (α-equivalent recursion variables are accepted).

A socket that names an undeclared session, or a session whose two roles fail duality, is rejected at axon check time.

backpressure: credit(<n>) (optional)

Declares the credit-refined index of v2.3.0 (paper section 4.2): the producer holds a sliding window of n in-flight sends; each send consumes one credit, each receive refills one (capped at n, standard TCP-window semantics).

n must be ≥ 1. A 0-credit window has no typing rule for a send (!⁰A.S is unprovable by the section 4.2 axiom); the compiler rejects credit(0).

The type checker discharges three Presburger constraints at compile time:

Verdict	When	Diagnostic
SendAtZero	Type contains an explicit !⁰A.S	"send A at credit n=0 has no typing rule"
BurstOverflow	Straight-line send-burst > n	"the protocol requires a send-burst of N but credit(n) cannot absorb it"
LoopUnsustainable	A recursive body has Δ = #send − #recv > 0	"recursive body is unsustainable: Δ = … > 0"

Omit backpressure: to run in the unbounded fragment (the v2.3.0 constraints are vacuously satisfied; the runtime never gates on credit).

reconnect: cognitive_state (optional)

Enables typed reconnection (v2.3.0). On a mid-protocol disconnect, the server seals the residual session-type cursor + live credit window into an AAD-bound cognitive_states snapshot keyed by (tenant_id, session_id, socket_name, subject_user_id). A reconnecting client presents the session_id via ?resume=<session_id> and the runtime restores from the exact residual.

Snapshot TTL defaults to 5 minutes; configurable at deploy time per the enterprise control plane.

Omitting reconnect: makes the socket one-shot: a mid-protocol drop is terminal; the client must start a fresh dialogue.

legal_basis: <basis> (optional)

Propagates the v2.0.0 legal-basis annotation into the audit hash-chain. Every utterance through this socket carries the basis in the session:ws_* audit rows, so an investigator can trace which legal basis covered each frame.

Runtime behaviour

The enterprise server (axon-enterprise-server v2.1.0+) mounts a declared socket at GET /api/v1/socket/<lowercase-name> automatically at boot. The route is protected by the v2.0.0 auth layer and the socket:connect RBAC capability (granted to owner/admin/developer by default; viewer excluded).

Carrier closure codes:

Code	Reason	Meaning
1000	session_end	Both peers reached end.
1002	payload_mismatch	Wrong payload type for the cursor.
1002	unexpected_frame	Wrong frame kind for the cursor.
1002	unknown_label	select/branch label not in the type.
1002	credit_exhausted	send attempted at credit n=0.
1002	already_complete	Peer sent more after end.
1002	malformed_frame	Envelope failed JSON / version parsing.
1002	no_interrupt_armed	signal fired outside an interrupt body (v2.36.0).
1002	signal_mismatch	Signal cause ≠ the region's on <Signal> (v2.36.0).
1002	watchdog_breach	WCET reaction bound exceeded — fail-closed (v2.36.0).
1002	double_resume	resume on an already-consumed continuation (v2.36.0).

Resume rejection codes (HTTP 410 Gone): resume_not_found, resume_expired, resume_aad_mismatch, resume_malformed, resume_schema_drift.

Interruptible sessions (v2.36.0)

A session step may declare an interruptible region — a barge-in the agent can resume, not a killed turn:

interrupt {
    <body>                       # the interruptible protocol (e.g. an utterance)
} on <Signal> as <sig> resumable {
    <handler>                    # runs on the signal; ends in `resume` or `end`
}

<Signal> is the closed CallInterruptCause catalog — CallerSpeech | Dtmf | SilenceTimeout | AgentFault (no free-form causes). The handler is a two-exit construct: its normal exit resume hands control back to the exact point in <body> where the signal fired (consuming a one-shot captured continuation); its abandon exit is end, taken on TTL expiry.

Carrier states (distinct from closure — the connection stays open):

State	Meaning
interrupted_by_peer	The signal fired; the body's residual is parked (a one-shot continuation), the handler is running.
resumed	The handler called resume; control is back in the body at its exact residual, with the pre-interrupt credit window restored exactly and the stream re-opened at the flushed offset.
interrupt_abandoned	The parked continuation's TTL expired; it is released (once) and the region terminates at end.

The parked continuation survives a reconnect by riding the same v2.3.0 cognitive_state AAD-bound snapshot as an ordinary residual cursor — no new state store. Honest scope: the WCET reaction bound is soft-real-time (statically-derived + runtime-verified by the fail-closed watchdog, not hard RTOS), and "delivered" means flushed to the carrier, not rendered on the caller's device. v1 is binary (2-role), single-level, single-signal.

SSE-as-fragment unification (v2.3.0)

If the bound session's server role is single-polarity (only send, select, end, loop — no receive, no branch), the same socket declaration ALSO speaks W3C Server-Sent Events on the same path with Accept: text/event-stream. The wire bytes are byte-compatible with v1.24.0's SSE machinery:

event: axon.send
data: {"payload_type":"Token","data":…}

event: axon.end
data: {}

This is the formal identity S_SSE = Π_↓(S_WS) shipped in code. For two-polarity protocols, SSE requests return one axon.error{ code:"non-sse-polarity-schema" } event and close; the full dialogue remains available over WebSocket.

What this primitive is NOT

• Not a generic WebSocket library. A socket without a protocol: field is rejected. The session type is the type of the connection.
• Not nested inside a flow. A flow consumes typed channels + utterances, but the carrier binding (the socket) is a top-level declaration like axonendpoint.
• Not auto-recovered without reconnect: cognitive_state. Omitting the annotation makes the socket one-shot by design — useful for request-style dialogues where replay would be a security issue.

See also

• axon://primitives/session — declares the bidirectional protocol the socket binds.
• axon://logic/session_duality — the v2.3.0 connection law rules (regular-coinductive equality, α-equivalent recursion variables).
• axon://primitives/cognitive_state — the AAD-bound snapshot store the reconnect: field hooks into.
• axon://compliance/legal_basis_catalog — the closed catalog the legal_basis: field draws from.
• papers/paper_websocket_cognitive_primitive.md — the four-pillar paper underpinning v2.3.0.