FA-75251 / CRDT convergence / Open access
Causal length set: any recorded history counts as membership · case 01
Removed elements keep appearing as members.
ROOT CAUSE
Membership tests for a positive length instead of an odd one.
VERIFIED REPAIR
An element is a member exactly when its causal length is odd.
Unsuccessful approach: Testing for length one ignores re-adds, which have lengths 3, 5 and so on.
Case contract
Each replica maps elements to a causal length. An element is present when its length is odd. ["add", r, e] increments the length only when it is even; ["rem", r, e] increments it only when it is odd. ["merge", s, d] takes the per-element maximum. Return per replica the sorted members and the sorted [element, length] pairs.
Why this case matters
Causal-length sets encode an element's add/remove history as a single counter whose parity is its membership.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
L = {r: {} for r in replicas}
for op in ops:
if op[0] == 'add':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 0:
L[r][e] = L[r].get(e, 0) + 1
elif op[0] == 'rem':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 1:
L[r][e] = L[r][e] + 1
else:
s, d = op[1], op[2]
for e, ln in L[s].items():
L[d][e] = max(L[d].get(e, 0), ln)
return [[sorted(e for e, ln in L[r].items() if ln > 0), sorted([e, ln] for e, ln in L[r].items())] for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]])],
2: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'q'], [['e0', 1], ['e1', 1], ['q', 1]]]])],
3: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['q', 1]]]])],
4: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['q', 1]]]])],
5: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3'], ['add', 'b', 'e4']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'e4', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['e4', 1], ['q', 1]]]])],
}[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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| add then remove | [[['x'], [['x', 2]]], [[], []]] | [[[], [['x', 2]]], [[], []]] | Failed |
| re-add after remove | [[['x'], [['x', 3]]], [[], []]] | [[['x'], [['x', 3]]], [[], []]] | Passed |
| adding a present element is a no-op | [[['y'], [['y', 1]]], [[], []]] | [[['y'], [['y', 1]]], [[], []]] | Passed |
| removing an absent element is a no-op | [[[], []], [['w'], [['w', 2]]]] | [[[], []], [[], [['w', 2]]]] | Failed |
| concurrent adds merge to present | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | Passed |
| removal propagates by merge | [[['r'], [['r', 2]]], [['r'], [['r', 2]]]] | [[[], [['r', 2]]], [[], [['r', 2]]]] | Failed |
| longer history wins | [[['h'], [['h', 4]]], [['h'], [['h', 4]]]] | [[[], [['h', 4]]], [[], [['h', 4]]]] | Failed |
| stale present copy does not revive | [[['q'], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | Failed |
SHA-256 / 585620e547b06b10c782e7be065a6fed581ee748b5b70da582538d83ca632806
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
L = {r: {} for r in replicas}
for op in ops:
if op[0] == 'add':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 0:
L[r][e] = L[r].get(e, 0) + 1
elif op[0] == 'rem':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 1:
L[r][e] = L[r][e] + 1
else:
s, d = op[1], op[2]
for e, ln in L[s].items():
L[d][e] = max(L[d].get(e, 0), ln)
return [[sorted(e for e, ln in L[r].items() if ln == 1), sorted([e, ln] for e, ln in L[r].items())] for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]])],
2: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'q'], [['e0', 1], ['e1', 1], ['q', 1]]]])],
3: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['q', 1]]]])],
4: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['q', 1]]]])],
5: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3'], ['add', 'b', 'e4']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'e4', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['e4', 1], ['q', 1]]]])],
}[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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| add then remove | [[[], [['x', 2]]], [[], []]] | [[[], [['x', 2]]], [[], []]] | Passed |
| re-add after remove | [[[], [['x', 3]]], [[], []]] | [[['x'], [['x', 3]]], [[], []]] | Failed |
| adding a present element is a no-op | [[['y'], [['y', 1]]], [[], []]] | [[['y'], [['y', 1]]], [[], []]] | Passed |
| removing an absent element is a no-op | [[[], []], [[], [['w', 2]]]] | [[[], []], [[], [['w', 2]]]] | Passed |
| concurrent adds merge to present | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | Passed |
| removal propagates by merge | [[[], [['r', 2]]], [[], [['r', 2]]]] | [[[], [['r', 2]]], [[], [['r', 2]]]] | Passed |
| longer history wins | [[[], [['h', 4]]], [[], [['h', 4]]]] | [[[], [['h', 4]]], [[], [['h', 4]]]] | Passed |
| stale present copy does not revive | [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | Passed |
SHA-256 / 7e2d08a253c2760eb35ce6e015ec805bb9a8d7543594cb5f5a381b140be909cf
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops, replicas):
L = {r: {} for r in replicas}
for op in ops:
if op[0] == 'add':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 0:
L[r][e] = L[r].get(e, 0) + 1
elif op[0] == 'rem':
r, e = op[1], op[2]
if L[r].get(e, 0) % 2 == 1:
L[r][e] = L[r][e] + 1
else:
s, d = op[1], op[2]
for e, ln in L[s].items():
L[d][e] = max(L[d].get(e, 0), ln)
return [[sorted(e for e, ln in L[r].items() if ln % 2 == 1), sorted([e, ln] for e, ln in L[r].items())] for r in replicas]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = {
1: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]])],
2: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'q'], [['e0', 1], ['e1', 1], ['q', 1]]]])],
3: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['q', 1]]]])],
4: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['q', 1]]]])],
5: [('add then remove', [[['add', 'a', 'x'], ['rem', 'a', 'x']], ['a', 'b']], [[[], [['x', 2]]], [[], []]]), ('re-add after remove', [[['add', 'a', 'x'], ['rem', 'a', 'x'], ['add', 'a', 'x']], ['a', 'b']], [[['x'], [['x', 3]]], [[], []]]), ('adding a present element is a no-op', [[['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y'], ['add', 'a', 'y']], ['a', 'b']], [[['y'], [['y', 1]]], [[], []]]), ('removing an absent element is a no-op', [[['rem', 'a', 'z'], ['rem', 'b', 'z'], ['add', 'b', 'w'], ['rem', 'b', 'w'], ['rem', 'b', 'w']], ['a', 'b']], [[[], []], [[], [['w', 2]]]]), ('concurrent adds merge to present', [[['add', 'a', 'k'], ['add', 'b', 'k'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[['k'], [['k', 1]]], [['k'], [['k', 1]]]]), ('removal propagates by merge', [[['add', 'a', 'r'], ['merge', 'a', 'b'], ['rem', 'b', 'r'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['r', 2]]], [[], [['r', 2]]]]), ('longer history wins', [[['add', 'a', 'h'], ['merge', 'a', 'b'], ['rem', 'a', 'h'], ['add', 'a', 'h'], ['rem', 'a', 'h'], ['merge', 'a', 'b'], ['merge', 'b', 'a']], ['a', 'b']], [[[], [['h', 4]]], [[], [['h', 4]]]]), ('stale present copy does not revive', [[['add', 'a', 'q'], ['merge', 'a', 'b'], ['rem', 'a', 'q'], ['merge', 'b', 'a'], ['add', 'b', 'e0'], ['add', 'b', 'e1'], ['add', 'b', 'e2'], ['add', 'b', 'e3'], ['add', 'b', 'e4']], ['a', 'b']], [[[], [['q', 2]]], [['e0', 'e1', 'e2', 'e3', 'e4', 'q'], [['e0', 1], ['e1', 1], ['e2', 1], ['e3', 1], ['e4', 1], ['q', 1]]]])],
}[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 fixture | Actual | Expected | Outcome |
|---|---|---|---|
| add then remove | [[[], [['x', 2]]], [[], []]] | [[[], [['x', 2]]], [[], []]] | Passed |
| re-add after remove | [[['x'], [['x', 3]]], [[], []]] | [[['x'], [['x', 3]]], [[], []]] | Passed |
| adding a present element is a no-op | [[['y'], [['y', 1]]], [[], []]] | [[['y'], [['y', 1]]], [[], []]] | Passed |
| removing an absent element is a no-op | [[[], []], [[], [['w', 2]]]] | [[[], []], [[], [['w', 2]]]] | Passed |
| concurrent adds merge to present | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | [[['k'], [['k', 1]]], [['k'], [['k', 1]]]] | Passed |
| removal propagates by merge | [[[], [['r', 2]]], [[], [['r', 2]]]] | [[[], [['r', 2]]], [[], [['r', 2]]]] | Passed |
| longer history wins | [[[], [['h', 4]]], [[], [['h', 4]]]] | [[[], [['h', 4]]], [[], [['h', 4]]]] | Passed |
| stale present copy does not revive | [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | [[[], [['q', 2]]], [['e0', 'q'], [['e0', 1], ['q', 1]]]] | Passed |
SHA-256 / 6dc9ae8c39eefdaf28f0d4f8ebbc85ff07bb249e8a1f3faad28921acb45d9426
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:04.460483+00:00.
Case digest / a4e4e7216b5fc47160bef2d2bb746fce27ea364519104b44ccda1dc346a67a78