stdlib.net

Networking Library

Generated from v0.65.7. 32 source files, 476 documented symbols.

address.xi

type Address

struct Address { family: Str; host: Str; port: Int } family is "ipv4", "ipv6" or "hostname"; port 0 means "no explicit port".

Field	Type
family	Str
host	Str
port	Int

fn address_parse(s: Str) -> Option[Address]

Parse a host:port address string into an Address. Parameters: s -- the address string ("example.com:8080", "127.0.0.1", "[::1]:53", "example.com"). Returns: Some(Address) when the string is well-formed (non-empty host and a valid port if present), None otherwise. Complexity: O(n). Pure.

• Postcondition: (result.is_some == false) || (s.len() != 0)

fn address_host(s: Str) -> Str

Extract the host part of an address string. Parameters: s -- the address string. Returns: the host (without brackets for IPv6 literals), or "" when the string is not a valid address. Complexity: O(n). Pure.

• Postcondition: (result == "") || (s.len() != 0)

fn address_port(s: Str) -> Int

Extract the port part of an address string. Parameters: s -- the address string. Returns: the port number (0 when absent), or 0 for an invalid address. Complexity: O(n). Pure.

• Postcondition: result >= 0

fn address_is_ipv4(s: Str) -> Bool

Test if the host part of an address string is an IPv4 address. Parameters: s -- the address string. Returns: true when the string parses and its host is dotted-quad IPv4. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() != 0)

fn address_is_ipv6(s: Str) -> Bool

Test if the host part of an address string is an IPv6 address. Parameters: s -- the address string. Returns: true when the string parses and its host is an IPv6 literal. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() != 0)

fn address_is_valid(s: Str) -> Bool

Test if the address string is well-formed. Parameters: s -- the address string. Returns: true when parsing succeeds with a non-empty host and a valid port (0..65535) if one is present. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() != 0)

---

---

---

cookie.xi

type Cookie

struct Cookie { name: Str; value: Str; domain: Str; path: Str; expires: Int; max_age: Int; secure: Bool; http_only: Bool; same_site: Str } expires is a unix timestamp (0 = session cookie); same_site is "Strict", "Lax" or "None" ("" when unset).

Field	Type
name	Str
value	Str
domain	Str
path	Str
expires	Int
max_age	Int
secure	Bool
http_only	Bool
same_site	Str

type CookieJar

struct CookieJar - an ordered collection of cookies.

Field	Type
cookies	Vec[Cookie]

fn cookie_parse(header: Str) -> Result[Cookie, Str]

Parse a request Cookie header into a cookie. Parameters: header -- the Cookie header value (e.g. "a=b; c=d"). Returns: Ok(Cookie) for the first name=value pair, Err when the header is empty or any segment is malformed. Complexity: O(n). Pure.

• Postcondition: ((header.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (header.len() > 0))

fn cookie_parse_set_cookie(header: Str) -> Result[Cookie, Str]

Parse a Set-Cookie header into a cookie. Parameters: header -- the Set-Cookie header value (e.g. "a=b; Path=/; HttpOnly; Max-Age=3600; SameSite=Strict"). Returns: Ok(Cookie) with attributes applied, Err when the name=value pair is missing or malformed. Complexity: O(n). Pure.

• Postcondition: ((header.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (header.len() > 0))

fn cookie_serialize(c: Cookie) -> Str

Serialize a cookie into Cookie header form ("name=value"). Parameters: c -- the cookie. Returns: the "name=value" string. Complexity: O(1). Pure.

• Postcondition: result == c.name + "=" + c.value

fn cookie_jar_new() -> CookieJar

Create an empty cookie jar. Returns: a jar holding no cookies. Complexity: O(1). Pure.

• Postcondition: result.cookies.len() == 0

fn cookie_jar_set(jar: &mut CookieJar, c: Cookie)

Store a cookie in the jar, replacing an existing cookie with the same name, domain and path. Parameters: jar -- the mutable jar; c -- the cookie to store. Returns: Unit. Complexity: O(n) with n = jar size. Pure.

• Postcondition: jar.cookies.len() >= 1

fn cookie_jar_get(jar: &CookieJar, name: Str, url: Str) -> Option[Cookie]

Fetch a cookie by name for a url. Parameters: jar -- the jar; name -- the cookie name; url -- the request url. Returns: Some(Cookie) for the first matching cookie, None otherwise. Complexity: O(n) with n = jar size. Pure.

• Postcondition: ((jar.cookies.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (jar.cookies.len() > 0))

fn cookie_jar_matches(c: Cookie, url: Str) -> Bool

Test if a cookie applies to a url (domain match, path match and not expired). Parameters: c -- the cookie; url -- the request url. Returns: true when the cookie applies. Complexity: O(n). Pure.

• Postcondition: (c.domain.len() == 0 && c.path.len() == 0 && c.expires <= 0) => (result == true)

fn cookie_jar_size(jar: &CookieJar) -> Int

Count cookies held in the jar. Parameters: jar -- the jar. Returns: the number of cookies. Complexity: O(1). Pure.

• Postcondition: result >= 0

fn cookie_expires_after(c: Cookie, seconds: Int) -> Bool

Test if the cookie expires within the given number of seconds. Parameters: c -- the cookie; seconds -- the window in seconds. Returns: true when the cookie has an expiry and it falls at or before now + seconds (already-expired cookies count as expiring). Complexity: O(1). Pure.

• Postcondition: ((c.expires <= 0) => (result == false)) && ((result == true) => (c.expires > 0))

fn cookie_domain_matches(domain: Str, host: Str) -> Bool

RFC 6265 domain-match test. Parameters: domain -- the cookie's Domain attribute; host -- the request host. Returns: true when host equals domain or is a subdomain of domain. Complexity: O(n). Pure.

• Postcondition: ((domain.len() == 0 || host.len() == 0) => (result == false)) && ((domain.len() > 0 && domain == host) => (result == true)) && ((result == true) => (domain.len() > 0 && host.len() > 0))

fn cookie_path_matches(path: Str, request_path: Str) -> Bool

RFC 6265 path-match test. Parameters: path -- the cookie's Path attribute; request_path -- the request path. Returns: true when request_path matches the cookie path. Complexity: O(n). Pure.

• Postcondition: ((path.len() == 0) => (result == true)) && ((path == request_path) => (result == true)) && ((result == true) => (request_path.len() >= path.len()))

---

---

---

dns.xi

fn dns_parse_ipv4(s: Str) -> Option[Vec[UInt8]]

dns_parse_ipv4 parses "a.b.c.d" into 4 bytes, or None on invalid input. Delegates to the canonical xiom.net.ip4 (dedup wave, 2026-09-16; parity proven in p_dns_parity). The Option/Result translation binds the parsed value to a named local first (R28 workaround: .value on a temporary aggregate payload is corrupt).

• Postcondition: ((s.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 7))

fn dns_ipv4_to_str(octets: &Vec[UInt8]) -> Option[Str]

dns_ipv4_to_str formats 4 bytes as "a.b.c.d", or None if the length is not 4. Delegates to the canonical xiom.net.ip4.

• Postcondition: ((octets.len() != 4) => (result.is_none == true)) && ((result.is_some == true) => (octets.len() == 4))

fn dns_parse_ipv6(s: Str) -> Option[Vec[UInt8]]

dns_parse_ipv6 parses a full-form IPv6 address (8 hex groups) or a compressed form with a single "::" into 16 bytes. Returns None on invalid input. Delegates to the canonical xiom.net.ip6 (parity proven in p_dns_parity).

• Postcondition: ((s.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 2))

fn dns_ipv6_to_str(bytes: &Vec[UInt8]) -> Option[Str]

dns_ipv6_to_str formats 16 bytes as a full-form IPv6 address (8 groups, no "::" compression). Delegates to the canonical xiom.net.ip6 (same full-form convention; parity proven in p_dns_parity).

• Postcondition: ((bytes.len() != 16) => (result.is_none == true)) && ((result.is_some == true) => (bytes.len() == 16))

fn dns_parse_record_line(line: Str) -> Option[(Str, Str, Str)]

dns_parse_record_line parses a presentation-format zone record line such as "example.com. 3600 IN A 93.184.216.34" into (name, type, rdata).

• Postcondition: ((line.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (line.len() >= 7))

fn dns_is_valid_hostname(name: Str) -> Bool

dns_is_valid_hostname validates a hostname: labels of [A-Za-z0-9-] with no leading/trailing hyphen, 1-63 chars each, total length <= 253, at least one label, and no empty labels. A single trailing dot is allowed.

• Postcondition: ((name.len() == 0) => (result == false)) && ((result == true) => (name.len() <= 253))

fn dns_reverse_ipv4(octets: &Vec[UInt8]) -> Option[Str]

dns_reverse_ipv4 formats 4 bytes as the in-addr.arpa reverse name, or None if the length is not 4.

• Postcondition: ((octets.len() != 4) => (result.is_none == true)) && ((result.is_some == true) => (octets.len() == 4))

fn dns_well_known_port(service: Str) -> Option[Int]

dns_well_known_port maps a well-known service name to its default port, or None for unknown services.

• Postcondition: ((service.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (service.len() >= 3))

---

---

---

ftp.xi

fn ftp_default_port() -> Int

ftp_default_port returns the default FTP control port (21). Complexity: O(1). Pure.

• Postcondition: result == 21

fn ftp_command_user(user: Str) -> Str

ftp_command_user formats a USER command. Complexity: O(1). Pure.

• Postcondition: result.len() == user.len() + 7

fn ftp_command_pass(pass: Str) -> Str

ftp_command_pass formats a PASS command. Complexity: O(1). Pure.

• Postcondition: result.len() == pass.len() + 7

fn ftp_command_retr(path: Str) -> Str

ftp_command_retr formats a RETR command for a remote path. Complexity: O(1). Pure.

• Postcondition: result.len() == path.len() + 7

fn ftp_command_stor(path: Str) -> Str

ftp_command_stor formats a STOR command for a remote path. Complexity: O(1). Pure.

• Postcondition: result.len() == path.len() + 7

fn ftp_command_list(path: Str) -> Str

ftp_command_list formats a LIST command with an optional path. Complexity: O(1). Pure.

• Postcondition: ((path.len() == 0) => (result.len() == 6)) && ((path.len() > 0) => (result.len() == path.len() + 7))

fn ftp_command_quit() -> Str

ftp_command_quit formats a QUIT command. Complexity: O(1). Pure.

• Postcondition: result.len() == 6

fn ftp_command_cwd(dir: Str) -> Str

ftp_command_cwd formats a CWD command. Complexity: O(1). Pure.

• Postcondition: result.len() == dir.len() + 6

fn ftp_command_type(kind: Str) -> Str

ftp_command_type formats a TYPE command (A or I). Complexity: O(1). Pure.

• Postcondition: result.len() == kind.len() + 7

fn ftp_parse_reply(line: Str) -> Option[(Int, Str)]

ftp_parse_reply parses an FTP reply line like "220 Ready" into (code, text). Returns None if the line does not start with a 3-digit code. Complexity: O(1). Pure.

• Postcondition: ((line.len() < 3) => (result.is_none == true)) && ((result.is_some == true) => (line.len() >= 3))

fn ftp_reply_is_success(code: Int) -> Bool

ftp_reply_is_success returns true for 2xx replies. Complexity: O(1). Pure.

• Postcondition: result == (code >= 200 && code < 300)

fn ftp_reply_is_positive_preliminary(code: Int) -> Bool

ftp_reply_is_positive_preliminary returns true for 1xx replies. Complexity: O(1). Pure.

• Postcondition: result == (code >= 100 && code < 200)

---

---

---

h2.xi

type H2FrameHeader

Decoded HTTP/2 frame header. length is the payload length (24-bit), stream_id has the reserved bit cleared (31-bit).

Field	Type
length	Int
frame_type	Int
flags	Int
stream_id	Int

fn h2_frame_header_encode(length: Int, frame_type: Int, flags: Int, stream_id: Int) -> Result[Vec[UInt8], Str]

Encode the 9-byte HTTP/2 frame header. Err when any field is outside its wire range (length 0..=0xFFFFFF, type/flags 0..=0xFF, stream id 0..=0x7FFFFFFF). The reserved stream-id bit is emitted as 0.

• Postcondition: (length < 0 || length > 16777215 || frame_type < 0 || frame_type > 255 || flags < 0 || flags > 255 || stream_id < 0 || stream_id > 2147483647) => (result.is_err)
• Postcondition: (length >= 0 && length <= 16777215 && frame_type >= 0 && frame_type <= 255 && flags >= 0 && flags <= 255 && stream_id >= 0 && stream_id <= 2147483647) => (result.is_ok)

fn h2_frame_header_decode(bytes: &Vec[UInt8]) -> Result[H2FrameHeader, Str]

Decode the 9-byte HTTP/2 frame header. Err("h2: incomplete frame header") when fewer than 9 bytes are available; the reserved stream-id bit is masked off.

• Postcondition: (bytes.len() < 9) => (result.is_err)
• Postcondition: (bytes.len() >= 9) => (result.is_ok)

fn h2_frame_encode(frame_type: Int, flags: Int, stream_id: Int, payload: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

Encode one complete HTTP/2 frame: the 9-byte header (length derived from payload) followed by the payload. Err on an out-of-range type/flags/ stream id or a payload longer than the 24-bit frame limit.

• Postcondition: (payload.len() > 16777215) => (result.is_err)
• Postcondition: (payload.len() <= 16777215 && frame_type >= 0 && frame_type <= 255 && flags >= 0 && flags <= 255 && stream_id >= 0 && stream_id <= 2147483647) => (result.is_ok)

fn h2_frame_decode(bytes: &Vec[UInt8]) -> Result[(H2FrameHeader, Vec[UInt8]), Str]

Decode one complete frame at the start of bytes (header + payload). Err on a short header, a short payload, or an invalid header field.

• Postcondition: (bytes.len() < 9) => (result.is_err)

type H2HeaderBlock

A header block being reassembled from one HEADERS frame and zero or more CONTINUATION frames. bytes is the concatenated header-block fragment.

Field	Type
stream_id	Int
bytes	Vec[UInt8]
complete	Bool

fn h2_header_block_new(stream_id: Int, payload: &Vec[UInt8], end_headers: Bool) -> H2HeaderBlock

Start a header block from a HEADERS payload (padding/priority already stripped by the caller). end_headers sets the complete flag.

• Precondition: stream_id > 0
• Postcondition: result.stream_id == stream_id
• Postcondition: result.complete == end_headers
• Postcondition: result.bytes.len() == payload.len()

fn h2_header_block_append(block: &mut H2HeaderBlock, frame_type: Int, flags: Int, stream_id: Int, payload: &Vec[UInt8]) -> Result[Bool, Str]

Append a CONTINUATION payload. Err when the block is already complete, the frame is not CONTINUATION, or the stream id differs. Returns whether the block is complete after the append.

• Precondition: block.stream_id > 0

fn h2_header_block_is_complete(block: &H2HeaderBlock) -> Bool

True once END_HEADERS has been seen.

• Postcondition: result == block.complete

fn h2_header_block_len(block: &H2HeaderBlock) -> Int

Total reassembled header-block length in bytes.

• Postcondition: result == block.bytes.len()

fn h2_header_block_to_bytes(block: &H2HeaderBlock) -> Vec[UInt8]

Copy the reassembled header-block bytes (for h2_hpack_* input).

• Postcondition: result.len() == block.bytes.len()

type H2Setting

One SETTINGS entry (6 bytes on the wire: 2-byte id, 4-byte value).

Field	Type
id	Int
value	Int

fn h2_settings_new() -> Vec[H2Setting]

New empty SETTINGS list. Module-side constructor so callers do not have to spell a qualified generic type (which the compiler erases at call sites).

• Postcondition: result.len() == 0

fn h2_settings_add(settings: &mut Vec[H2Setting], id: Int, value: Int)

Append one SETTINGS entry to a caller-owned list.

• Precondition: true

fn h2_settings_encode(settings: &Vec[H2Setting]) -> Result[Vec[UInt8], Str]

Encode a SETTINGS payload (6 bytes per entry). Err when an id is outside 0..=0xFFFF or a value outside 0..=0xFFFFFFFF.

• Precondition: true

fn h2_settings_decode(payload: &Vec[UInt8]) -> Result[Vec[H2Setting], Str]

Decode a SETTINGS payload. Err when the length is not a multiple of 6.

• Postcondition: (payload.len() % 6 != 0) => (result.is_err)

fn h2_settings_decode_into(payload: &Vec[UInt8], out: &mut Vec[H2Setting]) -> Result[Unit, Str]

Decode a SETTINGS payload into a caller-owned list. Preferred over the returning form when the caller inspects the struct fields: a nested generic return (Result[Vec[H2Setting], Str]) is type-erased at some call sites. The list is cleared first.

• Postcondition: (payload.len() % 6 != 0) => (result.is_err)

fn h2_settings_validate(settings: &Vec[H2Setting]) -> Result[Unit, Str]

Validate the SETTINGS entries: duplicate ids, ENABLE_PUSH 0/1, INITIAL_WINDOW_SIZE <= 2^31-1, and MAX_FRAME_SIZE 16384..=16777215. Unknown ids are accepted (RFC 9113 section 6.5.2).

• Precondition: true

type H2Window

A one-direction HTTP/2 flow-control window.

Field	Type
available	Int
initial	Int

fn h2_window_new(initial: Int) -> H2Window

Create a window with initial available bytes.

• Precondition: initial >= 0 && initial <= H2_MAX_WINDOW
• Postcondition: result.available == initial
• Postcondition: result.initial == initial

fn h2_window_available(w: &H2Window) -> Int

Current available window bytes.

• Postcondition: result == w.available

fn h2_window_consume(w: &mut H2Window, n: Int) -> Result[Int, Str]

Consume up to n bytes. Err on a negative value or an underflow.

• Precondition: w.available >= 0 && w.available <= H2_MAX_WINDOW

fn h2_window_increment(w: &mut H2Window, n: Int) -> Result[Int, Str]

Add n bytes (WINDOW_UPDATE). Err on a non-positive value or overflow.

• Precondition: w.available >= 0 && w.available <= H2_MAX_WINDOW

fn h2_window_resize(w: &mut H2Window, new_initial: Int) -> Result[Int, Str]

Apply a SETTINGS INITIAL_WINDOW_SIZE change: shift available by the difference and record the new initial. Err when the shift underflows or overflows.

• Precondition: new_initial >= 0 && new_initial <= H2_MAX_WINDOW
• Precondition: w.available >= 0 && w.available <= H2_MAX_WINDOW

enum H2StreamState

Per-stream HTTP/2 state.

• Idle
• Open
• HalfClosedLocal
• HalfClosedRemote
• Closed

enum H2StreamEvent

Events that drive the per-stream state machine. HEADERS/DATA with END_STREAM are modelled as the frame event followed by the EndStream event.

• SendHeaders
• RecvHeaders
• SendData
• RecvData
• SendEndStream
• RecvEndStream
• SendRst
• RecvRst

fn h2_stream_state_name(state: H2StreamState) -> Str

Stable diagnostic name for a stream state.

• Precondition: true

fn h2_stream_transition(state: H2StreamState, event: H2StreamEvent) -> Result[H2StreamState, Str]

Apply one event to a stream state. Err on a protocol-invalid transition (for example DATA on an idle stream, a send after local END_STREAM, or any event on a closed stream).

• Precondition: true

fn h2_stream_id_next(last_id: Int, local_is_client: Bool) -> Result[Int, Str]

Next locally initiated stream id. Client ids are odd, server ids even; last_id is the last locally used id (0 = none). Err above 2^31-1.

• Precondition: last_id >= 0 && last_id <= 2147483647

fn h2_stream_id_is_client(id: Int) -> Bool

True for client-initiated (odd) stream ids.

• Precondition: id > 0

fn h2_rst_stream_encode(error_code: Int) -> Result[Vec[UInt8], Str]

RST_STREAM payload (4-byte error code).

• Postcondition: (error_code < 0 || error_code > 4294967295) => (result.is_err)

fn h2_rst_stream_decode(payload: &Vec[UInt8]) -> Result[Int, Str]

Decode a RST_STREAM payload. Err when the length is not 4.

• Postcondition: (payload.len() != 4) => (result.is_err)

fn h2_goaway_encode(last_stream_id: Int, error_code: Int, debug: &Vec[UInt8]) -> Result[Vec[UInt8], Str]

GOAWAY payload: last stream id (31 bits), error code, debug data.

• Postcondition: (last_stream_id < 0 || last_stream_id > 2147483647 || error_code < 0 || error_code > 4294967295) => (result.is_err)

fn h2_goaway_decode_into(payload: &Vec[UInt8], debug: &mut Vec[UInt8]) -> Result[(Int, Int), Str]

Decode GOAWAY into (last_stream_id, error_code) and copy the debug data into the caller-owned vector. The last-id reserved bit is masked.

• Postcondition: (payload.len() < 8) => (result.is_err)

fn h2_window_update_encode(increment: Int) -> Result[Vec[UInt8], Str]

WINDOW_UPDATE payload (4-byte increment, reserved bit 0, 1..=2^31-1).

• Postcondition: (increment < 1 || increment > 2147483647) => (result.is_err)

fn h2_window_update_decode(payload: &Vec[UInt8]) -> Result[Int, Str]

Decode a WINDOW_UPDATE payload; the reserved bit is masked and an increment of 0 is a protocol error.

• Postcondition: (payload.len() != 4) => (result.is_err)

fn h2_hpack_int_encode(value: Int, prefix_bits: Int, first_byte: Int) -> Result[Vec[UInt8], Str]

Encode an HPACK integer (RFC 7541 section 5.1) with a prefix_bits-wide prefix. first_byte supplies the high bits (pattern bits); its low prefix_bits are replaced. Err on a negative value or a prefix outside 1..=8.

• Postcondition: (value < 0 || prefix_bits < 1 || prefix_bits > 8 || first_byte < 0 || first_byte > 255) => (result.is_err)
• Postcondition: (value >= 0 && prefix_bits >= 1 && prefix_bits <= 8 && first_byte >= 0 && first_byte <= 255) => (result.is_ok)

fn h2_hpack_int_decode(bytes: &Vec[UInt8], pos: Int, prefix_bits: Int) -> Result[(Int, Int), Str]

Decode an HPACK integer at pos. Returns (value, consumed bytes). Err on an invalid position/prefix, a truncated continuation, or an overflow.

• Postcondition: (pos < 0 || pos >= bytes.len() || prefix_bits < 1 || prefix_bits > 8) => (result.is_err)

fn h2_hpack_string_encode(s: Str) -> Vec[UInt8]

Encode an HPACK string without Huffman coding (H=0): the 7-bit length prefix followed by the raw bytes.

• Postcondition: result.len() >= 1

fn h2_hpack_string_decode(bytes: &Vec[UInt8], pos: Int) -> Result[(Str, Int), Str]

Decode an HPACK string at pos. Returns (string, consumed bytes). Both H=0 and H=1 (Huffman) string bodies are supported.

• Postcondition: (pos < 0 || pos >= bytes.len()) => (result.is_err)

type H2HpackDynamicTable

HPACK dynamic table. Entries are stored oldest-first; dynamic index 1 is the most recently added entry. An entry costs name.len + value.len + 32 bytes (RFC 7541 section 4.1).

Field	Type
names	Vec[Str]
values	Vec[Str]
size	Int
max_size	Int

fn h2_hpack_dynamic_new(max_size: Int) -> H2HpackDynamicTable

Create an empty dynamic table with the given maximum size in bytes.

• Precondition: max_size >= 0
• Postcondition: result.size == 0
• Postcondition: result.max_size == max_size

fn h2_hpack_dynamic_len(t: &H2HpackDynamicTable) -> Int

Number of entries currently in the dynamic table.

• Postcondition: result == t.names.len()

fn h2_hpack_dynamic_size(t: &H2HpackDynamicTable) -> Int

Current byte size of the dynamic table.

• Postcondition: result == t.size

fn h2_hpack_dynamic_add(t: &mut H2HpackDynamicTable, name: Str, value: Str)

Insert (name, value) as the newest entry, evicting oldest entries until it fits. An entry larger than max_size clears the table and is not inserted.

• Precondition: t.max_size >= 0

fn h2_hpack_dynamic_get(t: &H2HpackDynamicTable, index: Int) -> Option[(Str, Str)]

Look up dynamic index (1 = newest). None when the index is outside 1..=len. Complexity: O(1).

• Precondition: true

fn h2_hpack_dynamic_set_max(t: &mut H2HpackDynamicTable, max_size: Int)

Set the maximum table size and evict until the size fits.

• Precondition: max_size >= 0

fn h2_hpack_dynamic_clear(t: &mut H2HpackDynamicTable)

Remove every entry (size becomes 0; max_size is preserved).

• Precondition: true

fn h2_hpack_huffman_decode(bytes: &Vec[UInt8]) -> Result[Str, Str]

Decode an RFC 7541 Huffman-coded string body (without the H bit/length prefix). Err on an invalid code, EOS, or bad padding.

• Precondition: true

fn h2_hpack_huffman_encode(s: Str) -> Vec[UInt8]

Encode a string body with the RFC 7541 Huffman code, padding the final byte with one-bits. The returned bytes do NOT include the H bit/length prefix; use h2_hpack_string_encode_huffman for a complete HPACK string.

• Precondition: true

fn h2_hpack_string_encode_huffman(s: Str) -> Vec[UInt8]

Encode a complete HPACK string with H=1: the 7-bit length prefix (with the high bit set) followed by the Huffman-coded bytes.

• Postcondition: result.len() >= 1

fn h2_hpack_static_len() -> Int

Number of HPACK static-table entries (61).

• Postcondition: result == 61

fn h2_hpack_static_name(index: Int) -> Option[Str]

Name of static-table entry index, or None when out of range (1..=61).

• Postcondition: (index < 1 || index > 61) => (result.is_none)

fn h2_hpack_static_value(index: Int) -> Option[Str]

Value of static-table entry index, or None when out of range (1..=61).

• Postcondition: (index < 1 || index > 61) => (result.is_none)

fn h2_hpack_static_find_name(name: Str) -> Option[Int]

First static-table index whose name equals name, or None. The first match is the canonical name index (e.g. ":method" -> 2).

• Postcondition: (name.len() == 0) => (result.is_none)

fn h2_hpack_static_find(name: Str, value: Str) -> Option[Int]

Exact static-table (name, value) index, or None.

• Postcondition: (name.len() == 0) => (result.is_none)

fn h2_hpack_encode_header(name: Str, value: Str) -> Result[Vec[UInt8], Str]

Encode one header field. An exact static (name, value) pair becomes an indexed field; otherwise a literal without indexing is emitted, using a static name index when the name is known or a new-name string otherwise. Huffman coding is not used. Err on an empty name.

• Postcondition: (name.len() == 0) => (result.is_err)

fn h2_hpack_decode_header(bytes: &Vec[UInt8], pos: Int) -> Result[(Str, Str, Int), Str]

Decode one header field at pos. Returns (name, value, consumed bytes). Supported: indexed static fields and literal fields without indexing (indexed or new name). Dynamic-table inserts (0x40), dynamic indexes (>61) and Huffman strings are rejected explicitly.

• Postcondition: (pos < 0 || pos >= bytes.len()) => (result.is_err)

type H2Connection

Connection-level multiplexing state for one HTTP/2 connection. active holds the locally initiated streams that are still open; draining means no new local streams may open (a GOAWAY was sent or received); peer_goaway distinguishes a received GOAWAY from a local graceful shutdown; goaway_last_id/goaway_error record the last stream id that may still be processed and the advertised error code.

Field	Type
local_is_client	Bool
max_concurrent	Int
last_local_id	Int
active	Vec[Int]
draining	Bool
peer_goaway	Bool
goaway_last_id	Int
goaway_error	Int

fn h2_conn_new(max_concurrent: Int, local_is_client: Bool) -> H2Connection

Create a connection state. max_concurrent <= 0 clamps to 1. Parameters: max_concurrent -- the peer's concurrency limit; local_is_client -- true for odd (client) local stream ids. Complexity: O(1).

• Postcondition: result.max_concurrent >= 1
• Postcondition: result.active.len() == 0
• Postcondition: result.draining == false

fn h2_conn_can_open(c: &H2Connection) -> Bool

True when a new local stream may be opened (not draining, under the concurrency cap). Complexity: O(1).

• Postcondition: result == (c.draining == false && c.peer_goaway == false && c.active.len() < c.max_concurrent)

fn h2_conn_open_stream(c: &mut H2Connection) -> Option[Int]

Allocate the next local stream id and mark it active. Returns None when draining, at the concurrency cap, or when the id space is exhausted. Complexity: O(1).

• Postcondition: (result.is_some == true) => (c.active.len() >= 1)

fn h2_conn_close_stream(c: &mut H2Connection, id: Int) -> Bool

Mark one local stream closed. False when the id is not active. Complexity: O(n) in the active count.

• Postcondition: (result == true) => (c.active.len() <= c.max_concurrent)

fn h2_conn_active(c: &H2Connection) -> Int

Number of locally initiated streams still open. Complexity: O(1).

• Postcondition: result >= 0 && result <= c.max_concurrent

fn h2_conn_recv_goaway(c: &mut H2Connection, last_stream_id: Int, error_code: Int) -> Bool

Handle a received GOAWAY. last_stream_id is the peer's last processed stream; local streams above it are dropped (they were not processed, so the caller may retry them). Returns false for out-of-range values or a GOAWAY that increases a previously received last-stream-id (RFC 9113 section 6.8 forbids that). Complexity: O(n) in the active count.

• Postcondition: (result == true) => (c.peer_goaway == true)
• Postcondition: (result == true) => (c.draining == true)

fn h2_conn_begin_drain(c: &mut H2Connection, last_processed_id: Int, error_code: Int) -> Bool

Start a local graceful shutdown. last_processed_id is the last peer-initiated stream the caller has processed (it goes into the GOAWAY frame); no new local stream opens afterwards. Returns false for out-of-range values or a last-stream-id that increases a previous GOAWAY's value. Complexity: O(1).

• Postcondition: (result == true) => (c.draining == true)

fn h2_conn_is_draining(c: &H2Connection) -> Bool

True once a GOAWAY was sent or received (no new local streams). Complexity: O(1).

• Postcondition: result == (c.draining == true)

fn h2_conn_is_closed(c: &H2Connection) -> Bool

True when draining and every locally initiated stream is closed: the connection may be closed. Complexity: O(1).

• Postcondition: (result == true) => (c.draining == true && c.active.len() == 0)

fn h2_conn_goaway_last_id(c: &H2Connection) -> Int

Last stream id recorded by the most recent GOAWAY (0 when none). Complexity: O(1).

• Postcondition: result >= 0

fn h2_conn_goaway_error(c: &H2Connection) -> Int

Error code recorded by the most recent GOAWAY (0 when none). Complexity: O(1).

• Postcondition: result >= 0

---

---

---

h2_io.xi

type H2Reader

Buffered HTTP/2 frame reader over a TcpStream. buf/start hold the read buffer and its consumed-prefix cursor; max_payload is the accepted frame payload size; closed records EOF.

Field	Type
stream	TcpStream
buf	Vec[UInt8]
start	Int
max_payload	Int
closed	Bool

fn h2_reader_new(stream: TcpStream, max_payload: Int) -> H2Reader

Create a frame reader. max_payload <= 0 selects 16384; values above 0xFFFFFF are clamped. Parameters: stream -- the transport; max_payload -- accepted payload cap. Complexity: O(1).

• Postcondition: result.max_payload >= 1
• Postcondition: result.max_payload <= 16777215

fn h2_reader_available(r: &H2Reader) -> Int

Bytes buffered but not yet consumed. Complexity: O(1).

• Postcondition: result >= 0

fn h2_reader_read_frame(r: &mut H2Reader) -> Result[(H2FrameHeader, Vec[UInt8]), Str]

Read one complete frame. Err on EOF (no partial header), a closed stream mid-frame, a payload above max_payload, or a transport failure. Complexity: O(frame).

• Postcondition: true

fn h2_join_header_block(r: &mut H2Reader, first: (H2FrameHeader, Vec[UInt8]), max_block: Int) -> Result[Vec[UInt8], Str]

Join a HEADERS frame payload with its CONTINUATION frames until END_HEADERS. Err when the first frame is not HEADERS, an intermediate frame is not CONTINUATION on the same stream, or the block exceeds max_block (<=0 selects 1 MiB). Parameters: r -- the reader; first -- the HEADERS frame just read; max_block -- the assembled block cap. Complexity: O(block).

• Postcondition: true

fn h2_reader_close(r: &mut H2Reader)

Close the underlying socket and mark the reader closed. Complexity: O(1).

• Postcondition: r.closed == true

fn h2_write_frame(stream: &TcpStream, frame_type: Int, flags: Int, stream_id: Int, payload: &Vec[UInt8]) -> Result[Int, Str]

Encode and write one frame. Returns the bytes written. Parameters: stream -- the transport; frame_type/flags/stream_id -- the frame header; payload -- the frame payload. Complexity: O(payload).

• Postcondition: (result.is_ok == true) => (result.value >= 9)

fn h2_write_settings_ack(stream: &TcpStream) -> Result[Int, Str]

Write an empty SETTINGS frame with the ACK flag on stream 0. Complexity: O(1).

• Postcondition: (result.is_ok == true) => (result.value == 9)

fn h2_write_ping_ack(stream: &TcpStream, payload: &Vec[UInt8]) -> Result[Int, Str]

Write a PING ACK carrying the 8-byte opaque payload. Complexity: O(1).

• Postcondition: (payload.len() != 8) => (result.is_err == true)
• Postcondition: (result.is_ok == true) => (result.value == 9 + payload.len())

fn h2_write_header_block(stream: &TcpStream, stream_id: Int, block: &Vec[UInt8], end_stream: Bool, max_frame: Int) -> Result[Int, Str]

Write a header block as HEADERS + CONTINUATION frames. The first frame carries END_STREAM when end_stream; the last carries END_HEADERS. max_frame <= 0 selects 16384. Returns the total bytes written. Parameters: stream -- the transport; stream_id -- the stream; block -- the encoded header block; end_stream -- END_STREAM on the HEADERS frame; max_frame -- fragment size. Complexity: O(block).

• Postcondition: (stream_id < 0 || stream_id > 2147483647) => (result.is_err == true)

---

---

---

header.xi

fn header_get(headers: &Vec[(Str, Str)], name: Str) -> Option[Str]

Fetch the first value for a header name (case-insensitive). Parameters: headers -- the header list; name -- the header name. Returns: Some(first value) when present, None otherwise. Complexity: O(n) with n = header count. Pure.

• Postcondition: ((headers.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (headers.len() > 0))

fn header_set(headers: &mut Vec[(Str, Str)], name: Str, value: Str)

Set a header, replacing any existing entry with the same name (case-insensitive); the new entry keeps the caller's spelling. Parameters: headers -- the mutable header list; name -- the header name; value -- the header value. Returns: Unit. Complexity: O(n) with n = header count. Pure.

• Postcondition: headers.len() >= 1

fn header_remove(headers: &mut Vec[(Str, Str)], name: Str) -> Bool

Remove all entries for a header name (case-insensitive). Parameters: headers -- the mutable header list; name -- the header name. Returns: true when at least one entry was removed. Complexity: O(n) with n = header count. Pure.

• Postcondition: headers.len() >= 0

fn header_contains(headers: &Vec[(Str, Str)], name: Str) -> Bool

Test if a header name is present (case-insensitive). Parameters: headers -- the header list; name -- the header name. Returns: true when at least one entry matches. Complexity: O(n) with n = header count. Pure.

• Postcondition: ((headers.len() == 0) => (result == false)) && ((result == true) => (headers.len() > 0))

fn header_parse_line(line: Str) -> Option[(Str, Str)]

Parse one "Name: value" line into a (name, value) pair. Parameters: line -- a single header line (may include a trailing CRLF). Returns: Some((name, value)) for a well-formed line, None otherwise. The name is preserved verbatim; the value is trimmed. Complexity: O(n). Pure.

• Postcondition: ((line.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (line.len() >= 2))

fn header_serialize(headers: &Vec[(Str, Str)]) -> Str

Serialize headers into "Name: value" lines. Parameters: headers -- the header list. Returns: the concatenated header block; each line ends with CRLF. Complexity: O(n) with n = header count. Pure.

• Postcondition: result.len() >= 4 * headers.len() && ((headers.len() == 0) => (result.len() == 0))

---

---

---

http.xi

type HttpResponse

type HttpResponse - an HTTP response: status code (Int), headers, and raw body bytes.

Field	Type
status	Int
headers	Vec[(Str, Str)]
body	Vec[UInt8]

Derives: Clone

fn http_status_text(code: Int) -> Str

http_status_text returns the standard reason phrase for a status code, or "Unknown" for codes not in the table. Complexity: O(1).

• Postcondition: result.len() > 0 && ((code == 200) => (result == "OK")) && ((code == 404) => (result == "Not Found")) && ((code == 500) => (result == "Internal Server Error"))

fn http_request_line(method: Str, target: Str) -> Str

http_request_line builds the request line for a method and target, e.g. http_request_line("GET", "/") == "GET / HTTP/1.1". Complexity: O(1). Pure.

• Postcondition: result == method + " " + target + " HTTP/1.1"

fn http_build_request(method: Str, url_str: Str, headers: &Vec[(Str, Str)], body: &Vec[UInt8]) -> Result[Str, Str]

http_build_request builds a full HTTP/1.1 request text from a parsed URL, method, headers, and body. Used by the client and exposed for callers that want to send raw requests themselves.

• Postcondition: ((url_str.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (url_str.len() != 0))

fn http_response_status(raw: Str) -> Option[Int]

http_response_status extracts the HTTP status code from a raw response without allocating a full response value. Returns None if the status line is malformed. Complexity: O(1). Pure.

• Postcondition: (raw.len() < 4) => (result.is_some == false)

fn http_parse_response_headers(raw: Str) -> Vec[(Str, Str)]

http_parse_response_headers extracts the (name, value) header pairs from a raw HTTP response block (everything after the status line and before the blank line). Complexity: O(n). Pure.

• Postcondition: ((raw.len() == 0) => (result.len() == 0)) && ((result.len() > 0) => (raw.len() > 0))

fn http_parse_response(raw: Str) -> Result[HttpResponse, Str]

http_parse_response parses a raw HTTP/1.1 response into an HttpResponse. Invalid input returns Err. Complexity: O(n). Pure.

• Postcondition: ((raw.len() < 4) => (result.is_err == true)) && ((result.is_ok == true) => (raw.len() >= 4))

fn http_status_code(resp: &HttpResponse) -> Int

http_status_code returns the HTTP status code of a response. Complexity: O(1). Pure.

• Postcondition: result == resp.status

fn http_header(resp: &HttpResponse, name: Str) -> Option[Str]

http_header returns the value of a named response header (matched case-insensitively), or None if absent. Complexity: O(h). Pure.

• Postcondition: ((resp.headers.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (resp.headers.len() > 0))

fn http_body_text(resp: &HttpResponse) -> Str

http_body_text decodes the response body bytes as UTF-8 text. Complexity: O(n). Pure.

• Postcondition: (resp.body.len() == 0) => (result.len() == 0)

fn http_url_encode(s: Str) -> Str

http_url_encode percent-encodes a string for use in a URL. Complexity: O(n). Pure.

• Postcondition: result.len() >= s.len() && result.len() <= s.len() * 3 && ((s.len() == 0) => (result.len() == 0))

fn http_url_decode(s: Str) -> Result[Str, Str]

http_url_decode percent-decodes a URL-encoded string. Returns Err on truncated or invalid escapes. Complexity: O(n). Pure.

• Postcondition: ((s.len() == 0) => (result.is_ok == true)) && ((result.is_err == true) => (s.len() > 0))

fn http_get(url: Str) -> Result[HttpResponse, Str]

http_get performs an HTTP GET request and returns the response. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_post(url: Str, body: &Vec[UInt8]) -> Result[HttpResponse, Str]

http_post performs an HTTP POST with a raw byte body. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_put(url: Str, body: &Vec[UInt8]) -> Result[HttpResponse, Str]

http_put performs an HTTP PUT with a raw byte body. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_delete(url: Str) -> Result[HttpResponse, Str]

http_delete performs an HTTP DELETE request. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_head(url: Str) -> Result[HttpResponse, Str]

http_head performs an HTTP HEAD request. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_patch(url: Str, body: &Vec[UInt8]) -> Result[HttpResponse, Str]

http_patch performs an HTTP PATCH with a raw byte body. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_get_text(url: Str) -> Result[Str, Str]

http_get_text performs an HTTP GET and returns the response body decoded as text. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_get_bytes(url: Str) -> Result[Vec[UInt8], Str]

http_get_bytes performs an HTTP GET and returns the raw body bytes. Complexity: network I/O.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_redirect_follow(url: Str, max: Int) -> Result[HttpResponse, Str]

http_redirect_follow follows up to max HTTP redirects (301/302/303/ 307/308) before returning the final response. Complexity: network I/O.

• Postcondition: ((max < 0) => (result.is_err == true)) && ((url.len() == 0) => (result.is_err == true))

fn http_request(method: Str, url: Str, headers: &Vec[(Str, Str)], body: &Vec[UInt8]) -> Result[HttpResponse, Str]

http_request performs a generic HTTP request; each tuple in headers is a (name, value) header pair. Complexity: network I/O.

• Postcondition: ((url.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (url.len() != 0))

---

---

---

https.xi

fn https_default_port() -> Int

https_default_port returns the default HTTPS port (443). Complexity: O(1). Pure.

• Postcondition: result == 443

fn https_request_line(method: Str, target: Str) -> Str

https_request_line builds the request line for a method and target, e.g. https_request_line("GET", "/") == "GET / HTTP/1.1". Complexity: O(1). Pure.

• Postcondition: result.len() == method.len() + target.len() + 10

fn https_build_request(method: Str, url_str: Str, headers: &Vec[(Str, Str)], body: &Vec[UInt8]) -> Result[Str, Str]

https_build_request builds a full HTTPS request text from a URL, method, headers, and body. The Host header carries the explicit port only when it differs from 443. Complexity: O(n). Pure.

• Postcondition: result is Ok(_) => result.value.len() >= 18

fn https_status_text(code: Int) -> Str

https_status_text returns the standard reason phrase for a status code, or "Unknown" for codes not in the table. Complexity: O(1).

• Postcondition: result.len() > 0

fn https_response_status(raw: Str) -> Option[Int]

https_response_status extracts the HTTP status code from a raw response. Returns None if malformed. Complexity: O(1). Pure.

• Postcondition: result is Some(_) => result.value >= 0 && result.value <= 999

fn https_parse_response_headers(raw: Str) -> Vec[(Str, Str)]

https_parse_response_headers extracts the (name, value) header pairs from a raw response block. Complexity: O(n). Pure.

• Postcondition: ((raw.len() == 0) => (result.len() == 0)) && ((result.len() > 0) => (raw.len() > 0))

fn https_url_encode(s: Str) -> Str

https_url_encode percent-encodes a string for use in a URL. Complexity: O(n). Pure.

• Postcondition: result.len() >= s.len() && result.len() <= s.len() * 3 && ((s.len() == 0) => (result.len() == 0))

fn https_url_decode(s: Str) -> Result[Str, Str]

https_url_decode percent-decodes a URL-encoded string. Complexity: O(n). Pure.

• Postcondition: ((s.len() == 0) => (result.is_ok == true)) && ((result.is_err == true) => (s.len() > 0))

---

---

---

ip.xi

enum IpAddr

type IpAddr - an IP address enum: V4 holding four octets, V6 holding eight 16-bit parts.

• V4(octets: Vec[UInt8])
• V6(parts: Vec[UInt16])

fn ipv4_parse(s: Str) -> Option[Vec[UInt8]]

Parse a dotted-quad IPv4 string into four octets. Parameters: s -- the address string. Returns: Some(four octets) for a valid address, None otherwise. Complexity: O(n). Pure.

• Postcondition: (result.is_some == false) || ((s.len() >= 7) && (s.len() <= 15))

fn ipv4_to_string(octets: &Vec[UInt8]) -> Str

Format four octets as a dotted-quad IPv4 string. Parameters: octets -- at least four octets (only the first four are used). Returns: the "a.b.c.d" representation, or "" for an undersized vector. Complexity: O(1). Pure.

• Postcondition: (result == "") || ((octets.len() >= 4) && (result.len() >= 7))

fn ipv6_parse(s: Str) -> Option[Vec[UInt16]]

Parse an IPv6 string (full form or single "::" compression) into eight 16-bit groups. Parameters: s -- the address string. Returns: Some(eight groups) for a valid address, None otherwise. Complexity: O(n). Pure.

• Postcondition: (result.is_some == false) || (s.len() >= 2)

fn ipv6_to_string(parts: &Vec[UInt16]) -> Str

Format eight 16-bit parts as a full-form IPv6 string (no "::" compression, leading zeros elided). Parameters: parts -- exactly eight 16-bit groups. Returns: the colon-separated string, or "" for a vector of the wrong size. Complexity: O(8). Pure.

• Postcondition: (result == "") || ((parts.len() == 8) && (result.len() >= 15))

fn ip_parse(s: Str) -> Option[IpAddr]

Parse an IPv4 or IPv6 string into an IpAddr. Parameters: s -- the address string. Returns: Some(IpAddr) for a valid address, None otherwise. Complexity: O(n). Pure.

• Postcondition: (result.is_some == false) || (s.len() >= 2)

fn ip_is_loopback(s: Str) -> Bool

Returns true for loopback addresses (127.0.0.0/8, ::1). Parameters: s -- the address string. Returns: true when the address parses and is loopback. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip_is_private(s: Str) -> Bool

Returns true for private-use ranges (10/8, 172.16/12, 192.168/16, fc00::/7). Parameters: s -- the address string. Returns: true when the address parses and is private-use. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip_is_link_local(s: Str) -> Bool

Returns true for link-local ranges (169.254/16, fe80::/10). Parameters: s -- the address string. Returns: true when the address parses and is link-local. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip_is_multicast(s: Str) -> Bool

Returns true for multicast ranges (224.0.0.0/4, ff00::/8). Parameters: s -- the address string. Returns: true when the address parses and is multicast. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip_is_unspecified(s: Str) -> Bool

Returns true for the all-zero address (0.0.0.0, ::). Parameters: s -- the address string. Returns: true when the address parses and is all zero. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip_masked(s: Str, prefix: Int) -> Str

Apply a CIDR prefix mask to an address and return the masked address string. Parameters: s -- the address string; prefix -- the prefix length (0..32 for IPv4, 0..128 for IPv6). Returns: the masked address, or "" for invalid input or an out-of-range prefix. Complexity: O(n). Pure.

• Postcondition: (result == "") || ((prefix >= 0) && (prefix <= 128) && (result.len() >= 7))

fn ip_in_subnet(ip: Str, subnet: Str) -> Bool

Test whether ip falls inside a CIDR subnet ("192.168.1.0/24" or "2001:db8::/32"). Parameters: ip -- the address string; subnet -- "address/prefix". Returns: true when the masked addresses are equal. Complexity: O(n). Pure.

• Postcondition: (result == true) => (subnet.len() >= 2)

fn ip_expand(s: Str) -> Str

Expand an IPv6 string to the full eight-part form with zero padding. Parameters: s -- the address string. Returns: the "0000:0000:...:0000" form, or "" for invalid input. IPv4 input is returned unchanged. Complexity: O(n). Pure.

• Postcondition: (result == "") || (result == s) || (result.len() == 39)

fn ip_compress(s: Str) -> Str

Compress an IPv6 string using "::" and leading-zero elision. Parameters: s -- the address string. Returns: the canonical compressed form, or "" for invalid input. IPv4 input is returned unchanged. Complexity: O(n). Pure.

• Postcondition: (result == "") || (result == s) || ((result.len() >= 2) && (result.len() <= 39))

fn ip_octets(s: Str) -> Vec[Int]

Split an IPv4 string into its numeric octets. Parameters: s -- the address string. Returns: four octets for a valid address, an empty vector otherwise. Complexity: O(n). Pure.

• Postcondition: (result.len() == 0) || (result.len() == 4)

---

---

---

ip4.xi

fn ip4_parse(s: Str) -> Result[Vec[UInt8], Str]

ip4_parse parses a dotted-quad IPv4 string into four octets. Invalid input (wrong segment count, non-numeric, or out-of-range octets) returns Err. Complexity: O(n). Pure.

• Postcondition: (result.is_ok == false) || ((s.len() >= 7) && (s.len() <= 15))

fn ip4_validate(s: Str) -> Bool

ip4_validate returns true if s is a valid dotted-quad IPv4 address. Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_to_str(octets: &Vec[UInt8]) -> Result[Str, Str]

ip4_to_str formats four octets as a dotted-quad string. Returns Err if octets.len() is not 4. Complexity: O(1). Pure.

• Postcondition: (result.is_ok == false) || (octets.len() == 4)

fn ip4_octets(s: Str) -> Vec[Int]

ip4_octets splits a dotted-quad IPv4 string into its four numeric octets as Int. Invalid input returns an empty vector. Pure.

• Postcondition: (result.len() == 0) || (result.len() == 4)

fn ip4_is_loopback(s: Str) -> Bool

ip4_is_loopback returns true for 127.0.0.0/8. Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_is_private(s: Str) -> Bool

ip4_is_private returns true for RFC 1918 ranges (10.0.0.0/8, 172.16.0.0/12, 192.168.0.0/16). Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_is_link_local(s: Str) -> Bool

ip4_is_link_local returns true for 169.254.0.0/16. Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_is_multicast(s: Str) -> Bool

ip4_is_multicast returns true for 224.0.0.0/4. Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_is_unspecified(s: Str) -> Bool

ip4_is_unspecified returns true for 0.0.0.0. Complexity: O(n). Pure.

• Postcondition: (result == true) => ((s.len() >= 7) && (s.len() <= 15))

fn ip4_is_broadcast(s: Str) -> Bool

ip4_is_broadcast returns true for 255.255.255.255. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s == "255.255.255.255")

---

---

---

ip6.xi

fn ip6_parse(s: Str) -> Result[Vec[UInt8], Str]

ip6_parse parses an IPv6 string (full form or with a single "::" compression) into 16 bytes. Invalid input returns Err. Complexity: O(n). Pure.

• Postcondition: (result.is_ok == false) || (s.len() >= 2)

fn ip6_validate(s: Str) -> Bool

ip6_validate returns true if s is a valid IPv6 address. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip6_to_str(bytes: &Vec[UInt8]) -> Result[Str, Str]

ip6_to_str formats 16 bytes as a full-form IPv6 address (eight 16-bit groups, no "::" compression). Returns Err if the length is not 16. Complexity: O(n). Pure.

• Postcondition: (result.is_ok == false) || (bytes.len() == 16)

fn ip6_expand(s: Str) -> Result[Str, Str]

ip6_expand returns the full eight-group form of an IPv6 string, expanding "::" and zero-padding each group to four hex digits. Returns Err on invalid input. Complexity: O(n). Pure.

• Postcondition: (result.is_ok == false) || (s.len() >= 2)

fn ip6_is_loopback(s: Str) -> Bool

ip6_is_loopback returns true for ::1. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip6_is_unspecified(s: Str) -> Bool

ip6_is_unspecified returns true for :: Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip6_is_multicast(s: Str) -> Bool

ip6_is_multicast returns true for ff00::/8. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

fn ip6_is_link_local(s: Str) -> Bool

ip6_is_link_local returns true for fe80::/10. Complexity: O(n). Pure.

• Postcondition: (result == true) => (s.len() >= 2)

---

---

---

jwt.xi

type Jwt

struct Jwt { header: Str; payload: Str; signature: Str }

Field	Type
header	Str
payload	Str
signature	Str

fn jwt_base64url_encode(data: &Vec[UInt8]) -> Str

Base64url encode bytes without padding. Parameters: data -- the bytes to encode. Returns: the unpadded URL-safe base64 string. Complexity: O(n). Pure.

• Postcondition: ((data.len() == 0) => (result.len() == 0)) && (result.len() >= data.len()) && (result.len() <= data.len() * 2)

fn jwt_base64url_decode(s: Str) -> Result[Vec[UInt8], Str]

Decode an unpadded base64url string back to bytes. Parameters: s -- the encoded string (padding optional). Returns: Ok(bytes) on success, Err for an invalid character. Complexity: O(n). Pure.

• Postcondition: ((s.len() == 0) => (result.is_ok == true)) && ((result.is_err == true) => (s.len() > 0))

fn jwt_alg_supported(alg: Str) -> Bool

Test if an algorithm is supported. Parameters: alg -- the algorithm name. Returns: true for "HS256" and "none". Complexity: O(1). Pure.

• Postcondition: result == (alg == "HS256" || alg == "none")

fn jwt_encode(header: Str, payload: Str, secret: Str, alg: Str) -> Result[Str, Str]

Build a signed JWT string. Parameters: header -- the JSON header (e.g. "{\"alg\":\"HS256\",\"typ\":\"JWT\"}"); payload -- the JSON claims; secret -- the HMAC secret; alg -- "HS256" or "none". Returns: Ok("header.payload.signature") on success, Err for an unsupported algorithm. Complexity: O(n). Pure.

• Postcondition: ((alg != "HS256" && alg != "none") => (result.is_err == true)) && ((alg == "HS256" || alg == "none") => (result.is_ok == true))

fn jwt_sign_b64(header_b64: Str, payload_b64: Str, secret: Str, alg: Str) -> Result[Str, Str]

Sign base64url parts and append the signature. Parameters: header_b64 -- the encoded header; payload_b64 -- the encoded payload; secret -- the HMAC secret; alg -- "HS256" or "none". Returns: Ok("header.payload.signature") on success, Err for an unsupported algorithm. Complexity: O(n). Pure.

• Postcondition: ((alg != "HS256" && alg != "none") => (result.is_err == true)) && ((alg == "HS256" || alg == "none") => (result.is_ok == true))

fn jwt_decode(token: Str) -> Result[Jwt, Str]

Split a JWT into header, payload, and signature. Parameters: token -- the full JWT string. Returns: Ok(Jwt) with exactly three dot-separated parts, Err otherwise. Complexity: O(n). Pure.

• Postcondition: ((token.len() < 4) => (result.is_err == true)) && ((result.is_ok == true) => (token.len() >= 4))

fn jwt_verify(token: Str, secret: Str) -> Bool

Verify a JWT signature with the given secret. Parameters: token -- the JWT string; secret -- the HMAC secret. Returns: true when the structure is valid and (for HS256) the signature matches; "none" tokens verify only when the signature part is empty. Complexity: O(n). Pure.

• Postcondition: ((token.len() < 4) => (result == false)) && ((result == true) => (token.len() >= 4))

fn jwt_expired(token: Str, now: Int) -> Bool

Test if the exp claim is before the given time. Parameters: token -- the JWT string; now -- the reference unix timestamp. Returns: true when the token has an exp claim at or before now, false when there is no exp claim or the token is malformed. Complexity: O(n). Pure.

• Postcondition: ((token.len() < 4) => (result == false)) && ((result == true) => (token.len() >= 4))

fn jwt_claims(token: Str) -> Result[Str, Str]

Extract the payload claims as JSON. Parameters: token -- the JWT string. Returns: Ok(decoded payload) on success, Err for a malformed token or an invalid base64url payload. Complexity: O(n). Pure.

• Postcondition: ((token.len() < 4) => (result.is_err == true)) && ((result.is_ok == true) => (token.len() >= 4))

---

---

---

mime.xi

type MimeType

struct MimeType { kind: Str; subtype: Str; params: Vec[(Str, Str)] } NOTE: the frozen spec documents params: Map[Str, Str]. The compiler cannot construct/return a struct containing a Map field (hangs/0xC0000005, see probe in agent_net2); the main-type field is named kind because the reserved word type is unreadable at call sites (P001) and breaks cross-module resolution. Params are stored as ordered (name, value) pairs.

Field	Type
subtype	Str
params	Vec[(Str, Str)]
kind	Str

type Link

struct Link { href: Str; rel: Str; title: Str; kind: Str }

Field	Type
href	Str
rel	Str
title	Str
kind	Str

fn mime_parse(s: Str) -> Result[MimeType, Str]

Parse a MIME type string into its parts. Parameters: s -- the MIME type (e.g. "text/html; charset=utf-8"). Returns: Ok(MimeType) with a lowercased type/subtype and parsed parameters (in declaration order); Err for a missing slash or an empty type. Complexity: O(n). Pure.

• Postcondition: ((s.len() < 3) => (result.is_err == true)) && ((result.is_ok == true) => (s.len() >= 3))

fn mime_type_of(path: Str) -> Str

Guess the MIME type from a file extension. Parameters: path -- the file path. Returns: the MIME type (lowercase) or "application/octet-stream". Complexity: O(1). Pure.

• Postcondition: result.len() >= 8 && ((path == "index.html") => (result == "text/html")) && ((path == "a.JPEG") => (result == "image/jpeg"))

fn mime_extension_of(mime: Str) -> Str

Guess a file extension for a MIME type. Parameters: mime -- the MIME type (lowercase). Returns: the extension without the leading dot, or "" when unknown. Complexity: O(1). Pure.

• Postcondition: result.len() <= 4 && (result.len() != 1) && ((mime == "text/html") => (result == "html")) && ((mime == "image/jpeg") => (result == "jpg"))

fn mime_matches(pattern: Str, mime: Str) -> Bool

Wildcard pattern match against a MIME type. Parameters: pattern -- e.g. "text/", "application/json" or "/*"; mime -- the actual MIME type. Returns: true when the pattern matches. Complexity: O(n). Pure.

• Postcondition: ((pattern == "*/*" || pattern == "*") => (result == true)) && ((pattern == mime) => (result == true))

fn mime_is_text(mime: Str) -> Bool

Test if a MIME type is text-based. Parameters: mime -- the MIME type. Returns: true for text/*, application/json, application/xml and related. Complexity: O(1). Pure.

• Postcondition: ((mime == "text/plain") => (result == true)) && ((mime == "application/json") => (result == true)) && ((result == true) => (mime.len() > 0))

fn mime_is_image(mime: Str) -> Bool

Test if a MIME type is an image. Parameters: mime -- the MIME type. Returns: true for image/* and image/x-* types. Complexity: O(1). Pure.

• Postcondition: ((result == true) => (mime.len() >= 6)) && ((mime == "image/png") => (result == true))

fn mime_is_audio(mime: Str) -> Bool

Test if a MIME type is audio. Parameters: mime -- the MIME type. Returns: true for audio/* types. Complexity: O(1). Pure.

• Postcondition: ((result == true) => (mime.len() >= 6)) && ((mime == "audio/mpeg") => (result == true))

fn mime_is_video(mime: Str) -> Bool

Test if a MIME type is video. Parameters: mime -- the MIME type. Returns: true for video/* types. Complexity: O(1). Pure.

• Postcondition: ((result == true) => (mime.len() >= 6)) && ((mime == "video/mp4") => (result == true))

fn mime_is_application(mime: Str) -> Bool

Test if a MIME type is an application type. Parameters: mime -- the MIME type. Returns: true for application/* types. Complexity: O(1). Pure.

• Postcondition: ((result == true) => (mime.len() >= 12)) && ((mime == "application/json") => (result == true))

fn charset_detect(data: &Vec[UInt8]) -> Str

Guess the character encoding of a byte buffer. Parameters: data -- the bytes to inspect. Returns: "utf-8", "utf-16le", "utf-16be", "utf-32le", "utf-32be", "ascii" or "binary". Complexity: O(n). Pure.

• Postcondition: ((data.len() == 0) => (result == "ascii")) && (result.len() >= 5)

fn charset_normalize(s: Str, charset: Str) -> Result[Str, Str]

Re-encode a string into a target charset. Parameters: s -- the input string (already UTF-8); charset -- the requested target charset. Returns: Ok(s) for UTF-8/ASCII targets (XIOM strings are always UTF-8), Err for unsupported targets. Complexity: O(1). Pure.

• Postcondition: ((charset == "") => (result.is_err == true)) && ((charset == "utf-8") => (result.is_ok == true)) && ((charset == "ASCII") => (result.is_ok == true))

fn etag_new(content: &Vec[UInt8]) -> Str

Compute a quoted etag for a byte buffer (SHA-256 hex). Parameters: content -- the bytes to hash. Returns: the quoted etag, e.g. "\"a1b2c3...\"". Complexity: O(n). Pure.

• Postcondition: result.len() == 66

fn etag_matches(etag: Str, if_none_match: Str) -> Bool

Test an etag against an If-None-Match header. Parameters: etag -- the entity tag (quoted); if_none_match -- the header value (a comma-separated list, optionally W/ prefixed). Returns: true when any list entry matches (including "*"). Complexity: O(n). Pure.

• Postcondition: ((if_none_match == "*") => (result == true)) && ((etag == if_none_match) => (result == true))

fn accept_parse(header: Str) -> Vec[(Str, Int)]

Parse an Accept header into mime pattern and q pairs. Parameters: header -- the Accept header value. Returns: the (pattern, q*1000) entries; malformed entries are skipped. Complexity: O(n). Pure.

• Postcondition: ((header.len() == 0) => (result.len() == 0)) && ((result.len() > 0) => (header.len() > 0))

fn accept_q_value(header: Str, mime: Str) -> Int

Look up the q value of a MIME type in an Accept header. Parameters: header -- the Accept header value; mime -- the actual MIME type. Returns: the highest matching q (scaled by 1000), or 0 when absent. Complexity: O(n). Pure.

• Postcondition: result >= 0 && result <= 1000

fn accept_negotiate(header: Str, available: &Vec[Str]) -> Option[Str]

Pick the best available MIME type for an Accept header. Parameters: header -- the Accept header value; available -- the candidate MIME types. Returns: Some(best) when a match with q > 0 exists, None otherwise. Complexity: O(n-m). Pure.

• Postcondition: ((available.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (available.len() > 0))

fn link_parse(header: Str) -> Vec[Link]

Parse a Link header into typed links. Parameters: header -- the Link header value (e.g. "https://a.com; rel=\"next\"; title=\"Next\""). Returns: the parsed links; malformed entries are skipped. Complexity: O(n). Pure.

• Postcondition: ((header.len() == 0) => (result.len() == 0)) && ((result.len() > 0) => (header.len() > 0))

fn link_find(links: &Vec[Link], rel: Str) -> Option[Str]

Find the href of a link with the given rel. Parameters: links -- the parsed links; rel -- the relation type. Returns: Some(href) for the first matching link, None otherwise. Complexity: O(n). Pure.

• Postcondition: ((links.len() == 0) => (result.is_some == false)) && ((result.is_some == true) => (links.len() > 0))

---

---

---

multipart.xi

type Part

struct Part { name: Str; filename: Str; content_type: Str; data: Vec[UInt8] }

Field	Type
name	Str
filename	Str
content_type	Str
data	Vec[UInt8]

fn multipart_part(name: Str, value: Str) -> Part

Build a plain text field part. Parameters: name -- the field name; value -- the field value. Returns: a Part with no filename or content type. Complexity: O(n). Pure.

• Postcondition: result.name == name && result.filename.len() == 0 && result.content_type.len() == 0 && result.data.len() >= value.len()

fn multipart_part_file(name: Str, filename: Str, content_type: Str, data: &Vec[UInt8]) -> Part

Build a file field part. Parameters: name -- the field name; filename -- the client file name; content_type -- the file's MIME type; data -- the file bytes. Returns: a Part carrying the file metadata and bytes. Complexity: O(n). Pure.

• Postcondition: result.name == name && result.filename == filename && result.content_type == content_type && result.data.len() == data.len()

fn multipart_build(parts: &Vec[Part], boundary: Str) -> Vec[UInt8]

Serialize parts into a multipart body. Parameters: parts -- the parts to serialize; boundary -- the boundary string. Returns: the multipart/form-data body bytes. Complexity: O(n). Pure.

• Postcondition: (result.len() >= boundary.len() + 6) && ((parts.len() == 0) => (result.len() == boundary.len() + 6))

fn multipart_parse(body: &Vec[UInt8], boundary: Str) -> Result[Vec[Part], Str]

Split a multipart body into parts. Parameters: body -- the multipart body bytes; boundary -- the boundary string. Returns: Ok(parts) on success, Err when the body has no boundary markers or is malformed. Complexity: O(n). Pure.

• Postcondition: ((body.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (body.len() > 0))

fn multipart_boundary_new() -> Str

Generate a random boundary string. Returns: a boundary of the form "----xiomboundary". Complexity: O(1). Pure (timestamp-based uniqueness).

• Postcondition: result.len() > 16

fn multipart_content_type(boundary: Str) -> Str

Build the Content-Type header value for a boundary. Parameters: boundary -- the boundary string. Returns: "multipart/form-data; boundary=". Complexity: O(1). Pure.

• Postcondition: result.len() == boundary.len() + 30

---

---

---

net.xi

type TcpStream

=== TCP ===

Field	Type
fd	Int

Derives: Clone

type TcpListener

Listening TCP socket handle.

Field	Type
fd	Int

Derives: Clone

type NetError

Network error with a message and an OS error code.

Field	Type
message	Str
code	Int

fn tcp_connect(host: Str, port: Int) -> Result[TcpStream, NetError]

Connect to host:port; Err with the OS message.

• Precondition: host.len() > 0
• Precondition: port > 0 && port <= 65535

fn tcp_listen(host: Str, port: Int) -> Result[TcpListener, NetError]

Bind and listen on host:port; Err on failure. Delegates to tcp_listen_with_backlog with the default backlog of 128.

• Precondition: host.len() > 0
• Precondition: port > 0 && port <= 65535

fn tcp_listen_with_backlog(host: Str, port: Int, backlog: Int) -> Result[TcpListener, NetError]

Bind and listen on host:port with an explicit listener backlog (1-1024); Err on failure. Real since wave 143.

• Precondition: host.len() > 0
• Precondition: port > 0 && port <= 65535
• Precondition: backlog >= 1 && backlog <= 1024

fn read(self: Self, buf: &mut Vec[UInt8]) -> Result[Int, NetError]

Read up to buffer capacity; Ok(bytes, 0 at EOF) or Err.

• Precondition: true

fn write(self: Self, data: &Vec[UInt8]) -> Result[Int, NetError]

Write bytes; Ok(bytes written) or Err.

• Precondition: true

fn write_all(self: Self, data: &Vec[UInt8]) -> Result[Int, NetError]

Write every byte, retrying after partial sends; Ok(total) or Err. Chunks the payload through a 64 KiB staging buffer and advances by the kernel-reported count, so payloads larger than the buffer and partial sends both complete. write keeps its documented single-send semantics.

• Precondition: true
• Postcondition: (data.len() == 0) => (result.is_ok == true)

fn close(self: Self) -> Result[Unit, NetError]

Close the stream; Err on failure.

• Postcondition: result.is_ok == true

fn send_file(self: Self, path: Str, offset: Int, count: Int) -> Result[Int, NetError]

Send a file to the peer with a kernel-side copy (zero-copy on Linux; TransmitFile on Windows). Wave 159 (REL-20261015-2202-pulse item 6): opens path read-only, delegates to xiom.os.fs_ffi.sendfile on this stream's socket fd, and closes the file fd. offset semantics: >= 0 is an explicit file offset, -1 is the current file position. count == 0 is Ok(0) before the open (a documented no-op). On Linux a short Ok count means EOF; on Windows the range is clamped to the remaining file size first. An empty path is Err. The socket fd is a real SOCKET on Windows (TransmitFile requirement). Returns: Ok(bytes sent) on success; Err with the underlying message.

• Postcondition: (count == 0) => (result.is_ok == true)

fn accept(self: Self) -> Result[(TcpStream, Str), NetError]

Accept a connection; Ok((stream, peer address)) or Err.

• Precondition: true

type NetHttpResponse

=== HTTP === NOTE: named NetHttpResponse to keep the bare type leaf distinct from xiom.net.http.HttpResponse (R44 same-leaf struct collision; both used to inject as %struct.HttpResponse and clobbered each other's fields).

Field	Type
status	Int
body	Str

Derives: Clone

fn http_get(url: Str) -> Result[NetHttpResponse, NetError]

HTTP GET; Ok parsed response or Err (transport or parse).

• Precondition: url.len() > 0

fn http_post(url: Str, body: Str) -> Result[NetHttpResponse, NetError]

HTTP POST with a body; Ok parsed response or Err.

• Postcondition: (url.len() == 0) => (result.is_err == true)

type UdpSocket

=== UDP ===

Field	Type
fd	Int

fn udp_bind(host: Str, port: Int) -> Result[UdpSocket, NetError]

Bind a UDP socket to host:port; Err on failure.

• Postcondition: ((port <= 0 || port >= 65536) => (result.is_err == true)) && ((result.is_ok == true) => (port > 0 && port <= 65535))

fn send_to(self: Self, data: &Vec[UInt8], addr: Str, port: Int) -> Result[Int, NetError]

Send a datagram to addr:port; Ok(bytes) or Err.

• Precondition: true

fn recv_from(self: Self, buf: &mut Vec[UInt8]) -> Result[(Int, Str, Int), NetError]

Receive a datagram; Ok((bytes, peer address, port)) or Err.

• Precondition: true

fn close(self: Self) -> Result[Unit, NetError]

Close the socket; Err on failure.

• Postcondition: result.is_ok == true

fn resolve_host(hostname: Str) -> Result[Vec[Str], NetError]

=== DNS ===

• Precondition: true

fn local_addr(port: Int) -> Result[Str, NetError]

Local address for binding to port; Err on failure.

• Precondition: true

type UrlParts

=== URL parsing ===

Field	Type
scheme	Str
host	Str
port	Int
path	Str
query	Str
fragment	Str

fn parse_url(url: Str) -> Result[UrlParts, NetError]

Split a URL into scheme/host/port/path; Err on malformed input.

• Postcondition: ((url.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (url.len() > 0))

enum HttpMethod

=== HTTP methods ===

• GET
• POST
• PUT
• DELETE
• PATCH
• HEAD
• OPTIONS

fn http_get_str(url: Str) -> Result[Str, NetError]

Performs an HTTP GET request and returns the response body as a string. Complexity: network I/O. Thread-safe: no shared state.

• Precondition: url.len() > 0

fn http_post_str(url: Str, body: Str) -> Result[Str, NetError]

Performs an HTTP POST request and returns the response body as a string. Complexity: network I/O. Thread-safe: no shared state.

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn http_status(url: Str) -> Option[Int]

Performs an HTTP GET request and returns only the status code, or None on error. Complexity: network I/O.

• Precondition: url.len() > 0

fn tcp_connect_str(host: Str, port: Int) -> Result[TcpStream, NetError]

Alias for tcp_connect. Connects to a TCP server at host:port. Complexity: network I/O.

• Precondition: host.len() > 0
• Precondition: port > 0 && port <= 65535

fn is_valid_ipv4(s: Str) -> Bool

Returns true if s is a valid IPv4 address (e.g. "192.168.1.1"). Delegates to the canonical xiom.net.ip4 (parity proven in p_netip_parity). Complexity: O(n). Pure, no side effects.

• Postcondition: ((s.len() == 0) => (result == false)) && ((result == true) => ((s.len() >= 7) && (s.len() <= 15)))

fn is_valid_port(p: Int) -> Bool

Returns true if p is a valid TCP/UDP port number (1-65535). Complexity: O(1). Pure.

• Postcondition: result == (p > 0 && p <= 65535)

fn url_parse_scheme(url: Str) -> Option[Str]

Extracts the scheme from a URL (e.g. "https" from "https://example.com"). Returns None if the URL is malformed. Complexity: O(n). Pure.

• Postcondition: ((url.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (url.len() > 0))

fn url_parse_host(url: Str) -> Option[Str]

Extracts the host from a URL (e.g. "example.com" from "https://example.com/path"). Returns None if the URL is malformed. Complexity: O(n). Pure.

• Postcondition: ((url.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (url.len() > 0))

fn url_parse_path(url: Str) -> Option[Str]

Extracts the path from a URL (e.g. "/path" from "https://example.com/path"). Returns None if the URL is malformed. Complexity: O(n). Pure.

• Postcondition: ((url.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (url.len() > 0))

fn url_parse_port(url: Str) -> Option[Int]

Extracts the port from a URL (e.g. 8080 from "https://example.com:8080/path"). Returns None if the URL is malformed or has no explicit port. Complexity: O(n). Pure.

• Postcondition: ((url.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (url.len() > 0))

fn dns_lookup(host: Str) -> Result[Vec[Str], NetError]

Resolves a hostname to a list of IP addresses. Delegates to resolve_host. Complexity: DNS network I/O.

• Precondition: host.len() > 0

---

---

ntp.xi

type NtpPacket

struct NtpPacket { li: Int; vn: Int; mode: Int; stratum: Int; poll: Int; precision: Int; root_delay: Float64; root_dispersion: Float64; ref_id: Int; ref_timestamp: Int; origin_timestamp: Int; recv_timestamp: Int; transmit_timestamp: Int } Timestamps are 64-bit NTP era timestamps (seconds since 1900-01-01).

Field	Type
li	Int
vn	Int
mode	Int
stratum	Int
poll	Int
precision	Int
root_delay	Float64
root_dispersion	Float64
ref_id	Int
ref_timestamp	Int
origin_timestamp	Int
recv_timestamp	Int
transmit_timestamp	Int

fn ntp_packet_new() -> NtpPacket

Build a client request packet with the current transmit time. Returns: an NtpPacket with LI=0, VN=4, Mode=3 (client), a zeroed header and the transmit timestamp set to the current NTP time. Complexity: O(1). Pure.

• Postcondition: result.li == 0 && result.vn == 4 && result.mode == 3 && result.stratum == 0 && result.poll == 0 && result.precision == 0 && result.root_delay == 0 && result.root_dispersion == 0

fn ntp_packet_to_bytes(p: NtpPacket) -> Vec[UInt8]

Serialize an NTP packet to 48 bytes (RFC 5905 wire format). Parameters: p -- the packet. Returns: the 48-byte big-endian packet. Complexity: O(1). Pure.

• Postcondition: result.len() == 48

fn ntp_packet_from_bytes(data: &Vec[UInt8]) -> Result[NtpPacket, Str]

Parse a 48-byte NTP packet. Parameters: data -- at least 48 bytes of packet data. Returns: Ok(NtpPacket) for a readable packet, Err when too short. Complexity: O(1). Pure.

• Postcondition: ((data.len() < 48) => (result.is_err == true)) && ((result.is_ok == true) => (data.len() >= 48))

fn ntp_validate(p: NtpPacket) -> Bool

Sanity-check a received packet. Parameters: p -- the packet. Returns: true when the version is 1..4, the mode is 1..7 (reserved 0 excluded) and the transmit timestamp is non-zero. Complexity: O(1). Pure.

• Postcondition: result == (p.vn >= 1 && p.vn <= 4 && p.mode >= 1 && p.mode <= 7 && p.transmit_timestamp != 0)

fn ntp_offset(packet: NtpPacket, local_t0: Int, local_t1: Int) -> Float64

Compute the clock offset in seconds (RFC 5905: (T2 - T1) + (T3 - T4)) / 2. Parameters: packet -- the server reply; local_t0 -- the client transmit time (unix seconds); local_t1 -- the client receive time (unix seconds). Returns: the offset in seconds (positive = local clock is behind). Complexity: O(1). Pure.

• Postcondition: (result == ((?) / 2))

fn ntp_roundtrip(packet: NtpPacket, local_t0: Int, local_t1: Int) -> Float64

Compute the roundtrip delay in seconds (RFC 5905: (T4 - T1) - (T3 - T2)). Parameters: packet -- the server reply; local_t0 -- the client transmit time (unix seconds); local_t1 -- the client receive time (unix seconds). Returns: the roundtrip delay in seconds. Complexity: O(1). Pure.

• Postcondition: (result == (?))

fn ntp_request(server: Str) -> Result[NtpPacket, Str]

Send an NTP request and read the reply packet. NOT IMPLEMENTED: requires a UDP socket layer that the pure stdlib does not expose. Use ntp_packet_new / ntp_packet_to_bytes / ntp_packet_from_bytes for offline encode/decode. Returns: Err("ntp_request: UDP sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn ntp_sync_time(server: Str) -> Result[Int, Str]

Fetch the server time as a unix timestamp. NOT IMPLEMENTED: requires the UDP socket layer (see ntp_request). Returns: Err("ntp_sync_time: UDP sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn sntp_request(server: Str) -> Result[Int, Str]

One-shot SNTP client returning a unix timestamp. NOT IMPLEMENTED: requires the UDP socket layer (see ntp_request). Returns: Err("sntp_request: UDP sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

---

---

---

ping.xi

type PingStats

struct PingStats { sent: Int; received: Int; min_ms: Int; avg_ms: Int; max_ms: Int }

Field	Type
sent	Int
received	Int
min_ms	Int
avg_ms	Int
max_ms	Int

fn icmp_checksum(data: &Vec[UInt8]) -> UInt16

Compute the ICMP header checksum (RFC 1071 one's-complement sum). Parameters: data -- the packet bytes (the checksum field should be zero). Returns: the 16-bit checksum. Complexity: O(n). Pure.

• Postcondition: (data.len() == 0) => (result == 65535)

fn ping_send_echo(host: Str, id: Int, seq: Int, payload: &Vec[UInt8]) -> Result[Int, Str]

Send one ICMP echo request. NOT IMPLEMENTED: requires raw sockets (ICMP) that the pure stdlib does not expose. Returns: Err("ping_send_echo: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn ping_recv_echo(timeout_ms: Int) -> Result[(Int, Int, Int), Str]

Wait for one echo reply. NOT IMPLEMENTED: requires raw sockets (ICMP) that the pure stdlib does not expose. Returns: Err("ping_recv_echo: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn ping_once(host: Str, timeout_ms: Int) -> Result[Int, Str]

Send one echo and return the round-trip time in milliseconds. NOT IMPLEMENTED: requires raw sockets (see ping_send_echo). Returns: Err("ping_once: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn ping(host: Str, timeout_ms: Int) -> Result[PingStats, Str]

Run a ping burst and return aggregate stats. NOT IMPLEMENTED: requires raw sockets (see ping_send_echo). Returns: Err("ping: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn traceroute_hop(host: Str, ttl: Int, timeout_ms: Int) -> Result[Str, Str]

Probe a single hop and return its address. NOT IMPLEMENTED: requires raw sockets (see ping_send_echo). Returns: Err("traceroute_hop: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn traceroute(host: Str, max_hops: Int, timeout_ms: Int) -> Result[Vec[Str], Str]

Trace the route to a host by hop. NOT IMPLEMENTED: requires raw sockets (see ping_send_echo). Returns: Err("traceroute: raw sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

---

---

---

proto.xi

fn jsonrpc_request(id: Int, method: Str, params_json: Str) -> Str

jsonrpc_request builds a JSON-RPC 2.0 request object. The params value is embedded verbatim as pre-serialized JSON.

• Postcondition: result.len() >= 46

fn jsonrpc_success(id: Int, result_json: Str) -> Str

jsonrpc_success builds a JSON-RPC 2.0 success response. The result value is embedded verbatim as pre-serialized JSON.

• Postcondition: result.len() >= 34

fn jsonrpc_error(id: Int, code: Int, message: Str) -> Str

jsonrpc_error builds a JSON-RPC 2.0 error response.

• Postcondition: result.len() >= 56

fn sse_format_event(event: Str, data: Str) -> Str

sse_format_event formats an SSE event with an "event:" line followed by "data:" lines and a terminating blank line.

• Postcondition: result.len() >= event.len() + 16

fn sse_format_data(data: Str) -> Str

sse_format_data formats a single SSE data message with a terminating blank line.

• Postcondition: result.len() >= data.len() + 8

fn http_header_parse(headers: Str) -> Vec[(Str, Str)]

http_header_parse parses a block of "Name: value" lines (one per line, '\r' tolerated) into (name, value) pairs. Blank lines are skipped.

• Postcondition: ((headers.len() == 0) => (result.len() == 0)) && (result.len() <= headers.len() + 1)

fn http_header_get(headers: Vec[(Str, Str)], name: Str) -> Option[Str]

http_header_get finds the value for a header name in a parsed header list, matching case-insensitively and returning the first match.

• Postcondition: ((headers.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (headers.len() > 0))

fn basic_auth_header(username: Str, password: Str) -> Str

basic_auth_header builds a "Basic " Authorization header value.

• Postcondition: result.len() >= 6

fn bearer_auth_header(token: Str) -> Str

bearer_auth_header builds a "Bearer " Authorization header value.

• Postcondition: result.len() == token.len() + 7

fn http_status_text(code: Int) -> Str

http_status_text maps an HTTP status code to its standard reason phrase, or "Unknown" for codes not in the table.

• Postcondition: result.len() >= 2 && result.len() <= 21 && ((code == 200) => (result == "OK")) && ((code == 404) => (result == "Not Found"))

---

---

---

server.xi

fn server_default_port() -> Int

server_default_port returns the default HTTP server port (80). Complexity: O(1). Pure.

• Postcondition: result == 80

fn server_parse_request_line(line: Str) -> Option[(Str, Str, Str)]

server_parse_request_line parses an HTTP request line like "GET /path HTTP/1.1" into (method, target, version). Returns None if the line does not contain three space-separated tokens. Complexity: O(n). Pure.

• Postcondition: ((line.len() < 5) => (result.is_none == true)) && ((result.is_some == true) => (line.len() >= 5))

type ServerRequest

Parsed HTTP/1.x request head plus the body span inside the raw buffer. body_len is the Content-Length value (0 when the header is absent); the body bytes are [body_start, body_start + body_len) in that buffer.

Field	Type
method	Str
target	Str
version	Str
headers	Vec[(Str, Str)]
body_start	Int
body_len	Int

fn server_parse_request(bytes: &Vec[UInt8]) -> Option[ServerRequest]

server_parse_request parses raw HTTP/1.x request bytes (head + body) into method/target/version, a lowercased (name, value) header list and the body span. Returns None when the request line is malformed or has a CTL/NUL/DEL or an extra token, the version is not HTTP/1.x, the header block is not CRLF-terminated, a field line is obs-folded/leading-spaced, a field line contains a forbidden CTL, a field name contains whitespace or has whitespace before the colon, a Content-Length is duplicated, non-digit or overflowing, a Transfer-Encoding is duplicated or not exactly "chunked", or both Content-Length and Transfer-Encoding are present. The body remains binary-safe (only the head is validated). The head is parsed directly from the byte buffer using (start, len) spans: no whole-head copy is made and each returned field is a single allocation. Complexity: O(n). Pure.

R3: the returned Some payload owns its Str leaves (method/target/version, header names/values) and its headers Vec buffer; the caller may reclaim them. #[owns_return] also forces main-heap allocation for the payload so a confined caller can free it.

• Postcondition: (bytes.len() == 0) => (result.is_none == true)

fn server_build_status_line(code: Int) -> Str

server_build_status_line builds a status line like "HTTP/1.1 200 OK". Complexity: O(1). Pure.

• Postcondition: result.len() >= 13 && ((code == 200) => (result == "HTTP/1.1 200 OK")) && ((code == 404) => (result == "HTTP/1.1 404 Not Found")) && ((code == 500) => (result == "HTTP/1.1 500 Internal Server Error"))

fn server_build_response(code: Int, body: Str) -> Str

server_build_response builds a minimal HTTP/1.1 response with a text/plain body. Complexity: O(n). Pure.

• Postcondition: result.len() >= body.len() + 81

fn server_build_response_headers(code: Int, headers: &Vec[(Str, Str)], body: Str) -> Str

server_build_response_headers builds an HTTP/1.1 response with custom (name, value) header pairs and a text body. Complexity: O(n). Pure.

• Postcondition: result.len() >= body.len() + (headers.len() * 4) + 36

fn server_status_text(code: Int) -> Str

server_status_text returns the standard reason phrase for a status code, or "Unknown" for codes not in the table. Complexity: O(1).

• Postcondition: result.len() > 0 && ((code == 200) => (result == "OK")) && ((code == 404) => (result == "Not Found")) && ((code == 500) => (result == "Internal Server Error"))

---

---

---

smtp.xi

fn smtp_default_port() -> Int

smtp_default_port returns the default SMTP port (25). Complexity: O(1). Pure.

• Postcondition: result == 25

fn smtp_command_helo(host: Str) -> Str

smtp_command_helo formats a HELO command. Complexity: O(1). Pure.

• Postcondition: result.len() == host.len() + 7

fn smtp_command_ehlo(host: Str) -> Str

smtp_command_ehlo formats an EHLO command. Complexity: O(1). Pure.

• Postcondition: result.len() == host.len() + 7

fn smtp_command_mail_from(addr: Str) -> Str

smtp_command_mail_from formats a MAIL FROM command with an address. Complexity: O(1). Pure.

• Postcondition: result.len() == addr.len() + 14

fn smtp_command_rcpt_to(addr: Str) -> Str

smtp_command_rcpt_to formats a RCPT TO command with an address. Complexity: O(1). Pure.

• Postcondition: result.len() == addr.len() + 12

fn smtp_command_data() -> Str

smtp_command_data formats a DATA command. Complexity: O(1). Pure.

• Postcondition: result.len() == 6

fn smtp_command_quit() -> Str

smtp_command_quit formats a QUIT command. Complexity: O(1). Pure.

• Postcondition: result.len() == 6

fn smtp_command_noop() -> Str

smtp_command_noop formats a NOOP command. Complexity: O(1). Pure.

• Postcondition: result.len() == 6

fn smtp_command_rset() -> Str

smtp_command_rset formats a RSET command. Complexity: O(1). Pure.

• Postcondition: result.len() == 6

fn smtp_command_auth_login() -> Str

smtp_command_auth_login formats an AUTH LOGIN command. Complexity: O(1). Pure.

• Postcondition: result.len() == 12

fn smtp_body_end() -> Str

smtp_body_end formats the end-of-data marker (dot on its own line). Complexity: O(1). Pure.

• Postcondition: result.len() == 5

fn smtp_parse_reply(line: Str) -> Option[(Int, Str)]

smtp_parse_reply parses an SMTP reply line like "250 OK" into (code, text). Returns None if the line does not start with a 3-digit code. Complexity: O(1). Pure.

• Postcondition: ((line.len() < 3) => (result.is_none == true)) && ((result.is_some == true) => (line.len() >= 3))

fn smtp_reply_is_success(code: Int) -> Bool

smtp_reply_is_success returns true for 2xx replies. Complexity: O(1). Pure.

• Postcondition: result == (code >= 200 && code < 300)

---

---

---

socket.xi

fn socket_tcp() -> Result[Int, Str]

socket_tcp creates a TCP socket and returns its fd, or Err. Complexity: O(1) syscall.

• Postcondition: (result.is_ok == false) || (result.is_err == false)

fn socket_udp() -> Result[Int, Str]

socket_udp creates a UDP socket and returns its fd, or Err. Complexity: O(1) syscall.

• Postcondition: (result.is_ok == false) || (result.is_err == false)

fn socket_bind(fd: Int, addr: Str, port: Int) -> Result[Unit, Str]

socket_bind binds a socket to addr:port on the given address (wave 155, REL-20261016-1404: the address is honored -- pass "0.0.0.0" for the wildcard; an unparsable IPv4 literal is a typed Err). Complexity: O(1) syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && addr.len() > 0 && port >= 1 && port <= 65535)

fn socket_listen(fd: Int, backlog: Int) -> Result[Unit, Str]

socket_listen marks a bound TCP socket as listening. Complexity: O(1) syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && backlog >= 0)

fn socket_accept(fd: Int) -> Result[Int, Str]

socket_accept accepts a connection and returns the new socket fd. Complexity: O(1) blocking syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0)

fn socket_connect(fd: Int, addr: Str, port: Int) -> Result[Unit, Str]

socket_connect connects a socket to a remote addr:port. Complexity: O(1) syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && addr.len() > 0 && port >= 1 && port <= 65535)

fn socket_send(fd: Int, data: &Vec[UInt8]) -> Result[Int, Str]

socket_send sends bytes on a socket; returns the count written. Complexity: O(n) syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && data.len() <= 65536)

fn socket_send_all(fd: Int, data: &Vec[UInt8]) -> Result[Int, Str]

socket_send_all writes every byte of data, advancing by the syscall's partial counts so a short send cannot silently truncate a response. Real implementation (wave 121). Returns: Ok(data.len()). Complexity: O(n) syscall loop.

• Postcondition: data.len() == 0 => result is Ok(_)
• Postcondition: result is Ok(_) => fd >= 0

fn socket_chunk_encode(data: &Vec[UInt8]) -> Str

socket_chunk_encode wraps data in one HTTP/1.1 chunked-transfer frame: "\r\n" + data + "\r\n". Empty data yields "" (a zero-length chunk would terminate the stream; use socket_chunked_end for that). Complexity: O(n). Pure.

• Postcondition: data.len() == 0 => result.len() == 0
• Postcondition: data.len() > 0 => result.len() >= data.len() + 3

fn socket_chunked_end() -> Str

socket_chunked_end returns the terminating zero-length chunk ("0\r\n\r\n") that finishes a chunked-transfer body. Complexity: O(1). Pure.

• Postcondition: result.len() == 5

fn socket_stream_chunk(fd: Int, data: &Vec[UInt8]) -> Result[Unit, Str]

socket_stream_chunk sends one chunk frame (encode + full send). Empty data is a documented no-op (Ok(())). Write the response head with Transfer-Encoding: chunked first (e.g. via server.server_build_response_headers), then chunks, then socket_stream_end. Returns: Ok(()) once the frame is on the wire; Err on failure. Complexity: O(n) network I/O.

• Postcondition: data.len() == 0 => result is Ok(_)
• Postcondition: result is Ok(_) => fd >= 0

fn socket_stream_end(fd: Int) -> Result[Unit, Str]

socket_stream_end sends the terminating zero-length chunk. Returns: Ok(()) once the terminator is on the wire; Err on failure. Complexity: O(1) network I/O.

• Postcondition: result is Ok(_) => fd >= 0

fn socket_recv(fd: Int, max: Int) -> Result[Vec[UInt8], Str]

socket_recv receives up to max bytes; returns the bytes received. Complexity: O(n) blocking syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && max > 0)

fn socket_recv_into(fd: Int, buf: &mut Vec[UInt8], max: Int) -> Result[Int, Str]

socket_recv_into receives up to max bytes into a caller-owned buffer: it clears buf, fills it with the bytes received, and returns the count (0 = clean EOF). Err on a socket failure; buf is left empty. The buffer's capacity is reused, so a per-connection buffer allocates at most once instead of once per call (REL-20261022-2049-pulse). Complexity: O(n) blocking syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && max > 0)

fn socket_send_to(fd: Int, data: &Vec[UInt8], addr: Str, port: Int) -> Result[Int, Str]

socket_send_to sends a datagram to addr:port; returns the count written. Complexity: O(n) syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && port >= 1 && port <= 65535 && data.len() <= 65536)

fn socket_recv_from(fd: Int, max: Int) -> Result[(Vec[UInt8], Str, Int), Str]

socket_recv_from receives a datagram; the tuple is (data, peer_addr, peer_port). Complexity: O(n) blocking syscall.

• Postcondition: (result.is_ok == false) || (fd >= 0 && max > 0)

fn socket_recv_timeout(fd: Int, max: Int, ms: Int) -> Result[Vec[UInt8], Str]

socket_recv_timeout receives up to max bytes with a per-call deadline: it sets the receive timeout to ms, receives, then restores no-timeout (0). A deadline expiry (or any recv failure) surfaces as Err -- the slowloris guard from REL-20261011-0317-pulse-2. Real since wave 119.

• Postcondition: (fd < 0) => (result is Err(_))
• Postcondition: (ms < 0) => (result is Err(_))

fn socket_recv_timeout_into(fd: Int, buf: &mut Vec[UInt8], max: Int, ms: Int) -> Result[Int, Str]

socket_recv_timeout_into is socket_recv_into with a per-call receive deadline: it sets the receive timeout to ms, receives into buf, then restores no-timeout (0). Ok(0) is a clean EOF; Err is a timeout or socket failure (the 408 path) and leaves buf empty. Buffer capacity is reused across calls (REL-20261022-2049-pulse). Complexity: O(n) syscall.

• Postcondition: (fd < 0) => (result is Err(_))
• Postcondition: (ms < 0) => (result is Err(_))

fn socket_close(fd: Int)

socket_close closes a socket, releasing the fd. Complexity: O(1) syscall.

• Postcondition: true

fn socket_set_timeout(fd: Int, ms: Int) -> Result[Unit, Str]

socket_set_timeout sets the receive timeout in milliseconds (SO_RCVTIMEO; 0 = no timeout). Real since wave 119. Invalid inputs keep the documented early-error path (no contract abort). Returns: Ok(()) once the option is set; Err on failure.

• Postcondition: (fd < 0) => (result is Err(_))
• Postcondition: (ms < 0) => (result is Err(_))

fn socket_set_nonblocking(fd: Int, on: Bool) -> Result[Unit, Str]

socket_set_nonblocking enables or disables non-blocking mode (fcntl O_NONBLOCK on POSIX, ioctlsocket FIONBIO on Windows). Real since wave 119; invalid fd keeps the documented early-error path.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_set_nodelay(fd: Int, on: Bool) -> Result[Unit, Str]

socket_set_nodelay disables or enables Nagle (TCP_NODELAY). Real since wave 143; invalid fds keep the documented early-error path.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_set_keepalive(fd: Int, on: Bool) -> Result[Unit, Str]

socket_set_keepalive enables or disables SO_KEEPALIVE on a socket. Real since wave 143; invalid fds keep the documented early-error path.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_shutdown(fd: Int, how: Int) -> Result[Unit, Str]

socket_shutdown shuts down reading, writing, or both per how (0 = receive, 1 = send, 2 = both). Real since wave 119; invalid fd/how keep the documented early-error path (no contract abort).

• Postcondition: (fd < 0) => (result is Err(_))
• Postcondition: (how < 0) => (result is Err(_))
• Postcondition: (how > 2) => (result is Err(_))

fn socket_peer_addr(fd: Int) -> Result[(Str, Int), Str]

socket_peer_addr returns the connected peer address. The runtime does not expose getpeername(); always returns a documented Err.

• Postcondition: result.is_err == true

fn socket_local_addr(fd: Int) -> Result[(Str, Int), Str]

socket_local_addr returns the bound local (addr, port) via getsockname (real since wave 155, REL-20261016-1404); an unbound or closed fd returns Err.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_available(fd: Int) -> Int

socket_available returns the number of bytes currently readable without blocking. The runtime does not expose FIONREAD; returns 0.

• Postcondition: result == 0

fn socket_reuse_addr(fd: Int, on: Bool) -> Result[Unit, Str]

socket_reuse_addr enables or disables SO_REUSEADDR. Real since wave 119 (setsockopt on both platforms; the Windows bind also sets it); invalid fd keeps the documented early-error path. Returns: Ok(()) once the option is set; Err on failure.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_set_reuseport(fd: Int, on: Bool) -> Result[Unit, Str]

socket_set_reuseport enables or disables SO_REUSEPORT (real since wave 122; POSIX only). Windows has no equivalent: the documented Err says to run N processes on distinct ports behind a reverse proxy. The double bind of one port by two SO_REUSEPORT listeners is the POSIX semantic. Returns: Ok(()) once the option is set; Err on failure or on Windows.

• Postcondition: (fd < 0) => (result is Err(_))

fn socket_poll_read(fds: &Vec[Int], timeout_ms: Int) -> Result[Vec[Int], Str]

socket_poll_read waits for read readiness over a list of sockets and returns the ready ones (in input order; up to 1024 fds per call). Real since wave 122: poll() on POSIX, WSAPoll on Windows. Errors and invalid entries count as ready so the caller can inspect them. timeout_ms: 0 = immediate, > 0 = wait that many ms (negative is Err; no unbounded wait). An empty list is an Ok empty result. Returns: Ok(ready fds); Err on bad arguments or poll failure. Complexity: network wait.

• Postcondition: result is Ok(_) => fds.len() <= 1024
• Postcondition: result is Ok(_) => timeout_ms >= 0

fn socket_poll_write(fds: &Vec[Int], timeout_ms: Int) -> Result[Vec[Int], Str]

socket_poll_write waits for write readiness over a list of sockets and returns the ready ones (in input order; up to 1024 fds per call). Real since wave 122: poll()/WSAPoll. Same bounds and conventions as socket_poll_read. Returns: Ok(ready fds); Err on bad arguments or poll failure. Complexity: network wait.

• Postcondition: result is Ok(_) => fds.len() <= 1024
• Postcondition: result is Ok(_) => timeout_ms >= 0

fn socket_listen_fds() -> Result[Vec[Int], Str]

socket_listen_fds adopts systemd socket activation: LISTEN_PID must equal this process, LISTEN_FDS is the inherited descriptor count, and the fds are 3..3+N-1 (the classic systemd convention). POSIX-only. On success the LISTEN_PID/LISTEN_FDS variables are consumed so a second call cannot double-adopt; LISTEN_FDNAMES stays in place for the caller. Err on Windows, a missing/mismatched PID, an invalid or negative count, or a count above the 1024-fd poll cap. Complexity: O(number of inherited fds).

• Postcondition: (env.host_is_windows()) => (result.is_err)

type EventLoop

Opaque readiness-loop handle (an epoll fd on Linux, a kqueue fd on macOS/FreeBSD, a slot handle on Windows).

Field	Type
handle	Int

type EventBatch

Readiness batch: parallel fds/flags vectors (no Vec[struct]). Flags: bit 1 = readable, bit 2 = writable, bit 4 = error/hangup.

Field	Type
fds	Vec[Int]
flags	Vec[Int]

fn eventbatch_new() -> EventBatch

New empty readiness batch.

• Postcondition: result.fds.len() == 0
• Postcondition: result.flags.len() == 0

fn eventloop_new() -> Result[EventLoop, Str]

Create a readiness loop. Linux uses epoll, macOS/FreeBSD use kqueue, Windows uses a WSAPoll readiness shim; other POSIX returns the documented Err.

• Postcondition: true

fn eventloop_add(loop: &EventLoop, fd: Int, read: Bool, write: Bool) -> Result[Unit, Str]

Register fd for read and/or write readiness. Err on a closed loop, a negative fd, or a backend failure.

• Postcondition: (loop.handle < 0 || fd < 0) => (result.is_err)

fn eventloop_modify(loop: &EventLoop, fd: Int, read: Bool, write: Bool) -> Result[Unit, Str]

Change the read/write interest for a registered fd.

• Postcondition: (loop.handle < 0 || fd < 0) => (result.is_err)

fn eventloop_remove(loop: &EventLoop, fd: Int) -> Result[Unit, Str]

Remove fd from the loop.

• Postcondition: (loop.handle < 0 || fd < 0) => (result.is_err)

fn eventloop_wait(loop: &EventLoop, timeout_ms: Int, out: &mut EventBatch) -> Result[Int, Str]

Wait for readiness and APPEND the ready entries to out. timeout_ms: 0 = immediate, > 0 = wait that many ms, -1 = block until an event. Returns the number of events appended. Err on a closed loop or a timeout below -1.

• Postcondition: (loop.handle < 0 || timeout_ms < 0 - 1) => (result.is_err)

fn eventloop_close(loop: &mut EventLoop) -> Bool

Close the loop and invalidate the handle. Idempotent: returns false when the loop was already closed, true when this call closed it. Registered fds are never closed by the loop.

• Postcondition: result == (loop.handle@pre >= 0)

---

---

---

sse.xi

type SseConnection

struct SseConnection { socket: TcpStream; url: Str; open: Bool; buf: Vec[UInt8]; start: Int } buf/start hold the read buffer and its consumed-prefix cursor. NOTE: the field type is the BARE leaf TcpStream (alias-qualified type paths are the known resolution trap -- see the catalog notes).

Field	Type
socket	TcpStream
url	Str
open	Bool
buf	Vec[UInt8]
start	Int

type SseEvent

struct SseEvent { id: Str; event: Str; data: Str; retry: Int }

Field	Type
id	Str
event	Str
data	Str
retry	Int

fn sse_parse_event(chunk: Str) -> Result[SseEvent, Str]

Parse one raw event chunk. Parameters: chunk -- a raw event block (a sequence of "field: value" lines ending with a blank line). Returns: Ok(SseEvent) for a well-formed chunk, Err for an empty chunk. Complexity: O(n). Pure.

• Postcondition: ((chunk.len() == 0) => (result.is_err == true)) && ((result.is_err == true) => (chunk.len() == 0)) && ((result.is_ok == true) => (chunk.len() > 0))

fn sse_event_id(e: SseEvent) -> Option[Str]

Return the event id field. Parameters: e -- the event. Returns: Some(id) when the id is non-empty, None otherwise. Complexity: O(1). Pure.

• Postcondition: ((e.id.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (e.id.len() > 0))

fn sse_event_data(e: SseEvent) -> Str

Return the event data field. Parameters: e -- the event. Returns: the data field (possibly ""). Complexity: O(1). Pure.

• Postcondition: result == e.data

fn sse_connect(url: Str) -> Result[SseConnection, Str]

Open a text/event-stream connection (plaintext http:// only; https:// is refused with a typed error until the TLS seam lands). Parameters: url -- http://host[:port]/path (a missing path becomes "/"). Returns: Ok(SseConnection) after a 200 + text/event-stream response head; Err on a bad/empty url, an unsupported scheme, a transport failure, a non-200 status, or a non-SSE content type. Complexity: O(response head).

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn sse_connect_headers(url: Str, headers: &Vec[(Str, Str)]) -> Result[SseConnection, Str]

Connect with custom request headers appended to the standard GET. Header names/values containing CR or LF are refused (request injection). Returns: as sse_connect. Complexity: O(response head + headers).

• Postcondition: (url.len() == 0) => (result.is_err == true)

fn sse_read_event(conn: &mut SseConnection) -> Result[SseEvent, Str]

Read and parse the next event block. Blocks on the socket until a blank-line-terminated block is buffered (set a socket timeout for a hard bound). Returns the RAW parsed chunk -- comment-only chunks come back with empty data (dispatch filtering is the consumer's step). Err after EOF, on a transport failure, or when a block exceeds 1 MiB without a terminator. Complexity: O(block).

• Postcondition: true

fn sse_close(conn: &mut SseConnection)

Close the stream (idempotent); the connection's open flag is cleared. Complexity: O(1).

• Postcondition: true

fn sse_read_events(conn: &mut SseConnection, out: &mut Vec[SseEvent]) -> Int

Drain events that are already readable (zero-timeout poll; the first pull may block inside a partially buffered block until the socket timeout). Appends to out and returns the number added (capped at 1024 per call). Complexity: O(drained bytes).

• Postcondition: result >= 0

fn sse_encode_event(e: SseEvent) -> Result[Str, Str]

Encode one SSE event in wire format (LF endings, blank-line terminated). Rejects CR in any field, LF in id/event, and a negative retry. LF in data becomes one data: line per segment; an empty data field is sent as data: so the chunk is still a complete event. Parameters: e -- the event to encode. Returns: Ok(wire text) or Err(reason). Complexity: O(n). Pure.

• Postcondition: (result.is_ok == true) => (result.value.len() >= 2)

fn sse_encode_comment(text: Str) -> Result[Str, Str]

Encode a comment (keep-alive) block: every LF-separated segment becomes a : text line, terminated by a blank line. CR is rejected (it would corrupt framing). An empty text yields a bare : comment. Parameters: text -- the comment text. Returns: Ok(wire text) or Err(reason). Complexity: O(n). Pure.

• Postcondition: (result.is_ok == true) => (result.value.len() >= 2)

fn sse_encode_heartbeat() -> Str

The canonical keep-alive comment block (": ping\n\n"). Complexity: O(1). Pure.

• Postcondition: result.len() == 8

fn sse_write_event(stream: &TcpStream, e: SseEvent) -> Result[Int, Str]

Write one event to a stream (server side). Uses write_all, so partial sends are completed before returning. Parameters: stream -- the client stream; e -- the event. Returns: Ok(bytes written) or Err(reason). Complexity: O(n) plus the transport write.

• Postcondition: (result.is_ok == true) => (result.value >= 1)

fn sse_write_comment(stream: &TcpStream, text: Str) -> Result[Int, Str]

Write a comment (keep-alive) block to a stream (server side). Parameters: stream -- the client stream; text -- the comment text. Returns: Ok(bytes written) or Err(reason). Complexity: O(n) plus the transport write.

• Postcondition: (result.is_ok == true) => (result.value >= 1)

fn sse_heartbeat(stream: &TcpStream) -> Result[Int, Str]

Write the canonical heartbeat comment (": ping\n\n"). Parameters: stream -- the client stream. Returns: Ok(8) or Err(reason). Complexity: O(1) plus the transport write.

• Postcondition: (result.is_ok == true) => (result.value == 8)

---

---

---

tcp.xi

fn tcp_validate_port(p: Int) -> Bool

tcp_validate_port returns true if p is a valid TCP port (1-65535). Complexity: O(1). Pure.

• Postcondition: result == (p > 0 && p <= 65535)

fn tcp_is_valid_port(p: Int) -> Bool

tcp_is_valid_port is an alias for tcp_validate_port. Complexity: O(1). Pure.

• Postcondition: result == (p > 0 && p <= 65535)

fn tcp_parse_endpoint(s: Str) -> Option[(Str, Int)]

tcp_parse_endpoint splits a "host:port" string into (host, port). Returns None if no colon or a malformed port is present. The host may be empty (an empty host string is rejected). Complexity: O(n). Pure.

• Postcondition: ((s.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 3))

fn tcp_format_endpoint(host: Str, port: Int) -> Str

tcp_format_endpoint builds a "host:port" string. Complexity: O(1). Pure.

• Postcondition: result == host + ":" + port.to_str()

---

---

---

tls.xi

fn tls_default_port() -> Int

tls_default_port returns the default TLS port (443). Complexity: O(1). Pure.

• Postcondition: result == 443

fn tls_version_name(version: Int) -> Str

tls_version_name maps a TLS version code point to its name. Recognised values: 0x0301 TLSv1.0, 0x0302 TLSv1.1, 0x0303 TLSv1.2, 0x0304 TLSv1.3. Unknown values return "unknown". Complexity: O(1).

• Postcondition: ((version == 768) => (result == "SSLv3")) && ((version == 769) => (result == "TLSv1.0")) && ((version == 770) => (result == "TLSv1.1")) && ((version == 771) => (result == "TLSv1.2")) && ((version == 772) => (result == "TLSv1.3")) && (result.len() > 0)

fn tls_handshake_type_name(t: Int) -> Str

tls_handshake_type_name maps a TLS handshake message type to its name. Complexity: O(1).

• Postcondition: ((t == 0) => (result == "hello_request")) && ((t == 1) => (result == "client_hello")) && ((t == 2) => (result == "server_hello")) && ((t == 11) => (result == "certificate")) && ((t == 16) => (result == "client_key_exchange")) && ((t == 20) => (result == "finished")) && (result.len() > 0)

fn tls_alert_name(code: Int) -> Str

tls_alert_name maps a TLS alert description to its name per RFC 5246 and RFC 8446. Complexity: O(1).

• Postcondition: ((code == 0) => (result == "close_notify")) && ((code == 20) => (result == "bad_record_mac")) && ((code == 40) => (result == "handshake_failure")) && ((code == 46) => (result == "certificate_unknown")) && ((code == 48) => (result == "unknown_ca")) && ((code == 70) => (result == "protocol_version")) && ((code == 120) => (result == "no_application_protocol")) && (result.len() > 0)

fn tls_cipher_suite_name(code: Int) -> Str

tls_cipher_suite_name maps a TLS cipher suite code to a human-readable name for the most common suites, or "unknown" (0x0000- 0xFFFF, two-byte IANA code). Complexity: O(1).

• Postcondition: ((code == 47) => (result == "TLS_RSA_WITH_AES_128_CBC_SHA")) && ((code == 49199) => (result == "TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256")) && ((code == 49200) => (result == "TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384")) && ((code == 4865) => (result == "TLS_AES_128_GCM_SHA256")) && ((code == 4866) => (result == "TLS_AES_256_GCM_SHA384")) && ((code == 4867) => (result == "TLS_CHACHA20_POLY1305_SHA256")) && (result.len() > 0)

fn alpn_encode(protocols: &Vec[Str]) -> Result[Vec[UInt8], Str]

alpn_encode serialises protocol names into the RFC 7301 ProtocolNameList wire format (2-byte big-endian total length, then one 1-byte-length-prefixed name each). Rejects an empty list, empty names, names longer than 255 bytes, and a list longer than 65535 bytes. Returns: Ok(the wire bytes); Err on an invalid protocol list. Complexity: O(n). Pure.

• Postcondition: protocols.len() == 0 => result.is_err == true
• Postcondition: result.is_ok == true => protocols.len() > 0

fn alpn_decode(bytes: &Vec[UInt8]) -> Result[Vec[Str], Str]

alpn_decode parses an RFC 7301 ProtocolNameList. Strict: the declared list length must consume the whole input, the list must hold at least one name, and every name must be 1..255 bytes. Err on malformed or truncated input (fewer than 2 bytes, a declared length below 2 or mismatching the input size, a zero-length name, or a name that runs past the end). Returns: Ok(the protocol names in wire order); Err on malformed input. Complexity: O(n). Pure.

• Postcondition: bytes.len() < 2 => result.is_err == true

type TlsBackend

TlsBackend is a loaded backend library: the module handle plus the resolved address of every mandatory backend symbol (see the module header for the symbol contract). Stage gate: nothing in this module calls through these addresses; the backend value owns the handle.

Field	Type
handle	Int
tls_init	Int
tls_server_new	Int
tls_client_new	Int
tls_handshake	Int
tls_read	Int
tls_write	Int
tls_close	Int
tls_alpn_selected	Int

fn tls_backend_load(path: Str) -> Result[TlsBackend, Str]

tls_backend_load opens the shared library at path and resolves the eight mandatory backend symbols. The library handle is closed on every failure path, so a failed load never leaks. Stage gate: no call is ever made into the loaded backend. Returns: Ok(TlsBackend) once every symbol resolves; Err("backend not found") when the library cannot be opened, or Err naming the missing symbol when one of the eight does not resolve. Complexity: O(1) OS calls.

• Postcondition: path.len() == 0 => result.is_err == true

fn tls_backend_available(path: Str) -> Bool

tls_backend_available reports whether path loads and exports every mandatory backend symbol (see the module header). It never calls into the backend and closes the library before returning; a library that loads but misses any symbol yields false. Returns: true only when all eight symbols resolve. Complexity: O(1) OS calls.

• Postcondition: path.len() == 0 => result == false

fn tls_err_kind_name(kind: Int) -> Str

tls_err_kind_name maps a taxonomy kind to a short stable name ("none", "load", "arg", "alloc", "cert", "alpn", "handshake", "verify", "io", "eof", "want-read", "want-write", "abi"; "unknown" for anything else). Complexity: O(1).

• Postcondition: ((kind == TLS_ERR_NONE) => (result == "none")) && ((kind == TLS_ERR_LOAD) => (result == "load")) && ((kind == TLS_ERR_HANDSHAKE) => (result == "handshake")) && ((kind == TLS_ERR_ABI) => (result == "abi")) && (result.len() > 0)

fn tls_err_kind_is_want(kind: Int) -> Bool

tls_err_kind_is_want reports whether the kind is the non-fatal readiness form (retry when the fd is readable/writable). Complexity: O(1). Pure.

• Postcondition: (kind == TLS_ERR_WANT_READ) => result == true
• Postcondition: (kind == TLS_ERR_WANT_WRITE) => result == true
• Postcondition: (kind == TLS_ERR_NONE) => result == false

fn tls_err_kind_is_fatal(kind: Int) -> Bool

tls_err_kind_is_fatal reports whether the kind means the session cannot continue (load/abi/arg/alloc/cert/alpn/handshake/verify/io). NONE, EOF and the WANT kinds are not fatal in this sense (EOF is a clean end of stream; ARG is caller misuse, not a session state). Complexity: O(1). Pure.

• Postcondition: (kind == TLS_ERR_HANDSHAKE) => result == true
• Postcondition: (kind == TLS_ERR_IO) => result == true
• Postcondition: (kind == TLS_ERR_EOF) => result == false
• Postcondition: (kind == TLS_ERR_NONE) => result == false

type TlsError

TlsError is a typed TLS failure: a taxonomy kind (TLS_ERR_*) plus a message.

Field	Type
kind	Int
message	Str

type TlsSession

TlsSession is one session on a loaded backend: the raw session id (> 0 while open, 0 after tls_session_close), the role, and the attached fd.

Field	Type
id	Int
server	Bool
fd	Int

fn tls_session_open(backend: &TlsBackend, server: Bool, fd: Int, cert_path: Str, key_path: Str, server_name: Str) -> Result[TlsSession, TlsError]

tls_session_open opens a session against a loaded backend: - server == true: cert_path/key_path are PEM file paths handed to the backend (the fd is already connected); both must be non-empty; - server == false: server_name is the peer name handed to the backend (SNI or equivalent; may be empty). The fd is attached by the backend's *_new call -- the contract has no separate attach symbol; the caller keeps ownership of the fd. The backend's tls_init runs first and must be idempotent (the driver calls it on every open). Returns: Ok(session); Err(TLS_ERR_LOAD) when the backend value is not loaded, Err(TLS_ERR_ARG) on a bad fd or empty material path, Err(TLS_ERR_ALLOC) when the backend refuses the session. Complexity: O(paths).

• Postcondition: (fd < 0) => (result.is_err == true)
• Postcondition: (server == true && cert_path.len() == 0) => (result.is_err == true)
• Postcondition: (server == true && key_path.len() == 0) => (result.is_err == true)

fn tls_session_step(backend: &TlsBackend, sess: &TlsSession) -> Result[Int, TlsError]

tls_session_step advances the handshake one step (server: accept side, client: connect side). Returns: Ok(TLS_STEP_DONE) when the handshake is complete; Ok(TLS_STEP_WANT_READ) / Ok(TLS_STEP_WANT_WRITE) when the caller must wait for fd readiness first (tls_wait_readable / tls_wait_writable) and call again; Err(TLS_ERR_HANDSHAKE) on a fatal handshake failure; Err(TLS_ERR_ARG/TLS_ERR_LOAD) on a bad handle or an unloaded backend. Complexity: O(handshake progress).

• Postcondition: (sess.id <= 0) => (result.is_err == true)

fn tls_session_read(backend: &TlsBackend, sess: &TlsSession, max: Int) -> Result[Vec[UInt8], TlsError]

tls_session_read reads up to max plaintext bytes. Returns: Ok(bytes) with bytes.len() >= 1; Err(TLS_ERR_EOF) when the peer closed the connection cleanly (close_notify); Err (TLS_ERR_IO) on a fatal read failure; Err(TLS_ERR_ARG) on a bad handle or max outside 1..65536. Complexity: O(max).

• Postcondition: (max <= 0) => (result.is_err == true)
• Postcondition: (max > 65536) => (result.is_err == true)

fn tls_session_write(backend: &TlsBackend, sess: &TlsSession, data: &Vec[UInt8]) -> Result[Int, TlsError]

tls_session_write writes data into the session. The contract is all-or-nothing per call: the driver hands the whole payload to the backend and a short count is a typed TLS_ERR_IO (the backend owns its retries). Returns: Ok(len) when the whole payload was accepted (Ok(0) for an empty payload on a live session); Err on a fatal write failure or a bad handle. Complexity: O(len).

• Postcondition: (sess.id <= 0) => (result.is_err == true)

fn tls_session_alpn_selected(backend: &TlsBackend, sess: &TlsSession) -> Result[Str, TlsError]

tls_session_alpn_selected reports the negotiated ALPN protocol name of the session ("" when none was selected -- server-side selection needs a C callback no XIOM backend can install; see tls_alpn_select_server for the application-layer policy). Returns: Ok(name); Err(TLS_ERR_IO) when the backend cannot report it; Err(TLS_ERR_ARG/TLS_ERR_LOAD) on a bad handle. Complexity: O(name length).

• Postcondition: (sess.id <= 0) => (result.is_err == true)

fn tls_session_close(backend: &TlsBackend, sess: &mut TlsSession) -> Result[Unit, TlsError]

tls_session_close releases the session through the backend and marks the handle closed (sess.id := 0), so a second close on the same value is a clean Ok: the backend is never called twice for one session. Returns: Ok(()) once closed (or already closed); Err(TLS_ERR_LOAD) when the backend value is not loaded; Err(TLS_ERR_ARG) for a negative id. Complexity: O(1).

• Postcondition: (backend.handle == 0) => (result.is_err == true)

fn tls_material_sniff(bytes: &Vec[UInt8]) -> Str

tls_material_sniff classifies certificate/key material by its leading bytes: "pem" (begin marker "-----BEGIN"), "der" (ASN.1 SEQUENCE tag 0x30), or "unknown" (empty or anything else). Pure; a pre-flight classification helper (backends load PEM files directly). Complexity: O(1).

• Postcondition: bytes.len() == 0 => result == "unknown"

fn tls_cert_material_check(cert_path: Str, key_path: Str) -> Result[Unit, Str]

tls_cert_material_check pre-validates a certificate/key file pair before any backend call: each path must be non-empty, the files must exist, be readable, and hold at least one byte. A cheap application -layer gate (a missing file is a configuration mistake, not a handshake failure); the material itself is not parsed. Returns: Ok(()) when both files pass; Err naming the first failure. Complexity: O(file size).

• Postcondition: (cert_path.len() == 0) => (result.is_err == true)
• Postcondition: (key_path.len() == 0) => (result.is_err == true)

fn tls_alpn_select_server(server_pref: &Vec[Str], client_offered: &Vec[Str]) -> Result[Str, Str]

tls_alpn_select_server picks the server-side ALPN protocol by server preference: the first entry of server_pref that the client offered. This is the application-layer policy the backend cannot express (no callback bridging), so servers negotiate here and can refuse with the classified no_application_protocol error. Returns: Ok(selected name); Err(TLS_ALPN_NO_APPLICATION_PROTOCOL) when the client offered nothing usable; Err on an empty server preference list (misconfiguration). Complexity: O(server_pref * client_offered). Pure.

• Postcondition: (server_pref.len() == 0) => (result.is_err == true)
• Postcondition: (client_offered.len() == 0) => (result.is_err == true)

fn tls_wait_readable(fd: Int, timeout_ms: Int) -> Result[Bool, Str]

tls_wait_readable waits until fd is readable or the timeout budget runs out (timeout_ms == 0 polls once). An already-ready fd returns immediately. Returns: Ok(true) when the fd reports activity, Ok(false) on timeout; Err on a negative fd or timeout. Complexity: network wait.

• Postcondition: (fd < 0) => (result.is_err == true)
• Postcondition: (timeout_ms < 0) => (result.is_err == true)

fn tls_wait_writable(fd: Int, timeout_ms: Int) -> Result[Bool, Str]

tls_wait_writable waits until fd is writable or the timeout budget runs out (timeout_ms == 0 polls once). Returns: Ok(true) when the fd reports writability, Ok(false) on timeout; Err on a negative fd or timeout. Complexity: network wait.

• Postcondition: (fd < 0) => (result.is_err == true)
• Postcondition: (timeout_ms < 0) => (result.is_err == true)

---

---

---

tls_helper.xi

fn der_length_decode(data: &Vec[UInt8], pos: Int) -> Result[(Int, Int), Str]

Read a DER length at pos. Parameters: data -- the DER bytes; pos -- the position of the length octet. Returns: Ok((length, bytes_consumed)) for short and long forms; Err for indefinite lengths or truncated input. Complexity: O(1). Pure.

• Postcondition: ((pos < 0 || pos >= data.len()) => (result.is_err == true)) && ((result.is_ok == true) => (pos >= 0 && pos < data.len()))

fn asn1_read_oid(data: &Vec[UInt8], pos: Int) -> Result[(Vec[Int], Int), Str]

Read an ASN.1 object identifier at pos. Parameters: data -- the DER bytes; pos -- the position of the OID tag. Returns: Ok((oid components, next_pos)) on success, Err on malformed input. Complexity: O(n). Pure.

• Postcondition: ((pos < 0 || pos >= data.len()) => (result.is_err == true)) && ((result.is_ok == true) => (pos >= 0 && pos < data.len()))

fn cert_fingerprint_sha256(der: &Vec[UInt8]) -> Vec[UInt8]

SHA-256 fingerprint of a DER certificate. Parameters: der -- the certificate DER bytes. Returns: the 32-byte SHA-256 digest. Complexity: O(n). Pure.

• Postcondition: result.len() == 32

fn cert_fingerprint_sha1(der: &Vec[UInt8]) -> Vec[UInt8]

SHA-1 fingerprint of a DER certificate. NOT AVAILABLE: xiom.crypto does not provide SHA-1. Returns an empty vector. Complexity: O(1). Pure.

• Postcondition: result.len() == 0

fn cert_validity_dates(der: &Vec[UInt8]) -> Result[(Str, Str), Str]

Certificate validity period. Parameters: der -- the certificate DER bytes. Returns: Ok((not_before, not_after)) as ASN.1 time strings, Err when the structure cannot be parsed. Complexity: O(n). Pure.

• Postcondition: ((der.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (der.len() > 0))

fn cert_subject_cn(der: &Vec[UInt8]) -> Result[Str, Str]

The common name of the certificate subject. Parameters: der -- the certificate DER bytes. Returns: Ok(CN) on success, Err when unparseable or missing. Complexity: O(n). Pure.

• Postcondition: ((der.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (der.len() > 0))

fn cert_issuer_cn(der: &Vec[UInt8]) -> Result[Str, Str]

The common name of the certificate issuer. Parameters: der -- the certificate DER bytes. Returns: Ok(CN) on success, Err when unparseable or missing. Complexity: O(n). Pure.

• Postcondition: ((der.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (der.len() > 0))

fn cert_public_key_info(der: &Vec[UInt8]) -> Result[(Str, Int), Str]

Public key metadata for a certificate. Parameters: der -- the certificate DER bytes. Returns: Ok((algorithm, bits)) on success, Err when unparseable. Complexity: O(n). Pure.

• Postcondition: ((der.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (der.len() > 0))

fn cert_is_self_signed(der: &Vec[UInt8]) -> Bool

True when subject equals issuer (by common name comparison). Parameters: der -- the certificate DER bytes. Returns: true when both subject and issuer CNs parse and match; false otherwise (including unparseable input). Complexity: O(n). Pure.

• Postcondition: (der.len() == 0) => (result == false)

fn pem_encode(der: &Vec[UInt8], label: Str) -> Str

Wrap DER bytes in a PEM armor with the given label. Parameters: der -- the DER bytes; label -- the PEM label (e.g. "CERTIFICATE"). Returns: the PEM string with 64-column base64 lines. Complexity: O(n). Pure.

• Postcondition: result.len() >= der.len() + 2 * label.len() + 32

fn pem_decode(pem: Str) -> Result[Vec[UInt8], Str]

Strip PEM armor and return the DER bytes. Parameters: pem -- the PEM string. Returns: Ok(DER bytes) on success, Err when no matching block is found. Complexity: O(n). Pure.

• Postcondition: ((pem.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (pem.len() > 0))

fn pem_parse_certificates(pem: Str) -> Result[Vec[Vec[UInt8]], Str]

Extract every certificate block from a PEM string. Parameters: pem -- the PEM string. Returns: Ok(the DER bytes of each CERTIFICATE block) on success, Err when no certificate block is present. Complexity: O(n). Pure.

• Postcondition: ((pem.len() == 0) => (result.is_err == true)) && ((result.is_ok == true) => (pem.len() > 0))

---

---

---

tls_libssl.xi

type TlsLibssl

TlsLibssl is a loaded libssl: the module handle plus the resolved session-surface entry points (17). Owned by the caller; release with tls_libssl_close.

Field	Type
handle	Int
soname	Str
p_tls_server_method	Int
p_tls_client_method	Int
p_ctx_new	Int
p_ctx_free	Int
p_ctx_use_cert_file	Int
p_ctx_use_key_file	Int
p_new	Int
p_free	Int
p_set_fd	Int
p_accept	Int
p_connect	Int
p_read	Int
p_write	Int
p_shutdown	Int
p_get_error	Int
p_ctx_set_alpn_protos	Int
p_get0_alpn_selected	Int

type TlsLibSession

TlsLibSession is one libssl session: the SSL* handle, its owning SSL_CTX and the attached fd. Owned by the caller; release with tls_libssl_free (which frees the session AND its context).

Field	Type
ssl	Int
ctx	Int
fd	Int

fn tls_libssl_load() -> Result[TlsLibssl, TlsError]

tls_libssl_load loads the first available system libssl from the candidate sonames (libssl-3-x64.dll, libssl-1_1-x64.dll, libssl-1_1.dll, libssl.dll). An unopenable candidate moves to the next; a candidate that opens but misses an entry point reports Err(TLS_ERR_ABI) immediately (a loud ABI mismatch must not be masked by falling through to another soname). Returns: Ok(library); Err(TLS_ERR_LOAD) when no candidate loaded. Complexity: O(candidates * entry points).

• Postcondition: true

fn tls_libssl_load_named(soname: Str) -> Result[TlsLibssl, TlsError]

tls_libssl_load_named loads an explicitly named libssl build (a bogus name exercises the absent/LOAD classification deterministically on any host). Returns: Ok(library); Err(TLS_ERR_LOAD) when the name does not open. Complexity: O(entry points).

• Postcondition: (soname.len() == 0) => (result.is_err == true)

fn tls_libssl_available() -> Bool

tls_libssl_available reports whether any candidate soname opens and exports every entry point. The library is closed before returning. Returns: true only when a full candidate is present. Complexity: O(candidates * entry points).

• Precondition: true

fn tls_libssl_close(lib: &TlsLibssl) -> Result[Unit, Str]

tls_libssl_close releases the library handle. Returns: Ok(()) once closed; Err with the loader error if the handle cannot be released. Complexity: O(1).

• Precondition: lib.handle != 0

fn tls_libssl_alpn_client_wire(names: &Vec[Str]) -> Result[Vec[UInt8], Str]

tls_libssl_alpn_client_wire builds the client ALPN protocol list in the format SSL_CTX_set_alpn_protos expects: one 1-byte-length-prefixed name each, names 1..255 bytes, at most 65535 bytes total, WITHOUT the RFC 7301 ProtocolNameList 2-byte outer length (the TLS stack adds that outside the extension data; the binding's live suite locks this format against OpenSSL 3.2.4). Use tls.alpn_encode when you need the on-the-wire extension format instead. Returns: Ok(wire bytes); Err on an empty list, empty/oversized name, or an oversized total. Complexity: O(total bytes). Pure.

• Postcondition: names.len() == 0 => result.is_err == true

fn tls_libssl_server_session(lib: &TlsLibssl, fd: Int, cert_path: Str, key_path: Str) -> Result[TlsLibSession, TlsError]

tls_libssl_server_session creates a server session on a connected fd: TLS_server_method + SSL_CTX_new, PEM cert/key load from files (SSL_CTX_use_certificate_file / SSL_CTX_use_PrivateKey_file, X509_FILETYPE_PEM), SSL_new and SSL_set_fd. On any failure the partially built context/session is released before returning. Returns: Ok(session); Err(TLS_ERR_ARG) on a bad fd/empty path, Err(TLS_ERR_ALLOC) when allocation fails, Err(TLS_ERR_CERT) when the material is rejected, Err(TLS_ERR_IO) when the fd cannot be attached; Err(TLS_ERR_LOAD) for an unloaded value. Complexity: O(file size).

• Postcondition: (fd < 0) => (result.is_err == true)
• Postcondition: (cert_path.len() == 0) => (result.is_err == true)
• Postcondition: (key_path.len() == 0) => (result.is_err == true)

fn tls_libssl_client_session(lib: &TlsLibssl, fd: Int, alpn: &Vec[Str]) -> Result[TlsLibSession, TlsError]

tls_libssl_client_session creates a client session on a connected fd: TLS_client_method + SSL_CTX_new, optional ALPN client list (set on the context BEFORE SSL_new -- SSL_new copies the list to the session), SSL_new and SSL_set_fd. On any failure the partially built context/session is released before returning. No SNI host name is set (out of the minimal entry-point set; xiom.ssl binds SSL_ctrl for it). Returns: Ok(session); Err(TLS_ERR_ARG) on a bad fd, Err (TLS_ERR_ALLOC) when allocation fails, Err(TLS_ERR_ALPN) when the build rejects the ALPN list, Err(TLS_ERR_IO) when the fd cannot be attached. Complexity: O(ALPN list).

• Postcondition: (fd < 0) => (result.is_err == true)

fn tls_libssl_step(lib: &TlsLibssl, sess: &TlsLibSession, server: Bool) -> Result[Int, TlsError]

tls_libssl_step advances the handshake one step (SSL_accept for server == true, SSL_connect otherwise) and classifies SSL_get_error into the tls.xi taxonomy. Returns: Ok(TLS_STEP_DONE) when the handshake completed; Ok(TLS_STEP_WANT_READ/WRITE) when the caller must wait for fd readiness first (tls_wait_readable / tls_wait_writable) and call again; Err(TLS_ERR_HANDSHAKE) on a fatal failure (including a peer close mid-handshake). Complexity: O(handshake progress).

• Postcondition: (sess.ssl <= 0) => (result.is_err == true)

fn tls_libssl_read(lib: &TlsLibssl, sess: &TlsLibSession, max: Int) -> Result[Vec[UInt8], TlsError]

tls_libssl_read reads up to max plaintext bytes. On a WANT state the call waits on the attached socket with a bounded poll and retries. Returns: Ok(bytes) with bytes.len() >= 1; Err(TLS_ERR_EOF) on a clean close_notify; Err(TLS_ERR_IO) on a fatal failure; Err (TLS_ERR_WANT_READ) when the bounded wait timed out. Complexity: O(max + wait).

• Postcondition: (max <= 0) => (result.is_err == true)
• Postcondition: (max > 65536) => (result.is_err == true)
• Postcondition: (sess.ssl <= 0) => (result.is_err == true)

fn tls_libssl_write(lib: &TlsLibssl, sess: &TlsLibSession, data: &Vec[UInt8]) -> Result[Int, TlsError]

tls_libssl_write writes every byte of data (Ok(0) for an empty payload on a live session), retrying partial writes and waiting on WANT states with a bounded socket poll. Returns: Ok(data.len()) when the whole payload was written; Err (TLS_ERR_IO) on a fatal failure or when the bounded wait runs out; Err(TLS_ERR_ARG) on a bad handle. Complexity: O(len + wait).

• Postcondition: (sess.ssl <= 0) => (result.is_err == true)

fn tls_libssl_shutdown(lib: &TlsLibssl, sess: &TlsLibSession) -> Result[Int, TlsError]

tls_libssl_shutdown runs one SSL_shutdown step. Returns: Ok(0) when this side's close_notify was sent and the peer's is pending; Ok(1) when the shutdown is complete; Err (TLS_ERR_WANT_READ/WRITE) when the caller should wait for fd readiness and call again; Err(TLS_ERR_IO) on a fatal failure. Complexity: O(1).

• Postcondition: (sess.ssl <= 0) => (result.is_err == true)

fn tls_libssl_alpn_selected(lib: &TlsLibssl, sess: &TlsLibSession) -> Result[Str, TlsError]

tls_libssl_alpn_selected reports the negotiated ALPN protocol of the session ("" when none was selected -- a server without a select callback negotiates none; see tls_alpn_select_server for the application-layer policy). The length comes from OpenSSL's out-parameter slots; the bytes copy out through the ffi SafePtr bounds-checked reader. Returns: Ok(name); Err(TLS_ERR_IO) when the report cannot be read. Complexity: O(name length).

• Postcondition: (sess.ssl <= 0) => (result.is_err == true)

fn tls_libssl_free(lib: &TlsLibssl, sess: &TlsLibSession)

tls_libssl_free releases the session and its owning context (SSL_free then SSL_CTX_free). A zeroed/closed session value is a clean no-op; the caller must not reuse the session after this. Complexity: O(1).

• Precondition: true

---

---

---

udp.xi

fn udp_validate_port(p: Int) -> Bool

udp_validate_port returns true if p is a valid UDP port (1-65535). Complexity: O(1). Pure.

• Postcondition: result == (p > 0 && p <= 65535)

fn udp_is_valid_port(p: Int) -> Bool

udp_is_valid_port is an alias for udp_validate_port. Complexity: O(1). Pure.

• Postcondition: result == (p > 0 && p <= 65535)

fn udp_parse_endpoint(s: Str) -> Option[(Str, Int)]

udp_parse_endpoint splits a "host:port" string into (host, port). Returns None if no colon or a malformed port is present. Complexity: O(n). Pure.

• Postcondition: ((s.len() == 0) => (result.is_none == true)) && ((result.is_some == true) => (s.len() >= 3))

fn udp_format_endpoint(host: Str, port: Int) -> Str

udp_format_endpoint builds a "host:port" string. Complexity: O(1). Pure.

• Postcondition: result == host + ":" + port.to_str()

---

---

---

unix.xi

type UnixSocket

struct UnixSocket { fd: Int; path: Str; listening: Bool }

Field	Type
fd	Int
path	Str
listening	Bool

fn unix_connect(path: Str) -> Result[UnixSocket, Str]

Connect to a listening unix socket. NOT IMPLEMENTED: requires the AF_UNIX socket layer (not available in the pure stdlib). Returns: Err("unix_connect: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_listen(path: Str) -> Result[UnixSocket, Str]

Create a listening socket on a path. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_listen: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_accept(sock: UnixSocket) -> Result[UnixSocket, Str]

Accept an incoming connection. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_accept: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_send(sock: UnixSocket, data: &Vec[UInt8]) -> Result[Int, Str]

Write bytes to a socket. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_send: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_recv(sock: UnixSocket, max: Int) -> Result[Vec[UInt8], Str]

Read up to max bytes from a socket. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_recv: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_close(sock: UnixSocket)

Close a socket and its fd. NO-OP: no live sockets exist in the pure stdlib.

• Postcondition: true

fn unix_bind(path: Str) -> Result[UnixSocket, Str]

Bind a socket to a path. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_bind: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_connect_timeout(path: Str, timeout_ms: Int) -> Result[UnixSocket, Str]

Connect with a timeout. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_connect_timeout: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_socketpair() -> Result[(UnixSocket, UnixSocket), Str]

Create an anonymous connected pair. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_socketpair: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

fn unix_peer_credentials(sock: UnixSocket) -> Result[(Int, Int, Int), Str]

Read the peer pid, uid, and gid. NOT IMPLEMENTED: requires the AF_UNIX socket layer (see unix_connect). Returns: Err("unix_peer_credentials: AF_UNIX sockets not available in the pure stdlib").

• Postcondition: result.is_err == true

---

---

---

url.xi

fn url_parse(url: Str) -> Result[UrlParts, Str]

url_parse parses a URL into its scheme/host/port/path/query/fragment components. Userinfo (user:pass@) is skipped.

• Postcondition: (result.is_ok == false) || (url.len() != 0)

fn url_decode_component(s: Str) -> Result[Str, Str]

url_decode_component percent-decodes %XX sequences. '+' is left as-is (component semantics -- '+' is only a space in form-encoding).

• Postcondition: (s.len() == 0) => (result.is_ok == true)

fn url_encode_component(s: Str) -> Result[Str, Str]

url_encode_component percent-encodes everything except the unreserved characters A-Z a-z 0-9 - _ . ~ (reuses xiom.encoding.percent_encode).

• Postcondition: (result.is_ok == true)

fn url_query_parse(query: Str) -> Vec[(Str, Str)]

url_query_parse splits a query string on '&' and each pair on the first '=', percent-decoding both sides and converting '+' to a space (application/x-www-form-urlencoded semantics).

• Postcondition: ((query.len() == 0) && (result.len() == 0)) || ((query.len() != 0) && (result.len() >= 1))

fn url_query_build(pairs: Vec[(Str, Str)]) -> Str

url_query_build joins key/value pairs as k=v separated by '&', applying component encoding to both keys and values.

• Postcondition: ((pairs.len() == 0) && (result == "")) || ((pairs.len() != 0) && (result.len() >= 1))

fn url_normalize(url: Str) -> Result[Str, Str]

url_normalize lowercases the scheme and host, strips the default port, and removes dot segments from the path. Query and fragment are kept.

• Postcondition: (result.is_ok == false) || (url.len() != 0)

fn url_is_absolute(url: Str) -> Bool

url_is_absolute returns true if the URL carries a scheme (a ':' before any '/').

• Postcondition: (result == true) => (url.len() >= 1)

fn url_join(base: Str, relative: Str) -> Result[Str, Str]

url_join resolves a relative reference against a base URL (RFC 3986 S5.3 merge), then normalizes dot segments. If the reference carries its own scheme it is returned unchanged.

• Postcondition: (result.is_ok == false) || (relative.len() != 0) || (base.len() != 0)

---

---

---

websocket.xi

type WsFrame

struct WsFrame { opcode: Int; fin: Bool; masked: Bool; payload: Vec[UInt8] }

Field	Type
opcode	Int
fin	Bool
masked	Bool
payload	Vec[UInt8]

Derives: Clone

type WsConnection

struct WsConnection { fd: Int; key: Str; open: Bool; pending: Vec[UInt8] } pending carries bytes received past a head/frame boundary across ws_recv calls; the fd stays a live socket owned by the connection until ws_close.

Field	Type
fd	Int
key	Str
open	Bool
pending	Vec[UInt8]

fn ws_handshake_request(host: Str, path: Str, key: Str) -> Str

ws_handshake_request builds a client upgrade request for the given host, path, and Sec-WebSocket-Key value. Complexity: O(1). Pure.

• Postcondition: ((path.len() == 0) => (result.len() == 115 + host.len() + key.len())) && ((path.len() > 0) => (result.len() == 114 + path.len() + host.len() + key.len()))

fn ws_accept_key(key: Str) -> Str

ws_accept_key computes the Sec-WebSocket-Accept value for a client key per RFC 6455: base64(SHA-1(key + GUID)). Complexity: O(n).

• Postcondition: result.len() == 28

fn ws_handshake_verify(response: Str, key: Str) -> Bool

ws_handshake_verify checks a server upgrade response against the client key: the status line must be 101 and the Sec-WebSocket-Accept header must match the computed accept value. Complexity: O(n). Pure.

• Postcondition: ((response.len() == 0) => (result == false)) && ((result == true) => (response.len() > 0))

fn ws_handshake_response(key: Str) -> Str

ws_handshake_response builds the server 101 upgrade response for a client's Sec-WebSocket-Key value (RFC 6455 4.2.2). Complexity: O(n). Pure.

• Postcondition: result.len() == 129

fn ws_request_key(request: Str) -> Result[Str, Str]

ws_request_key extracts the Sec-WebSocket-Key header value from a client upgrade request (case-insensitive name, optional whitespace trimmed, value up to the line end). Returns Err when the header is missing or empty. Complexity: O(n). Pure.

• Postcondition: result is Ok(_) => request.len() > 0

fn ws_frame_encode(opcode: Int, payload: &Vec[UInt8], mask: Bool) -> Vec[UInt8]

ws_frame_encode serializes one final WebSocket frame (FIN set): a thin delegate to ws_frame_encode_fin with fin = true. When mask is true a deterministic client mask (derived from the payload length) is applied -- adequate for protocol correctness; layer a random key at the call site if unpredictability matters. Complexity: O(n). Pure.

• Postcondition: (result.len() >= 2) && ((mask == false && payload.len() < 126) => (result.len() == payload.len() + 2)) && ((mask == true && payload.len() < 126) => (result.len() == payload.len() + 6)) && ((payload.len() >= 126) => (result.len() >= payload.len() + 4))

fn ws_frame_encode_fin(opcode: Int, fin: Bool, payload: &Vec[UInt8], mask: Bool) -> Vec[UInt8]

ws_frame_encode_fin serializes one WebSocket frame with an explicit FIN flag (fragmented messages send continuation frames with fin = false and opcode 0; the first frame carries the message opcode). When mask is true a deterministic client mask (derived from the payload length) is applied. Complexity: O(n). Pure.

• Postcondition: (result.len() >= 2) && ((mask == false && payload.len() < 126) => (result.len() == payload.len() + 2)) && ((mask == true && payload.len() < 126) => (result.len() == payload.len() + 6)) && ((payload.len() >= 126) => (result.len() >= payload.len() + 4))

fn ws_frame_take(bytes: &Vec[UInt8]) -> Result[(WsFrame, Int), Str]

ws_frame_take parses the first WebSocket frame from bytes and reports how many bytes it consumed (only that many belong to the frame; any trailing bytes stay with the caller). Err("incomplete frame") means "read more bytes and retry" -- the incremental reader treats every Err as insufficient input and is bounded by its own size cap. Validation: RSV bits are rejected, only known opcodes are accepted, control frames must be final and <=125 bytes, lengths must be minimal, the 64-bit MSB must be clear, declared payloads above 1 MiB are rejected, close codes must be wire-valid (with a UTF-8 reason), and a final text frame must be valid UTF-8. Fragmented text/continuation validity is the caller's reassembly responsibility. Complexity: O(n). Pure.

• Postcondition: result is Ok(_) => bytes.len() >= 2

fn ws_frame_decode(frame: &Vec[UInt8]) -> Result[WsFrame, Str]

ws_frame_decode parses one WebSocket frame from bytes (a thin wrapper over ws_frame_take that drops the consumed count). Err means the input does not hold a complete frame. Complexity: O(n). Pure.

• Postcondition: result is Ok(_) => frame.len() >= 2

fn ws_close_code(frame: &WsFrame) -> Option[Int]

ws_close_code extracts the 2-byte close code from a close frame's payload (RFC 6455 7.4); None for non-close frames or short payloads. Complexity: O(1). Pure.

• Postcondition: frame.opcode != 8 => result is None

fn ws_random_key() -> Str

ws_random_key generates a Sec-WebSocket-Key value (base64 of 16 bytes) for use in client handshakes. Deterministic derivation from the current time keeps the module free of external RNG state.

• Postcondition: result.len() == 24

fn ws_parse_url(url: Str) -> Result[(Str, Int, Str), Str]

ws_parse_url splits a ws:// or wss:// URL into host, port, and path. The port is the explicit port when present, otherwise the scheme default. Returns Err for malformed input. Complexity: O(n). Pure.

• Postcondition: ((url.len() < 4) => (result.is_err == true)) && ((result.is_ok == true) => (url.len() >= 4))

fn ws_split_headers(bytes: &Vec[UInt8]) -> Result[(Str, Vec[UInt8]), Str]

ws_split_headers splits an HTTP head from the bytes after its CRLFCRLF terminator, preserving any leftover bytes byte-exact (they may already belong to the next frame). Err("incomplete headers") means "read more bytes and retry". Complexity: O(n). Pure.

• Postcondition: result is Ok(_) => bytes.len() >= 4

fn ws_connect(url: Str) -> Result[WsConnection, Str]

ws_connect opens a WebSocket connection to a ws:// or wss:// URL, performing the client handshake. The response head is consumed exactly at CRLFCRLF and any extra bytes are carried in the connection's pending buffer. TLS (wss) is not supported by the runtime socket layer; use ws://. Complexity: network I/O.

• Postcondition: result is Ok(_) => url.len() >= 4

fn ws_send(conn: &WsConnection, text: Str) -> Result[Unit, Str]

ws_send sends a text message over an open connection. Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == true

fn ws_send_binary(conn: &WsConnection, data: &Vec[UInt8]) -> Result[Unit, Str]

ws_send_binary sends a binary message over an open connection. Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == true

fn ws_recv(conn: &mut WsConnection) -> Result[WsFrame, Str]

ws_recv receives the next frame from the connection. Bytes are read incrementally from the connection's pending buffer plus the socket, stopping exactly at the frame boundary (bounded by a 1 MiB frame cap); a persistent connection is never read to EOF. Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == true

fn ws_close(conn: &mut WsConnection, code: Int) -> Result[Unit, Str]

ws_close sends a close frame, closes the socket and marks the connection closed. Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == false

fn ws_ping(conn: &WsConnection) -> Result[Unit, Str]

ws_ping sends a ping frame. Returns: Ok(()) once the frame is on the wire; Err (including a closed connection). Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == true

fn ws_pong(conn: &WsConnection) -> Result[Unit, Str]

ws_pong sends a pong frame. Returns: Ok(()) once the frame is on the wire; Err (including a closed connection). Complexity: network I/O.

• Postcondition: result is Ok(_) => conn.open == true

---

---

---

ws.xi

fn ws_default_port(scheme: Str) -> Int

ws_default_port returns the default port for a ws scheme ("ws" -> 80, "wss" -> 443, anything else -> 80). Complexity: O(1). Pure.

• Postcondition: ((scheme == "wss") => (result == 443)) && ((scheme != "wss") => (result == 80))

fn ws_parse_url(url: Str) -> Result[(Str, Int, Str), Str]

ws_parse_url splits a ws:// or wss:// URL into (host, port, path). The port is the explicit port from the URL when present, otherwise the scheme default. Returns Err for malformed input. Complexity: O(n).

• Postcondition: ((url.len() < 6) => (result.is_err == true)) && ((result.is_ok == true) => (url.len() >= 6))

fn ws_build_url(scheme: Str, host: Str, port: Int, path: Str) -> Str

ws_build_url builds a ws:// or wss:// URL from host, port, and path. When port matches the scheme default it is omitted. Complexity: O(1).

• Postcondition: result.len() >= scheme.len() + host.len() + 4

fn ws_is_ws_url(url: Str) -> Bool

ws_is_ws_url returns true if url starts with ws://. Complexity: O(n). Pure.

• Postcondition: ((url.len() < 5) => (result == false)) && ((result == true) => (url.len() >= 5))

fn ws_is_wss_url(url: Str) -> Bool

ws_is_wss_url returns true if url starts with wss://. Complexity: O(n). Pure.

• Postcondition: ((url.len() < 6) => (result == false)) && ((result == true) => (url.len() >= 6))

---

---

---