FAILURE MAP
← Case archive

FA-75046 / CRDT convergence / Open access

Bounded counter with rights transfer: rights are computed from the global value · case 01

Two replicas both spend the whole observed balance and the merged counter drops below zero.

Verified by executionVariant 1 · 8 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

A replica's own rights use the sum of all increments and decrements instead of its own slots.

THE FAILURE

A replica's own rights use the sum of all increments and decrements instead of its own slots.

Unsuccessful approach: Charging everyone's decrements against the replica's own increments rejects spending that is locally funded.

Case contract

Replicas share maps P (increments by replica), D (decrements by replica) and T ("from>to" transferred rights). A replica's rights are its own P minus its own D plus transfers to it minus transfers from it, all read from its local view. ["inc", r, k] grows P[r]; ["dec", r, k] and ["move", r, to, k] are rejected (event index recorded) unless rights >= k. ["sync", s, d] folds s's maps into d by maximum. Return values (sum P - sum D), rights, and rejected indices.

Why this case matters

Bounded counters keep a global non-negativity invariant without coordination by escrowing rights per replica.

1 / The failure

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(events, replicas):
    P = {r: {} for r in replicas}
    D = {r: {} for r in replicas}
    T = {r: {} for r in replicas}
    rejected = []
    def rights(r):
        own = sum(P[r].values()) - sum(D[r].values())
        incoming = sum(v for k, v in T[r].items() if k.split('>')[1] == r)
        outgoing = sum(v for k, v in T[r].items() if k.split('>')[0] == r)
        return own + incoming - outgoing
    for i, ev in enumerate(events):
        kind = ev[0]
        if kind == 'sync':
            s, d = ev[1], ev[2]
            for src, dst in ((P[s], P[d]), (D[s], D[d]), (T[s], T[d])):
                for k, v in src.items():
                    dst[k] = max(dst.get(k, 0), v)
        elif kind == 'inc':
            P[ev[1]][ev[1]] = P[ev[1]].get(ev[1], 0) + ev[2]
        elif kind == 'dec':
            r, k = ev[1], ev[2]
            if rights(r) < k:
                rejected.append(i)
            else:
                D[r][r] = D[r].get(r, 0) + k
        else:
            r, to, k = ev[1], ev[2], ev[3]
            if rights(r) < k:
                rejected.append(i)
            else:
                key = r + '>' + to
                T[r][key] = T[r].get(key, 0) + k
    return {'values': [sum(P[r].values()) - sum(D[r].values()) for r in replicas], 'rights': [rights(r) for r in replicas], 'rejected': rejected}
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
    1: [('each replica spends only its own rights', [[['inc', 'a', 2], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 4], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [2, 2, 0], 'rights': [2, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 2], ['move', 'a', 'c', 1], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 1], ['dec', 'c', 1], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [1, 0, 1], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 1], ['dec', 'b', 1], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 4, 3], 'rights': [1, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [2, 5, 2], 'rights': [2, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 1], ['dec', 'c', 4], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    2: [('each replica spends only its own rights', [[['inc', 'a', 3], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [0, 3, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 5], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [3, 3, 0], 'rights': [3, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 4], ['move', 'a', 'c', 2], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 2], ['dec', 'c', 2], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [2, 0, 2], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 2], ['dec', 'b', 2], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 2], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 5, 3], 'rights': [2, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [3, 6, 3], 'rights': [3, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 2], ['dec', 'c', 5], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    3: [('each replica spends only its own rights', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [0, 4, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 6], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [4, 4, 0], 'rights': [4, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 6], ['move', 'a', 'c', 3], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 3], ['dec', 'c', 3], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [3, 0, 3], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 3], ['dec', 'b', 3], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 3], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [6, 6, 3], 'rights': [3, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 7], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [4, 7, 4], 'rights': [4, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 3], ['dec', 'c', 6], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    4: [('each replica spends only its own rights', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [0, 5, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 7], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [5, 5, 0], 'rights': [5, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 8], ['move', 'a', 'c', 4], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 4], ['dec', 'c', 4], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [4, 0, 4], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 4], ['dec', 'b', 4], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 4], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [7, 7, 3], 'rights': [4, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 8], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [5, 8, 5], 'rights': [5, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 4], ['dec', 'c', 7], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    5: [('each replica spends only its own rights', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 6]], ['a', 'b', 'c']], {'values': [0, 6, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 8], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [6, 6, 0], 'rights': [6, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 10], ['move', 'a', 'c', 5], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 5], ['dec', 'c', 5], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [5, 0, 5], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 5], ['dec', 'b', 5], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 5], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [8, 8, 3], 'rights': [5, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 9], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [6, 9, 6], 'rights': [6, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 5], ['dec', 'c', 8], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
}[N]
for label, args, expected in cases:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
each replica spends only its own rights{'rejected': [], 'rights': [0, 1, 0], 'values': [0, 1, 0]}{'rejected': [2], 'rights': [0, 0, 0], 'values': [0, 2, 0]}Failed
transferred rights can be spent{'rejected': [], 'rights': [0, 4, 0], 'values': [2, 2, 0]}{'rejected': [], 'rights': [2, 0, 0], 'values': [2, 2, 0]}Failed
outgoing transfers reduce rights{'rejected': [2], 'rights': [0, 0, 0], 'values': [2, 0, 0]}{'rejected': [2], 'rights': [0, 0, 0], 'values': [2, 0, 0]}Passed
concurrent spending cannot go negative{'rejected': [], 'rights': [0, -1, 2], 'values': [1, -1, 1]}{'rejected': [6], 'rights': [0, 0, 0], 'values': [1, 0, 1]}Failed
rights exhausted exactly{'rejected': [2, 3], 'rights': [0, 0, 0], 'values': [0, 0, 0]}{'rejected': [2, 3], 'rights': [0, 0, 0], 'values': [0, 0, 0]}Passed
decrements propagate by sync{'rejected': [], 'rights': [4, 4, 3], 'values': [4, 4, 3]}{'rejected': [], 'rights': [1, 0, 3], 'values': [4, 4, 3]}Failed
stale peer does not undo local decrements{'rejected': [], 'rights': [2, 5, 2], 'values': [2, 5, 2]}{'rejected': [], 'rights': [2, 0, 0], 'values': [2, 5, 2]}Failed
transfer received before own increments{'rejected': [], 'rights': [1, 0, 3], 'values': [4, 0, 1]}{'rejected': [5], 'rights': [1, 0, 0], 'values': [4, 0, 1]}Failed

SHA-256 / d4a081f9d717ccd531f73c58f71c8993504bab769c24efd54026b09da139556a

2 / The unsuccessful fix

Exit 1
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(events, replicas):
    P = {r: {} for r in replicas}
    D = {r: {} for r in replicas}
    T = {r: {} for r in replicas}
    rejected = []
    def rights(r):
        own = P[r].get(r, 0) - sum(D[r].values())
        incoming = sum(v for k, v in T[r].items() if k.split('>')[1] == r)
        outgoing = sum(v for k, v in T[r].items() if k.split('>')[0] == r)
        return own + incoming - outgoing
    for i, ev in enumerate(events):
        kind = ev[0]
        if kind == 'sync':
            s, d = ev[1], ev[2]
            for src, dst in ((P[s], P[d]), (D[s], D[d]), (T[s], T[d])):
                for k, v in src.items():
                    dst[k] = max(dst.get(k, 0), v)
        elif kind == 'inc':
            P[ev[1]][ev[1]] = P[ev[1]].get(ev[1], 0) + ev[2]
        elif kind == 'dec':
            r, k = ev[1], ev[2]
            if rights(r) < k:
                rejected.append(i)
            else:
                D[r][r] = D[r].get(r, 0) + k
        else:
            r, to, k = ev[1], ev[2], ev[3]
            if rights(r) < k:
                rejected.append(i)
            else:
                key = r + '>' + to
                T[r][key] = T[r].get(key, 0) + k
    return {'values': [sum(P[r].values()) - sum(D[r].values()) for r in replicas], 'rights': [rights(r) for r in replicas], 'rejected': rejected}
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
    1: [('each replica spends only its own rights', [[['inc', 'a', 2], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 4], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [2, 2, 0], 'rights': [2, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 2], ['move', 'a', 'c', 1], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 1], ['dec', 'c', 1], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [1, 0, 1], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 1], ['dec', 'b', 1], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 4, 3], 'rights': [1, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [2, 5, 2], 'rights': [2, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 1], ['dec', 'c', 4], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    2: [('each replica spends only its own rights', [[['inc', 'a', 3], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [0, 3, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 5], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [3, 3, 0], 'rights': [3, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 4], ['move', 'a', 'c', 2], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 2], ['dec', 'c', 2], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [2, 0, 2], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 2], ['dec', 'b', 2], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 2], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 5, 3], 'rights': [2, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [3, 6, 3], 'rights': [3, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 2], ['dec', 'c', 5], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    3: [('each replica spends only its own rights', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [0, 4, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 6], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [4, 4, 0], 'rights': [4, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 6], ['move', 'a', 'c', 3], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 3], ['dec', 'c', 3], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [3, 0, 3], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 3], ['dec', 'b', 3], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 3], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [6, 6, 3], 'rights': [3, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 7], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [4, 7, 4], 'rights': [4, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 3], ['dec', 'c', 6], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    4: [('each replica spends only its own rights', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [0, 5, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 7], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [5, 5, 0], 'rights': [5, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 8], ['move', 'a', 'c', 4], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 4], ['dec', 'c', 4], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [4, 0, 4], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 4], ['dec', 'b', 4], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 4], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [7, 7, 3], 'rights': [4, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 8], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [5, 8, 5], 'rights': [5, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 4], ['dec', 'c', 7], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
    5: [('each replica spends only its own rights', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'b', 1], ['dec', 'a', 6]], ['a', 'b', 'c']], {'values': [0, 6, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('transferred rights can be spent', [[['inc', 'a', 8], ['move', 'a', 'b', 2], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a']], ['a', 'b', 'c']], {'values': [6, 6, 0], 'rights': [6, 0, 0], 'rejected': []}), ('outgoing transfers reduce rights', [[['inc', 'a', 3], ['move', 'a', 'b', 2], ['dec', 'a', 2], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rights': [0, 0, 0], 'rejected': [2]}), ('concurrent spending cannot go negative', [[['inc', 'a', 10], ['move', 'a', 'c', 5], ['sync', 'a', 'b'], ['sync', 'a', 'c'], ['dec', 'a', 5], ['dec', 'c', 5], ['dec', 'b', 1], ['sync', 'a', 'b'], ['sync', 'c', 'b']], ['a', 'b', 'c']], {'values': [5, 0, 5], 'rights': [0, 0, 0], 'rejected': [6]}), ('rights exhausted exactly', [[['inc', 'b', 5], ['dec', 'b', 5], ['dec', 'b', 1], ['move', 'b', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rights': [0, 0, 0], 'rejected': [2, 3]}), ('decrements propagate by sync', [[['inc', 'c', 5], ['sync', 'c', 'a'], ['dec', 'c', 2], ['sync', 'c', 'a'], ['inc', 'a', 5], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [8, 8, 3], 'rights': [5, 0, 3], 'rejected': []}), ('stale peer does not undo local decrements', [[['inc', 'a', 9], ['sync', 'a', 'b'], ['dec', 'a', 3], ['sync', 'b', 'a'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [6, 9, 6], 'rights': [6, 0, 0], 'rejected': []}), ('transfer received before own increments', [[['inc', 'a', 4], ['move', 'a', 'c', 3], ['sync', 'a', 'c'], ['inc', 'c', 5], ['dec', 'c', 8], ['move', 'c', 'b', 1]], ['a', 'b', 'c']], {'values': [4, 0, 1], 'rights': [1, 0, 0], 'rejected': [5]})],
}[N]
for label, args, expected in cases:
    check(label, solve(*args), expected)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)
Boundary fixtureActualExpectedOutcome
each replica spends only its own rights{'rejected': [2], 'rights': [0, 0, 0], 'values': [0, 2, 0]}{'rejected': [2], 'rights': [0, 0, 0], 'values': [0, 2, 0]}Passed
transferred rights can be spent{'rejected': [], 'rights': [0, 0, 0], 'values': [2, 2, 0]}{'rejected': [], 'rights': [2, 0, 0], 'values': [2, 2, 0]}Failed
outgoing transfers reduce rights{'rejected': [2], 'rights': [0, 0, 0], 'values': [2, 0, 0]}{'rejected': [2], 'rights': [0, 0, 0], 'values': [2, 0, 0]}Passed
concurrent spending cannot go negative{'rejected': [6], 'rights': [0, -2, 0], 'values': [1, 0, 1]}{'rejected': [6], 'rights': [0, 0, 0], 'values': [1, 0, 1]}Failed
rights exhausted exactly{'rejected': [2, 3], 'rights': [0, 0, 0], 'values': [0, 0, 0]}{'rejected': [2, 3], 'rights': [0, 0, 0], 'values': [0, 0, 0]}Passed
decrements propagate by sync{'rejected': [], 'rights': [-1, -2, 3], 'values': [4, 4, 3]}{'rejected': [], 'rights': [1, 0, 3], 'values': [4, 4, 3]}Failed
stale peer does not undo local decrements{'rejected': [], 'rights': [2, 0, -3], 'values': [2, 5, 2]}{'rejected': [], 'rights': [2, 0, 0], 'values': [2, 5, 2]}Failed
transfer received before own increments{'rejected': [5], 'rights': [1, 0, 0], 'values': [4, 0, 1]}{'rejected': [5], 'rights': [1, 0, 0], 'values': [4, 0, 1]}Passed

SHA-256 / f1f8c137ad6c5cd45dd847095371c862344ac7b803403fb10dde6446de0795ec

HELD IN THE MEMBER ARCHIVE

The verified repair and its recorded checks are member-only.

This mechanism has 8 recorded checks per implementation. The open-access tier publishes the failure and the unsuccessful fix; the repaired source that passes every check, and the observations that prove it, are available to members.

Every case sharing this mechanism uses the same contract and the same repair, so this one record is held back for all of them.

Member access is invitation-based. Sign in with your invited account to inspect the repair.

Sign in to the archive ↗

Verification & scope

A deterministic, bounded teaching model of one replicated data type with stipulated operation and merge rules; it is not a production CRDT library and makes no claim of conformance to any specific published design. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:49:02.515531+00:00.

Case digest / 5c46523938e3aacd9f6d6fc0fb8809a4f3ad5a8727dc183e73efa5837f07d180