{"abstract":"Storage-dead boundary leaks demand into a previous local incarnation.","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=='storage_dead': live.add(a), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-reference-demand-storage-kill","id":"FA-43011","implementations":{"attempt":{"sha256":"b3d922b759de874dcf2d5f710818afbcd605b610440e276872dfffa1d1b9fc34","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.add(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":"04d8646abcd69d6bab1867460e2afef82ea01b1eaed5d54ce87c42e1a7ec6b96","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': pass\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-storage-kill","generated_at":"2026-09-29T14:43:57.457086+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=='storage_dead': live.discard(a).","root_cause":"The static analyzer mishandles storage kill: storage-dead boundary leaks demand into a previous local incarnation.","sha256":"30720de65b6fdebe2cfea3e804d1fc0d6286f7b4be16525469e54d91532a066c","title":"Storage-dead boundary leaks demand into a previous local incarnation · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":43.166,"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":["r1"],"check":"definition","expected":["r1"],"passed":true},{"actual":["a"],"check":"dead boundary","expected":[],"passed":false},{"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\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"dead boundary\", \"actual\": [\"a\"], \"expected\": [], \"passed\": false}, {\"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":43.19,"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":["r1"],"check":"definition","expected":["r1"],"passed":true},{"actual":["a"],"check":"dead boundary","expected":[],"passed":false},{"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\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"dead boundary\", \"actual\": [\"a\"], \"expected\": [], \"passed\": false}, {\"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.546,"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"}