{"abstract":"A symbolic right index is omitted from alias symmetry.","category":"Borrow checking","checks":13,"contract":"Places are lists of projections: root name, then fields or integer indices. Different roots and unequal fields or known indices are disjoint. A wildcard index ? aliases any index. A union projection | overlaps any sibling. Dereference * conservatively overlaps another projection at that depth. Prefix places overlap; empty denotes no place. Return overlap.","contract_signature":"a, b","evaluation_group":"s3-borrow-checking-place-conflict","failed_approach":"The partial repair uses if y == '?' and x == 0: continue, which still violates the stipulated analysis contract.","family":"s3-borrow-checking-place-conflict-right-dynamic-index","id":"FA-42871","implementations":{"attempt":{"sha256":"23d1d3947db0ff86ec7f939ef92f923869ac0539369325b9dff1ca9214029f4d","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(a, b):\n    if not a or not b: return False\n    if a[0] != b[0]: return False\n    for x, y in zip(a[1:], b[1:]):\n        if x == y: continue\n        if x == '|' or y == '|': return True\n        if x == '*' or y == '*': return True\n        if x == '?' and isinstance(y, int): continue\n        if y == '?' and x == 0: continue\n        if isinstance(x, int) and isinstance(y, int): return False\n        if isinstance(x, str) and isinstance(y, str): return False\n        return False\n    return True\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('absent',solve([],['r']),False)\ncheck('both absent',solve([],[]),False)\ncheck('roots depths',solve(['r'],['s','a']),False)\ncheck('shared prefix',solve(['r','a','b'],['r','a','c']),False)\ncheck('union',solve(['r','|'],['r','a']),True)\ncheck('deref',solve(['r','*'],['r','a']),True)\ncheck('dynamic left',solve(['r','?'],['r',N]),True)\ncheck('dynamic right',solve(['r',N],['r','?']),True)\ncheck('separated indices',solve(['r',N],['r',N+3]),False)\ncheck('adjacent indices',solve(['r',N],['r',N+1]),False)\ncheck('fields',solve(['r','a'],['r','b']),False)\ncheck('parent',solve(['r'],['r','a']),True)\ncheck('same',solve(['r',N],['r',N]),True)\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":"69521410c435c4e34fe40211d142483770dd266ed97c4ab04ba7d9985d81206e","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(a, b):\n    if not a or not b: return False\n    if a[0] != b[0]: return False\n    for x, y in zip(a[1:], b[1:]):\n        if x == y: continue\n        if x == '|' or y == '|': return True\n        if x == '*' or y == '*': return True\n        if x == '?' and isinstance(y, int): continue\n        if False: continue\n        if isinstance(x, int) and isinstance(y, int): return False\n        if isinstance(x, str) and isinstance(y, str): return False\n        return False\n    return True\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('absent',solve([],['r']),False)\ncheck('both absent',solve([],[]),False)\ncheck('roots depths',solve(['r'],['s','a']),False)\ncheck('shared prefix',solve(['r','a','b'],['r','a','c']),False)\ncheck('union',solve(['r','|'],['r','a']),True)\ncheck('deref',solve(['r','*'],['r','a']),True)\ncheck('dynamic left',solve(['r','?'],['r',N]),True)\ncheck('dynamic right',solve(['r',N],['r','?']),True)\ncheck('separated indices',solve(['r',N],['r',N+3]),False)\ncheck('adjacent indices',solve(['r',N],['r',N+1]),False)\ncheck('fields',solve(['r','a'],['r','b']),False)\ncheck('parent',solve(['r'],['r','a']),True)\ncheck('same',solve(['r',N],['r',N]),True)\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-place-conflict-right-dynamic-index","generated_at":"2026-09-29T14:43:56.304675+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 right dynamic index: a symbolic right index is omitted from alias symmetry.","sha256":"c1bacafcf03e7fc1b60eb3087576d420fc4ef71cbc95badfaf238578c7523993","title":"A symbolic right index is omitted from alias symmetry · 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":51.201,"exit_code":1,"observations":[{"actual":false,"check":"absent","expected":false,"passed":true},{"actual":false,"check":"both absent","expected":false,"passed":true},{"actual":false,"check":"roots depths","expected":false,"passed":true},{"actual":false,"check":"shared prefix","expected":false,"passed":true},{"actual":true,"check":"union","expected":true,"passed":true},{"actual":true,"check":"deref","expected":true,"passed":true},{"actual":true,"check":"dynamic left","expected":true,"passed":true},{"actual":false,"check":"dynamic right","expected":true,"passed":false},{"actual":false,"check":"separated indices","expected":false,"passed":true},{"actual":false,"check":"adjacent indices","expected":false,"passed":true},{"actual":false,"check":"fields","expected":false,"passed":true},{"actual":true,"check":"parent","expected":true,"passed":true},{"actual":true,"check":"same","expected":true,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"absent\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"both absent\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"roots depths\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"shared prefix\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"union\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"deref\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"dynamic left\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"dynamic right\", \"actual\": false, \"expected\": true, \"passed\": false}, {\"check\": \"separated indices\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"adjacent indices\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"fields\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"parent\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"same\", \"actual\": true, \"expected\": true, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":44.732,"exit_code":1,"observations":[{"actual":false,"check":"absent","expected":false,"passed":true},{"actual":false,"check":"both absent","expected":false,"passed":true},{"actual":false,"check":"roots depths","expected":false,"passed":true},{"actual":false,"check":"shared prefix","expected":false,"passed":true},{"actual":true,"check":"union","expected":true,"passed":true},{"actual":true,"check":"deref","expected":true,"passed":true},{"actual":true,"check":"dynamic left","expected":true,"passed":true},{"actual":false,"check":"dynamic right","expected":true,"passed":false},{"actual":false,"check":"separated indices","expected":false,"passed":true},{"actual":false,"check":"adjacent indices","expected":false,"passed":true},{"actual":false,"check":"fields","expected":false,"passed":true},{"actual":true,"check":"parent","expected":true,"passed":true},{"actual":true,"check":"same","expected":true,"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"absent\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"both absent\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"roots depths\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"shared prefix\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"union\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"deref\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"dynamic left\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"dynamic right\", \"actual\": false, \"expected\": true, \"passed\": false}, {\"check\": \"separated indices\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"adjacent indices\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"fields\", \"actual\": false, \"expected\": false, \"passed\": true}, {\"check\": \"parent\", \"actual\": true, \"expected\": true, \"passed\": true}, {\"check\": \"same\", \"actual\": true, \"expected\": true, \"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."}}