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
Remarks:
  • Option precedence: When the same read or write option is given multiple times, the first occurrence is used.

Inherited public predicates:

Public predicates

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

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

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.


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.


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.


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)

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.


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.


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

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_)

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)

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)

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

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

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

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)