FA-42841 / Borrow checking / Open access

Absent places are treated as aliases · case 01

Absent places are treated as aliases.

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

ROOT CAUSE

The static analyzer mishandles empty place: absent places are treated as aliases.

VERIFIED REPAIR

Apply the specified transfer or inference rule at this site: if not a or not b: return False.

Unsuccessful approach: The partial repair uses if not a or not b: return bool(a or 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 True
    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	`True`	`False`	Failed
both absent	`True`	`False`	Failed
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 / a5617342eda4cd7fe6fc1496a78f7f72fa17626451b07a353512364d2db05b7f

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 bool(a or b)
    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	`True`	`False`	Failed
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 / ac13bb77491c55d1d20e35c2a36303c9bc231b4abf7df1333f2c28b7bda368c4

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:55.858460+00:00.

Case digest / 32bc5853c46baacc49a46f1ca9f763cbecb0f848dff4766807a78158c852ff68