{"abstract":"Transitive lifetime constraints stop after a single ordered pass.","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.","contract_signature":"regions, edges, equalities, demands, universal, forbidden","evaluation_group":"s3-borrow-checking-region-constraint-closure","failed_approach":"The partial repair uses if points[a]!=before and len(links)<2: changed=True, which still violates the stipulated analysis contract.","family":"s3-borrow-checking-region-constraint-closure-iterate-to-fixed","id":"FA-43076","implementations":{"attempt":{"sha256":"6b575a0dabbcfe0c47eb860e82cf78d9fece44efd1fd9dcb68c0c9ba63304250","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 and len(links)<2: 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":"f9af5f8d88026c5862f260a4582b050f3feb622d9eda1eff71822b69ac897e17","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 False: 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-iterate-to-fixed","generated_at":"2026-09-29T14:43:58.180376+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 iterate to fixed: transitive lifetime constraints stop after a single ordered pass.","sha256":"d94aa31167bb9e062144b303465f410d2e8e71c70d5391144878c60f077290fa","title":"Transitive lifetime constraints stop after a single ordered pass · 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":47.592,"exit_code":1,"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":[],"b":[1],"c":[1]},[]],"check":"transitive reversed order","expected":[{"a":[1],"b":[1],"c":[1]},[]],"passed":false},{"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\": \"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\": [], \"b\": [1], \"c\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"passed\": false}, {\"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":43.908,"exit_code":1,"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":[],"b":[1],"c":[1]},[]],"check":"transitive reversed order","expected":[{"a":[1],"b":[1],"c":[1]},[]],"passed":false},{"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\": \"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\": [], \"b\": [1], \"c\": [1]}, []], \"expected\": [{\"a\": [1], \"b\": [1], \"c\": [1]}, []], \"passed\": false}, {\"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"}},"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."}}