{"abstract":"Reference definition kills demands for unrelated live locals.","category":"Borrow checking","checks":13,"contract":"Backward reference-demand transfer over a finite straight-line IR. ops execute forward and analysis traverses backward. use/return demand one reference; call demands all actual references. def and storage_dead kill a local. assign(d,s) propagates demand from destination to source, killing destination. reborrow(d,p) kills child demand and adds parent unconditionally because construction reads parent. phi(d,sources) propagates destination demand to every source. drop(ref,needs_drop) demands only when destructor can observe referent. branch supplies two already-computed successor demand sets, both unioned. Return sorted entry-demand names.","evaluation_group":"s3-borrow-checking-reference-demand","failed_approach":"The partial repair uses elif op=='def': live.clear(), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-reference-demand-definition-kill","id":"FA-43006","implementations":{"attempt":{"sha256":"d2c5401c4e0486d594112a3d6c42a80ee411bab6498657f99963a68854c7ebaa","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(ops):\n    live=set()\n    for op,a,b in reversed(ops):\n        if op=='use': live.add(a)\n        elif op=='return': live.add(a)\n        elif op=='call': live.update(a)\n        elif op=='def': live.clear()\n        elif op=='storage_dead': live.discard(a)\n        elif op=='assign':\n            needed=a in live; live.discard(a)\n            if needed: live.add(b)\n        elif op=='reborrow':\n            live.discard(a); live.add(b)\n        elif op=='phi':\n            needed=a in live; live.discard(a)\n            if needed: live.update(b)\n        elif op=='drop':\n            if b: live.add(a)\n        elif op=='branch': live.update(set(a)|set(b))\n    return sorted(live)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='r'+str(N)\ncheck('empty',solve([]),[])\ncheck('use',solve([('use',x,None)]),[x])\ncheck('return',solve([('return',x,None)]),[x])\ncheck('call',solve([('call',['a',x],None)]),['a',x])\ncheck('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])\ncheck('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])\ncheck('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])\ncheck('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])\ncheck('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])\ncheck('trivial drop',solve([('drop',x,False)]),[])\ncheck('observing drop',solve([('drop',x,True)]),[x])\ncheck('branch union',solve([('branch',['a'],[x])]),['a',x])\ncheck('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))\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":"20bbcbf10f0bd6adf5c6e143acabcc260688300970e5c43be33425c6c7cda1dc","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(ops):\n    live=set()\n    for op,a,b in reversed(ops):\n        if op=='use': live.add(a)\n        elif op=='return': live.add(a)\n        elif op=='call': live.update(a)\n        elif op=='def': pass\n        elif op=='storage_dead': live.discard(a)\n        elif op=='assign':\n            needed=a in live; live.discard(a)\n            if needed: live.add(b)\n        elif op=='reborrow':\n            live.discard(a); live.add(b)\n        elif op=='phi':\n            needed=a in live; live.discard(a)\n            if needed: live.update(b)\n        elif op=='drop':\n            if b: live.add(a)\n        elif op=='branch': live.update(set(a)|set(b))\n    return sorted(live)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='r'+str(N)\ncheck('empty',solve([]),[])\ncheck('use',solve([('use',x,None)]),[x])\ncheck('return',solve([('return',x,None)]),[x])\ncheck('call',solve([('call',['a',x],None)]),['a',x])\ncheck('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])\ncheck('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])\ncheck('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])\ncheck('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])\ncheck('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])\ncheck('trivial drop',solve([('drop',x,False)]),[])\ncheck('observing drop',solve([('drop',x,True)]),[x])\ncheck('branch union',solve([('branch',['a'],[x])]),['a',x])\ncheck('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))\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":"b6e537905467c375d1a94f1167707d079a663a06707c381a5902435053ddbd24","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(ops):\n    live=set()\n    for op,a,b in reversed(ops):\n        if op=='use': live.add(a)\n        elif op=='return': live.add(a)\n        elif op=='call': live.update(a)\n        elif op=='def': live.discard(a)\n        elif op=='storage_dead': live.discard(a)\n        elif op=='assign':\n            needed=a in live; live.discard(a)\n            if needed: live.add(b)\n        elif op=='reborrow':\n            live.discard(a); live.add(b)\n        elif op=='phi':\n            needed=a in live; live.discard(a)\n            if needed: live.update(b)\n        elif op=='drop':\n            if b: live.add(a)\n        elif op=='branch': live.update(set(a)|set(b))\n    return sorted(live)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nx='r'+str(N)\ncheck('empty',solve([]),[])\ncheck('use',solve([('use',x,None)]),[x])\ncheck('return',solve([('return',x,None)]),[x])\ncheck('call',solve([('call',['a',x],None)]),['a',x])\ncheck('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])\ncheck('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])\ncheck('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])\ncheck('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])\ncheck('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])\ncheck('trivial drop',solve([('drop',x,False)]),[])\ncheck('observing drop',solve([('drop',x,True)]),[x])\ncheck('branch union',solve([('branch',['a'],[x])]),['a',x])\ncheck('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))\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-reference-demand-definition-kill","generated_at":"2026-09-29T14:43:57.324289+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=='def': live.discard(a).","root_cause":"The static analyzer mishandles definition kill: reference definition kills demands for unrelated live locals.","sha256":"374afb5a9f97a92518e1b18eefd7aa16cb7c8dfb8d32457d5ec5c64e5c324b63","title":"Reference definition kills demands for unrelated live locals · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":44.892,"exit_code":1,"observations":[{"actual":[],"check":"empty","expected":[],"passed":true},{"actual":["r1"],"check":"use","expected":["r1"],"passed":true},{"actual":["r1"],"check":"return","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"call","expected":["a","r1"],"passed":true},{"actual":[],"check":"definition","expected":["r1"],"passed":false},{"actual":[],"check":"dead boundary","expected":[],"passed":true},{"actual":["r1"],"check":"assign demanded","expected":["r1"],"passed":true},{"actual":["r1"],"check":"reborrow constructor","expected":["r1"],"passed":true},{"actual":["b","r1"],"check":"phi second origin","expected":["b","r1"],"passed":true},{"actual":[],"check":"trivial drop","expected":[],"passed":true},{"actual":["r1"],"check":"observing drop","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"branch union","expected":["a","r1"],"passed":true},{"actual":[0,1],"check":"variable arity","expected":[0,1],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"use\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"return\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"call\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"definition\", \"actual\": [], \"expected\": [\"r1\"], \"passed\": false}, {\"check\": \"dead boundary\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"assign demanded\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"reborrow constructor\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"phi second origin\", \"actual\": [\"b\", \"r1\"], \"expected\": [\"b\", \"r1\"], \"passed\": true}, {\"check\": \"trivial drop\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"observing drop\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"branch union\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"variable arity\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.006,"exit_code":1,"observations":[{"actual":[],"check":"empty","expected":[],"passed":true},{"actual":["r1"],"check":"use","expected":["r1"],"passed":true},{"actual":["r1"],"check":"return","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"call","expected":["a","r1"],"passed":true},{"actual":["a","r1"],"check":"definition","expected":["r1"],"passed":false},{"actual":[],"check":"dead boundary","expected":[],"passed":true},{"actual":["r1"],"check":"assign demanded","expected":["r1"],"passed":true},{"actual":["r1"],"check":"reborrow constructor","expected":["r1"],"passed":true},{"actual":["b","r1"],"check":"phi second origin","expected":["b","r1"],"passed":true},{"actual":[],"check":"trivial drop","expected":[],"passed":true},{"actual":["r1"],"check":"observing drop","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"branch union","expected":["a","r1"],"passed":true},{"actual":[0,1],"check":"variable arity","expected":[0,1],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"use\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"return\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"call\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"definition\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"r1\"], \"passed\": false}, {\"check\": \"dead boundary\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"assign demanded\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"reborrow constructor\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"phi second origin\", \"actual\": [\"b\", \"r1\"], \"expected\": [\"b\", \"r1\"], \"passed\": true}, {\"check\": \"trivial drop\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"observing drop\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"branch union\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"variable arity\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":42.475,"exit_code":0,"observations":[{"actual":[],"check":"empty","expected":[],"passed":true},{"actual":["r1"],"check":"use","expected":["r1"],"passed":true},{"actual":["r1"],"check":"return","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"call","expected":["a","r1"],"passed":true},{"actual":["r1"],"check":"definition","expected":["r1"],"passed":true},{"actual":[],"check":"dead boundary","expected":[],"passed":true},{"actual":["r1"],"check":"assign demanded","expected":["r1"],"passed":true},{"actual":["r1"],"check":"reborrow constructor","expected":["r1"],"passed":true},{"actual":["b","r1"],"check":"phi second origin","expected":["b","r1"],"passed":true},{"actual":[],"check":"trivial drop","expected":[],"passed":true},{"actual":["r1"],"check":"observing drop","expected":["r1"],"passed":true},{"actual":["a","r1"],"check":"branch union","expected":["a","r1"],"passed":true},{"actual":[0,1],"check":"variable arity","expected":[0,1],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"use\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"return\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"call\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"definition\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"dead boundary\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"assign demanded\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"reborrow constructor\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"phi second origin\", \"actual\": [\"b\", \"r1\"], \"expected\": [\"b\", \"r1\"], \"passed\": true}, {\"check\": \"trivial drop\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"observing drop\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"branch union\", \"actual\": [\"a\", \"r1\"], \"expected\": [\"a\", \"r1\"], \"passed\": true}, {\"check\": \"variable arity\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}