{"abstract":"Unsatisfied lifetime obligations report extra availability as missing.","category":"Borrow checking","checks":17,"contract":"Finite lexical regions map names to sets of program-point integers. Longer region contains every point of shorter. Queries: outlives(a,b), meet(a,b), join(a,b), missing(a,b), strict(a,b), eq(a,b), disjoint(a,b), covers(a, list-of-regions), gap(a,b,c) requires a cover intersection of b,c, and choose(a,candidates) returns lexically sorted candidate regions containing a with smallest cardinality, ties lexical. Return booleans or sorted lists as appropriate.","contract_signature":"regions, op, a, b, c=None","evaluation_group":"s3-borrow-checking-region-relations","failed_approach":"The partial repair uses if op=='missing': return sorted(x ^ set(regions[b])), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-region-relations-missing-direction","id":"FA-42906","implementations":{"attempt":{"sha256":"6498055e75bc41c01742acb4bb1c371a5a9f304b1942b41cbe1a563c78bc88f0","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, op, a, b, c=None):\n    x=set(regions[a])\n    if op=='outlives': return x.issuperset(regions[b])\n    if op=='meet': return sorted(x.intersection(regions[b]))\n    if op=='join': return sorted(x.union(regions[b]))\n    if op=='missing': return sorted(x ^ set(regions[b]))\n    if op=='strict': return x>set(regions[b])\n    if op=='eq': return x==set(regions[b])\n    if op=='disjoint': return x.isdisjoint(regions[b])\n    if op=='covers': return all(x.issuperset(regions[k]) for k in b)\n    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)\n    if op=='choose':\n        candidates=[k for k in b if set(regions[k]).issuperset(x)]\n        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None\n    return None\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nr={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}\ncheck('outlives',solve(r,'outlives','a','s'),True)\ncheck('incomparable',solve(r,'outlives','a','b'),False)\ncheck('meet',solve(r,'meet','a','b'),[N+1])\ncheck('join',solve(r,'join','a','b'),[N,N+1,N+2])\ncheck('missing',solve(r,'missing','a','b'),[N+2])\ncheck('strict equal',solve(r,'strict','a','a'),False)\ncheck('strict incomparable',solve(r,'strict','aa','b'),True)\ncheck('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)\ncheck('equivalent unordered',solve(r,'eq','a','z'),True)\ncheck('equivalent distinct',solve(r,'eq','a','b'),False)\ncheck('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)\ncheck('overlap disjoint',solve(r,'disjoint','a','b'),False)\ncheck('mixed obligations',solve(r,'covers','a',['s','b']),False)\ncheck('no obligations',solve(r,'covers','a',[]),True)\ncheck('joint demand',solve(r,'gap','e','a','b'),[N+1])\ncheck('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')\ncheck('no candidate',solve(r,'choose','aa',['a','s']),None)\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":"ecd66483498cdf67ba862db9ab4adf8e8a7c534aca22ebefb5c5c09b919b933b","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(regions, op, a, b, c=None):\n    x=set(regions[a])\n    if op=='outlives': return x.issuperset(regions[b])\n    if op=='meet': return sorted(x.intersection(regions[b]))\n    if op=='join': return sorted(x.union(regions[b]))\n    if op=='missing': return sorted(x-set(regions[b]))\n    if op=='strict': return x>set(regions[b])\n    if op=='eq': return x==set(regions[b])\n    if op=='disjoint': return x.isdisjoint(regions[b])\n    if op=='covers': return all(x.issuperset(regions[k]) for k in b)\n    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)\n    if op=='choose':\n        candidates=[k for k in b if set(regions[k]).issuperset(x)]\n        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None\n    return None\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nr={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}\ncheck('outlives',solve(r,'outlives','a','s'),True)\ncheck('incomparable',solve(r,'outlives','a','b'),False)\ncheck('meet',solve(r,'meet','a','b'),[N+1])\ncheck('join',solve(r,'join','a','b'),[N,N+1,N+2])\ncheck('missing',solve(r,'missing','a','b'),[N+2])\ncheck('strict equal',solve(r,'strict','a','a'),False)\ncheck('strict incomparable',solve(r,'strict','aa','b'),True)\ncheck('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)\ncheck('equivalent unordered',solve(r,'eq','a','z'),True)\ncheck('equivalent distinct',solve(r,'eq','a','b'),False)\ncheck('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)\ncheck('overlap disjoint',solve(r,'disjoint','a','b'),False)\ncheck('mixed obligations',solve(r,'covers','a',['s','b']),False)\ncheck('no obligations',solve(r,'covers','a',[]),True)\ncheck('joint demand',solve(r,'gap','e','a','b'),[N+1])\ncheck('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')\ncheck('no candidate',solve(r,'choose','aa',['a','s']),None)\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-relations-missing-direction","generated_at":"2026-09-29T14:43:56.632501+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 missing direction: unsatisfied lifetime obligations report extra availability as missing.","sha256":"eaba43ae3f57cde593a990fecfe77639ff2a9b8d9453c05bff3a21aea719fd47","title":"Unsatisfied lifetime obligations report extra availability as missing · 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":42.378,"exit_code":1,"observations":[{"actual":true,"check":"outlives","expected":true,"passed":true},{"actual":false,"check":"incomparable","expected":false,"passed":true},{"actual":[2],"check":"meet","expected":[2],"passed":true},{"actual":[1,2,3],"check":"join","expected":[1,2,3],"passed":true},{"actual":[1,3],"check":"missing","expected":[3],"passed":false},{"actual":false,"check":"strict equal","expected":false,"passed":true},{"actual":true,"check":"strict incomparable","expected":true,"passed":true},{"actual":false,"check":"strict size insufficient","expected":false,"passed":true},{"actual":true,"check":"equivalent unordered","expected":true,"passed":true},{"actual":false,"check":"equivalent distinct","expected":false,"passed":true},{"actual":true,"check":"nonempty disjoint","expected":true,"passed":true},{"actual":false,"check":"overlap disjoint","expected":false,"passed":true},{"actual":false,"check":"mixed obligations","expected":false,"passed":true},{"actual":true,"check":"no obligations","expected":true,"passed":true},{"actual":[2],"check":"joint demand","expected":[2],"passed":true},{"actual":"s","check":"choose shortest","expected":"s","passed":true},{"actual":null,"check":"no candidate","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"outlives\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"incomparable\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"meet\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"join\", \"actual\": [1, 2, 3], \"expected\": [1, 2, 3], \"passed\": true}, {\"check\": \"missing\", \"actual\": [1, 3], \"expected\": [3], \"passed\": false}, {\"check\": \"strict equal\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"strict incomparable\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"strict size insufficient\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"equivalent unordered\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"equivalent distinct\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"nonempty disjoint\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"overlap disjoint\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"mixed obligations\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"no obligations\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"joint demand\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"choose shortest\", \"actual\": \"s\", \"expected\": \"s\", \"passed\": true}, {\"check\": \"no candidate\", \"actual\": null, \"expected\": null, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":40.039,"exit_code":1,"observations":[{"actual":true,"check":"outlives","expected":true,"passed":true},{"actual":false,"check":"incomparable","expected":false,"passed":true},{"actual":[2],"check":"meet","expected":[2],"passed":true},{"actual":[1,2,3],"check":"join","expected":[1,2,3],"passed":true},{"actual":[1],"check":"missing","expected":[3],"passed":false},{"actual":false,"check":"strict equal","expected":false,"passed":true},{"actual":true,"check":"strict incomparable","expected":true,"passed":true},{"actual":false,"check":"strict size insufficient","expected":false,"passed":true},{"actual":true,"check":"equivalent unordered","expected":true,"passed":true},{"actual":false,"check":"equivalent distinct","expected":false,"passed":true},{"actual":true,"check":"nonempty disjoint","expected":true,"passed":true},{"actual":false,"check":"overlap disjoint","expected":false,"passed":true},{"actual":false,"check":"mixed obligations","expected":false,"passed":true},{"actual":true,"check":"no obligations","expected":true,"passed":true},{"actual":[2],"check":"joint demand","expected":[2],"passed":true},{"actual":"s","check":"choose shortest","expected":"s","passed":true},{"actual":null,"check":"no candidate","expected":null,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"outlives\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"incomparable\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"meet\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"join\", \"actual\": [1, 2, 3], \"expected\": [1, 2, 3], \"passed\": true}, {\"check\": \"missing\", \"actual\": [1], \"expected\": [3], \"passed\": false}, {\"check\": \"strict equal\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"strict incomparable\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"strict size insufficient\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"equivalent unordered\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"equivalent distinct\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"nonempty disjoint\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"overlap disjoint\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"mixed obligations\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"no obligations\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"joint demand\", \"actual\": [2], \"expected\": [2], \"passed\": true}, {\"check\": \"choose shortest\", \"actual\": \"s\", \"expected\": \"s\", \"passed\": true}, {\"check\": \"no candidate\", \"actual\": null, \"expected\": null, \"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."}}