FA-42996 / Borrow checking / Open access
Returned references disappear from entry lifetime obligations · case 01
Returned references disappear from entry lifetime obligations.
ROOT CAUSE
The static analyzer mishandles return demand: returned references disappear from entry lifetime obligations.
VERIFIED REPAIR
Apply the specified transfer or inference rule at this site: elif op=='return': live.add(a).
Unsuccessful approach: The partial repair uses elif op=='return': live.clear(), which still violates the stipulated analysis contract.
Case contract
Backward reference-demand transfer over a finite straight-line IR. ops execute forward and analysis traverses backward. use/return demand one reference; call demands all actual references. def and storage_dead kill a local. assign(d,s) propagates demand from destination to source, killing destination. reborrow(d,p) kills child demand and adds parent unconditionally because construction reads parent. phi(d,sources) propagates destination demand to every source. drop(ref,needs_drop) demands only when destructor can observe referent. branch supplies two already-computed successor demand sets, both unioned. Return sorted entry-demand names.
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(ops):
live=set()
for op,a,b in reversed(ops):
if op=='use': live.add(a)
elif op=='return': pass
elif op=='call': live.update(a)
elif op=='def': live.discard(a)
elif op=='storage_dead': live.discard(a)
elif op=='assign':
needed=a in live; live.discard(a)
if needed: live.add(b)
elif op=='reborrow':
live.discard(a); live.add(b)
elif op=='phi':
needed=a in live; live.discard(a)
if needed: live.update(b)
elif op=='drop':
if b: live.add(a)
elif op=='branch': live.update(set(a)|set(b))
return sorted(live)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
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 |
|---|---|---|---|
| empty | [] | [] | Passed |
| use | ['r1'] | ['r1'] | Passed |
| return | [] | ['r1'] | Failed |
| call | ['a', 'r1'] | ['a', 'r1'] | Passed |
| definition | ['r1'] | ['r1'] | Passed |
| dead boundary | [] | [] | Passed |
| assign demanded | ['r1'] | ['r1'] | Passed |
| reborrow constructor | ['r1'] | ['r1'] | Passed |
| phi second origin | ['b', 'r1'] | ['b', 'r1'] | Passed |
| trivial drop | [] | [] | Passed |
| observing drop | ['r1'] | ['r1'] | Passed |
| branch union | ['a', 'r1'] | ['a', 'r1'] | Passed |
| variable arity | [0, 1] | [0, 1] | Passed |
SHA-256 / f7940be23161be216e2a4187d8be92486638b2d953830a7c7d46b25f56ed81a1
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops):
live=set()
for op,a,b in reversed(ops):
if op=='use': live.add(a)
elif op=='return': live.clear()
elif op=='call': live.update(a)
elif op=='def': live.discard(a)
elif op=='storage_dead': live.discard(a)
elif op=='assign':
needed=a in live; live.discard(a)
if needed: live.add(b)
elif op=='reborrow':
live.discard(a); live.add(b)
elif op=='phi':
needed=a in live; live.discard(a)
if needed: live.update(b)
elif op=='drop':
if b: live.add(a)
elif op=='branch': live.update(set(a)|set(b))
return sorted(live)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
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 |
|---|---|---|---|
| empty | [] | [] | Passed |
| use | ['r1'] | ['r1'] | Passed |
| return | [] | ['r1'] | Failed |
| call | ['a', 'r1'] | ['a', 'r1'] | Passed |
| definition | ['r1'] | ['r1'] | Passed |
| dead boundary | [] | [] | Passed |
| assign demanded | ['r1'] | ['r1'] | Passed |
| reborrow constructor | ['r1'] | ['r1'] | Passed |
| phi second origin | ['b', 'r1'] | ['b', 'r1'] | Passed |
| trivial drop | [] | [] | Passed |
| observing drop | ['r1'] | ['r1'] | Passed |
| branch union | ['a', 'r1'] | ['a', 'r1'] | Passed |
| variable arity | [0, 1] | [0, 1] | Passed |
SHA-256 / dc5508453675a6b83c4cc0f121e18b836b7c4b6ebb3f3ec0a330af11e66e7e73
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops):
live=set()
for op,a,b in reversed(ops):
if op=='use': live.add(a)
elif op=='return': live.add(a)
elif op=='call': live.update(a)
elif op=='def': live.discard(a)
elif op=='storage_dead': live.discard(a)
elif op=='assign':
needed=a in live; live.discard(a)
if needed: live.add(b)
elif op=='reborrow':
live.discard(a); live.add(b)
elif op=='phi':
needed=a in live; live.discard(a)
if needed: live.update(b)
elif op=='drop':
if b: live.add(a)
elif op=='branch': live.update(set(a)|set(b))
return sorted(live)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='r'+str(N)
check('empty',solve([]),[])
check('use',solve([('use',x,None)]),[x])
check('return',solve([('return',x,None)]),[x])
check('call',solve([('call',['a',x],None)]),['a',x])
check('definition',solve([('def','a',None),('use','a',None),('use',x,None)]),[x])
check('dead boundary',solve([('storage_dead','a',None),('use','a',None)]),[])
check('assign demanded',solve([('assign','a',x),('use','a',None)]),[x])
check('reborrow constructor',solve([('reborrow','a',x),('use','a',None)]),[x])
check('phi second origin',solve([('phi','a',['b',x]),('use','a',None)]),['b',x])
check('trivial drop',solve([('drop',x,False)]),[])
check('observing drop',solve([('drop',x,True)]),[x])
check('branch union',solve([('branch',['a'],[x])]),['a',x])
check('variable arity',solve([('call',list(range(N+1)),None)]),list(range(N+1)))
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 |
|---|---|---|---|
| empty | [] | [] | Passed |
| use | ['r1'] | ['r1'] | Passed |
| return | ['r1'] | ['r1'] | Passed |
| call | ['a', 'r1'] | ['a', 'r1'] | Passed |
| definition | ['r1'] | ['r1'] | Passed |
| dead boundary | [] | [] | Passed |
| assign demanded | ['r1'] | ['r1'] | Passed |
| reborrow constructor | ['r1'] | ['r1'] | Passed |
| phi second origin | ['b', 'r1'] | ['b', 'r1'] | Passed |
| trivial drop | [] | [] | Passed |
| observing drop | ['r1'] | ['r1'] | Passed |
| branch union | ['a', 'r1'] | ['a', 'r1'] | Passed |
| variable arity | [0, 1] | [0, 1] | Passed |
SHA-256 / b6e537905467c375d1a94f1167707d079a663a06707c381a5902435053ddbd24
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:57.306150+00:00.
Case digest / e8e9191453f830a22ddb304728f45c6a99a42501e71865a48f21af313fbad28d