broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if False: errors.append('lending-collection')
    if d['empty'] and bool(d['yielded_loans']): errors.append('empty-yield')
    if d['destroyed'] and bool(set(d['owned_items'])&set(d['invalidated_items'])): errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if d['collected'] and d['collection_end']>d['iteration_end']+1: errors.append('lending-collection')
    if d['empty'] and bool(d['yielded_loans']): errors.append('empty-yield')
    if d['destroyed'] and bool(set(d['owned_items'])&set(d['invalidated_items'])): errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

prompt:
Collected lending references survive the iteration that owns their loan.

Check iterator lifetime summaries. Yielded shared items borrow backing storage; lending items borrow the iterator until next call; mutable yields must have disjoint element footprints; next consumes the prior lending-item loan; double-ended iteration cannot yield a crossed element twice; chunked iteration retains remainder ownership; adapter closures cannot extend item lifetime; collection of lending references cannot outlive iteration; empty iterator yields no loan; iterator destruction releases its backing borrow but not independently owned items. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if d['collected'] and d['collection_end']>d['iteration_end']: errors.append('lending-collection')
    if False: errors.append('empty-yield')
    if d['destroyed'] and bool(set(d['owned_items'])&set(d['invalidated_items'])): errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

meaning: Fixture-count band, not measured model difficulty

deps: stdlib

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if d['collected'] and d['collection_end']>d['iteration_end']: errors.append('lending-collection')
    if d['empty'] and len(d['yielded_loans'])>1: errors.append('empty-yield')
    if d['destroyed'] and bool(set(d['owned_items'])&set(d['invalidated_items'])): errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

prompt:
An empty iterator summary invents a yielded borrow.

Check iterator lifetime summaries. Yielded shared items borrow backing storage; lending items borrow the iterator until next call; mutable yields must have disjoint element footprints; next consumes the prior lending-item loan; double-ended iteration cannot yield a crossed element twice; chunked iteration retains remainder ownership; adapter closures cannot extend item lifetime; collection of lending references cannot outlive iteration; empty iterator yields no loan; iterator destruction releases its backing borrow but not independently owned items. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if d['collected'] and d['collection_end']>d['iteration_end']: errors.append('lending-collection')
    if d['empty'] and bool(d['yielded_loans']): errors.append('empty-yield')
    if False: errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['yield_origins'])<=set(d['backing_origins']): errors.append('yield-origin')
    if d['lending'] and d['item_end']>d['next_point']: errors.append('lending-call-bound')
    if d['mutable'] and bool(set(d['yield_a'])&set(d['yield_b'])): errors.append('mutable-yield-disjoint')
    if d['next_called'] and d['prior_lending_live']: errors.append('next-reborrow-kill')
    if bool(set(d['front_indices'])&set(d['back_indices'])): errors.append('double-ended-crossing')
    if not set(d['remainder'])<=set(d['accounted']): errors.append('chunk-remainder')
    if d['adapter_bound']>d['item_bound']: errors.append('adapter-lifetime')
    if d['collected'] and d['collection_end']>d['iteration_end']: errors.append('lending-collection')
    if d['empty'] and bool(d['yielded_loans']): errors.append('empty-yield')
    if d['destroyed'] and len(set(d['owned_items'])&set(d['invalidated_items']))>1: errors.append('iterator-drop-owned-items')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'yield_origins': [], 'backing_origins': [], 'lending': False, 'item_end': 0, 'next_point': 0, 'yield_a': [], 'yield_b': [], 'mutable': False, 'prior_lending_live': False, 'next_called': False, 'front_indices': [], 'back_indices': [], 'remainder': [], 'accounted': [], 'adapter_bound': 0, 'item_bound': 0, 'collected': False, 'collection_end': 0, 'iteration_end': 0, 'empty': False, 'yielded_loans': [], 'destroyed': False, 'backing_live': False, 'owned_items': [], 'invalidated_items': []}
check('well formed empty obligations',solve(base),[])
check('yield-origin regression 0', solve(dict(base, **({'yield_origins':['a','b'],'backing_origins':['a']}))), ['yield-origin'])
check('yield-origin regression 1', solve(dict(base, **({'yield_origins':[N,N+1],'backing_origins':[N]}))), ['yield-origin'])
check('lending-call-bound regression 0', solve(dict(base, **({'lending':True,'item_end':N+1,'next_point':N}))), ['lending-call-bound'])
check('lending-call-bound regression 1', solve(dict(base, **({'lending':True,'item_end':N+2,'next_point':N+1}))), ['lending-call-bound'])
check('mutable-yield-disjoint regression 0', solve(dict(base, **({'mutable':True,'yield_a':[N,N+1],'yield_b':[N]}))), ['mutable-yield-disjoint'])
check('mutable-yield-disjoint regression 1', solve(dict(base, **({'mutable':True,'yield_a':[N],'yield_b':[N,N+1]}))), ['mutable-yield-disjoint'])
check('next-reborrow-kill regression 0', solve(dict(base, **({'next_called':True,'prior_lending_live':True}))), ['next-reborrow-kill'])
check('next-reborrow-kill regression 1', solve(dict(base, **({'next_called':True,'prior_lending_live':True,'next_point':N}))), ['next-reborrow-kill'])
check('double-ended-crossing regression 0', solve(dict(base, **({'front_indices':[N,N+1],'back_indices':[N+1]}))), ['double-ended-crossing'])
check('double-ended-crossing regression 1', solve(dict(base, **({'front_indices':[N],'back_indices':[N,N+1]}))), ['double-ended-crossing'])
check('chunk-remainder regression 0', solve(dict(base, **({'remainder':[N,N+1],'accounted':[N]}))), ['chunk-remainder'])
check('chunk-remainder regression 1', solve(dict(base, **({'remainder':list(range(N+1)),'accounted':[0]}))), ['chunk-remainder'])
check('adapter-lifetime regression 0', solve(dict(base, **({'adapter_bound':N+1,'item_bound':N}))), ['adapter-lifetime'])
check('adapter-lifetime regression 1', solve(dict(base, **({'adapter_bound':N+2,'item_bound':N+1}))), ['adapter-lifetime'])
check('lending-collection regression 0', solve(dict(base, **({'collected':True,'collection_end':N+1,'iteration_end':N}))), ['lending-collection'])
check('lending-collection regression 1', solve(dict(base, **({'collected':True,'collection_end':N+2,'iteration_end':N+1}))), ['lending-collection'])
check('empty-yield regression 0', solve(dict(base, **({'empty':True,'yielded_loans':['r']}))), ['empty-yield'])
check('empty-yield regression 1', solve(dict(base, **({'empty':True,'yielded_loans':[N]}))), ['empty-yield'])
check('iterator-drop-owned-items regression 0', solve(dict(base, **({'destroyed':True,'owned_items':['x'],'invalidated_items':['x']}))), ['iterator-drop-owned-items'])
check('iterator-drop-owned-items regression 1', solve(dict(base, **({'destroyed':True,'owned_items':[N],'invalidated_items':[N]}))), ['iterator-drop-owned-items'])
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)

prompt:
Destroying an iterator invalidates an independently owned yielded value.

Check iterator lifetime summaries. Yielded shared items borrow backing storage; lending items borrow the iterator until next call; mutable yields must have disjoint element footprints; next consumes the prior lending-item loan; double-ended iteration cannot yield a crossed element twice; chunked iteration retains remainder ownership; adapter closures cannot extend item lifetime; collection of lending references cannot outlive iteration; empty iterator yields no loan; iterator destruction releases its backing borrow but not independently owned items. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if False: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique'] and d['nested_mut']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
Reference freezing is treated as reversible to exclusive access.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if False: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner'] is not None and d['target_owner'] is None: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
Unsizing manufactures a new referent allocation identity.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if False: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata'] and d['array_coerce']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
Trait-object reference coercion loses the borrowed metadata witness.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if False: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']<d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
Array-to-slice borrow omits the final owned element.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if False: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_after']>d['inner_before']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
A mutable reference to a reference permits inner lifetime shortening.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access


broken_source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if False: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

source:
"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(d):
    errors=[]
    if d['source_shared'] and d['target_unique']: errors.append('freeze-direction')
    if d['source_owner']!=d['target_owner']: errors.append('unsize-owner')
    if d['unsized'] and not d['metadata']: errors.append('unsize-metadata')
    if d['array_coerce'] and d['array_size']!=d['slice_size']: errors.append('array-slice-extent')
    if d['nested_mut'] and d['inner_before']!=d['inner_after']: errors.append('nested-mut-invariance')
    if d['shared_outer'] and d['outer_after']>d['outer_before']+1: errors.append('outer-shared-shortening')
    if not set(d['intermediate'])<=set(d['recorded']): errors.append('deref-intermediates')
    if d['implicit'] and d['moving_deref']: errors.append('implicit-moving-deref')
    if not set(d['captured'])<=set(d['reified']): errors.append('function-reification-capture')
    if d['never_branch'] and bool(d['invented']): errors.append('never-no-origin')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'source_shared': False, 'target_unique': False, 'source_owner': None, 'target_owner': None, 'unsized': False, 'metadata': True, 'array_size': 0, 'slice_size': 0, 'array_coerce': False, 'nested_mut': False, 'inner_before': 0, 'inner_after': 0, 'shared_outer': False, 'outer_before': 0, 'outer_after': 0, 'intermediate': [], 'recorded': [], 'moving_deref': False, 'implicit': False, 'captured': [], 'reified': [], 'never_branch': False, 'invented': []}
check('well formed empty obligations',solve(base),[])
check('freeze-direction regression 0', solve(dict(base, **({'source_shared':True,'target_unique':True}))), ['freeze-direction'])
check('freeze-direction regression 1', solve(dict(base, **({'source_shared':True,'target_unique':True,'outer_before':N,'outer_after':N}))), ['freeze-direction'])
check('unsize-owner regression 0', solve(dict(base, **({'source_owner':'a','target_owner':'b'}))), ['unsize-owner'])
check('unsize-owner regression 1', solve(dict(base, **({'source_owner':N,'target_owner':N+1}))), ['unsize-owner'])
check('unsize-metadata regression 0', solve(dict(base, **({'unsized':True,'metadata':False}))), ['unsize-metadata'])
check('unsize-metadata regression 1', solve(dict(base, **({'unsized':True,'metadata':False,'outer_before':N,'outer_after':N}))), ['unsize-metadata'])
check('array-slice-extent regression 0', solve(dict(base, **({'array_coerce':True,'array_size':N+1,'slice_size':N}))), ['array-slice-extent'])
check('array-slice-extent regression 1', solve(dict(base, **({'array_coerce':True,'array_size':N+2,'slice_size':N+1}))), ['array-slice-extent'])
check('nested-mut-invariance regression 0', solve(dict(base, **({'nested_mut':True,'inner_before':N+1,'inner_after':N}))), ['nested-mut-invariance'])
check('nested-mut-invariance regression 1', solve(dict(base, **({'nested_mut':True,'inner_before':N+2,'inner_after':N+1}))), ['nested-mut-invariance'])
check('outer-shared-shortening regression 0', solve(dict(base, **({'shared_outer':True,'outer_before':N,'outer_after':N+1}))), ['outer-shared-shortening'])
check('outer-shared-shortening regression 1', solve(dict(base, **({'shared_outer':True,'outer_before':N+1,'outer_after':N+2}))), ['outer-shared-shortening'])
check('deref-intermediates regression 0', solve(dict(base, **({'intermediate':['a','b'],'recorded':['a']}))), ['deref-intermediates'])
check('deref-intermediates regression 1', solve(dict(base, **({'intermediate':list(range(N+1)),'recorded':[0]}))), ['deref-intermediates'])
check('implicit-moving-deref regression 0', solve(dict(base, **({'implicit':True,'moving_deref':True}))), ['implicit-moving-deref'])
check('implicit-moving-deref regression 1', solve(dict(base, **({'implicit':True,'moving_deref':True,'outer_before':N,'outer_after':N}))), ['implicit-moving-deref'])
check('function-reification-capture regression 0', solve(dict(base, **({'captured':['a','b'],'reified':['a']}))), ['function-reification-capture'])
check('function-reification-capture regression 1', solve(dict(base, **({'captured':[N,N+1],'reified':[N]}))), ['function-reification-capture'])
check('never-no-origin regression 0', solve(dict(base, **({'never_branch':True,'invented':['r']}))), ['never-no-origin'])
check('never-no-origin regression 1', solve(dict(base, **({'never_branch':True,'invented':[N]}))), ['never-no-origin'])
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)

prompt:
Shared-reference coercion extends the outer borrow lifetime.

Check reference coercion proof steps. Unique-to-shared freeze is one-way; unsizing preserves owner; trait unsizing retains metadata; array-to-slice length equals array extent; nested mutable references cannot shorten inner lifetime; shared outer references may shorten; deref coercion records every intermediate loan; implicit coercion cannot execute a moving deref; reification of a borrowed function pointer preserves captured lifetimes; never-type branch coercion contributes no invented loan. 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.

split: open-access