FA-43611 / Borrow checking / Open access
A mutable dynamic method is callable through a shared object borrow · case 01
A mutable dynamic method is callable through a shared object borrow.
ROOT CAUSE
The static analyzer mishandles mutable dispatch: a mutable dynamic method is callable through a shared object borrow.
VERIFIED REPAIR
Apply the specified transfer or inference rule at this site: if d['mut_method'] and not d['exclusive_access']: errors.append('mutable-dispatch').
Unsuccessful approach: The partial repair uses if d['mut_method'] and not d['exclusive_access'] and d['object_unique']: errors.append('mutable-dispatch'), which still violates the stipulated analysis contract.
Case contract
Check erased borrowed trait objects in a stipulated object calculus. Erasure retains referent lifetime and ownership capability; default object bound inside reference inherits reference bound; object method return aliases must be represented in the vtable summary; mutable methods require exclusive object access; upcasting cannot enlarge lifetime or change data-address provenance; thin conversion cannot discard lifetime metadata; associated borrowed output includes owner lifetime; object-safe methods cannot expose a locally quantified lifetime as an unbound output; dynamic destruction observes declared borrowed fields. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.
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(d):
errors=[]
if d['source_bound']!=d['erased_bound']: errors.append('erasure-bound')
if d['object_unique'] and not d['source_unique']: errors.append('erasure-capability')
if d['reference_bound'] is not None and d['default_bound']!=d['reference_bound']: errors.append('reference-default-bound')
if not set(d['method_aliases'])<=set(d['vtable_aliases']): errors.append('vtable-alias')
if False: errors.append('mutable-dispatch')
if not set(d['upcast_after'])<=set(d['upcast_before']): errors.append('upcast-lifetime')
if d['source_address']!=d['upcast_address']: errors.append('upcast-provenance')
if d['thin'] and not d['lifetime_metadata']: errors.append('thin-metadata')
if bool(set(d['local_quantified'])&set(d['output_free'])): errors.append('associated-owner')
if not set(d['drop_observes'])<=set(d['drop_summary']): errors.append('dynamic-drop-summary')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_bound': [], 'erased_bound': [], 'source_unique': False, 'object_unique': False, 'reference_bound': None, 'default_bound': None, 'method_aliases': [], 'vtable_aliases': [], 'mut_method': False, 'exclusive_access': True, 'upcast_before': [], 'upcast_after': [], 'source_address': None, 'upcast_address': None, 'thin': False, 'lifetime_metadata': True, 'assoc_owner': [], 'assoc_output': [], 'local_quantified': [], 'output_free': [], 'drop_observes': [], 'drop_summary': []}
check('well formed empty obligations',solve(base),[])
check('erasure-bound regression 0', solve(dict(base, **({'source_bound':[N],'erased_bound':[N+1]}))), ['erasure-bound'])
check('erasure-bound regression 1', solve(dict(base, **({'source_bound':[N,N+1],'erased_bound':[N+1,N+2]}))), ['erasure-bound'])
check('erasure-capability regression 0', solve(dict(base, **({'object_unique':True}))), ['erasure-capability'])
check('erasure-capability regression 1', solve(dict(base, **({'object_unique':True,'source_bound':[N],'erased_bound':[N]}))), ['erasure-capability'])
check('reference-default-bound regression 0', solve(dict(base, **({'reference_bound':'a','default_bound':'static'}))), ['reference-default-bound'])
check('reference-default-bound regression 1', solve(dict(base, **({'reference_bound':N,'default_bound':N+1}))), ['reference-default-bound'])
check('vtable-alias regression 0', solve(dict(base, **({'method_aliases':['a','b'],'vtable_aliases':['a']}))), ['vtable-alias'])
check('vtable-alias regression 1', solve(dict(base, **({'method_aliases':[N,N+1],'vtable_aliases':[N]}))), ['vtable-alias'])
check('mutable-dispatch regression 0', solve(dict(base, **({'mut_method':True,'exclusive_access':False}))), ['mutable-dispatch'])
check('mutable-dispatch regression 1', solve(dict(base, **({'mut_method':True,'exclusive_access':False,'source_bound':[N],'erased_bound':[N]}))), ['mutable-dispatch'])
check('upcast-lifetime regression 0', solve(dict(base, **({'upcast_before':[N],'upcast_after':[N+1]}))), ['upcast-lifetime'])
check('upcast-lifetime regression 1', solve(dict(base, **({'upcast_before':[N,N+1],'upcast_after':[N+1,N+2]}))), ['upcast-lifetime'])
check('upcast-provenance regression 0', solve(dict(base, **({'source_address':N,'upcast_address':N+1}))), ['upcast-provenance'])
check('upcast-provenance regression 1', solve(dict(base, **({'source_address':'owner','upcast_address':'vtable'}))), ['upcast-provenance'])
check('thin-metadata regression 0', solve(dict(base, **({'thin':True,'lifetime_metadata':False}))), ['thin-metadata'])
check('thin-metadata regression 1', solve(dict(base, **({'thin':True,'lifetime_metadata':False,'source_bound':[N],'erased_bound':[N]}))), ['thin-metadata'])
check('associated-owner regression 0', solve(dict(base, **({'local_quantified':['a'],'output_free':['a']}))), ['associated-owner'])
check('associated-owner regression 1', solve(dict(base, **({'local_quantified':[N],'output_free':[N]}))), ['associated-owner'])
check('dynamic-drop-summary regression 0', solve(dict(base, **({'drop_observes':['a','b'],'drop_summary':['a']}))), ['dynamic-drop-summary'])
check('dynamic-drop-summary regression 1', solve(dict(base, **({'drop_observes':[N,N+1],'drop_summary':[N]}))), ['dynamic-drop-summary'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| erasure-bound regression 0 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-bound regression 1 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-capability regression 0 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| erasure-capability regression 1 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| reference-default-bound regression 0 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| reference-default-bound regression 1 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| vtable-alias regression 0 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| vtable-alias regression 1 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| mutable-dispatch regression 0 | [] | ['mutable-dispatch'] | Failed |
| mutable-dispatch regression 1 | [] | ['mutable-dispatch'] | Failed |
| upcast-lifetime regression 0 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-lifetime regression 1 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-provenance regression 0 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| upcast-provenance regression 1 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| thin-metadata regression 0 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| thin-metadata regression 1 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| associated-owner regression 0 | ['associated-owner'] | ['associated-owner'] | Passed |
| associated-owner regression 1 | ['associated-owner'] | ['associated-owner'] | Passed |
| dynamic-drop-summary regression 0 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
| dynamic-drop-summary regression 1 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
SHA-256 / 337f789eb00b119c57dc086c6f52c2ffd6008ececb977e69bd6f56522309fb2e
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(d):
errors=[]
if d['source_bound']!=d['erased_bound']: errors.append('erasure-bound')
if d['object_unique'] and not d['source_unique']: errors.append('erasure-capability')
if d['reference_bound'] is not None and d['default_bound']!=d['reference_bound']: errors.append('reference-default-bound')
if not set(d['method_aliases'])<=set(d['vtable_aliases']): errors.append('vtable-alias')
if d['mut_method'] and not d['exclusive_access'] and d['object_unique']: errors.append('mutable-dispatch')
if not set(d['upcast_after'])<=set(d['upcast_before']): errors.append('upcast-lifetime')
if d['source_address']!=d['upcast_address']: errors.append('upcast-provenance')
if d['thin'] and not d['lifetime_metadata']: errors.append('thin-metadata')
if bool(set(d['local_quantified'])&set(d['output_free'])): errors.append('associated-owner')
if not set(d['drop_observes'])<=set(d['drop_summary']): errors.append('dynamic-drop-summary')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_bound': [], 'erased_bound': [], 'source_unique': False, 'object_unique': False, 'reference_bound': None, 'default_bound': None, 'method_aliases': [], 'vtable_aliases': [], 'mut_method': False, 'exclusive_access': True, 'upcast_before': [], 'upcast_after': [], 'source_address': None, 'upcast_address': None, 'thin': False, 'lifetime_metadata': True, 'assoc_owner': [], 'assoc_output': [], 'local_quantified': [], 'output_free': [], 'drop_observes': [], 'drop_summary': []}
check('well formed empty obligations',solve(base),[])
check('erasure-bound regression 0', solve(dict(base, **({'source_bound':[N],'erased_bound':[N+1]}))), ['erasure-bound'])
check('erasure-bound regression 1', solve(dict(base, **({'source_bound':[N,N+1],'erased_bound':[N+1,N+2]}))), ['erasure-bound'])
check('erasure-capability regression 0', solve(dict(base, **({'object_unique':True}))), ['erasure-capability'])
check('erasure-capability regression 1', solve(dict(base, **({'object_unique':True,'source_bound':[N],'erased_bound':[N]}))), ['erasure-capability'])
check('reference-default-bound regression 0', solve(dict(base, **({'reference_bound':'a','default_bound':'static'}))), ['reference-default-bound'])
check('reference-default-bound regression 1', solve(dict(base, **({'reference_bound':N,'default_bound':N+1}))), ['reference-default-bound'])
check('vtable-alias regression 0', solve(dict(base, **({'method_aliases':['a','b'],'vtable_aliases':['a']}))), ['vtable-alias'])
check('vtable-alias regression 1', solve(dict(base, **({'method_aliases':[N,N+1],'vtable_aliases':[N]}))), ['vtable-alias'])
check('mutable-dispatch regression 0', solve(dict(base, **({'mut_method':True,'exclusive_access':False}))), ['mutable-dispatch'])
check('mutable-dispatch regression 1', solve(dict(base, **({'mut_method':True,'exclusive_access':False,'source_bound':[N],'erased_bound':[N]}))), ['mutable-dispatch'])
check('upcast-lifetime regression 0', solve(dict(base, **({'upcast_before':[N],'upcast_after':[N+1]}))), ['upcast-lifetime'])
check('upcast-lifetime regression 1', solve(dict(base, **({'upcast_before':[N,N+1],'upcast_after':[N+1,N+2]}))), ['upcast-lifetime'])
check('upcast-provenance regression 0', solve(dict(base, **({'source_address':N,'upcast_address':N+1}))), ['upcast-provenance'])
check('upcast-provenance regression 1', solve(dict(base, **({'source_address':'owner','upcast_address':'vtable'}))), ['upcast-provenance'])
check('thin-metadata regression 0', solve(dict(base, **({'thin':True,'lifetime_metadata':False}))), ['thin-metadata'])
check('thin-metadata regression 1', solve(dict(base, **({'thin':True,'lifetime_metadata':False,'source_bound':[N],'erased_bound':[N]}))), ['thin-metadata'])
check('associated-owner regression 0', solve(dict(base, **({'local_quantified':['a'],'output_free':['a']}))), ['associated-owner'])
check('associated-owner regression 1', solve(dict(base, **({'local_quantified':[N],'output_free':[N]}))), ['associated-owner'])
check('dynamic-drop-summary regression 0', solve(dict(base, **({'drop_observes':['a','b'],'drop_summary':['a']}))), ['dynamic-drop-summary'])
check('dynamic-drop-summary regression 1', solve(dict(base, **({'drop_observes':[N,N+1],'drop_summary':[N]}))), ['dynamic-drop-summary'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| erasure-bound regression 0 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-bound regression 1 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-capability regression 0 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| erasure-capability regression 1 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| reference-default-bound regression 0 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| reference-default-bound regression 1 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| vtable-alias regression 0 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| vtable-alias regression 1 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| mutable-dispatch regression 0 | [] | ['mutable-dispatch'] | Failed |
| mutable-dispatch regression 1 | [] | ['mutable-dispatch'] | Failed |
| upcast-lifetime regression 0 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-lifetime regression 1 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-provenance regression 0 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| upcast-provenance regression 1 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| thin-metadata regression 0 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| thin-metadata regression 1 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| associated-owner regression 0 | ['associated-owner'] | ['associated-owner'] | Passed |
| associated-owner regression 1 | ['associated-owner'] | ['associated-owner'] | Passed |
| dynamic-drop-summary regression 0 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
| dynamic-drop-summary regression 1 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
SHA-256 / 57b938dcff35025cb942e5a8b87d58d458c2be349976c582de5ce30e8c3166d2
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(d):
errors=[]
if d['source_bound']!=d['erased_bound']: errors.append('erasure-bound')
if d['object_unique'] and not d['source_unique']: errors.append('erasure-capability')
if d['reference_bound'] is not None and d['default_bound']!=d['reference_bound']: errors.append('reference-default-bound')
if not set(d['method_aliases'])<=set(d['vtable_aliases']): errors.append('vtable-alias')
if d['mut_method'] and not d['exclusive_access']: errors.append('mutable-dispatch')
if not set(d['upcast_after'])<=set(d['upcast_before']): errors.append('upcast-lifetime')
if d['source_address']!=d['upcast_address']: errors.append('upcast-provenance')
if d['thin'] and not d['lifetime_metadata']: errors.append('thin-metadata')
if bool(set(d['local_quantified'])&set(d['output_free'])): errors.append('associated-owner')
if not set(d['drop_observes'])<=set(d['drop_summary']): errors.append('dynamic-drop-summary')
return errors
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_bound': [], 'erased_bound': [], 'source_unique': False, 'object_unique': False, 'reference_bound': None, 'default_bound': None, 'method_aliases': [], 'vtable_aliases': [], 'mut_method': False, 'exclusive_access': True, 'upcast_before': [], 'upcast_after': [], 'source_address': None, 'upcast_address': None, 'thin': False, 'lifetime_metadata': True, 'assoc_owner': [], 'assoc_output': [], 'local_quantified': [], 'output_free': [], 'drop_observes': [], 'drop_summary': []}
check('well formed empty obligations',solve(base),[])
check('erasure-bound regression 0', solve(dict(base, **({'source_bound':[N],'erased_bound':[N+1]}))), ['erasure-bound'])
check('erasure-bound regression 1', solve(dict(base, **({'source_bound':[N,N+1],'erased_bound':[N+1,N+2]}))), ['erasure-bound'])
check('erasure-capability regression 0', solve(dict(base, **({'object_unique':True}))), ['erasure-capability'])
check('erasure-capability regression 1', solve(dict(base, **({'object_unique':True,'source_bound':[N],'erased_bound':[N]}))), ['erasure-capability'])
check('reference-default-bound regression 0', solve(dict(base, **({'reference_bound':'a','default_bound':'static'}))), ['reference-default-bound'])
check('reference-default-bound regression 1', solve(dict(base, **({'reference_bound':N,'default_bound':N+1}))), ['reference-default-bound'])
check('vtable-alias regression 0', solve(dict(base, **({'method_aliases':['a','b'],'vtable_aliases':['a']}))), ['vtable-alias'])
check('vtable-alias regression 1', solve(dict(base, **({'method_aliases':[N,N+1],'vtable_aliases':[N]}))), ['vtable-alias'])
check('mutable-dispatch regression 0', solve(dict(base, **({'mut_method':True,'exclusive_access':False}))), ['mutable-dispatch'])
check('mutable-dispatch regression 1', solve(dict(base, **({'mut_method':True,'exclusive_access':False,'source_bound':[N],'erased_bound':[N]}))), ['mutable-dispatch'])
check('upcast-lifetime regression 0', solve(dict(base, **({'upcast_before':[N],'upcast_after':[N+1]}))), ['upcast-lifetime'])
check('upcast-lifetime regression 1', solve(dict(base, **({'upcast_before':[N,N+1],'upcast_after':[N+1,N+2]}))), ['upcast-lifetime'])
check('upcast-provenance regression 0', solve(dict(base, **({'source_address':N,'upcast_address':N+1}))), ['upcast-provenance'])
check('upcast-provenance regression 1', solve(dict(base, **({'source_address':'owner','upcast_address':'vtable'}))), ['upcast-provenance'])
check('thin-metadata regression 0', solve(dict(base, **({'thin':True,'lifetime_metadata':False}))), ['thin-metadata'])
check('thin-metadata regression 1', solve(dict(base, **({'thin':True,'lifetime_metadata':False,'source_bound':[N],'erased_bound':[N]}))), ['thin-metadata'])
check('associated-owner regression 0', solve(dict(base, **({'local_quantified':['a'],'output_free':['a']}))), ['associated-owner'])
check('associated-owner regression 1', solve(dict(base, **({'local_quantified':[N],'output_free':[N]}))), ['associated-owner'])
check('dynamic-drop-summary regression 0', solve(dict(base, **({'drop_observes':['a','b'],'drop_summary':['a']}))), ['dynamic-drop-summary'])
check('dynamic-drop-summary regression 1', solve(dict(base, **({'drop_observes':[N,N+1],'drop_summary':[N]}))), ['dynamic-drop-summary'])
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 |
|---|---|---|---|
| well formed empty obligations | [] | [] | Passed |
| erasure-bound regression 0 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-bound regression 1 | ['erasure-bound'] | ['erasure-bound'] | Passed |
| erasure-capability regression 0 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| erasure-capability regression 1 | ['erasure-capability'] | ['erasure-capability'] | Passed |
| reference-default-bound regression 0 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| reference-default-bound regression 1 | ['reference-default-bound'] | ['reference-default-bound'] | Passed |
| vtable-alias regression 0 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| vtable-alias regression 1 | ['vtable-alias'] | ['vtable-alias'] | Passed |
| mutable-dispatch regression 0 | ['mutable-dispatch'] | ['mutable-dispatch'] | Passed |
| mutable-dispatch regression 1 | ['mutable-dispatch'] | ['mutable-dispatch'] | Passed |
| upcast-lifetime regression 0 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-lifetime regression 1 | ['upcast-lifetime'] | ['upcast-lifetime'] | Passed |
| upcast-provenance regression 0 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| upcast-provenance regression 1 | ['upcast-provenance'] | ['upcast-provenance'] | Passed |
| thin-metadata regression 0 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| thin-metadata regression 1 | ['thin-metadata'] | ['thin-metadata'] | Passed |
| associated-owner regression 0 | ['associated-owner'] | ['associated-owner'] | Passed |
| associated-owner regression 1 | ['associated-owner'] | ['associated-owner'] | Passed |
| dynamic-drop-summary regression 0 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
| dynamic-drop-summary regression 1 | ['dynamic-drop-summary'] | ['dynamic-drop-summary'] | Passed |
SHA-256 / e16c8f605e6207ea051f4ebfb95d0467eaea1137a8ed7c885479fc9e2e1fa481
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:44:03.819483+00:00.
Case digest / c1e4eeb2753a6c1d747aee8ef4060d7fc3737bd84253f5cc05eb39ea0664ee33