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.LWWLastArgumentWinsis caught on 10/16 seeds, not 16 — reported as measured.[C]—ORSetagrees withRefORSet, 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, soto_state()is lossless rather thanrepr-based. LWWRegisterassumes replica ids are unique per node; two nodes sharing an id and writing at the same timestamp raiseCRDTErrorinstead 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.