{"abstract":"A missing endpoint in an equality is not diagnosed.","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 if any(a not in names or b not in names for a,b in edges+equalities): return None, which still violates the stipulated analysis contract.","family":"s3-borrow-checking-region-constraint-closure-endpoint-validation","id":"FA-43046","implementations":{"attempt":{"sha256":"f86f684b915ec60f47308250abe463b537e9cce687e5fdbe93ffcb0bf8691f58","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 None\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":"aa36c7e324cb9144b6712dafb0672c8c0ad1bfff856ea7eca892c07b428e705a","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 [{},[]]\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-endpoint-validation","generated_at":"2026-09-29T14:43:57.899732+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: if any(a not in names or b not in names for a,b in edges+equalities): return 'unknown'.","root_cause":"The static analyzer mishandles endpoint validation: a missing endpoint in an equality is not diagnosed.","sha256":"c536db551000db1fb5040ddc64450815cfa774e20ade3c67a6e04deda3f0d8bc","title":"A missing endpoint in an equality is not diagnosed · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":41.224,"exit_code":1,"observations":[{"actual":[{},[]],"check":"empty","expected":[{},[]],"passed":true},{"actual":[{"a":[]},[]],"check":"disconnected","expected":[{"a":[]},[]],"passed":true},{"actual":null,"check":"unknown edge","expected":"unknown","passed":false},{"actual":null,"check":"unknown equality","expected":"unknown","passed":false},{"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":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [{}, []], \"expected\": [{}, []], \"passed\": true}, {\"check\": \"disconnected\", \"actual\": [{\"a\": []}, []], \"expected\": [{\"a\": []}, []], \"passed\": true}, {\"check\": \"unknown edge\", \"actual\": null, \"expected\": \"unknown\", \"passed\": false}, {\"check\": \"unknown equality\", \"actual\": null, \"expected\": \"unknown\", \"passed\": false}, {\"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\": false}\n"},"broken":{"elapsed_ms":40.422,"exit_code":1,"observations":[{"actual":[{},[]],"check":"empty","expected":[{},[]],"passed":true},{"actual":[{"a":[]},[]],"check":"disconnected","expected":[{"a":[]},[]],"passed":true},{"actual":[{},[]],"check":"unknown edge","expected":"unknown","passed":false},{"actual":[{},[]],"check":"unknown equality","expected":"unknown","passed":false},{"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":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"empty\", \"actual\": [{}, []], \"expected\": [{}, []], \"passed\": true}, {\"check\": \"disconnected\", \"actual\": [{\"a\": []}, []], \"expected\": [{\"a\": []}, []], \"passed\": true}, {\"check\": \"unknown edge\", \"actual\": [{}, []], \"expected\": \"unknown\", \"passed\": false}, {\"check\": \"unknown equality\", \"actual\": [{}, []], \"expected\": \"unknown\", \"passed\": false}, {\"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\": false}\n"},"fixed":{"elapsed_ms":42.112,"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"}