FA-42941 / Borrow checking / Open access
Initialization invents paths absent from the declared record · case 01
Initialization invents paths absent from the declared record.
ROOT CAUSE
The static analyzer mishandles init declared only: initialization invents paths absent from the declared record.
VERIFIED REPAIR
Apply the specified transfer or inference rule at this site: live.update(set(arg)&allowed); out.append(sorted(live)).
Unsuccessful approach: The partial repair uses live.update(set(arg) if arg else allowed); out.append(sorted(live)), which still violates the stipulated analysis contract.
Case contract
Static path initialization lattice for a record with declared leaf names. Commands init/move/read/whole/assign/drop/reset/copy/merge/available. init and assign initialize one leaf. move consumes only initialized named leaf and reports success; read tests one; whole tests all. drop consumes all and reports previously initialized names. reset clears; copy tests without consumption. merge intersects current initialized leaves with supplied branch leaves. available returns sorted initialized names. Unknown leaves never initialize. Return one result per command. This is definite-initialization analysis, not runtime borrowing.
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(leaves, ops):
allowed=set(leaves); live=set(); out=[]
for op,arg in ops:
if op=='init':
live.update(arg); out.append(sorted(live))
elif op=='move':
ok=arg in live
if ok: live.remove(arg)
out.append(ok)
elif op=='read': out.append(arg in live)
elif op=='whole': out.append(live==allowed)
elif op=='assign':
if arg in allowed: live.add(arg)
out.append(sorted(live))
elif op=='drop':
out.append(sorted(live)); live.clear()
elif op=='reset':
live.clear(); out.append([])
elif op=='copy': out.append(arg in live)
elif op=='merge':
live.intersection_update(arg); out.append(sorted(live))
elif op=='available': out.append(sorted(live))
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('unknown init',solve(['a'],[('init',['a',x])]),[['a']])
check('last move',solve(['a'],[('init',['a']),('move','a'),('read','a')]),[['a'],True,False])
check('uninitialized sibling',solve(['a','b'],[('init',['a']),('read','b')]),[['a'],False])
check('empty whole',solve([], [('whole',None)]),[True])
check('partial whole',solve(['a','b'],[('init',['a']),('whole',None)]),[['a'],False])
check('reassign empty',solve(['a'],[('assign','a'),('read','a')]),[['a'],True])
check('drop clears',solve(['a'],[('init',['a']),('drop',None),('read','a')]),[['a'],['a'],False])
check('storage reset',solve(['a'],[('init',['a']),('reset',None),('read','a')]),[['a'],[],False])
check('copy preserves',solve(['a'],[('init',['a']),('copy','a'),('read','a')]),[['a'],True,True])
check('join intersection',solve(['a','b'],[('init',['a']),('merge',['b']),('available',None)]),[['a'],[],[]])
check('available subset',solve(['a','b'],[('init',['a']),('available',None)]),[['a'],['a']])
check('variant leaf',solve([x],[('init',[x]),('move',x),('available',None)]),[[x],True,[]])
check('record arity',solve(list(range(N+1)),[('init',list(range(N+1))),('move',N),('available',None)]),[list(range(N+1)),True,list(range(N))])
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 |
|---|---|---|---|
| unknown init | [['a', 'v1']] | [['a']] | Failed |
| last move | [['a'], True, False] | [['a'], True, False] | Passed |
| uninitialized sibling | [['a'], False] | [['a'], False] | Passed |
| empty whole | [True] | [True] | Passed |
| partial whole | [['a'], False] | [['a'], False] | Passed |
| reassign empty | [['a'], True] | [['a'], True] | Passed |
| drop clears | [['a'], ['a'], False] | [['a'], ['a'], False] | Passed |
| storage reset | [['a'], [], False] | [['a'], [], False] | Passed |
| copy preserves | [['a'], True, True] | [['a'], True, True] | Passed |
| join intersection | [['a'], [], []] | [['a'], [], []] | Passed |
| available subset | [['a'], ['a']] | [['a'], ['a']] | Passed |
| variant leaf | [['v1'], True, []] | [['v1'], True, []] | Passed |
| record arity | [[0, 1], True, [0]] | [[0, 1], True, [0]] | Passed |
SHA-256 / 278ed9596070f478e8149c8d198a082e94e169151a33bf7b1568132d7ab6e49d
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(leaves, ops):
allowed=set(leaves); live=set(); out=[]
for op,arg in ops:
if op=='init':
live.update(set(arg) if arg else allowed); out.append(sorted(live))
elif op=='move':
ok=arg in live
if ok: live.remove(arg)
out.append(ok)
elif op=='read': out.append(arg in live)
elif op=='whole': out.append(live==allowed)
elif op=='assign':
if arg in allowed: live.add(arg)
out.append(sorted(live))
elif op=='drop':
out.append(sorted(live)); live.clear()
elif op=='reset':
live.clear(); out.append([])
elif op=='copy': out.append(arg in live)
elif op=='merge':
live.intersection_update(arg); out.append(sorted(live))
elif op=='available': out.append(sorted(live))
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('unknown init',solve(['a'],[('init',['a',x])]),[['a']])
check('last move',solve(['a'],[('init',['a']),('move','a'),('read','a')]),[['a'],True,False])
check('uninitialized sibling',solve(['a','b'],[('init',['a']),('read','b')]),[['a'],False])
check('empty whole',solve([], [('whole',None)]),[True])
check('partial whole',solve(['a','b'],[('init',['a']),('whole',None)]),[['a'],False])
check('reassign empty',solve(['a'],[('assign','a'),('read','a')]),[['a'],True])
check('drop clears',solve(['a'],[('init',['a']),('drop',None),('read','a')]),[['a'],['a'],False])
check('storage reset',solve(['a'],[('init',['a']),('reset',None),('read','a')]),[['a'],[],False])
check('copy preserves',solve(['a'],[('init',['a']),('copy','a'),('read','a')]),[['a'],True,True])
check('join intersection',solve(['a','b'],[('init',['a']),('merge',['b']),('available',None)]),[['a'],[],[]])
check('available subset',solve(['a','b'],[('init',['a']),('available',None)]),[['a'],['a']])
check('variant leaf',solve([x],[('init',[x]),('move',x),('available',None)]),[[x],True,[]])
check('record arity',solve(list(range(N+1)),[('init',list(range(N+1))),('move',N),('available',None)]),[list(range(N+1)),True,list(range(N))])
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 |
|---|---|---|---|
| unknown init | [['a', 'v1']] | [['a']] | Failed |
| last move | [['a'], True, False] | [['a'], True, False] | Passed |
| uninitialized sibling | [['a'], False] | [['a'], False] | Passed |
| empty whole | [True] | [True] | Passed |
| partial whole | [['a'], False] | [['a'], False] | Passed |
| reassign empty | [['a'], True] | [['a'], True] | Passed |
| drop clears | [['a'], ['a'], False] | [['a'], ['a'], False] | Passed |
| storage reset | [['a'], [], False] | [['a'], [], False] | Passed |
| copy preserves | [['a'], True, True] | [['a'], True, True] | Passed |
| join intersection | [['a'], [], []] | [['a'], [], []] | Passed |
| available subset | [['a'], ['a']] | [['a'], ['a']] | Passed |
| variant leaf | [['v1'], True, []] | [['v1'], True, []] | Passed |
| record arity | [[0, 1], True, [0]] | [[0, 1], True, [0]] | Passed |
SHA-256 / fd966e9291404a22daca0f3aa5fdfae25d3407948db9ab9096d1a2111aee37d6
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(leaves, ops):
allowed=set(leaves); live=set(); out=[]
for op,arg in ops:
if op=='init':
live.update(set(arg)&allowed); out.append(sorted(live))
elif op=='move':
ok=arg in live
if ok: live.remove(arg)
out.append(ok)
elif op=='read': out.append(arg in live)
elif op=='whole': out.append(live==allowed)
elif op=='assign':
if arg in allowed: live.add(arg)
out.append(sorted(live))
elif op=='drop':
out.append(sorted(live)); live.clear()
elif op=='reset':
live.clear(); out.append([])
elif op=='copy': out.append(arg in live)
elif op=='merge':
live.intersection_update(arg); out.append(sorted(live))
elif op=='available': out.append(sorted(live))
return out
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
x='v'+str(N)
check('unknown init',solve(['a'],[('init',['a',x])]),[['a']])
check('last move',solve(['a'],[('init',['a']),('move','a'),('read','a')]),[['a'],True,False])
check('uninitialized sibling',solve(['a','b'],[('init',['a']),('read','b')]),[['a'],False])
check('empty whole',solve([], [('whole',None)]),[True])
check('partial whole',solve(['a','b'],[('init',['a']),('whole',None)]),[['a'],False])
check('reassign empty',solve(['a'],[('assign','a'),('read','a')]),[['a'],True])
check('drop clears',solve(['a'],[('init',['a']),('drop',None),('read','a')]),[['a'],['a'],False])
check('storage reset',solve(['a'],[('init',['a']),('reset',None),('read','a')]),[['a'],[],False])
check('copy preserves',solve(['a'],[('init',['a']),('copy','a'),('read','a')]),[['a'],True,True])
check('join intersection',solve(['a','b'],[('init',['a']),('merge',['b']),('available',None)]),[['a'],[],[]])
check('available subset',solve(['a','b'],[('init',['a']),('available',None)]),[['a'],['a']])
check('variant leaf',solve([x],[('init',[x]),('move',x),('available',None)]),[[x],True,[]])
check('record arity',solve(list(range(N+1)),[('init',list(range(N+1))),('move',N),('available',None)]),[list(range(N+1)),True,list(range(N))])
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 |
|---|---|---|---|
| unknown init | [['a']] | [['a']] | Passed |
| last move | [['a'], True, False] | [['a'], True, False] | Passed |
| uninitialized sibling | [['a'], False] | [['a'], False] | Passed |
| empty whole | [True] | [True] | Passed |
| partial whole | [['a'], False] | [['a'], False] | Passed |
| reassign empty | [['a'], True] | [['a'], True] | Passed |
| drop clears | [['a'], ['a'], False] | [['a'], ['a'], False] | Passed |
| storage reset | [['a'], [], False] | [['a'], [], False] | Passed |
| copy preserves | [['a'], True, True] | [['a'], True, True] | Passed |
| join intersection | [['a'], [], []] | [['a'], [], []] | Passed |
| available subset | [['a'], ['a']] | [['a'], ['a']] | Passed |
| variant leaf | [['v1'], True, []] | [['v1'], True, []] | Passed |
| record arity | [[0, 1], True, [0]] | [[0, 1], True, [0]] | Passed |
SHA-256 / 387a35b8e885bbc7a8a218ef7169356754c561fb33ef9e719085fa119ba50c48
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.767675+00:00.
Case digest / 486b37a7d8dd3861412f8206616f32b0e56a3fb2e5b0fc5a843950957efe4235