{"abstract":"Copy transfer incorrectly consumes a copyable 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.","evaluation_group":"s3-borrow-checking-move-paths","failed_approach":"The partial repair uses elif op=='copy': out.append(arg in live); live.clear(), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-move-paths-copy-nonconsuming","id":"FA-42976","implementations":{"attempt":{"sha256":"89d78992b624505a53c35e2bd8c99471a00394df2620cfd96382f827dbd24f23","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: 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); live.clear()\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":"a2a239e9a1c4dcbb7ee682a5f5e6981b1d0bd494be07c022c0768c4d5a567e06","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: 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); live.discard(arg)\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"},"fixed":{"sha256":"387a35b8e885bbc7a8a218ef7169356754c561fb33ef9e719085fa119ba50c48","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: 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-copy-nonconsuming","generated_at":"2026-09-29T14:43:57.231887+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.","repair":"Apply the specified transfer or inference rule at this site: elif op=='copy': out.append(arg in live).","root_cause":"The static analyzer mishandles copy nonconsuming: copy transfer incorrectly consumes a copyable leaf.","sha256":"2fcf714eed7014aecf023dd293fd6a1b1bd69ccb35b97030f66a55e423fc636b","title":"Copy transfer incorrectly consumes a copyable leaf · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":43.237,"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":[["a"],true],"check":"reassign empty","expected":[["a"],true],"passed":true},{"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,false],"check":"copy preserves","expected":[["a"],true,true],"passed":false},{"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\": [[\"a\"], true], \"expected\": [[\"a\"], true], \"passed\": true}, {\"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, false], \"expected\": [[\"a\"], true, true], \"passed\": false}, {\"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":41.597,"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":[["a"],true],"check":"reassign empty","expected":[["a"],true],"passed":true},{"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,false],"check":"copy preserves","expected":[["a"],true,true],"passed":false},{"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\": [[\"a\"], true], \"expected\": [[\"a\"], true], \"passed\": true}, {\"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, false], \"expected\": [[\"a\"], true, true], \"passed\": false}, {\"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"},"fixed":{"elapsed_ms":42.968,"exit_code":0,"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":[["a"],true],"check":"reassign empty","expected":[["a"],true],"passed":true},{"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":true,"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\": [[\"a\"], true], \"expected\": [[\"a\"], true], \"passed\": true}, {\"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\": true}\n"}},"verified":true,"visibility":"public"}