FA-74876 / CRDT convergence / Open access
PN-Counter with local floor: the floor check ignores decrements already applied · case 01
Repeated decrements drive a replica's observed value below zero.
ROOT CAUSE
The floor guard compares against the positive total only, ignoring earlier decrements.
VERIFIED REPAIR
Guard against the full locally observed value: all positive slots minus all negative slots.
Unsuccessful approach: Using only the replica's own slots rejects decrements that are funded by increments learned from peers.
Case contract
Replicas keep a positive map and a negative map (replica->total). ["inc", r, k] and ["dec", r, k] need k > 0, otherwise the event index is rejected. A decrement is also rejected when r's locally observed value is below k. ["sync", src, dst] merges both maps of src into dst by pointwise maximum. Return values and rejected indices.
Why this case matters
Positive/negative counters are the standard way to support decrements in a state-based counter.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(events, replicas):
pos = {r: {} for r in replicas}
neg = {r: {} for r in replicas}
rejected = []
def value(r):
return sum(pos[r].values()) - sum(neg[r].values())
for i, ev in enumerate(events):
kind = ev[0]
if kind == 'sync':
s, d = ev[1], ev[2]
for k, v in pos[s].items():
pos[d][k] = max(pos[d].get(k, 0), v)
for k, v in neg[s].items():
neg[d][k] = max(neg[d].get(k, 0), v)
continue
r, amt = ev[1], ev[2]
if amt <= 0:
rejected.append(i)
continue
if kind == 'inc':
pos[r][r] = pos[r].get(r, 0) + amt
else:
if sum(pos[r].values()) < amt:
rejected.append(i)
continue
neg[r][r] = neg[r].get(r, 0) + amt
return {'values': [value(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: [('decrement to exactly zero is allowed', [[['inc', 'a', 1], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 1], ['dec', 'b', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 3], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 4], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 2], ['dec', 'a', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 1], ['inc', 'b', 1], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [1, 1, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 1], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []})],
2: [('decrement to exactly zero is allowed', [[['inc', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 2], ['dec', 'b', 1], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'b', 3], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 5], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 3], ['dec', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 2], ['inc', 'b', 2], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 3, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 2], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []})],
3: [('decrement to exactly zero is allowed', [[['inc', 'a', 3], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 3], ['dec', 'b', 1], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [3, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'b', 4], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 8], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 6], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 4], ['dec', 'a', 3], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 3], ['inc', 'b', 3], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 5, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 3], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []})],
4: [('decrement to exactly zero is allowed', [[['inc', 'a', 4], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 4], ['dec', 'b', 1], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [4, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'b', 5], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 10], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [7, 7, 7], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 7], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 5], ['dec', 'a', 4], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 4], ['inc', 'b', 4], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 7, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 4], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []})],
5: [('decrement to exactly zero is allowed', [[['inc', 'a', 5], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 5], ['dec', 'b', 1], ['dec', 'a', 6]], ['a', 'b', 'c']], {'values': [5, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 7], ['sync', 'a', 'b'], ['dec', 'b', 6], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 12], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [9, 9, 9], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 8], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [6, 6, 6], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 6], ['dec', 'a', 5], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 5], ['inc', 'b', 5], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 9, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 5], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []})],
}[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 |
|---|---|---|---|
| decrement to exactly zero is allowed | {'rejected': [], 'values': [0, 0, 0]} | {'rejected': [], 'values': [0, 0, 0]} | Passed |
| decrement beyond local view is rejected | {'rejected': [1, 2], 'values': [1, 0, 0]} | {'rejected': [1, 2], 'values': [1, 0, 0]} | Passed |
| decrement funded by learned increments | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
| concurrent decrements converge | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
| zero amounts are rejected | {'rejected': [0, 2], 'values': [0, 2, 0]} | {'rejected': [0, 2], 'values': [0, 2, 0]} | Passed |
| repeated decrement slot is refreshed | {'rejected': [], 'values': [2, 2, 2]} | {'rejected': [], 'values': [2, 2, 2]} | Passed |
| second decrement cannot pass the floor | {'rejected': [], 'values': [-1, 0, 0]} | {'rejected': [2], 'values': [1, 0, 0]} | Failed |
| one-way sync does not pull from the receiver | {'rejected': [], 'values': [1, 1, 0]} | {'rejected': [], 'values': [1, 1, 0]} | Passed |
| mixed history | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
SHA-256 / 96ca975ced10f5214574899e7c8781ec0fee7f1df02d82c7c192d7e52fa82ea7
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(events, replicas):
pos = {r: {} for r in replicas}
neg = {r: {} for r in replicas}
rejected = []
def value(r):
return sum(pos[r].values()) - sum(neg[r].values())
for i, ev in enumerate(events):
kind = ev[0]
if kind == 'sync':
s, d = ev[1], ev[2]
for k, v in pos[s].items():
pos[d][k] = max(pos[d].get(k, 0), v)
for k, v in neg[s].items():
neg[d][k] = max(neg[d].get(k, 0), v)
continue
r, amt = ev[1], ev[2]
if amt <= 0:
rejected.append(i)
continue
if kind == 'inc':
pos[r][r] = pos[r].get(r, 0) + amt
else:
if pos[r].get(r, 0) - neg[r].get(r, 0) < amt:
rejected.append(i)
continue
neg[r][r] = neg[r].get(r, 0) + amt
return {'values': [value(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: [('decrement to exactly zero is allowed', [[['inc', 'a', 1], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 1], ['dec', 'b', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 3], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 4], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 2], ['dec', 'a', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 1], ['inc', 'b', 1], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [1, 1, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 1], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []})],
2: [('decrement to exactly zero is allowed', [[['inc', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 2], ['dec', 'b', 1], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'b', 3], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 5], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 3], ['dec', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 2], ['inc', 'b', 2], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 3, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 2], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []})],
3: [('decrement to exactly zero is allowed', [[['inc', 'a', 3], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 3], ['dec', 'b', 1], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [3, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'b', 4], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 8], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 6], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 4], ['dec', 'a', 3], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 3], ['inc', 'b', 3], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 5, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 3], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []})],
4: [('decrement to exactly zero is allowed', [[['inc', 'a', 4], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 4], ['dec', 'b', 1], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [4, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'b', 5], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 10], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [7, 7, 7], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 7], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 5], ['dec', 'a', 4], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 4], ['inc', 'b', 4], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 7, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 4], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []})],
5: [('decrement to exactly zero is allowed', [[['inc', 'a', 5], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 5], ['dec', 'b', 1], ['dec', 'a', 6]], ['a', 'b', 'c']], {'values': [5, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 7], ['sync', 'a', 'b'], ['dec', 'b', 6], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 12], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [9, 9, 9], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 8], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [6, 6, 6], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 6], ['dec', 'a', 5], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 5], ['inc', 'b', 5], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 9, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 5], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []})],
}[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 |
|---|---|---|---|
| decrement to exactly zero is allowed | {'rejected': [], 'values': [0, 0, 0]} | {'rejected': [], 'values': [0, 0, 0]} | Passed |
| decrement beyond local view is rejected | {'rejected': [1, 2], 'values': [1, 0, 0]} | {'rejected': [1, 2], 'values': [1, 0, 0]} | Passed |
| decrement funded by learned increments | {'rejected': [2], 'values': [3, 3, 3]} | {'rejected': [], 'values': [1, 1, 1]} | Failed |
| concurrent decrements converge | {'rejected': [3], 'values': [3, 3, 3]} | {'rejected': [], 'values': [1, 1, 1]} | Failed |
| zero amounts are rejected | {'rejected': [0, 2], 'values': [0, 2, 0]} | {'rejected': [0, 2], 'values': [0, 2, 0]} | Passed |
| repeated decrement slot is refreshed | {'rejected': [], 'values': [2, 2, 2]} | {'rejected': [], 'values': [2, 2, 2]} | Passed |
| second decrement cannot pass the floor | {'rejected': [2], 'values': [1, 0, 0]} | {'rejected': [2], 'values': [1, 0, 0]} | Passed |
| one-way sync does not pull from the receiver | {'rejected': [], 'values': [1, 1, 0]} | {'rejected': [], 'values': [1, 1, 0]} | Passed |
| mixed history | {'rejected': [4], 'values': [3, 3, 3]} | {'rejected': [], 'values': [1, 1, 1]} | Failed |
SHA-256 / 19d4d67e308126ee1e991dfc4acb536b7cbaa1b646e7104314f6ec6990f74c2f
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(events, replicas):
pos = {r: {} for r in replicas}
neg = {r: {} for r in replicas}
rejected = []
def value(r):
return sum(pos[r].values()) - sum(neg[r].values())
for i, ev in enumerate(events):
kind = ev[0]
if kind == 'sync':
s, d = ev[1], ev[2]
for k, v in pos[s].items():
pos[d][k] = max(pos[d].get(k, 0), v)
for k, v in neg[s].items():
neg[d][k] = max(neg[d].get(k, 0), v)
continue
r, amt = ev[1], ev[2]
if amt <= 0:
rejected.append(i)
continue
if kind == 'inc':
pos[r][r] = pos[r].get(r, 0) + amt
else:
if value(r) < amt:
rejected.append(i)
continue
neg[r][r] = neg[r].get(r, 0) + amt
return {'values': [value(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: [('decrement to exactly zero is allowed', [[['inc', 'a', 1], ['dec', 'a', 1]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 1], ['dec', 'b', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 3], ['sync', 'a', 'b'], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 4], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 2], ['dec', 'a', 1], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 1], ['inc', 'b', 1], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [1, 1, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 1], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []})],
2: [('decrement to exactly zero is allowed', [[['inc', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 2], ['dec', 'b', 1], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [2, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 4], ['sync', 'a', 'b'], ['dec', 'b', 3], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 5], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 3], ['dec', 'a', 2], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 2], ['inc', 'b', 2], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [2, 3, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 2], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [2, 2, 2], 'rejected': []})],
3: [('decrement to exactly zero is allowed', [[['inc', 'a', 3], ['dec', 'a', 3]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 3], ['dec', 'b', 1], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [3, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 5], ['sync', 'a', 'b'], ['dec', 'b', 4], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 8], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 6], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 4], ['dec', 'a', 3], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 3], ['inc', 'b', 3], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [3, 5, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 3], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [3, 3, 3], 'rejected': []})],
4: [('decrement to exactly zero is allowed', [[['inc', 'a', 4], ['dec', 'a', 4]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 4], ['dec', 'b', 1], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [4, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 6], ['sync', 'a', 'b'], ['dec', 'b', 5], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 10], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [7, 7, 7], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 7], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 5], ['dec', 'a', 4], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 4], ['inc', 'b', 4], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [4, 7, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 4], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [4, 4, 4], 'rejected': []})],
5: [('decrement to exactly zero is allowed', [[['inc', 'a', 5], ['dec', 'a', 5]], ['a', 'b', 'c']], {'values': [0, 0, 0], 'rejected': []}), ('decrement beyond local view is rejected', [[['inc', 'a', 5], ['dec', 'b', 1], ['dec', 'a', 6]], ['a', 'b', 'c']], {'values': [5, 0, 0], 'rejected': [1, 2]}), ('decrement funded by learned increments', [[['inc', 'a', 7], ['sync', 'a', 'b'], ['dec', 'b', 6], ['sync', 'b', 'a'], ['sync', 'b', 'c'], ['sync', 'a', 'c']], ['a', 'b', 'c']], {'values': [1, 1, 1], 'rejected': []}), ('concurrent decrements converge', [[['inc', 'a', 12], ['sync', 'a', 'b'], ['dec', 'a', 1], ['dec', 'b', 2], ['sync', 'a', 'b'], ['sync', 'b', 'a'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [9, 9, 9], 'rejected': []}), ('zero amounts are rejected', [[['inc', 'a', 0], ['inc', 'b', 3], ['dec', 'b', 0], ['dec', 'b', 1]], ['a', 'b', 'c']], {'values': [0, 2, 0], 'rejected': [0, 2]}), ('repeated decrement slot is refreshed', [[['inc', 'c', 8], ['dec', 'c', 1], ['sync', 'c', 'a'], ['dec', 'c', 1], ['sync', 'c', 'a'], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [6, 6, 6], 'rejected': []}), ('second decrement cannot pass the floor', [[['inc', 'a', 6], ['dec', 'a', 5], ['dec', 'a', 2]], ['a', 'b', 'c']], {'values': [1, 0, 0], 'rejected': [2]}), ('one-way sync does not pull from the receiver', [[['inc', 'a', 5], ['inc', 'b', 5], ['dec', 'b', 1], ['sync', 'a', 'b']], ['a', 'b', 'c']], {'values': [5, 9, 0], 'rejected': []}), ('mixed history', [[['inc', 'a', 3], ['dec', 'a', 1], ['sync', 'a', 'b'], ['inc', 'b', 5], ['dec', 'b', 2], ['sync', 'b', 'a'], ['sync', 'a', 'c'], ['sync', 'b', 'c']], ['a', 'b', 'c']], {'values': [5, 5, 5], 'rejected': []})],
}[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 |
|---|---|---|---|
| decrement to exactly zero is allowed | {'rejected': [], 'values': [0, 0, 0]} | {'rejected': [], 'values': [0, 0, 0]} | Passed |
| decrement beyond local view is rejected | {'rejected': [1, 2], 'values': [1, 0, 0]} | {'rejected': [1, 2], 'values': [1, 0, 0]} | Passed |
| decrement funded by learned increments | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
| concurrent decrements converge | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
| zero amounts are rejected | {'rejected': [0, 2], 'values': [0, 2, 0]} | {'rejected': [0, 2], 'values': [0, 2, 0]} | Passed |
| repeated decrement slot is refreshed | {'rejected': [], 'values': [2, 2, 2]} | {'rejected': [], 'values': [2, 2, 2]} | Passed |
| second decrement cannot pass the floor | {'rejected': [2], 'values': [1, 0, 0]} | {'rejected': [2], 'values': [1, 0, 0]} | Passed |
| one-way sync does not pull from the receiver | {'rejected': [], 'values': [1, 1, 0]} | {'rejected': [], 'values': [1, 1, 0]} | Passed |
| mixed history | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
SHA-256 / 3adf2aa219bbf8f7be38ef729ec20b58a77ed0d029c1bf2975b91368aacc6a4b
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:00.907939+00:00.
Case digest / 1265de106d1a11c2763c961b18c6b875e9f5a6907122df0145fc6251df313b30