FA-74881 / CRDT convergence / Open access
PN-Counter with local floor: decrementing to exactly zero is refused · case 01
A decrement that would leave the counter at exactly zero is rejected.
ROOT CAUSE
The guard uses a non-strict comparison, treating a zero result as a floor violation.
VERIFIED REPAIR
Reject only when the observed value is strictly smaller than the amount.
Unsuccessful approach: Loosening the bound by one admits a decrement that leaves the counter at minus one.
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 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': [1], 'values': [1, 0, 0]} | {'rejected': [], 'values': [0, 0, 0]} | Failed |
| 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': [2], 'values': [1, 2, 0]} | {'rejected': [], 'values': [1, 1, 0]} | Failed |
| mixed history | {'rejected': [], 'values': [1, 1, 1]} | {'rejected': [], 'values': [1, 1, 1]} | Passed |
SHA-256 / e0edaef0d082ec330b569ff25e8b493492e085b6f6be8068e2ef8351a2bd42e4
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 value(r) < amt - 1:
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': [], 'values': [-1, -1, 0]} | {'rejected': [1, 2], 'values': [1, 0, 0]} | Failed |
| 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 / 2a0a3a653dbb253a359f1e735cebc535a97743f83166b9a572995f4b2865cc30
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.927378+00:00.
Case digest / 22de894feb42e5c4102ff9ca9bcb0bd89a09ee89ce0eb7d9a4df43c094c48d5e