Files
troupe-standup/wizard-work/null/crdtkit/README-crdtkit.md
T

4.8 KiB

crdtkit — state-based CRDTs with proven merge laws

Three dependency-free CvRDTs in orcrdt.py, and a test suite that checks the merge laws two ways: by random gossip simulation, and by mutation — deliberately broken merges must be caught by the same check, or the check is decoration.

crdtkit/orcrdt.py        ORSet, PNCounter, LWWRegister, CRDTError   (stdlib only)
crdtkit/test_crdt.py     29 unittest cases: laws, semantics, serialization,
                         convergence, mutation teeth, differential oracle
crdtkit/evidence_run.py  prints the evidence matrix; exit 0 iff every claim holds
crdtkit/evidence.txt     captured output of the run below

Re-run (any cwd):

python3 /root/troupe-standup/wizard-work/null/crdtkit/test_crdt.py
python3 /root/troupe-standup/wizard-work/null/crdtkit/evidence_run.py

Semantics

type state merge guarantee
ORSet elem -> {tag}, tombstone set of tags; tag = (replica, counter) union of both sets add-wins: a remove kills only the tags it observed
PNCounter per-replica inc/dec vectors pointwise max each replica writes only its own slot, so max is a join
LWWRegister (value, stamp); stamp = (timestamp:int, replica:str) max stamp winner independent of merge order; equal stamp + differing value is refused

merge is pure — it never mutates self or its arguments — and every state has a canonical state_key() plus a to_state()/dumps()/loads() JSON round-trip.

Measured evidence (verbatim evidence.txt)

orcrdt evidence run
python 3.14.7 on Linux
seeds 0..15, 3 replicas x 80 ops x 4 gossip rounds (5x150 for the big one)

[A] convergence: every replica equals the join of all pre-gossip states
    ORSet        16/16 seeds  5-replica ensemble: converged
    PNCounter    16/16 seeds  5-replica ensemble: converged
    LWWRegister  16/16 seeds  5-replica ensemble: converged

[B] mutation teeth: a broken merge must be caught by the same check
    ORSetDropsForeignTombstones      caught at 16/16 seeds; semantic divergence: yes; real class green on those seeds: yes
    PNCounterDropsDecrements         caught at 16/16 seeds; semantic divergence: yes; real class green on those seeds: yes
    LWWLastArgumentWins              caught at 10/16 seeds; semantic divergence: yes; real class green on those seeds: yes
    ORSetNoOpMerge                   caught at 16/16 seeds; semantic divergence: yes; real class green on those seeds: yes
    PNCounterSumMerge                caught at 16/16 seeds; semantic divergence: yes; real class green on those seeds: yes

[C] differential vs independent reference model (OR-Set)
    16/16 seeds agree (both implementations, all replicas)

FAILURES: none

Additional runs (measured, not claimed): suite exits 0 under PYTHONHASHSEED in {0, 1, 7, 42, 12345} (no dict-iteration-order dependence) and under python3 -O.

Negative control (measured): a copy of this kit whose ORSet.merge drops foreign tombstones — a one-line change in the merge — exits 1 with 7 failures, while the unmodified kit exits 0. The CHECK is therefore a real test, not a tautology.

What each block proves, and what it does not

  • [A] — replicas that gossip serialized snapshots in random order, with duplicate deliveries, all end at the exact join of their pre-gossip states, in both state and semantic value. 3 replicas x 80 ops x 16 seeds, plus a 5-replica x 150-op ensemble. Not proven: any real transport, reordering under partitions, or Byzantine behaviour.
  • [B] — five wrong merges (drop foreign tombstones, drop decrements, last-argument wins, ignore the argument, sum instead of max) all go red on the same check, while the real class stays green on exactly those seeds. This is the part that makes [A] evidence rather than a green light that would also shine on broken code. LWWLastArgumentWins is caught on 10/16 seeds, not 16 — reported as measured.
  • [C] — ORSet agrees with RefORSet, a separately written naive model with a different state layout (flat (elem, replica, counter) tag set). Agreement is cross-implementation, not self-confirmation. Not proven: agreement on workloads outside the harness (only 5 distinct elements, 3 replicas, one op mix).

Honest limits

  • Elements must be JSON scalars (str/int/float/bool/None) — deliberate, so to_state() is lossless rather than repr-based.
  • LWWRegister assumes replica ids are unique per node; two nodes sharing an id and writing at the same timestamp raise CRDTError instead of silently diverging.
  • Tombstones and per-replica vector slots are never garbage-collected: state grows with history. No delta-CRDT or anti-entropy protocol is provided.
  • Merge is whole-state (O(state)), not incremental.