{"abstract":"Disconnected region declarations vanish from the constraint solution.","category":"Borrow checking","checks":11,"contract":"Solve finite outlives constraints a:b meaning a contains b. regions is universe, edges named constraints, equalities are bidirectional, demands maps region to points, universal maps region to required external points, forbidden maps region to points forbidden by storage scope. Compute least fixed point. Unknown edge endpoints produce error unknown; own seeds are retained; report sorted point sets and region names violating forbidden points. The static solution includes disconnected regions and propagates through cycles.","evaluation_group":"s3-borrow-checking-region-constraint-closure","failed_approach":"The partial repair uses names=set(a for a,b in edges)|set(b for a,b in edges), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-region-constraint-closure-universe","id":"FA-43041","implementations":{"attempt":{"sha256":"d6f2d8c8a62765bb9452b64363b3782b93ad81c48d6630668c69b78e773528bc","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, edges, equalities, demands, universal, forbidden):\n    names=set(a for a,b in edges)|set(b for a,b in edges)\n    if any(a not in names or b not in names for a,b in edges+equalities): return 'unknown'\n    links=list(edges)\n    for a,b in equalities: links.extend([(a,b),(b,a)])\n    points={r:set(demands.get(r,[])) for r in names}\n    for r in names: points[r].update(universal.get(r,[]))\n    changed=True\n    while changed:\n        changed=False\n        for a,b in links:\n            before=set(points[a])\n            points[a].update(points[b])\n            if points[a]!=before: changed=True\n    bad=sorted(r for r in names if points[r]&set(forbidden.get(r,[])))\n    return [dict((r,sorted(points[r])) for r in sorted(names)),bad]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('empty',solve([],[],[],{},{},{}),[{},[]])\ncheck('disconnected',solve(['a'],[],[],{},{},{}),[{'a':[]},[]])\ncheck('unknown edge',solve(['a'],[('a','z')],[],{},{},{}),'unknown')\ncheck('unknown equality',solve(['a'],[],[('a','z')],{},{},{}),'unknown')\ncheck('seed both',solve(['a'],[],[],{'a':[N,N+1]},{'a':[N+2]},{}),[{'a':[N,N+1,N+2]},[]])\ncheck('equality',solve(['a','b'],[],[('a','b')],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N,N+1]},[]])\ncheck('transitive reversed order',solve(['a','b','c'],[('a','b'),('b','c')],[],{'c':[N]},{},{}),[{'a':[N],'b':[N],'c':[N]},[]])\ncheck('one-way',solve(['a','b'],[('a','b')],[],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N+1]},[]])\ncheck('forbidden partial',solve(['a'],[],[],{'a':[N,N+1]},{},{'a':[N]}),[{'a':[N,N+1]},['a']])\ncheck('empty not forbidden',solve(['a'],[],[],{},{},{'a':[N]}),[{'a':[]},[]])\ncheck('cycle',solve(['a','b'],[('a','b'),('b','a')],[],{'a':[N]},{},{}),[{'a':[N],'b':[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":"512471000080608686526e851f766e615edd65f9a91b2ddd21c6bbb5661411ea","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, edges, equalities, demands, universal, forbidden):\n    names=set(a for a,b in edges)\n    if any(a not in names or b not in names for a,b in edges+equalities): return 'unknown'\n    links=list(edges)\n    for a,b in equalities: links.extend([(a,b),(b,a)])\n    points={r:set(demands.get(r,[])) for r in names}\n    for r in names: points[r].update(universal.get(r,[]))\n    changed=True\n    while changed:\n        changed=False\n        for a,b in links:\n            before=set(points[a])\n            points[a].update(points[b])\n            if points[a]!=before: changed=True\n    bad=sorted(r for r in names if points[r]&set(forbidden.get(r,[])))\n    return [dict((r,sorted(points[r])) for r in sorted(names)),bad]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('empty',solve([],[],[],{},{},{}),[{},[]])\ncheck('disconnected',solve(['a'],[],[],{},{},{}),[{'a':[]},[]])\ncheck('unknown edge',solve(['a'],[('a','z')],[],{},{},{}),'unknown')\ncheck('unknown equality',solve(['a'],[],[('a','z')],{},{},{}),'unknown')\ncheck('seed both',solve(['a'],[],[],{'a':[N,N+1]},{'a':[N+2]},{}),[{'a':[N,N+1,N+2]},[]])\ncheck('equality',solve(['a','b'],[],[('a','b')],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N,N+1]},[]])\ncheck('transitive reversed order',solve(['a','b','c'],[('a','b'),('b','c')],[],{'c':[N]},{},{}),[{'a':[N],'b':[N],'c':[N]},[]])\ncheck('one-way',solve(['a','b'],[('a','b')],[],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N+1]},[]])\ncheck('forbidden partial',solve(['a'],[],[],{'a':[N,N+1]},{},{'a':[N]}),[{'a':[N,N+1]},['a']])\ncheck('empty not forbidden',solve(['a'],[],[],{},{},{'a':[N]}),[{'a':[]},[]])\ncheck('cycle',solve(['a','b'],[('a','b'),('b','a')],[],{'a':[N]},{},{}),[{'a':[N],'b':[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":"1dbb57e6da8e9f3b108903ab31dd1b60550d3943df2a19ff59d724a4eb839507","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, edges, equalities, demands, universal, forbidden):\n    names=set(regions)\n    if any(a not in names or b not in names for a,b in edges+equalities): return 'unknown'\n    links=list(edges)\n    for a,b in equalities: links.extend([(a,b),(b,a)])\n    points={r:set(demands.get(r,[])) for r in names}\n    for r in names: points[r].update(universal.get(r,[]))\n    changed=True\n    while changed:\n        changed=False\n        for a,b in links:\n            before=set(points[a])\n            points[a].update(points[b])\n            if points[a]!=before: changed=True\n    bad=sorted(r for r in names if points[r]&set(forbidden.get(r,[])))\n    return [dict((r,sorted(points[r])) for r in sorted(names)),bad]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('empty',solve([],[],[],{},{},{}),[{},[]])\ncheck('disconnected',solve(['a'],[],[],{},{},{}),[{'a':[]},[]])\ncheck('unknown edge',solve(['a'],[('a','z')],[],{},{},{}),'unknown')\ncheck('unknown equality',solve(['a'],[],[('a','z')],{},{},{}),'unknown')\ncheck('seed both',solve(['a'],[],[],{'a':[N,N+1]},{'a':[N+2]},{}),[{'a':[N,N+1,N+2]},[]])\ncheck('equality',solve(['a','b'],[],[('a','b')],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N,N+1]},[]])\ncheck('transitive reversed order',solve(['a','b','c'],[('a','b'),('b','c')],[],{'c':[N]},{},{}),[{'a':[N],'b':[N],'c':[N]},[]])\ncheck('one-way',solve(['a','b'],[('a','b')],[],{'a':[N],'b':[N+1]},{},{}),[{'a':[N,N+1],'b':[N+1]},[]])\ncheck('forbidden partial',solve(['a'],[],[],{'a':[N,N+1]},{},{'a':[N]}),[{'a':[N,N+1]},['a']])\ncheck('empty not forbidden',solve(['a'],[],[],{},{},{'a':[N]}),[{'a':[]},[]])\ncheck('cycle',solve(['a','b'],[('a','b'),('b','a')],[],{'a':[N]},{},{}),[{'a':[N],'b':[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-region-constraint-closure-universe","generated_at":"2026-09-29T14:43:57.893463+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: names=set(regions).","root_cause":"The static analyzer mishandles universe: disconnected region declarations vanish from the constraint solution.","sha256":"75b571ac909e133f6b35ec1df786caad9c720d6fe95f175ba06f02471c6a8588","title":"Disconnected region declarations vanish from the constraint solution · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":44.811,"exit_code":1,"observations":[{"actual":[{},[]],"check":"empty","expected":[{},[]],"passed":true},{"actual":[{},[]],"check":"disconnected","expected":[{"a":[]},[]],"passed":false},{"actual":[{"a":[],"z":[]},[]],"check":"unknown edge","expected":"unknown","passed":false},{"actual":"unknown","check":"unknown equality","expected":"unknown","passed":true},{"actual":[{},[]],"check":"seed both","expected":[{"a":[1,2,3]},[]],"passed":false},{"actual":"unknown","check":"equality","expected":[{"a":[1,2],"b":[1,2]},[]],"passed":false},{"actual":[{"a":[1],"b":[1],"c":[1]},[]],"check":"transitive reversed order","expected":[{"a":[1],"b":[1],"c":[1]},[]],"passed":true},{"actual":[{"a":[1,2],"b":[2]},[]],"check":"one-way","expected":[{"a":[1,2],"b":[2]},[]],"passed":true},{"actual":[{},[]],"check":"forbidden partial","expected":[{"a":[1,2]},["a"]],"passed":false},{"actual":[{},[]],"check":"empty not forbidden","expected":[{"a":[]},[]],"passed":false},{"actual":[{"a":[1],"b":[1]},[]],"check":"cycle","expected":[{"a":[1],"b":[1]},[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [{}, []], \"expected\": [{}, []], \"passed\": true}, {\"check\": \"disconnected\", \"actual\": [{}, []], \"expected\": [{\"a\": []}, []], \"passed\": false}, {\"check\": \"unknown edge\", \"actual\": [{\"a\": [], \"z\": []}, []], \"expected\": \"unknown\", \"passed\": false}, {\"check\": \"unknown equality\", \"actual\": \"unknown\", \"expected\": \"unknown\", \"passed\": true}, {\"check\": \"seed both\", \"actual\": [{}, []], \"expected\": [{\"a\": [1, 2, 3]}, []], \"passed\": false}, {\"check\": \"equality\", \"actual\": \"unknown\", \"expected\": [{\"a\": [1, 2], \"b\": [1, 2]}, []], \"passed\": false}, {\"check\": \"transitive reversed order\", \"actual\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"passed\": true}, {\"check\": \"one-way\", \"actual\": [{\"a\": [1, 2], \"b\": [2]}, []], \"expected\": [{\"a\": [1, 2], \"b\": [2]}, []], \"passed\": true}, {\"check\": \"forbidden partial\", \"actual\": [{}, []], \"expected\": [{\"a\": [1, 2]}, [\"a\"]], \"passed\": false}, {\"check\": \"empty not forbidden\", \"actual\": [{}, []], \"expected\": [{\"a\": []}, []], \"passed\": false}, {\"check\": \"cycle\", \"actual\": [{\"a\": [1], \"b\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1]}, []], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":39.653,"exit_code":1,"observations":[{"actual":[{},[]],"check":"empty","expected":[{},[]],"passed":true},{"actual":[{},[]],"check":"disconnected","expected":[{"a":[]},[]],"passed":false},{"actual":"unknown","check":"unknown edge","expected":"unknown","passed":true},{"actual":"unknown","check":"unknown equality","expected":"unknown","passed":true},{"actual":[{},[]],"check":"seed both","expected":[{"a":[1,2,3]},[]],"passed":false},{"actual":"unknown","check":"equality","expected":[{"a":[1,2],"b":[1,2]},[]],"passed":false},{"actual":"unknown","check":"transitive reversed order","expected":[{"a":[1],"b":[1],"c":[1]},[]],"passed":false},{"actual":"unknown","check":"one-way","expected":[{"a":[1,2],"b":[2]},[]],"passed":false},{"actual":[{},[]],"check":"forbidden partial","expected":[{"a":[1,2]},["a"]],"passed":false},{"actual":[{},[]],"check":"empty not forbidden","expected":[{"a":[]},[]],"passed":false},{"actual":[{"a":[1],"b":[1]},[]],"check":"cycle","expected":[{"a":[1],"b":[1]},[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [{}, []], \"expected\": [{}, []], \"passed\": true}, {\"check\": \"disconnected\", \"actual\": [{}, []], \"expected\": [{\"a\": []}, []], \"passed\": false}, {\"check\": \"unknown edge\", \"actual\": \"unknown\", \"expected\": \"unknown\", \"passed\": true}, {\"check\": \"unknown equality\", \"actual\": \"unknown\", \"expected\": \"unknown\", \"passed\": true}, {\"check\": \"seed both\", \"actual\": [{}, []], \"expected\": [{\"a\": [1, 2, 3]}, []], \"passed\": false}, {\"check\": \"equality\", \"actual\": \"unknown\", \"expected\": [{\"a\": [1, 2], \"b\": [1, 2]}, []], \"passed\": false}, {\"check\": \"transitive reversed order\", \"actual\": \"unknown\", \"expected\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"passed\": false}, {\"check\": \"one-way\", \"actual\": \"unknown\", \"expected\": [{\"a\": [1, 2], \"b\": [2]}, []], \"passed\": false}, {\"check\": \"forbidden partial\", \"actual\": [{}, []], \"expected\": [{\"a\": [1, 2]}, [\"a\"]], \"passed\": false}, {\"check\": \"empty not forbidden\", \"actual\": [{}, []], \"expected\": [{\"a\": []}, []], \"passed\": false}, {\"check\": \"cycle\", \"actual\": [{\"a\": [1], \"b\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1]}, []], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":42.197,"exit_code":0,"observations":[{"actual":[{},[]],"check":"empty","expected":[{},[]],"passed":true},{"actual":[{"a":[]},[]],"check":"disconnected","expected":[{"a":[]},[]],"passed":true},{"actual":"unknown","check":"unknown edge","expected":"unknown","passed":true},{"actual":"unknown","check":"unknown equality","expected":"unknown","passed":true},{"actual":[{"a":[1,2,3]},[]],"check":"seed both","expected":[{"a":[1,2,3]},[]],"passed":true},{"actual":[{"a":[1,2],"b":[1,2]},[]],"check":"equality","expected":[{"a":[1,2],"b":[1,2]},[]],"passed":true},{"actual":[{"a":[1],"b":[1],"c":[1]},[]],"check":"transitive reversed order","expected":[{"a":[1],"b":[1],"c":[1]},[]],"passed":true},{"actual":[{"a":[1,2],"b":[2]},[]],"check":"one-way","expected":[{"a":[1,2],"b":[2]},[]],"passed":true},{"actual":[{"a":[1,2]},["a"]],"check":"forbidden partial","expected":[{"a":[1,2]},["a"]],"passed":true},{"actual":[{"a":[]},[]],"check":"empty not forbidden","expected":[{"a":[]},[]],"passed":true},{"actual":[{"a":[1],"b":[1]},[]],"check":"cycle","expected":[{"a":[1],"b":[1]},[]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [{}, []], \"expected\": [{}, []], \"passed\": true}, {\"check\": \"disconnected\", \"actual\": [{\"a\": []}, []], \"expected\": [{\"a\": []}, []], \"passed\": true}, {\"check\": \"unknown edge\", \"actual\": \"unknown\", \"expected\": \"unknown\", \"passed\": true}, {\"check\": \"unknown equality\", \"actual\": \"unknown\", \"expected\": \"unknown\", \"passed\": true}, {\"check\": \"seed both\", \"actual\": [{\"a\": [1, 2, 3]}, []], \"expected\": [{\"a\": [1, 2, 3]}, []], \"passed\": true}, {\"check\": \"equality\", \"actual\": [{\"a\": [1, 2], \"b\": [1, 2]}, []], \"expected\": [{\"a\": [1, 2], \"b\": [1, 2]}, []], \"passed\": true}, {\"check\": \"transitive reversed order\", \"actual\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"passed\": true}, {\"check\": \"one-way\", \"actual\": [{\"a\": [1, 2], \"b\": [2]}, []], \"expected\": [{\"a\": [1, 2], \"b\": [2]}, []], \"passed\": true}, {\"check\": \"forbidden partial\", \"actual\": [{\"a\": [1, 2]}, [\"a\"]], \"expected\": [{\"a\": [1, 2]}, [\"a\"]], \"passed\": true}, {\"check\": \"empty not forbidden\", \"actual\": [{\"a\": []}, []], \"expected\": [{\"a\": []}, []], \"passed\": true}, {\"check\": \"cycle\", \"actual\": [{\"a\": [1], \"b\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1]}, []], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}