{"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. Moving ownership requires a live object and no shared or exclusive borrows.","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. Moving ownership requires a live object and no shared or exclusive borrows. Inputs are the finite Python values shown by the executable fixtures; no concurrent execution is assumed.","contract_signature":"x, y=None","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-move-forbidden-during-borrow","id":"FA-4501","implementations":{"attempt":{"sha256":"3f67ce95f67f2914ef27aea0cfa07cefbe70815a47d063e9de92f7b92635cb23","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\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":"3ec03684af9d24778b0f8febf3b5ed17b88d609f005c7729af6e2562cee491c6","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 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-move-forbidden-during-borrow","generated_at":"2026-09-29T14:37:39.897982+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.","root_cause":"Moving ownership requires a live object and no shared or exclusive borrows. The broken transition violates that invariant.","sha256":"c34ddd068886c9efbbe08ca72f2a7099fad9971421d8482cf544f955bccb47f1","title":"Owner move 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.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":38.17,"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,false,true,false,"denied",["initial",false,[],"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, 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, true, false, \"denied\", [\"initial\", false, [], \"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"},"broken":{"elapsed_ms":36.339,"exit_code":1,"observations":[{"actual":[true,false,true,false,false,false,true,"denied","denied",["initial",false,["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, false, true, \"denied\", \"denied\", [\"initial\", false, [\"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"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}