85 lines
4.8 KiB
Markdown
85 lines
4.8 KiB
Markdown
# 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.
|