FA-42921 / Borrow checking / Open access

Disjoint live regions are rejected unless one is empty · case 01

Disjoint live regions are rejected unless one is empty.

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

ROOT CAUSE

The static analyzer mishandles nonoverlap: disjoint live regions are rejected unless one is empty.

THE FAILURE

The static analyzer mishandles nonoverlap: disjoint live regions are rejected unless one is empty.

Unsuccessful approach: The partial repair uses if op=='disjoint': return not x or not 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.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!=set(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	`True`	`False`	Failed
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 / b156f77818bb433ceb0223c6aea5875417702a9691af728c7f376c268f3f128b

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 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 not x or not 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	`False`	`True`	Failed
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 / 9e313c6866e0f15faa3d0ef41712e57ba2ca3be05e967b22f9fc8c806ff9bbc5

HELD IN THE MEMBER ARCHIVE

The verified repair and its recorded checks are member-only.

This mechanism has 17 recorded checks per implementation. The open-access tier publishes the failure and the unsuccessful fix; the repaired source that passes every check, and the observations that prove it, are available to members.

Every case sharing this mechanism uses the same contract and the same repair, so this one record is held back for all of them.

Member access is invitation-based. Sign in with your invited account to inspect the repair.

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

Case digest / c19fd321e35ce59be304ae7002d37a0e54e1b61d6a493016b0190d2c27e5d938