Marrakesh
Express
Daemon
A Hotline protocol server in Rust. Hexagonal architecture, dual-database support, formally verified invariants. The protocol is the product.
Welcome to the mxd project site. These pages document the architecture, protocol surface, deployment options, and verification strategy behind the Marrakesh Express Daemon — a Hotline protocol server written in Rust. Use the navigation above to explore the quickstart guide, installation instructions, configuration reference, compatibility matrix, and roadmap.
The Hotline protocol, treated seriously
mxd is building toward Hotline server protocol v1.8.5 coverage. The evidence-backed core today is narrower than the full design set: the 12-byte handshake and 8-byte reply, compatibility-aware login replies, authenticated-session continuity, and selected routed file and news flows. The binary wire format still matters — 20-byte frame headers, big-endian integers, multi-fragment reassembly — but broad chat, presence, and full client parity remain roadmap work.
Hotline 1.8.5, Hotline 1.9, and SynHX compatibility is partial
rather than complete. Runtime selection is part of that operator
surface too: the legacy-networking
feature remains enabled by default, so the classic mxd
binary stays available unless the build deliberately targets a
Wireframe-only runtime.
Handshake validation, timeout handling, login compatibility negotiation, selected file and news routes, and the verification workflow that backs those claims.
Compatibility rows are intentionally narrow. Hotline banner fields 161/162, SynHX omission semantics, XOR heuristics, and selected routed transactions are covered; user-list and messaging parity are not.
Chat invites, subjects, history, object-store-backed file services, aliases, drop boxes, bundles, categories, and threaded news pointers are documented models whose broader runtime wiring still sits on the roadmap.
Built to be reasoned about
Hexagonal Architecture
Domain logic sits behind ports. The Wireframe transport adapter handles framing and routing; Diesel handles persistence. Neither leaks into the other. Swap the database. Swap the transport. The domain doesn't notice.
Dual Database
SQLite for a single-file deployment that fits in a pocket. PostgreSQL when concurrent access matters at scale. One codebase, dual migration trees, compile-time backend selection. Recursive CTEs work on both.
Client Compatibility
Hotline 1.8.5, Hotline 1.9, and SynHX. Banner field augmentation, XOR text obfuscation detection, sub-version gating — all handled at the adapter boundary. A compatibility matrix tracks what works, what's partial, and what remains roadmap work. No over-claiming.
Verified Correct
TLA+ specifications model the handshake state machine. Stateright explores concurrent session interleavings. Kani proves bounded invariants for XOR round-trips and frame validation. Protocol correctness is not left to hope.
Every byte accounted for
The Hotline transaction frame is 20 bytes: flags, reply bit, transaction type, ID, error code, total size, data size. When data_size < total_size, continuation frames follow until the payload is fully assembled. Each continuation must echo the original header's flags, type, ID, error, and total size.
mxd's codec validates all of this in a single decoding pass. Payloads exceeding 1 MiB are rejected. Fragment sizes are clamped to 32 KiB. Outbound encoding produces byte-for-byte parity with the legacy runtime.
Property tests confirm it. Kani proves it. AFL++ fuzzes it nightly.
Configuration without ceremony
mxd ships two documented runtime binaries. With
legacy-networking
enabled by default, the classic mxd
daemon remains available alongside
mxd-wireframe-server.
Both binaries share the same CLI module, environment overrides,
.mxd.toml
defaults, and admin subcommands such as
create-user.
OrthoConfig merges configuration layers in the documented order:
defaults < file < env < CLI. Set
MXD_DATABASE
to a Postgres connection string. Set
MXD_BIND
to a socket address. Drop a
.mxd.toml
for persistent defaults. Migrations apply automatically before
administrative commands insert users or before the daemon starts.
Wireframe-only builds are deliberate, not implicit. Disable default
features to omit the legacy binary and force
server::run()
onto the Wireframe runtime. That selection is part of documented
behaviour coverage and is tested as such.
Tested at every layer
TLA+/TLC handles abstract state machines and policy invariants. Stateright explores authenticated-session continuity, privilege gating, and ordering across multiple clients. Kani proves sharp local invariants such as XOR round-trips, header validation, and login compatibility boundary checks. Adapters are exercised through targeted integration tests rather than treated as the semantic source of truth.
The pull-request suite runs bounded Stateright models, the
highest-value Kani harnesses, and the critical TLC specs. Nightly
jobs deepen the bounds and publish counterexample artefacts for
triage. Counterexamples become regression tests under
tests/regression/.
The explicit invariants called out in the reference set include handshake gating, privilege enforcement, drop-box visibility, and threaded news consistency. Release notes are expected to describe any compatibility deviation with the matrix, not leave it buried in CI output.