.. index:: single: http_websocket_session(Role,TextRepresentation) .. _http_websocket_session/2: .. rst-class:: right **object** ``http_websocket_session(Role,TextRepresentation)`` =================================================== * ``Role`` - Peer role for masking policy. Possible values are ``client`` and ``server``. * ``TextRepresentation`` - Text representation to be used for text messages and close reasons. Possible values are ``atom`` (default), ``chars``, and ``codes``. Stateful WebSocket session predicates that build on top of the message layer to surface interleaved control frames, apply role-aware masking policies, and track close-handshake state. The callback-driven session loops are provided by the http_websocket_service library. | **Availability:** | ``logtalk_load(http_websocket_session(loader))`` | **Author:** Paulo Moura | **Version:** 1:0:0 | **Date:** 2026-06-26 | **Compilation flags:** | ``static, context_switching_calls`` | **Extends:** | ``public`` :ref:`http_websocket_messages(TextRepresentation) ` | **Uses:** | :ref:`crypto ` | :ref:`http_websocket_frames ` | :ref:`http_websocket_session_read_options ` | :ref:`http_websocket_session_write_options ` | :ref:`list ` | **Remarks:** - Option precedence: When the same read or write option is given multiple times, the first occurrence is used. | **Inherited public predicates:** |  :ref:`http_websocket_messages/1::is_message/1`  :ref:`http_websocket_messages/1::message/3`  :ref:`http_websocket_messages/1::payload/2`  :ref:`http_websocket_messages/1::read_message/2`  :ref:`http_websocket_messages/1::type/2`   .. contents:: :local: :backlinks: top Public predicates ----------------- .. index:: initial_state/1 .. _http_websocket_session/2::initial_state/1: ``initial_state/1`` ^^^^^^^^^^^^^^^^^^^ Returns the initial session state term to be threaded through stateful reads. | **Compilation flags:** | ``static`` | **Template:** | ``initial_state(State)`` | **Mode and number of proofs:** | ``initial_state(-compound)`` - ``one`` ------------ .. index:: is_state/1 .. _http_websocket_session/2::is_state/1: ``is_state/1`` ^^^^^^^^^^^^^^ True when the argument is a valid session state term. | **Compilation flags:** | ``static`` | **Template:** | ``is_state(State)`` | **Mode and number of proofs:** | ``is_state(@term)`` - ``zero_or_one`` ------------ .. index:: read_message/4 .. _http_websocket_session/2::read_message/4: ``read_message/4`` ^^^^^^^^^^^^^^^^^^ Reads the next session-level WebSocket message from a binary stream using the given input state. Fragmented text and binary messages are reassembled across calls, interleaved control frames are surfaced immediately, and close-message state transitions are tracked in the returned state. | **Compilation flags:** | ``static`` | **Template:** | ``read_message(Stream,State,UpdatedState,Message)`` | **Mode and number of proofs:** | ``read_message(+stream_or_alias,+compound,-compound,-term)`` - ``one_or_error`` | **Exceptions:** | ``Stream`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | The inbound frame/message sequence violates RFC 6455 session rules: | ``domain_error(http_websocket_session_sequence,Frame)`` | The inbound frame violates the current peer masking policy: | ``domain_error(http_websocket_session_masking,Frame)`` | The inbound frame uses unsupported extensions: | ``domain_error(http_websocket_session_extensions,Frame)`` | The inbound frame is invalid: | ``domain_error(http_websocket_frame,Frame)`` | The inbound message text is invalid: | ``domain_error(http_websocket_message_text,Payload)`` | **Remarks:** - End of file: Returns ``end_of_file`` only when the input state is idle and the stream is already exhausted. - Masking policy: Incoming frame masking is validated against the session role: client sessions expect unmasked inbound frames and server sessions expect masked inbound frames. - Peer close: When a close frame is read, any fragmented data message in progress is discarded. Subsequent reads from the resulting ``close_received/1`` or ``closed/2`` state are rejected. ------------ .. index:: read_message/5 .. _http_websocket_session/2::read_message/5: ``read_message/5`` ^^^^^^^^^^^^^^^^^^ Reads the next session-level WebSocket message from a binary input stream using the given state and automatically orchestrates the close handshake on the given binary output stream when a close message is received. | **Compilation flags:** | ``static`` | **Template:** | ``read_message(Input,Output,State,UpdatedState,Message)`` | **Mode and number of proofs:** | ``read_message(+stream_or_alias,+stream_or_alias,+compound,-compound,-term)`` - ``one_or_error`` | **Exceptions:** | ``Input`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | The inbound frame/message sequence violates RFC 6455 session rules: | ``domain_error(http_websocket_session_sequence,Frame)`` | The inbound frame violates the current peer masking policy: | ``domain_error(http_websocket_session_masking,Frame)`` | The inbound frame uses unsupported extensions: | ``domain_error(http_websocket_session_extensions,Frame)`` | The inbound frame is invalid: | ``domain_error(http_websocket_frame,Frame)`` | The inbound message text is invalid: | ``domain_error(http_websocket_message_text,Payload)`` | **Remarks:** - Close handshake: When a close message is received and no close message has yet been sent for the tracked session state, a matching close message is written automatically on the output stream and the returned state records the completed handshake. ------------ .. index:: read_message/6 .. _http_websocket_session/2::read_message/6: ``read_message/6`` ^^^^^^^^^^^^^^^^^^ Reads the next session-level WebSocket message from a binary input stream using the given state, automatically orchestrates the close handshake on the given binary output stream, and applies optional automatic control-message policies. | **Compilation flags:** | ``static`` | **Template:** | ``read_message(Input,Output,State,UpdatedState,Message,Options)`` | **Mode and number of proofs:** | ``read_message(+stream_or_alias,+stream_or_alias,+compound,-compound,-term,+list)`` - ``one_or_error`` | **Exceptions:** | ``Input`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | ``Options`` is a variable or a partial list: | ``instantiation_error`` | ``Options`` is neither a variable nor a list: | ``type_error(list,Options)`` | An element ``Option`` of the list ``Options`` is neither a variable nor a compound term: | ``type_error(compound,Option)`` | An element ``Option`` of the list ``Options`` is a compound term but not a valid read option: | ``domain_error(http_websocket_session_read_option,Option)`` | The inbound frame/message sequence violates RFC 6455 session rules: | ``domain_error(http_websocket_session_sequence,Frame)`` | The inbound frame violates the current peer masking policy: | ``domain_error(http_websocket_session_masking,Frame)`` | The inbound frame uses unsupported extensions: | ``domain_error(http_websocket_session_extensions,Frame)`` | The inbound payload length exceeds the configured limit: | ``domain_error(http_websocket_payload_length_limit,PayloadLength)`` | **Remarks:** - Option ``auto_pong(on)``: Automatically writes a pong message with the same payload when a ping message is read while still returning the ping message to the caller. - Option ``auto_pong(off)``: Disables automatic pong replies. This is the default. - Option ``max_payload_length(Bytes)``: Rejects inbound frames whose declared payload length is greater than ``Bytes`` before allocating payload storage. Use a non-negative integer. ------------ .. index:: write_message/2 .. _http_websocket_session/2::write_message/2: ``write_message/2`` ^^^^^^^^^^^^^^^^^^^ Stateless convenience wrapper that writes one validated WebSocket message using the masking policy implied by the session role. Client sessions mask all outgoing frames; server sessions leave them unmasked. | **Compilation flags:** | ``static`` | **Template:** | ``write_message(Stream,Message)`` | **Mode and number of proofs:** | ``write_message(+stream_or_alias,+compound)`` - ``one_or_error`` | **Exceptions:** | ``Stream`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``Message`` is not a valid normalized WebSocket message term: | ``domain_error(http_websocket_message,Message)`` | ``Message`` contains invalid text: | ``domain_error(http_websocket_message_text,Text)`` | The generated outbound frame is invalid: | ``domain_error(http_websocket_frame,Frame)`` ------------ .. index:: write_message/3 .. _http_websocket_session/2::write_message/3: ``write_message/3`` ^^^^^^^^^^^^^^^^^^^ Stateless convenience wrapper that writes one validated WebSocket message using the masking policy implied by the session role and the given write options. | **Compilation flags:** | ``static`` | **Template:** | ``write_message(Stream,Message,Options)`` | **Mode and number of proofs:** | ``write_message(+stream_or_alias,+compound,+list)`` - ``one_or_error`` | **Exceptions:** | ``Stream`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``Message`` is not a valid normalized WebSocket message term: | ``domain_error(http_websocket_message,Message)`` | ``Options`` is a variable or a partial list: | ``instantiation_error`` | ``Options`` is neither a variable nor a list: | ``type_error(list,Options)`` | An element ``Option`` of the list ``Options`` is neither a variable nor a compound term: | ``type_error(compound,Option)`` | An element ``Option`` of the list ``Options`` is a compound term but not a valid write option: | ``domain_error(http_websocket_session_write_option,Option)`` | The generated outbound frame is invalid: | ``domain_error(http_websocket_frame,Frame)`` | **Remarks:** - Option ``fragment_size(Size)``: When writing ``text`` or ``binary`` messages, split the payload into frames of at most ``Size`` bytes. Control messages always remain single final frames. ------------ .. index:: write_message/4 .. _http_websocket_session/2::write_message/4: ``write_message/4`` ^^^^^^^^^^^^^^^^^^^ Writes one validated WebSocket message using the masking policy implied by the session role and updates the given session state with any close-handshake transition caused by the write. | **Compilation flags:** | ``static`` | **Template:** | ``write_message(Stream,State,UpdatedState,Message)`` | **Mode and number of proofs:** | ``write_message(+stream_or_alias,+compound,-compound,+compound)`` - ``one_or_error`` | **Exceptions:** | ``Stream`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | ``Message`` is not a valid normalized WebSocket message term: | ``domain_error(http_websocket_message,Message)`` | The write violates the current close-handshake state: | ``domain_error(http_websocket_session_state,State)`` | **Remarks:** - Closing state: After a peer close is recorded, only the matching close reply may be written. After a local close is recorded, further data messages are rejected. ------------ .. index:: write_message/5 .. _http_websocket_session/2::write_message/5: ``write_message/5`` ^^^^^^^^^^^^^^^^^^^ Writes one validated WebSocket message using the masking policy implied by the session role and the given write options while updating the given session state with any close-handshake transition caused by the write. | **Compilation flags:** | ``static`` | **Template:** | ``write_message(Stream,State,UpdatedState,Message,Options)`` | **Mode and number of proofs:** | ``write_message(+stream_or_alias,+compound,-compound,+compound,+list)`` - ``one_or_error`` | **Exceptions:** | ``Stream`` is a variable: | ``instantiation_error`` | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | ``Message`` is not a valid normalized WebSocket message term: | ``domain_error(http_websocket_message,Message)`` | ``Options`` is a variable or a partial list: | ``instantiation_error`` | ``Options`` is neither a variable nor a list: | ``type_error(list,Options)`` | An element ``Option`` of the list ``Options`` is neither a variable nor a compound term: | ``type_error(compound,Option)`` | An element ``Option`` of the list ``Options`` is a compound term but not a valid write option: | ``domain_error(http_websocket_session_write_option,Option)`` | The write violates the current close-handshake state: | ``domain_error(http_websocket_session_state,State)`` | **Remarks:** - Option ``fragment_size(Size)``: When writing ``text`` or ``binary`` messages, split the payload into frames of at most ``Size`` bytes. Control messages always remain single final frames. ------------ Protected predicates -------------------- .. index:: validate_role/0 .. _http_websocket_session/2::validate_role/0: ``validate_role/0`` ^^^^^^^^^^^^^^^^^^^ Validates the session role parameter. Throws a domain error when the role is neither ``client`` nor ``server``. | **Compilation flags:** | ``static`` | **Mode and number of proofs:** | ``validate_role`` - ``one_or_error`` | **Exceptions:** | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` ------------ .. index:: read_session_message/5 .. _http_websocket_session/2::read_session_message/5: ``read_session_message/5`` ^^^^^^^^^^^^^^^^^^^^^^^^^^ Protected helper that validates the session role and state and reads the next session-level message, returning the updated pending-fragment bookkeeping term and the message. Close-state transitions are left to the caller. | **Compilation flags:** | ``static`` | **Template:** | ``read_session_message(Stream,State,MaxPayloadLength,Pending,Message)`` | **Mode and number of proofs:** | ``read_session_message(+stream_or_alias,+compound,+term,-compound,-term)`` - ``one_or_error`` | **Exceptions:** | The session role parameter is neither ``client`` nor ``server``: | ``domain_error(http_websocket_session_role,_Role_)`` | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | The inbound frame/message sequence violates RFC 6455 session rules: | ``domain_error(http_websocket_session_sequence,Frame)`` | The inbound frame violates the current peer masking policy: | ``domain_error(http_websocket_session_masking,Frame)`` | The inbound frame uses unsupported extensions: | ``domain_error(http_websocket_session_extensions,Frame)`` ------------ .. index:: apply_session_read/6 .. _http_websocket_session/2::apply_session_read/6: ``apply_session_read/6`` ^^^^^^^^^^^^^^^^^^^^^^^^ Protected helper that applies the close-state and automatic control-message transitions for a message read outside this object and returns the updated session state. | **Compilation flags:** | ``static`` | **Template:** | ``apply_session_read(Output,State,AutoPong,Pending,Message,UpdatedState)`` | **Mode and number of proofs:** | ``apply_session_read(+stream_or_alias,+compound,+atom,+compound,+term,-compound)`` - ``one_or_error`` | **Exceptions:** | ``State`` is not a valid WebSocket session state: | ``domain_error(http_websocket_session_state,State)`` | ``AutoPong`` is not a supported automatic pong setting: | ``domain_error(http_websocket_session_read_option,auto_pong(AutoPong))`` | ``Message`` is not a valid normalized WebSocket message term: | ``domain_error(http_websocket_message,Message)`` ------------ .. index:: current_close_state/2 .. _http_websocket_session/2::current_close_state/2: ``current_close_state/2`` ^^^^^^^^^^^^^^^^^^^^^^^^^ Protected helper that returns the close-handshake component of a session state term. Open states are reported as ``open``. | **Compilation flags:** | ``static`` | **Template:** | ``current_close_state(State,CloseState)`` | **Mode and number of proofs:** | ``current_close_state(+compound,-compound)`` - ``one`` ------------ .. index:: close_handshake_completed/1 .. _http_websocket_session/2::close_handshake_completed/1: ``close_handshake_completed/1`` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Protected helper that is true when the given session state records a completed close handshake. | **Compilation flags:** | ``static`` | **Template:** | ``close_handshake_completed(State)`` | **Mode and number of proofs:** | ``close_handshake_completed(+compound)`` - ``zero_or_one`` ------------ .. index:: best_effort_protocol_error_close/3 .. _http_websocket_session/2::best_effort_protocol_error_close/3: ``best_effort_protocol_error_close/3`` ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Protected helper that writes a best-effort close message mapping the given protocol error to its close status code when the session close state still allows it. Write errors are ignored. | **Compilation flags:** | ``static`` | **Template:** | ``best_effort_protocol_error_close(Output,State,Error)`` | **Mode and number of proofs:** | ``best_effort_protocol_error_close(+stream_or_alias,+compound,+callable)`` - ``one`` ------------ .. index:: generate_masking_key/1 .. _http_websocket_session/2::generate_masking_key/1: ``generate_masking_key/1`` ^^^^^^^^^^^^^^^^^^^^^^^^^^ Protected hook that returns the four-byte masking key to use for outgoing client frames. The default implementation delegates to ``crypto::random_bytes/2``. | **Compilation flags:** | ``static`` | **Template:** | ``generate_masking_key(Key)`` | **Mode and number of proofs:** | ``generate_masking_key(-list(byte))`` - ``one`` ------------ Private predicates ------------------ (no local declarations; see entity ancestors if any) Operators --------- (none)