{"abstract":"New deque edit retains the abandoned redo branch.","category":"Bounded deques","checks":6,"contract":"Bounded deque edits store the complete prior logical snapshot. Undo and redo transfer current snapshots between independent history stacks. A new edit invalidates redo history.","evaluation_group":"s3-bounded-deques-undo-snapshots","failed_approach":"The partial repair still applies the incorrect transition to an admitted boundary or multi-element case.","family":"s3-bounded-deques-undo-snapshots-redo-invalidation","id":"FA-46216","implementations":{"attempt":{"sha256":"af6d73b47645bb147003cc4c7a96f0c0246bc41bcfe7fd8a1e459332c726e627","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x):\n    a,past,future,command,value,cap=x\n    if command=='edit':\n        new=(a+[value])[-cap:] if cap else []\n        return [new,past+[a],future if past else []]\n    if command=='undo' and past:\n        return [past[-1],past[:-1],future+[a]]\n    if command=='redo' and future:\n        return [future[-1],past+[a],future[:-1]]\n    return [a,past,future]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('edit invalidates redo', solve([[N],[[N-1]],[[N+1]],\"edit\",N+2,3]), {1: [[1, 3], [[0], [1]], []], 2: [[2, 4], [[1], [2]], []], 3: [[3, 5], [[2], [3]], []], 4: [[4, 6], [[3], [4]], []], 5: [[5, 7], [[4], [5]], []]}[N])\ncheck('undo latest', solve([[N+2],[[N],[N+1]],[],\"undo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('redo latest', solve([[N],[],[[N+2],[N+1]],\"redo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('empty undo', solve([[N],[],[],\"undo\",0,3]), {1: [[1], [], []], 2: [[2], [], []], 3: [[3], [], []], 4: [[4], [], []], 5: [[5], [], []]}[N])\ncheck('overflow snapshot', solve([[N,N+1],[],[],\"edit\",N+2,2]), {1: [[2, 3], [[1, 2]], []], 2: [[3, 4], [[2, 3]], []], 3: [[4, 5], [[3, 4]], []], 4: [[5, 6], [[4, 5]], []], 5: [[6, 7], [[5, 6]], []]}[N])\ncheck('zero bound edit', solve([[],[[N]],[],\"edit\",N+1,0]), {1: [[], [[1], []], []], 2: [[], [[2], []], []], 3: [[], [[3], []], []], 4: [[], [[4], []], []], 5: [[], [[5], []], []]}[N])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"162838e4a31d8ebfe6c70b110442f40de36ea7df6ac705159b71b38bb780bca1","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x):\n    a,past,future,command,value,cap=x\n    if command=='edit':\n        new=(a+[value])[-cap:] if cap else []\n        return [new,past+[a],future]\n    if command=='undo' and past:\n        return [past[-1],past[:-1],future+[a]]\n    if command=='redo' and future:\n        return [future[-1],past+[a],future[:-1]]\n    return [a,past,future]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('edit invalidates redo', solve([[N],[[N-1]],[[N+1]],\"edit\",N+2,3]), {1: [[1, 3], [[0], [1]], []], 2: [[2, 4], [[1], [2]], []], 3: [[3, 5], [[2], [3]], []], 4: [[4, 6], [[3], [4]], []], 5: [[5, 7], [[4], [5]], []]}[N])\ncheck('undo latest', solve([[N+2],[[N],[N+1]],[],\"undo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('redo latest', solve([[N],[],[[N+2],[N+1]],\"redo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('empty undo', solve([[N],[],[],\"undo\",0,3]), {1: [[1], [], []], 2: [[2], [], []], 3: [[3], [], []], 4: [[4], [], []], 5: [[5], [], []]}[N])\ncheck('overflow snapshot', solve([[N,N+1],[],[],\"edit\",N+2,2]), {1: [[2, 3], [[1, 2]], []], 2: [[3, 4], [[2, 3]], []], 3: [[4, 5], [[3, 4]], []], 4: [[5, 6], [[4, 5]], []], 5: [[6, 7], [[5, 6]], []]}[N])\ncheck('zero bound edit', solve([[],[[N]],[],\"edit\",N+1,0]), {1: [[], [[1], []], []], 2: [[], [[2], []], []], 3: [[], [[3], []], []], 4: [[], [[4], []], []], 5: [[], [[5], []], []]}[N])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"da55aae5a8afface8a7c50ef27009098fbb82025e99083b705a070db635cce46","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x):\n    a,past,future,command,value,cap=x\n    if command=='edit':\n        new=(a+[value])[-cap:] if cap else []\n        return [new,past+[a],[]]\n    if command=='undo' and past:\n        return [past[-1],past[:-1],future+[a]]\n    if command=='redo' and future:\n        return [future[-1],past+[a],future[:-1]]\n    return [a,past,future]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('edit invalidates redo', solve([[N],[[N-1]],[[N+1]],\"edit\",N+2,3]), {1: [[1, 3], [[0], [1]], []], 2: [[2, 4], [[1], [2]], []], 3: [[3, 5], [[2], [3]], []], 4: [[4, 6], [[3], [4]], []], 5: [[5, 7], [[4], [5]], []]}[N])\ncheck('undo latest', solve([[N+2],[[N],[N+1]],[],\"undo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('redo latest', solve([[N],[],[[N+2],[N+1]],\"redo\",0,3]), {1: [[2], [[1]], [[3]]], 2: [[3], [[2]], [[4]]], 3: [[4], [[3]], [[5]]], 4: [[5], [[4]], [[6]]], 5: [[6], [[5]], [[7]]]}[N])\ncheck('empty undo', solve([[N],[],[],\"undo\",0,3]), {1: [[1], [], []], 2: [[2], [], []], 3: [[3], [], []], 4: [[4], [], []], 5: [[5], [], []]}[N])\ncheck('overflow snapshot', solve([[N,N+1],[],[],\"edit\",N+2,2]), {1: [[2, 3], [[1, 2]], []], 2: [[3, 4], [[2, 3]], []], 3: [[4, 5], [[3, 4]], []], 4: [[5, 6], [[4, 5]], []], 5: [[6, 7], [[5, 6]], []]}[N])\ncheck('zero bound edit', solve([[],[[N]],[],\"edit\",N+1,0]), {1: [[], [[1], []], []], 2: [[], [[2], []], []], 3: [[], [[3], []], []], 4: [[], [[4], []], []], 5: [[], [[5], []], []]}[N])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-bounded-deques-undo-snapshots-redo-invalidation","generated_at":"2026-09-29T14:44:29.911238+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Controlled bounded deque implementation model with explicit storage and lifecycle observations.","repair":"Restore the documented redo invalidation invariant in undo-snapshots.","root_cause":"New deque edit retains the abandoned redo branch.","sha256":"4c2849a194c605e442855191191e617280eecabb9f6b444378d9dfcdeb3dc88b","title":"New deque edit retains the abandoned redo branch · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.82,"exit_code":1,"observations":[{"actual":[[1,3],[[0],[1]],[[2]]],"check":"edit invalidates redo","expected":[[1,3],[[0],[1]],[]],"passed":false},{"actual":[[2],[[1]],[[3]]],"check":"undo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[2],[[1]],[[3]]],"check":"redo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[1],[],[]],"check":"empty undo","expected":[[1],[],[]],"passed":true},{"actual":[[2,3],[[1,2]],[]],"check":"overflow snapshot","expected":[[2,3],[[1,2]],[]],"passed":true},{"actual":[[],[[1],[]],[]],"check":"zero bound edit","expected":[[],[[1],[]],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"edit invalidates redo\", \"actual\": [[1, 3], [[0], [1]], [[2]]], \"expected\": [[1, 3], [[0], [1]], []], \"passed\": false}, {\"check\": \"undo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"redo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"empty undo\", \"actual\": [[1], [], []], \"expected\": [[1], [], []], \"passed\": true}, {\"check\": \"overflow snapshot\", \"actual\": [[2, 3], [[1, 2]], []], \"expected\": [[2, 3], [[1, 2]], []], \"passed\": true}, {\"check\": \"zero bound edit\", \"actual\": [[], [[1], []], []], \"expected\": [[], [[1], []], []], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":40.237,"exit_code":1,"observations":[{"actual":[[1,3],[[0],[1]],[[2]]],"check":"edit invalidates redo","expected":[[1,3],[[0],[1]],[]],"passed":false},{"actual":[[2],[[1]],[[3]]],"check":"undo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[2],[[1]],[[3]]],"check":"redo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[1],[],[]],"check":"empty undo","expected":[[1],[],[]],"passed":true},{"actual":[[2,3],[[1,2]],[]],"check":"overflow snapshot","expected":[[2,3],[[1,2]],[]],"passed":true},{"actual":[[],[[1],[]],[]],"check":"zero bound edit","expected":[[],[[1],[]],[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"edit invalidates redo\", \"actual\": [[1, 3], [[0], [1]], [[2]]], \"expected\": [[1, 3], [[0], [1]], []], \"passed\": false}, {\"check\": \"undo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"redo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"empty undo\", \"actual\": [[1], [], []], \"expected\": [[1], [], []], \"passed\": true}, {\"check\": \"overflow snapshot\", \"actual\": [[2, 3], [[1, 2]], []], \"expected\": [[2, 3], [[1, 2]], []], \"passed\": true}, {\"check\": \"zero bound edit\", \"actual\": [[], [[1], []], []], \"expected\": [[], [[1], []], []], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":44.808,"exit_code":0,"observations":[{"actual":[[1,3],[[0],[1]],[]],"check":"edit invalidates redo","expected":[[1,3],[[0],[1]],[]],"passed":true},{"actual":[[2],[[1]],[[3]]],"check":"undo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[2],[[1]],[[3]]],"check":"redo latest","expected":[[2],[[1]],[[3]]],"passed":true},{"actual":[[1],[],[]],"check":"empty undo","expected":[[1],[],[]],"passed":true},{"actual":[[2,3],[[1,2]],[]],"check":"overflow snapshot","expected":[[2,3],[[1,2]],[]],"passed":true},{"actual":[[],[[1],[]],[]],"check":"zero bound edit","expected":[[],[[1],[]],[]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"edit invalidates redo\", \"actual\": [[1, 3], [[0], [1]], []], \"expected\": [[1, 3], [[0], [1]], []], \"passed\": true}, {\"check\": \"undo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"redo latest\", \"actual\": [[2], [[1]], [[3]]], \"expected\": [[2], [[1]], [[3]]], \"passed\": true}, {\"check\": \"empty undo\", \"actual\": [[1], [], []], \"expected\": [[1], [], []], \"passed\": true}, {\"check\": \"overflow snapshot\", \"actual\": [[2, 3], [[1, 2]], []], \"expected\": [[2, 3], [[1, 2]], []], \"passed\": true}, {\"check\": \"zero bound edit\", \"actual\": [[], [[1], []], []], \"expected\": [[], [[1], []], []], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}