FA-42886 / Borrow checking / Open access

A whole aggregate loses its conflict with a borrowed subplace · case 01

A whole aggregate loses its conflict with a borrowed subplace.

Verified by executionVariant 1 · 13 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The static analyzer mishandles prefix conflict: a whole aggregate loses its conflict with a borrowed subplace.

VERIFIED REPAIR

Apply the specified transfer or inference rule at this site: return True.

Unsuccessful approach: The partial repair uses return len(a)==len(b), which still violates the stipulated analysis contract.

Case 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.

Why this case matters

A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    if not a or not b: return False
    if a[0] != b[0]: return False
    for x, y in zip(a[1:], b[1:]):
        if x == y: continue
        if x == '|' or y == '|': return True
        if x == '*' or y == '*': return True
        if x == '?' and isinstance(y, int): continue
        if y == '?' and isinstance(x, int): continue
        if isinstance(x, int) and isinstance(y, int): return False
        if isinstance(x, str) and isinstance(y, str): return False
        return False
    return False
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('absent',solve([],['r']),False)
check('both absent',solve([],[]),False)
check('roots depths',solve(['r'],['s','a']),False)
check('shared prefix',solve(['r','a','b'],['r','a','c']),False)
check('union',solve(['r','|'],['r','a']),True)
check('deref',solve(['r','*'],['r','a']),True)
check('dynamic left',solve(['r','?'],['r',N]),True)
check('dynamic right',solve(['r',N],['r','?']),True)
check('separated indices',solve(['r',N],['r',N+3]),False)
check('adjacent indices',solve(['r',N],['r',N+1]),False)
check('fields',solve(['r','a'],['r','b']),False)
check('parent',solve(['r'],['r','a']),True)
check('same',solve(['r',N],['r',N]),True)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
absent	`False`	`False`	Passed
both absent	`False`	`False`	Passed
roots depths	`False`	`False`	Passed
shared prefix	`False`	`False`	Passed
union	`True`	`True`	Passed
deref	`True`	`True`	Passed
dynamic left	`False`	`True`	Failed
dynamic right	`False`	`True`	Failed
separated indices	`False`	`False`	Passed
adjacent indices	`False`	`False`	Passed
fields	`False`	`False`	Passed
parent	`False`	`True`	Failed
same	`False`	`True`	Failed

SHA-256 / 50fc33edbd65d04bcd93ac1a25aeee981d2819a1e431a79eeb0ee59f6fbe0943

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    if not a or not b: return False
    if a[0] != b[0]: return False
    for x, y in zip(a[1:], b[1:]):
        if x == y: continue
        if x == '|' or y == '|': return True
        if x == '*' or y == '*': return True
        if x == '?' and isinstance(y, int): continue
        if y == '?' and isinstance(x, int): continue
        if isinstance(x, int) and isinstance(y, int): return False
        if isinstance(x, str) and isinstance(y, str): return False
        return False
    return len(a)==len(b)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('absent',solve([],['r']),False)
check('both absent',solve([],[]),False)
check('roots depths',solve(['r'],['s','a']),False)
check('shared prefix',solve(['r','a','b'],['r','a','c']),False)
check('union',solve(['r','|'],['r','a']),True)
check('deref',solve(['r','*'],['r','a']),True)
check('dynamic left',solve(['r','?'],['r',N]),True)
check('dynamic right',solve(['r',N],['r','?']),True)
check('separated indices',solve(['r',N],['r',N+3]),False)
check('adjacent indices',solve(['r',N],['r',N+1]),False)
check('fields',solve(['r','a'],['r','b']),False)
check('parent',solve(['r'],['r','a']),True)
check('same',solve(['r',N],['r',N]),True)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
absent	`False`	`False`	Passed
both absent	`False`	`False`	Passed
roots depths	`False`	`False`	Passed
shared prefix	`False`	`False`	Passed
union	`True`	`True`	Passed
deref	`True`	`True`	Passed
dynamic left	`True`	`True`	Passed
dynamic right	`True`	`True`	Passed
separated indices	`False`	`False`	Passed
adjacent indices	`False`	`False`	Passed
fields	`False`	`False`	Passed
parent	`False`	`True`	Failed
same	`True`	`True`	Passed

SHA-256 / b9c16b0ea9aa390090eb7e86d633394c25a063476267d1de6c47ea7194505cc0

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(a, b):
    if not a or not b: return False
    if a[0] != b[0]: return False
    for x, y in zip(a[1:], b[1:]):
        if x == y: continue
        if x == '|' or y == '|': return True
        if x == '*' or y == '*': return True
        if x == '?' and isinstance(y, int): continue
        if y == '?' and isinstance(x, int): continue
        if isinstance(x, int) and isinstance(y, int): return False
        if isinstance(x, str) and isinstance(y, str): return False
        return False
    return True
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('absent',solve([],['r']),False)
check('both absent',solve([],[]),False)
check('roots depths',solve(['r'],['s','a']),False)
check('shared prefix',solve(['r','a','b'],['r','a','c']),False)
check('union',solve(['r','|'],['r','a']),True)
check('deref',solve(['r','*'],['r','a']),True)
check('dynamic left',solve(['r','?'],['r',N]),True)
check('dynamic right',solve(['r',N],['r','?']),True)
check('separated indices',solve(['r',N],['r',N+3]),False)
check('adjacent indices',solve(['r',N],['r',N+1]),False)
check('fields',solve(['r','a'],['r','b']),False)
check('parent',solve(['r'],['r','a']),True)
check('same',solve(['r',N],['r',N]),True)
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
absent	`False`	`False`	Passed
both absent	`False`	`False`	Passed
roots depths	`False`	`False`	Passed
shared prefix	`False`	`False`	Passed
union	`True`	`True`	Passed
deref	`True`	`True`	Passed
dynamic left	`True`	`True`	Passed
dynamic right	`True`	`True`	Passed
separated indices	`False`	`False`	Passed
adjacent indices	`False`	`False`	Passed
fields	`False`	`False`	Passed
parent	`True`	`True`	Passed
same	`True`	`True`	Passed

SHA-256 / 846279339f8864ff194ad03b3f05bd15c20a7b6e33da39c9941a82318118cee2

Verification & scope

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.

Observations recorded using Python 3.12.14 at 2026-09-29T14:43:56.304675+00:00.

Case digest / e8574a09ec496d5d06e7ce59d4cd0f8701e4c74fd5a410082edf1809d1f28de1