FA-45936 / Bounded deques / Open access
Unlink leaves the predecessor pointing at the detached node · case 01
Unlink leaves the predecessor pointing at the detached node.
ROOT CAUSE
Only the sentinel fast path is repaired, leaving interior forward edges stale.
VERIFIED REPAIR
Restore the documented predecessor edge invariant in intrusive-unlink.
Unsuccessful approach: The partial repair still applies the incorrect transition to an admitted boundary or multi-element case.
Case contract
Unlink one selected node from a finite doubly linked deque with sentinel S. Nodes are keyed by identity; return forward IDs, backward IDs, removed node links, size, sentinel endpoint links and reciprocal-link validity. Every input ID is unique.
Why this case matters
Controlled bounded deque implementation model with explicit storage and lifecycle observations.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
ids, victim = x
nodes = {'S': ['S','S']}
for i, value in enumerate(ids):
nodes[value] = [ids[i-1] if i else 'S', ids[i+1] if i+1 < len(ids) else 'S']
if ids:
nodes['S'] = [ids[-1],ids[0]]
size = len(ids)
left, right = nodes[victim]
nodes[left][1] = victim
nodes[right][0] = left
nodes[victim] = [None,None]
size -= 1
forward = []
current = nodes['S'][1]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
forward.append(current)
current = nodes[current][1]
backward = []
current = nodes['S'][0]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
backward.append(current)
current = nodes[current][0]
valid = all(nodes[nodes[v][0]][1] == v and nodes[nodes[v][1]][0] == v for v in forward if nodes[v][0] is not None and nodes[v][1] is not None)
return [forward,backward,nodes[victim],size,nodes['S'],valid]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('middle unlink', solve([[N,N+1,N+2],N+1]), [[N,N+2],[N+2,N],[None,None],2,[N+2,N],True])
check('head unlink', solve([[N,N+1,N+2],N]), [[N+1,N+2],[N+2,N+1],[None,None],2,[N+2,N+1],True])
check('tail unlink', solve([[N,N+1,N+2],N+2]), [[N,N+1],[N+1,N],[None,None],2,[N+1,N],True])
check('only node', solve([[N],N]), [[],[],[None,None],0,["S","S"],True])
check('pair head', solve([[N,N+1],N]), [[N+1],[N+1],[None,None],1,[N+1,N+1],True])
check('long middle', solve([[N,N+1,N+2,N+3,N+4],N+2]), [[N,N+1,N+3,N+4],[N+4,N+3,N+1,N],[None,None],4,[N+4,N],True])
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 |
|---|---|---|---|
| middle unlink | [[1, 2], [3, 1], [None, None], 2, [3, 1], False] | [[1, 3], [3, 1], [None, None], 2, [3, 1], True] | Failed |
| head unlink | [[1], [3, 2], [None, None], 2, [3, 1], True] | [[2, 3], [3, 2], [None, None], 2, [3, 2], True] | Failed |
| tail unlink | [[1, 2, 3], [2, 1], [None, None], 2, [2, 1], False] | [[1, 2], [2, 1], [None, None], 2, [2, 1], True] | Failed |
| only node | [[1], [], [None, None], 0, ['S', 1], True] | [[], [], [None, None], 0, ['S', 'S'], True] | Failed |
| pair head | [[1], [2], [None, None], 1, [2, 1], True] | [[2], [2], [None, None], 1, [2, 2], True] | Failed |
| long middle | [[1, 2, 3], [5, 4, 2, 1], [None, None], 4, [5, 1], False] | [[1, 2, 4, 5], [5, 4, 2, 1], [None, None], 4, [5, 1], True] | Failed |
SHA-256 / 4a0682b164fdec098af2ac4b34fc883d02a2003ac1e046c746ad2d29760d6ef9
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
ids, victim = x
nodes = {'S': ['S','S']}
for i, value in enumerate(ids):
nodes[value] = [ids[i-1] if i else 'S', ids[i+1] if i+1 < len(ids) else 'S']
if ids:
nodes['S'] = [ids[-1],ids[0]]
size = len(ids)
left, right = nodes[victim]
nodes[left][1] = right if left == "S" else victim
nodes[right][0] = left
nodes[victim] = [None,None]
size -= 1
forward = []
current = nodes['S'][1]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
forward.append(current)
current = nodes[current][1]
backward = []
current = nodes['S'][0]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
backward.append(current)
current = nodes[current][0]
valid = all(nodes[nodes[v][0]][1] == v and nodes[nodes[v][1]][0] == v for v in forward if nodes[v][0] is not None and nodes[v][1] is not None)
return [forward,backward,nodes[victim],size,nodes['S'],valid]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('middle unlink', solve([[N,N+1,N+2],N+1]), [[N,N+2],[N+2,N],[None,None],2,[N+2,N],True])
check('head unlink', solve([[N,N+1,N+2],N]), [[N+1,N+2],[N+2,N+1],[None,None],2,[N+2,N+1],True])
check('tail unlink', solve([[N,N+1,N+2],N+2]), [[N,N+1],[N+1,N],[None,None],2,[N+1,N],True])
check('only node', solve([[N],N]), [[],[],[None,None],0,["S","S"],True])
check('pair head', solve([[N,N+1],N]), [[N+1],[N+1],[None,None],1,[N+1,N+1],True])
check('long middle', solve([[N,N+1,N+2,N+3,N+4],N+2]), [[N,N+1,N+3,N+4],[N+4,N+3,N+1,N],[None,None],4,[N+4,N],True])
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 |
|---|---|---|---|
| middle unlink | [[1, 2], [3, 1], [None, None], 2, [3, 1], False] | [[1, 3], [3, 1], [None, None], 2, [3, 1], True] | Failed |
| head unlink | [[2, 3], [3, 2], [None, None], 2, [3, 2], True] | [[2, 3], [3, 2], [None, None], 2, [3, 2], True] | Passed |
| tail unlink | [[1, 2, 3], [2, 1], [None, None], 2, [2, 1], False] | [[1, 2], [2, 1], [None, None], 2, [2, 1], True] | Failed |
| only node | [[], [], [None, None], 0, ['S', 'S'], True] | [[], [], [None, None], 0, ['S', 'S'], True] | Passed |
| pair head | [[2], [2], [None, None], 1, [2, 2], True] | [[2], [2], [None, None], 1, [2, 2], True] | Passed |
| long middle | [[1, 2, 3], [5, 4, 2, 1], [None, None], 4, [5, 1], False] | [[1, 2, 4, 5], [5, 4, 2, 1], [None, None], 4, [5, 1], True] | Failed |
SHA-256 / 7e44c20b02467c949cd295e1e9e6b3152d1f6b846af63cbee0585ae89e70f068
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(x):
ids, victim = x
nodes = {'S': ['S','S']}
for i, value in enumerate(ids):
nodes[value] = [ids[i-1] if i else 'S', ids[i+1] if i+1 < len(ids) else 'S']
if ids:
nodes['S'] = [ids[-1],ids[0]]
size = len(ids)
left, right = nodes[victim]
nodes[left][1] = right
nodes[right][0] = left
nodes[victim] = [None,None]
size -= 1
forward = []
current = nodes['S'][1]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
forward.append(current)
current = nodes[current][1]
backward = []
current = nodes['S'][0]
for _ in range(len(ids)+1):
if current == 'S' or current is None: break
backward.append(current)
current = nodes[current][0]
valid = all(nodes[nodes[v][0]][1] == v and nodes[nodes[v][1]][0] == v for v in forward if nodes[v][0] is not None and nodes[v][1] is not None)
return [forward,backward,nodes[victim],size,nodes['S'],valid]
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('middle unlink', solve([[N,N+1,N+2],N+1]), [[N,N+2],[N+2,N],[None,None],2,[N+2,N],True])
check('head unlink', solve([[N,N+1,N+2],N]), [[N+1,N+2],[N+2,N+1],[None,None],2,[N+2,N+1],True])
check('tail unlink', solve([[N,N+1,N+2],N+2]), [[N,N+1],[N+1,N],[None,None],2,[N+1,N],True])
check('only node', solve([[N],N]), [[],[],[None,None],0,["S","S"],True])
check('pair head', solve([[N,N+1],N]), [[N+1],[N+1],[None,None],1,[N+1,N+1],True])
check('long middle', solve([[N,N+1,N+2,N+3,N+4],N+2]), [[N,N+1,N+3,N+4],[N+4,N+3,N+1,N],[None,None],4,[N+4,N],True])
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 |
|---|---|---|---|
| middle unlink | [[1, 3], [3, 1], [None, None], 2, [3, 1], True] | [[1, 3], [3, 1], [None, None], 2, [3, 1], True] | Passed |
| head unlink | [[2, 3], [3, 2], [None, None], 2, [3, 2], True] | [[2, 3], [3, 2], [None, None], 2, [3, 2], True] | Passed |
| tail unlink | [[1, 2], [2, 1], [None, None], 2, [2, 1], True] | [[1, 2], [2, 1], [None, None], 2, [2, 1], True] | Passed |
| only node | [[], [], [None, None], 0, ['S', 'S'], True] | [[], [], [None, None], 0, ['S', 'S'], True] | Passed |
| pair head | [[2], [2], [None, None], 1, [2, 2], True] | [[2], [2], [None, None], 1, [2, 2], True] | Passed |
| long middle | [[1, 2, 4, 5], [5, 4, 2, 1], [None, None], 4, [5, 1], True] | [[1, 2, 4, 5], [5, 4, 2, 1], [None, None], 4, [5, 1], True] | Passed |
SHA-256 / 3ae9149a9b856352139003db699b56d2d0ed738050dc647ebe38200d700331f0
Verification & scope
Offline finite deterministic model; no claim of production implementation or concurrent memory-model conformance. 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:44:27.195587+00:00.
Case digest / 3b8eb5ffcd4446f8bcf19c285225fffa32ba45f87e1bdc58cd07c1a56b830cb2