FA-43021 / Borrow checking / Open access

Reborrow construction leaves the child demanded before its definition · case 01

Reborrow construction leaves the child demanded before its definition.

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

ROOT CAUSE

The static analyzer mishandles reborrow parent: reborrow construction leaves the child demanded before its definition.

THE FAILURE

The static analyzer mishandles reborrow parent: reborrow construction leaves the child demanded before its definition.

Unsuccessful approach: The partial repair uses live.add(b), 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': 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)
        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']`	Failed
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 / c1ca1fbbf6420a7d05d3eac86dc4b81bc0efa8dd2d7de6482fbdd640025bcdcf

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.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.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	`['a', 'r1']`	`['r1']`	Failed
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 / 3a95641ec68720cca7adef5cab790a7fe8d6b48b3bc645f90028bf7962b24095

HELD IN THE MEMBER ARCHIVE

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

This mechanism has 13 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:57.725831+00:00.

Case digest / 48c0cdf821d01723651ba6d90053ef949382c1620ab0601bd85fd4a00f61d9c3