{"abstract":"Reading a reference fails to extend its inferred loan lifetime.","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.","contract_signature":"ops","evaluation_group":"s3-borrow-checking-reference-demand","failed_approach":"The partial repair uses if op=='use': live.discard(a), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-reference-demand-use-gen","id":"FA-42991","implementations":{"attempt":{"sha256":"6dfa35262b2e7b1c06b09059465607f583d657929eddb4f7b7d9b9063b931696","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.discard(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"},"broken":{"sha256":"7a67a5df9b32db24ac24a480c433bb700b279913a9c93499d8a8510c8065755d","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': pass\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-use-gen","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.","root_cause":"The static analyzer mishandles use gen: reading a reference fails to extend its inferred loan lifetime.","sha256":"216a414b77924252130a7393273c338d3bb7f6f6db526362776352f799228a53","title":"Reading a reference fails to extend its inferred loan lifetime · 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":39.779,"exit_code":1,"observations":[{"actual":[],"check":"empty","expected":[],"passed":true},{"actual":[],"check":"use","expected":["r1"],"passed":false},{"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":[],"check":"assign demanded","expected":["r1"],"passed":false},{"actual":["r1"],"check":"reborrow constructor","expected":["r1"],"passed":true},{"actual":[],"check":"phi second origin","expected":["b","r1"],"passed":false},{"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\": [], \"expected\": [\"r1\"], \"passed\": false}, {\"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\": [], \"expected\": [\"r1\"], \"passed\": false}, {\"check\": \"reborrow constructor\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"phi second origin\", \"actual\": [], \"expected\": [\"b\", \"r1\"], \"passed\": false}, {\"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.943,"exit_code":1,"observations":[{"actual":[],"check":"empty","expected":[],"passed":true},{"actual":[],"check":"use","expected":["r1"],"passed":false},{"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":[],"check":"assign demanded","expected":["r1"],"passed":false},{"actual":["r1"],"check":"reborrow constructor","expected":["r1"],"passed":true},{"actual":[],"check":"phi second origin","expected":["b","r1"],"passed":false},{"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\": [], \"expected\": [\"r1\"], \"passed\": false}, {\"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\": [], \"expected\": [\"r1\"], \"passed\": false}, {\"check\": \"reborrow constructor\", \"actual\": [\"r1\"], \"expected\": [\"r1\"], \"passed\": true}, {\"check\": \"phi second origin\", \"actual\": [], \"expected\": [\"b\", \"r1\"], \"passed\": false}, {\"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"}},"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."}}