{"abstract":"Reinitializing a completely moved record fails to restore its leaf.","category":"Borrow checking","checks":13,"contract":"Static path initialization lattice for a record with declared leaf names. Commands init/move/read/whole/assign/drop/reset/copy/merge/available. init and assign initialize one leaf. move consumes only initialized named leaf and reports success; read tests one; whole tests all. drop consumes all and reports previously initialized names. reset clears; copy tests without consumption. merge intersects current initialized leaves with supplied branch leaves. available returns sorted initialized names. Unknown leaves never initialize. Return one result per command. This is definite-initialization analysis, not runtime borrowing.","contract_signature":"leaves, ops","evaluation_group":"s3-borrow-checking-move-paths","failed_approach":"The partial repair uses if arg in allowed and live: live.add(arg), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-move-paths-assign-restore","id":"FA-42961","implementations":{"attempt":{"sha256":"6d1c97e8c516dcee009fdb0549688feadf0dc047c3bb5b12769c13eaf44b027a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(leaves, ops):\n    allowed=set(leaves); live=set(); out=[]\n    for op,arg in ops:\n        if op=='init':\n            live.update(set(arg)&allowed); out.append(sorted(live))\n        elif op=='move':\n            ok=arg in live\n            if ok: live.remove(arg)\n            out.append(ok)\n        elif op=='read': out.append(arg in live)\n        elif op=='whole': out.append(live==allowed)\n        elif op=='assign':\n            if arg in allowed and live: live.add(arg)\n            out.append(sorted(live))\n        elif op=='drop':\n            out.append(sorted(live)); live.clear()\n        elif op=='reset':\n            live.clear(); out.append([])\n        elif op=='copy': out.append(arg in live)\n        elif op=='merge':\n            live.intersection_update(arg); out.append(sorted(live))\n        elif op=='available': out.append(sorted(live))\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='v'+str(N)\ncheck('unknown init',solve(['a'],[('init',['a',x])]),[['a']])\ncheck('last move',solve(['a'],[('init',['a']),('move','a'),('read','a')]),[['a'],True,False])\ncheck('uninitialized sibling',solve(['a','b'],[('init',['a']),('read','b')]),[['a'],False])\ncheck('empty whole',solve([], [('whole',None)]),[True])\ncheck('partial whole',solve(['a','b'],[('init',['a']),('whole',None)]),[['a'],False])\ncheck('reassign empty',solve(['a'],[('assign','a'),('read','a')]),[['a'],True])\ncheck('drop clears',solve(['a'],[('init',['a']),('drop',None),('read','a')]),[['a'],['a'],False])\ncheck('storage reset',solve(['a'],[('init',['a']),('reset',None),('read','a')]),[['a'],[],False])\ncheck('copy preserves',solve(['a'],[('init',['a']),('copy','a'),('read','a')]),[['a'],True,True])\ncheck('join intersection',solve(['a','b'],[('init',['a']),('merge',['b']),('available',None)]),[['a'],[],[]])\ncheck('available subset',solve(['a','b'],[('init',['a']),('available',None)]),[['a'],['a']])\ncheck('variant leaf',solve([x],[('init',[x]),('move',x),('available',None)]),[[x],True,[]])\ncheck('record arity',solve(list(range(N+1)),[('init',list(range(N+1))),('move',N),('available',None)]),[list(range(N+1)),True,list(range(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":"52c811d721363b74b1127dfc8b880e1f482a2109d372e0309ce5d180b4457aa6","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(leaves, ops):\n    allowed=set(leaves); live=set(); out=[]\n    for op,arg in ops:\n        if op=='init':\n            live.update(set(arg)&allowed); out.append(sorted(live))\n        elif op=='move':\n            ok=arg in live\n            if ok: live.remove(arg)\n            out.append(ok)\n        elif op=='read': out.append(arg in live)\n        elif op=='whole': out.append(live==allowed)\n        elif op=='assign':\n            if False: live.add(arg)\n            out.append(sorted(live))\n        elif op=='drop':\n            out.append(sorted(live)); live.clear()\n        elif op=='reset':\n            live.clear(); out.append([])\n        elif op=='copy': out.append(arg in live)\n        elif op=='merge':\n            live.intersection_update(arg); out.append(sorted(live))\n        elif op=='available': out.append(sorted(live))\n    return out\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='v'+str(N)\ncheck('unknown init',solve(['a'],[('init',['a',x])]),[['a']])\ncheck('last move',solve(['a'],[('init',['a']),('move','a'),('read','a')]),[['a'],True,False])\ncheck('uninitialized sibling',solve(['a','b'],[('init',['a']),('read','b')]),[['a'],False])\ncheck('empty whole',solve([], [('whole',None)]),[True])\ncheck('partial whole',solve(['a','b'],[('init',['a']),('whole',None)]),[['a'],False])\ncheck('reassign empty',solve(['a'],[('assign','a'),('read','a')]),[['a'],True])\ncheck('drop clears',solve(['a'],[('init',['a']),('drop',None),('read','a')]),[['a'],['a'],False])\ncheck('storage reset',solve(['a'],[('init',['a']),('reset',None),('read','a')]),[['a'],[],False])\ncheck('copy preserves',solve(['a'],[('init',['a']),('copy','a'),('read','a')]),[['a'],True,True])\ncheck('join intersection',solve(['a','b'],[('init',['a']),('merge',['b']),('available',None)]),[['a'],[],[]])\ncheck('available subset',solve(['a','b'],[('init',['a']),('available',None)]),[['a'],['a']])\ncheck('variant leaf',solve([x],[('init',[x]),('move',x),('available',None)]),[[x],True,[]])\ncheck('record arity',solve(list(range(N+1)),[('init',list(range(N+1))),('move',N),('available',None)]),[list(range(N+1)),True,list(range(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":"The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. 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-borrow-checking-move-paths-assign-restore","generated_at":"2026-09-29T14:43:57.261096+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.","root_cause":"The static analyzer mishandles assign restore: reinitializing a completely moved record fails to restore its leaf.","sha256":"7b5d7eef4236e4a054741afe3f4249aaeafb5301450de3fb8101f22430182db9","title":"Reinitializing a completely moved record fails to restore its leaf · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":43.682,"exit_code":1,"observations":[{"actual":[["a"]],"check":"unknown init","expected":[["a"]],"passed":true},{"actual":[["a"],true,false],"check":"last move","expected":[["a"],true,false],"passed":true},{"actual":[["a"],false],"check":"uninitialized sibling","expected":[["a"],false],"passed":true},{"actual":[true],"check":"empty whole","expected":[true],"passed":true},{"actual":[["a"],false],"check":"partial whole","expected":[["a"],false],"passed":true},{"actual":[[],false],"check":"reassign empty","expected":[["a"],true],"passed":false},{"actual":[["a"],["a"],false],"check":"drop clears","expected":[["a"],["a"],false],"passed":true},{"actual":[["a"],[],false],"check":"storage reset","expected":[["a"],[],false],"passed":true},{"actual":[["a"],true,true],"check":"copy preserves","expected":[["a"],true,true],"passed":true},{"actual":[["a"],[],[]],"check":"join intersection","expected":[["a"],[],[]],"passed":true},{"actual":[["a"],["a"]],"check":"available subset","expected":[["a"],["a"]],"passed":true},{"actual":[["v1"],true,[]],"check":"variant leaf","expected":[["v1"],true,[]],"passed":true},{"actual":[[0,1],true,[0]],"check":"record arity","expected":[[0,1],true,[0]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"unknown init\", \"actual\": [[\"a\"]], \"expected\": [[\"a\"]], \"passed\": true}, {\"check\": \"last move\", \"actual\": [[\"a\"], true, false], \"expected\": [[\"a\"], true, false], \"passed\": true}, {\"check\": \"uninitialized sibling\", \"actual\": [[\"a\"], false], \"expected\": [[\"a\"], false], \"passed\": true}, {\"check\": \"empty whole\", \"actual\": [true], \"expected\": [true], \"passed\": true}, {\"check\": \"partial whole\", \"actual\": [[\"a\"], false], \"expected\": [[\"a\"], false], \"passed\": true}, {\"check\": \"reassign empty\", \"actual\": [[], false], \"expected\": [[\"a\"], true], \"passed\": false}, {\"check\": \"drop clears\", \"actual\": [[\"a\"], [\"a\"], false], \"expected\": [[\"a\"], [\"a\"], false], \"passed\": true}, {\"check\": \"storage reset\", \"actual\": [[\"a\"], [], false], \"expected\": [[\"a\"], [], false], \"passed\": true}, {\"check\": \"copy preserves\", \"actual\": [[\"a\"], true, true], \"expected\": [[\"a\"], true, true], \"passed\": true}, {\"check\": \"join intersection\", \"actual\": [[\"a\"], [], []], \"expected\": [[\"a\"], [], []], \"passed\": true}, {\"check\": \"available subset\", \"actual\": [[\"a\"], [\"a\"]], \"expected\": [[\"a\"], [\"a\"]], \"passed\": true}, {\"check\": \"variant leaf\", \"actual\": [[\"v1\"], true, []], \"expected\": [[\"v1\"], true, []], \"passed\": true}, {\"check\": \"record arity\", \"actual\": [[0, 1], true, [0]], \"expected\": [[0, 1], true, [0]], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":44.835,"exit_code":1,"observations":[{"actual":[["a"]],"check":"unknown init","expected":[["a"]],"passed":true},{"actual":[["a"],true,false],"check":"last move","expected":[["a"],true,false],"passed":true},{"actual":[["a"],false],"check":"uninitialized sibling","expected":[["a"],false],"passed":true},{"actual":[true],"check":"empty whole","expected":[true],"passed":true},{"actual":[["a"],false],"check":"partial whole","expected":[["a"],false],"passed":true},{"actual":[[],false],"check":"reassign empty","expected":[["a"],true],"passed":false},{"actual":[["a"],["a"],false],"check":"drop clears","expected":[["a"],["a"],false],"passed":true},{"actual":[["a"],[],false],"check":"storage reset","expected":[["a"],[],false],"passed":true},{"actual":[["a"],true,true],"check":"copy preserves","expected":[["a"],true,true],"passed":true},{"actual":[["a"],[],[]],"check":"join intersection","expected":[["a"],[],[]],"passed":true},{"actual":[["a"],["a"]],"check":"available subset","expected":[["a"],["a"]],"passed":true},{"actual":[["v1"],true,[]],"check":"variant leaf","expected":[["v1"],true,[]],"passed":true},{"actual":[[0,1],true,[0]],"check":"record arity","expected":[[0,1],true,[0]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"unknown init\", \"actual\": [[\"a\"]], \"expected\": [[\"a\"]], \"passed\": true}, {\"check\": \"last move\", \"actual\": [[\"a\"], true, false], \"expected\": [[\"a\"], true, false], \"passed\": true}, {\"check\": \"uninitialized sibling\", \"actual\": [[\"a\"], false], \"expected\": [[\"a\"], false], \"passed\": true}, {\"check\": \"empty whole\", \"actual\": [true], \"expected\": [true], \"passed\": true}, {\"check\": \"partial whole\", \"actual\": [[\"a\"], false], \"expected\": [[\"a\"], false], \"passed\": true}, {\"check\": \"reassign empty\", \"actual\": [[], false], \"expected\": [[\"a\"], true], \"passed\": false}, {\"check\": \"drop clears\", \"actual\": [[\"a\"], [\"a\"], false], \"expected\": [[\"a\"], [\"a\"], false], \"passed\": true}, {\"check\": \"storage reset\", \"actual\": [[\"a\"], [], false], \"expected\": [[\"a\"], [], false], \"passed\": true}, {\"check\": \"copy preserves\", \"actual\": [[\"a\"], true, true], \"expected\": [[\"a\"], true, true], \"passed\": true}, {\"check\": \"join intersection\", \"actual\": [[\"a\"], [], []], \"expected\": [[\"a\"], [], []], \"passed\": true}, {\"check\": \"available subset\", \"actual\": [[\"a\"], [\"a\"]], \"expected\": [[\"a\"], [\"a\"]], \"passed\": true}, {\"check\": \"variant leaf\", \"actual\": [[\"v1\"], true, []], \"expected\": [[\"v1\"], true, []], \"passed\": true}, {\"check\": \"record arity\", \"actual\": [[0, 1], true, [0]], \"expected\": [[0, 1], true, [0]], \"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."}}