{"abstract":"The operation returns a result or retained state that violates this contract: A single local object grants either any number of shared borrows or one exclusive borrow. Commands are [operation,token,value]. Reads return the value or denied; writes and acquisitions return booleans. Ownership can move only with no borrows. Releasing an unrelated token must not clear the exclusive borrow.","category":"Borrow checking","checks":5,"contract":"A single local object grants either any number of shared borrows or one exclusive borrow. Commands are [operation,token,value]. Reads return the value or denied; writes and acquisitions return booleans. Ownership can move only with no borrows. Releasing an unrelated token must not clear the exclusive borrow. Inputs are the finite Python values shown by the executable fixtures; no concurrent execution is assumed.","evaluation_group":"xr-suite-shared-borrow-excludes-writer","failed_approach":"The attempted transition changes the behavior but still violates the same invariant in at least one independent regression fixture.","family":"xr-release-checks-exclusive-identity","id":"FA-4481","implementations":{"attempt":{"sha256":"6d192d7d1789ef167e038ac548ddcf2205c0f8ee9fae18dc79693855a2bed5ff","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x, y=None):\n    shared=set(); exclusive=None; value=y; live=True; out=[]\n    for op,k,arg in x:\n        if op=='shared':\n            ok=live and exclusive is None and k not in shared\n            if ok: shared.add(k)\n            out.append(ok)\n        elif op=='exclusive':\n            ok=live and not shared and exclusive is None\n            if ok: exclusive=k\n            out.append(ok)\n        elif op=='release':\n            shared.discard(k)\n            if k not in shared: exclusive=None\n            out.append(True)\n        elif op=='read':\n            out.append(value if live and (k in shared or (exclusive is not None and k==exclusive)) else 'denied')\n        elif op=='write':\n            ok=live and exclusive is not None and k==exclusive\n            if ok: value=arg\n            out.append(ok)\n        elif op=='ownerwrite':\n            ok=live and not shared and exclusive is None\n            if ok: value=arg\n            out.append(ok)\n        elif op=='move':\n            ok=live and not shared and exclusive is None\n            if ok: live=False\n            out.append(ok)\n        elif op=='inspect': out.append([value,live,sorted(shared),exclusive])\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('shared readers prohibit mutation', solve([['shared', 'a', None], ['shared', 'a', None], ['shared', 'b', None], ['exclusive', 'w', None], ['write', 'a', 'bad'], ['ownerwrite', None, 'bad'], ['move', None, None], ['read', 'a', None], ['read', 'ghost', None], ['inspect', None, None]], 'initial'), [True, False, True, False, False, False, False, 'initial', 'denied', ['initial', True, ['a', 'b'], None]])\ncheck('exclusive token protects identity', solve([['exclusive', 'w', None], ['exclusive', 'other', None], ['shared', 'a', None], ['write', 'ghost', 'bad'], ['release', 'ghost', None], ['ownerwrite', None, 'bad'], ['move', None, None], ['write', 'w', 'new'], ['read', 'w', None], ['inspect', None, None]], 'initial'), [True, False, False, False, True, False, False, True, 'new', ['new', True, [], 'w']])\ncheck('released token loses rights', solve([['shared', 'a', None], ['release', 'a', None], ['read', 'a', None], ['exclusive', 'w', None], ['release', 'w', None], ['write', 'w', 'bad'], ['ownerwrite', None, 'new'], ['inspect', None, None]], 'initial'), [True, True, 'denied', True, True, False, True, ['new', True, [], None]])\ncheck('moved object stays unavailable', solve([['move', None, None], ['shared', 'a', None], ['exclusive', 'w', None], ['ownerwrite', None, 'bad'], ['read', None, None], ['move', None, None], ['inspect', None, None]], 'initial'), [True, False, False, False, 'denied', False, ['initial', False, [], None]])\ncheck('None is not a borrowed token', solve([['read',None,None]], 'initial'), ['denied'])\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":"474fd164e8b54765bfe9eb506f4f274123f554003038ae4cb44264529f34d827","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x, y=None):\n    shared=set(); exclusive=None; value=y; live=True; out=[]\n    for op,k,arg in x:\n        if op=='shared':\n            ok=live and exclusive is None and k not in shared\n            if ok: shared.add(k)\n            out.append(ok)\n        elif op=='exclusive':\n            ok=live and not shared and exclusive is None\n            if ok: exclusive=k\n            out.append(ok)\n        elif op=='release':\n            shared.discard(k)\n            if True: exclusive=None\n            out.append(True)\n        elif op=='read':\n            out.append(value if live and (k in shared or (exclusive is not None and k==exclusive)) else 'denied')\n        elif op=='write':\n            ok=live and exclusive is not None and k==exclusive\n            if ok: value=arg\n            out.append(ok)\n        elif op=='ownerwrite':\n            ok=live and not shared and exclusive is None\n            if ok: value=arg\n            out.append(ok)\n        elif op=='move':\n            ok=live and not shared and exclusive is None\n            if ok: live=False\n            out.append(ok)\n        elif op=='inspect': out.append([value,live,sorted(shared),exclusive])\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('shared readers prohibit mutation', solve([['shared', 'a', None], ['shared', 'a', None], ['shared', 'b', None], ['exclusive', 'w', None], ['write', 'a', 'bad'], ['ownerwrite', None, 'bad'], ['move', None, None], ['read', 'a', None], ['read', 'ghost', None], ['inspect', None, None]], 'initial'), [True, False, True, False, False, False, False, 'initial', 'denied', ['initial', True, ['a', 'b'], None]])\ncheck('exclusive token protects identity', solve([['exclusive', 'w', None], ['exclusive', 'other', None], ['shared', 'a', None], ['write', 'ghost', 'bad'], ['release', 'ghost', None], ['ownerwrite', None, 'bad'], ['move', None, None], ['write', 'w', 'new'], ['read', 'w', None], ['inspect', None, None]], 'initial'), [True, False, False, False, True, False, False, True, 'new', ['new', True, [], 'w']])\ncheck('released token loses rights', solve([['shared', 'a', None], ['release', 'a', None], ['read', 'a', None], ['exclusive', 'w', None], ['release', 'w', None], ['write', 'w', 'bad'], ['ownerwrite', None, 'new'], ['inspect', None, None]], 'initial'), [True, True, 'denied', True, True, False, True, ['new', True, [], None]])\ncheck('moved object stays unavailable', solve([['move', None, None], ['shared', 'a', None], ['exclusive', 'w', None], ['ownerwrite', None, 'bad'], ['read', None, None], ['move', None, None], ['inspect', None, None]], 'initial'), [True, False, False, False, 'denied', False, ['initial', False, [], None]])\ncheck('None is not a borrowed token', solve([['read',None,None]], 'initial'), ['denied'])\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":"179e9bebac9713850918ef163042ca730821218a1f1f0f23d55cf7caa0466f20","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(x, y=None):\n    shared=set(); exclusive=None; value=y; live=True; out=[]\n    for op,k,arg in x:\n        if op=='shared':\n            ok=live and exclusive is None and k not in shared\n            if ok: shared.add(k)\n            out.append(ok)\n        elif op=='exclusive':\n            ok=live and not shared and exclusive is None\n            if ok: exclusive=k\n            out.append(ok)\n        elif op=='release':\n            shared.discard(k)\n            if exclusive==k: exclusive=None\n            out.append(True)\n        elif op=='read':\n            out.append(value if live and (k in shared or (exclusive is not None and k==exclusive)) else 'denied')\n        elif op=='write':\n            ok=live and exclusive is not None and k==exclusive\n            if ok: value=arg\n            out.append(ok)\n        elif op=='ownerwrite':\n            ok=live and not shared and exclusive is None\n            if ok: value=arg\n            out.append(ok)\n        elif op=='move':\n            ok=live and not shared and exclusive is None\n            if ok: live=False\n            out.append(ok)\n        elif op=='inspect': out.append([value,live,sorted(shared),exclusive])\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('shared readers prohibit mutation', solve([['shared', 'a', None], ['shared', 'a', None], ['shared', 'b', None], ['exclusive', 'w', None], ['write', 'a', 'bad'], ['ownerwrite', None, 'bad'], ['move', None, None], ['read', 'a', None], ['read', 'ghost', None], ['inspect', None, None]], 'initial'), [True, False, True, False, False, False, False, 'initial', 'denied', ['initial', True, ['a', 'b'], None]])\ncheck('exclusive token protects identity', solve([['exclusive', 'w', None], ['exclusive', 'other', None], ['shared', 'a', None], ['write', 'ghost', 'bad'], ['release', 'ghost', None], ['ownerwrite', None, 'bad'], ['move', None, None], ['write', 'w', 'new'], ['read', 'w', None], ['inspect', None, None]], 'initial'), [True, False, False, False, True, False, False, True, 'new', ['new', True, [], 'w']])\ncheck('released token loses rights', solve([['shared', 'a', None], ['release', 'a', None], ['read', 'a', None], ['exclusive', 'w', None], ['release', 'w', None], ['write', 'w', 'bad'], ['ownerwrite', None, 'new'], ['inspect', None, None]], 'initial'), [True, True, 'denied', True, True, False, True, ['new', True, [], None]])\ncheck('moved object stays unavailable', solve([['move', None, None], ['shared', 'a', None], ['exclusive', 'w', None], ['ownerwrite', None, 'bad'], ['read', None, None], ['move', None, None], ['inspect', None, None]], 'initial'), [True, False, False, False, 'denied', False, ['initial', False, [], None]])\ncheck('None is not a borrowed token', solve([['read',None,None]], 'initial'), ['denied'])\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":" 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":"xr-release-checks-exclusive-identity","generated_at":"2026-09-29T14:37:39.682988+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A controlled local-runtime regression for collection APIs, language semantics, or ownership wrappers. Fixtures include boundary and interaction cases.","repair":"A single local object grants either any number of shared borrows or one exclusive borrow. Commands are [operation,token,value]. Reads return the value or denied; writes and acquisitions return booleans. Ownership can move only with no borrows. Releasing an unrelated token must not clear the exclusive borrow.","root_cause":"Releasing an unrelated token must not clear the exclusive borrow. The broken transition violates that invariant.","sha256":"71dcad06f1a5be4034f1d5cf2a074dbae451e3b018833158795090861934b978","title":"Release checks exclusive identity · case 01","variant":1,"variant_policy":"Five execution reruns of a fixed adversarial fixture suite; variant number does not alter semantic inputs.","verification":{"attempt":{"elapsed_ms":112.394,"exit_code":1,"observations":[{"actual":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"check":"shared readers prohibit mutation","expected":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"passed":true},{"actual":[true,false,false,false,true,true,true,false,"denied",["bad",false,[],null]],"check":"exclusive token protects identity","expected":[true,false,false,false,true,false,false,true,"new",["new",true,[],"w"]],"passed":false},{"actual":[true,true,"denied",true,true,false,true,["new",true,[],null]],"check":"released token loses rights","expected":[true,true,"denied",true,true,false,true,["new",true,[],null]],"passed":true},{"actual":[true,false,false,false,"denied",false,["initial",false,[],null]],"check":"moved object stays unavailable","expected":[true,false,false,false,"denied",false,["initial",false,[],null]],"passed":true},{"actual":["denied"],"check":"None is not a borrowed token","expected":["denied"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"shared readers prohibit mutation\", \"actual\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"expected\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"passed\": true}, {\"check\": \"exclusive token protects identity\", \"actual\": [true, false, false, false, true, true, true, false, \"denied\", [\"bad\", false, [], null]], \"expected\": [true, false, false, false, true, false, false, true, \"new\", [\"new\", true, [], \"w\"]], \"passed\": false}, {\"check\": \"released token loses rights\", \"actual\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"expected\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"passed\": true}, {\"check\": \"moved object stays unavailable\", \"actual\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"expected\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"passed\": true}, {\"check\": \"None is not a borrowed token\", \"actual\": [\"denied\"], \"expected\": [\"denied\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":43.295,"exit_code":1,"observations":[{"actual":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"check":"shared readers prohibit mutation","expected":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"passed":true},{"actual":[true,false,false,false,true,true,true,false,"denied",["bad",false,[],null]],"check":"exclusive token protects identity","expected":[true,false,false,false,true,false,false,true,"new",["new",true,[],"w"]],"passed":false},{"actual":[true,true,"denied",true,true,false,true,["new",true,[],null]],"check":"released token loses rights","expected":[true,true,"denied",true,true,false,true,["new",true,[],null]],"passed":true},{"actual":[true,false,false,false,"denied",false,["initial",false,[],null]],"check":"moved object stays unavailable","expected":[true,false,false,false,"denied",false,["initial",false,[],null]],"passed":true},{"actual":["denied"],"check":"None is not a borrowed token","expected":["denied"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"shared readers prohibit mutation\", \"actual\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"expected\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"passed\": true}, {\"check\": \"exclusive token protects identity\", \"actual\": [true, false, false, false, true, true, true, false, \"denied\", [\"bad\", false, [], null]], \"expected\": [true, false, false, false, true, false, false, true, \"new\", [\"new\", true, [], \"w\"]], \"passed\": false}, {\"check\": \"released token loses rights\", \"actual\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"expected\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"passed\": true}, {\"check\": \"moved object stays unavailable\", \"actual\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"expected\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"passed\": true}, {\"check\": \"None is not a borrowed token\", \"actual\": [\"denied\"], \"expected\": [\"denied\"], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":41.898,"exit_code":0,"observations":[{"actual":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"check":"shared readers prohibit mutation","expected":[true,false,true,false,false,false,false,"initial","denied",["initial",true,["a","b"],null]],"passed":true},{"actual":[true,false,false,false,true,false,false,true,"new",["new",true,[],"w"]],"check":"exclusive token protects identity","expected":[true,false,false,false,true,false,false,true,"new",["new",true,[],"w"]],"passed":true},{"actual":[true,true,"denied",true,true,false,true,["new",true,[],null]],"check":"released token loses rights","expected":[true,true,"denied",true,true,false,true,["new",true,[],null]],"passed":true},{"actual":[true,false,false,false,"denied",false,["initial",false,[],null]],"check":"moved object stays unavailable","expected":[true,false,false,false,"denied",false,["initial",false,[],null]],"passed":true},{"actual":["denied"],"check":"None is not a borrowed token","expected":["denied"],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"shared readers prohibit mutation\", \"actual\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"expected\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"passed\": true}, {\"check\": \"exclusive token protects identity\", \"actual\": [true, false, false, false, true, false, false, true, \"new\", [\"new\", true, [], \"w\"]], \"expected\": [true, false, false, false, true, false, false, true, \"new\", [\"new\", true, [], \"w\"]], \"passed\": true}, {\"check\": \"released token loses rights\", \"actual\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"expected\": [true, true, \"denied\", true, true, false, true, [\"new\", true, [], null]], \"passed\": true}, {\"check\": \"moved object stays unavailable\", \"actual\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"expected\": [true, false, false, false, \"denied\", false, [\"initial\", false, [], null]], \"passed\": true}, {\"check\": \"None is not a borrowed token\", \"actual\": [\"denied\"], \"expected\": [\"denied\"], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}