{"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. Direct owner writes require a live object with no outstanding 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. Direct owner writes require a live object with no outstanding 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-owner-write-forbidden-during-borrow","id":"FA-4496","implementations":{"attempt":{"sha256":"08dc8b6a0df5cbf4faba5a2dc0f4afd822756a18a91f98172a7d4129614e7f15","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 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":"a73cc9866f8550c44861a45283d45cf11506ee1234a4a74a1e6f54470cb0fc99","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\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-owner-write-forbidden-during-borrow","generated_at":"2026-09-29T14:37:39.809317+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. Direct owner writes require a live object with no outstanding borrow.","root_cause":"Direct owner writes require a live object with no outstanding borrow. The broken transition violates that invariant.","sha256":"d3c1a970309ab72b10b6d19d7e126cdc26d0f382a4e30d4ed562783948e86eca","title":"Owner write forbidden during borrow · 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":44.137,"exit_code":1,"observations":[{"actual":[true,false,true,false,false,true,false,"bad","denied",["bad",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":false},{"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":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"shared readers prohibit mutation\", \"actual\": [true, false, true, false, false, true, false, \"bad\", \"denied\", [\"bad\", true, [\"a\", \"b\"], null]], \"expected\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"passed\": false}, {\"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\": false}\n"},"broken":{"elapsed_ms":40.59,"exit_code":1,"observations":[{"actual":[true,false,true,false,false,true,false,"bad","denied",["bad",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":false},{"actual":[true,false,false,false,true,true,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":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, true, false, \"bad\", \"denied\", [\"bad\", true, [\"a\", \"b\"], null]], \"expected\": [true, false, true, false, false, false, false, \"initial\", \"denied\", [\"initial\", true, [\"a\", \"b\"], null]], \"passed\": false}, {\"check\": \"exclusive token protects identity\", \"actual\": [true, false, false, false, true, true, false, true, \"new\", [\"new\", true, [], \"w\"]], \"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":38.615,"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"}