{"abstract":"Branch liveness loses references demanded only on its second successor.","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=='branch': live.update(a), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-reference-demand-successor-union","id":"FA-43036","implementations":{"attempt":{"sha256":"cb33a101bec7017ed3ed7a475340f37429dd8cf66396a4f472aaaf55f19f15ed","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(a)\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":"7615684f92a04469ae20b24746b256b22641351baecdadf885bc32f4b2618bf9","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"},"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-successor-union","generated_at":"2026-09-29T14:43:57.725831+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=='branch': live.update(set(a)|set(b)).","root_cause":"The static analyzer mishandles successor union: branch liveness loses references demanded only on its second successor.","sha256":"9c2ea64141923d0e41bc62cb6cb396c7e18b49432515708e07cb20daedfba242","title":"Branch liveness loses references demanded only on its second successor · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.749,"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":[],"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"],"check":"branch union","expected":["a","r1"],"passed":false},{"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\": [], \"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\"], \"expected\": [\"a\", \"r1\"], \"passed\": false}, {\"check\": \"variable arity\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.809,"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":[],"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":[],"check":"branch union","expected":["a","r1"],"passed":false},{"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\": [], \"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\": [], \"expected\": [\"a\", \"r1\"], \"passed\": false}, {\"check\": \"variable arity\", \"actual\": [0, 1], \"expected\": [0, 1], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":40.335,"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"}