Skip to content
XTXP

Verification

decided in shape, draft in detail (hashes use canonical form v0)

No implementation code gets written until its behaviour is defined. The source of truth is:

  • Gherkin .feature files describing behaviour in plain language
  • JSON test vectors generated from them: an initial state, plus per-client operation streams delivered late and out of order

One suite, every implementation

Section titled “One suite, every implementation”
Verification: feature files feed a fuzzer that emits JSON vectors; vectors run through the Xmesh harness and its invariant checks, and SHA-256 hashes of canonical XML are compared across delivery orders; a later native C++ rewrite is held to the same vectors; for M1 the same vectors are replayed by CLI peers through a Rust host over WebSocket, with forced disconnects.Verification: feature files feed a fuzzer that emits JSON vectors; vectors run through the Xmesh harness and its invariant checks, and SHA-256 hashes of canonical XML are compared across delivery orders; a later native C++ rewrite is held to the same vectors; for M1 the same vectors are replayed by CLI peers through a Rust host over WebSocket, with forced disconnects.
Select the diagram to view it full screenPlantUML source
Harness Why it exists
Xmesh on Yrs (cargo test) The implementation. Every vector is replayed in many delivery orders.
Native C++ Xmesh Later spike. Held to the same vectors and cross-checked against Xmesh on Yrs.

The pass conditions are invariants, checked on every run:

  • Convergence: every delivery order ends with the same SHA-256 of the canonical XML.
  • No cycles: the materialised tree is always a tree.
  • Idempotence: delivering an operation twice changes nothing.

Vectors also pin down the session rules (decision 19):

  • Fork after a deletion: a fork rebuilt from its snapshot still holds content deleted after the fork.
  • ETag on delete: deleting a shape changes the snapshot hash.
  • Refusal doesn’t stall: a refused session is never merged, and every admitted session keeps converging.
  • Held dependencies: a session built on an unadmitted one is held back with it, with a defined error.
  • Client ID reuse: a binding for a client ID already in the session’s history is rejected.

And the tree rules (decision 20):

  • Moves never form cycles: concurrent moves that would make a cycle of two, three or more elements converge to the same tree in every delivery order.
  • Same-spot inserts: two peers inserting at the same place get the same order on every peer.
  • Deletion: a deleted element and its subtree leave the document; undo brings them back.
  • Known gaps, as expected failures (moves in v1): an edit made during a move appears on the copy; two concurrent moves of one element leave one copy. These vectors are kept so the gaps stay visible, and pass once a tree layer of our own lands.
  • Signatures: a challenge answer, binding or grant is rejected on a different host, for a different session, or under the wrong domain tag.
  • Duplicate ids: two sessions creating the same id merge, converge, and flag the duplicate.
  • Mixed content, namespaces and every node kind: <text> with interleaved <tspan>s, inkscape: and sodipodi: attributes, comments, processing instructions and CDATA all round-trip.

The fuzzer

Section titled “The fuzzer”

The first task from the original handover, re-scoped to feed every harness. It generates:

  • an initial SVG (a root <svg> with one <g> layer)
  • randomised operations from several clients: inserting paths, updating attributes, moving nodes, adding comments
  • one chronological stream per client, plus heavily delayed and shuffled delivery orders

Over a real network

Section titled “Over a real network”

Milestone M1 runs the same vectors through three CLI peers (one a late joiner) and a headless muppet hosting the session, all embedding Xmesh, over WebSocket, including dropped connections and reconnect sync. Convergence then holds over a real, unreliable network, not just in a test process.