FA-42891 / Borrow checking / Open access

Outlives substitutes cardinality for program-point containment · case 01

Outlives substitutes cardinality for program-point containment.

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

ROOT CAUSE

The static analyzer mishandles outlives direction: outlives substitutes cardinality for program-point containment.

VERIFIED REPAIR

Apply the specified transfer or inference rule at this site: if op=='outlives': return x.issuperset(regions[b]).

Unsuccessful approach: The partial repair uses if op=='outlives': return len(x)>=len(regions[b]), which still violates the stipulated analysis contract.

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

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(regions, op, a, b, c=None):
    x=set(regions[a])
    if op=='outlives': return x.issubset(regions[b])
    if op=='meet': return sorted(x.intersection(regions[b]))
    if op=='join': return sorted(x.union(regions[b]))
    if op=='missing': return sorted(set(regions[b])-x)
    if op=='strict': return x>set(regions[b])
    if op=='eq': return x==set(regions[b])
    if op=='disjoint': return x.isdisjoint(regions[b])
    if op=='covers': return all(x.issuperset(regions[k]) for k in b)
    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)
    if op=='choose':
        candidates=[k for k in b if set(regions[k]).issuperset(x)]
        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None
    return None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
r={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}
check('outlives',solve(r,'outlives','a','s'),True)
check('incomparable',solve(r,'outlives','a','b'),False)
check('meet',solve(r,'meet','a','b'),[N+1])
check('join',solve(r,'join','a','b'),[N,N+1,N+2])
check('missing',solve(r,'missing','a','b'),[N+2])
check('strict equal',solve(r,'strict','a','a'),False)
check('strict incomparable',solve(r,'strict','aa','b'),True)
check('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)
check('equivalent unordered',solve(r,'eq','a','z'),True)
check('equivalent distinct',solve(r,'eq','a','b'),False)
check('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)
check('overlap disjoint',solve(r,'disjoint','a','b'),False)
check('mixed obligations',solve(r,'covers','a',['s','b']),False)
check('no obligations',solve(r,'covers','a',[]),True)
check('joint demand',solve(r,'gap','e','a','b'),[N+1])
check('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')
check('no candidate',solve(r,'choose','aa',['a','s']),None)
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
outlives	`False`	`True`	Failed
incomparable	`False`	`False`	Passed
meet	`[2]`	`[2]`	Passed
join	`[1, 2, 3]`	`[1, 2, 3]`	Passed
missing	`[3]`	`[3]`	Passed
strict equal	`False`	`False`	Passed
strict incomparable	`True`	`True`	Passed
strict size insufficient	`False`	`False`	Passed
equivalent unordered	`True`	`True`	Passed
equivalent distinct	`False`	`False`	Passed
nonempty disjoint	`True`	`True`	Passed
overlap disjoint	`False`	`False`	Passed
mixed obligations	`False`	`False`	Passed
no obligations	`True`	`True`	Passed
joint demand	`[2]`	`[2]`	Passed
choose shortest	`s`	`s`	Passed
no candidate	`None`	`None`	Passed

SHA-256 / fc9a2db73234bffb48715d9a6b71458e80a2c57d0ed6cf31e8a4fdfff4249999

2 / The unsuccessful fix

Exit 1

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

N = 1
observations = []
def solve(regions, op, a, b, c=None):
    x=set(regions[a])
    if op=='outlives': return len(x)>=len(regions[b])
    if op=='meet': return sorted(x.intersection(regions[b]))
    if op=='join': return sorted(x.union(regions[b]))
    if op=='missing': return sorted(set(regions[b])-x)
    if op=='strict': return x>set(regions[b])
    if op=='eq': return x==set(regions[b])
    if op=='disjoint': return x.isdisjoint(regions[b])
    if op=='covers': return all(x.issuperset(regions[k]) for k in b)
    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)
    if op=='choose':
        candidates=[k for k in b if set(regions[k]).issuperset(x)]
        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None
    return None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
r={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}
check('outlives',solve(r,'outlives','a','s'),True)
check('incomparable',solve(r,'outlives','a','b'),False)
check('meet',solve(r,'meet','a','b'),[N+1])
check('join',solve(r,'join','a','b'),[N,N+1,N+2])
check('missing',solve(r,'missing','a','b'),[N+2])
check('strict equal',solve(r,'strict','a','a'),False)
check('strict incomparable',solve(r,'strict','aa','b'),True)
check('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)
check('equivalent unordered',solve(r,'eq','a','z'),True)
check('equivalent distinct',solve(r,'eq','a','b'),False)
check('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)
check('overlap disjoint',solve(r,'disjoint','a','b'),False)
check('mixed obligations',solve(r,'covers','a',['s','b']),False)
check('no obligations',solve(r,'covers','a',[]),True)
check('joint demand',solve(r,'gap','e','a','b'),[N+1])
check('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')
check('no candidate',solve(r,'choose','aa',['a','s']),None)
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
outlives	`True`	`True`	Passed
incomparable	`True`	`False`	Failed
meet	`[2]`	`[2]`	Passed
join	`[1, 2, 3]`	`[1, 2, 3]`	Passed
missing	`[3]`	`[3]`	Passed
strict equal	`False`	`False`	Passed
strict incomparable	`True`	`True`	Passed
strict size insufficient	`False`	`False`	Passed
equivalent unordered	`True`	`True`	Passed
equivalent distinct	`False`	`False`	Passed
nonempty disjoint	`True`	`True`	Passed
overlap disjoint	`False`	`False`	Passed
mixed obligations	`False`	`False`	Passed
no obligations	`True`	`True`	Passed
joint demand	`[2]`	`[2]`	Passed
choose shortest	`s`	`s`	Passed
no candidate	`None`	`None`	Passed

SHA-256 / 628274d75dd944b1232b2e4954553f9f44782e0271a98bbacbb7a1bcf1a94203

3 / The verified repair

Exit 0

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

N = 1
observations = []
def solve(regions, op, a, b, c=None):
    x=set(regions[a])
    if op=='outlives': return x.issuperset(regions[b])
    if op=='meet': return sorted(x.intersection(regions[b]))
    if op=='join': return sorted(x.union(regions[b]))
    if op=='missing': return sorted(set(regions[b])-x)
    if op=='strict': return x>set(regions[b])
    if op=='eq': return x==set(regions[b])
    if op=='disjoint': return x.isdisjoint(regions[b])
    if op=='covers': return all(x.issuperset(regions[k]) for k in b)
    if op=='gap': return sorted((set(regions[b]) & set(regions[c]))-x)
    if op=='choose':
        candidates=[k for k in b if set(regions[k]).issuperset(x)]
        return min(candidates,key=lambda k:(len(set(regions[k])),k)) if candidates else None
    return None
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
r={'a':[N,N+1],'b':[N+1,N+2],'s':[N+1],'e':[],'z':[N+1,N],'aa':[N,N+1,N+2]}
check('outlives',solve(r,'outlives','a','s'),True)
check('incomparable',solve(r,'outlives','a','b'),False)
check('meet',solve(r,'meet','a','b'),[N+1])
check('join',solve(r,'join','a','b'),[N,N+1,N+2])
check('missing',solve(r,'missing','a','b'),[N+2])
check('strict equal',solve(r,'strict','a','a'),False)
check('strict incomparable',solve(r,'strict','aa','b'),True)
check('strict size insufficient',solve({'a':[N,N+1],'b':[N+2]},'strict','a','b'),False)
check('equivalent unordered',solve(r,'eq','a','z'),True)
check('equivalent distinct',solve(r,'eq','a','b'),False)
check('nonempty disjoint',solve({'a':[N],'b':[N+1]},'disjoint','a','b'),True)
check('overlap disjoint',solve(r,'disjoint','a','b'),False)
check('mixed obligations',solve(r,'covers','a',['s','b']),False)
check('no obligations',solve(r,'covers','a',[]),True)
check('joint demand',solve(r,'gap','e','a','b'),[N+1])
check('choose shortest',solve(r,'choose','s',['aa','a','s']), 's')
check('no candidate',solve(r,'choose','aa',['a','s']),None)
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
outlives	`True`	`True`	Passed
incomparable	`False`	`False`	Passed
meet	`[2]`	`[2]`	Passed
join	`[1, 2, 3]`	`[1, 2, 3]`	Passed
missing	`[3]`	`[3]`	Passed
strict equal	`False`	`False`	Passed
strict incomparable	`True`	`True`	Passed
strict size insufficient	`False`	`False`	Passed
equivalent unordered	`True`	`True`	Passed
equivalent distinct	`False`	`False`	Passed
nonempty disjoint	`True`	`True`	Passed
overlap disjoint	`False`	`False`	Passed
mixed obligations	`False`	`False`	Passed
no obligations	`True`	`True`	Passed
joint demand	`[2]`	`[2]`	Passed
choose shortest	`s`	`s`	Passed
no candidate	`None`	`None`	Passed

SHA-256 / 96edea118f7a3dfe79867e896f40641c6e4c7a17dd487f924ed6f170809fbc79

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

Case digest / 65f98dc55d7609679fd140b214b80a7586b7a722f2181fc8dddfc25539b190d3