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

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['uses'])<=set(d['alive']): errors.append('temporary-use')
    if d['arg_end']>d['call_end']: errors.append('argument-scope')
    if d['let_extended'] and d['temp_end']!=d['block_end']: errors.append('let-extension')
    if d['assignment_extended']: errors.append('assignment-no-extension')
    if d['operand_end']<d['expr_end']: errors.append('operand-expression')
    if d['condition'] and bool(d['then_uses']): errors.append('condition-escape')
    if d['rhs_created'] and not d['rhs_executed']: errors.append('short-circuit-creation')
    if not set(d['drop_uses'])<=set(d['alive']): errors.append('destructor-use')
    if d['promoted'] and not d['static_storage']: errors.append('promotion-storage')
    if False: errors.append('bound-owner-scope')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'uses': [], 'alive': [], 'call_end': 0, 'arg_end': 0, 'let_extended': False, 'temp_end': 0, 'block_end': 0, 'assignment_extended': False, 'expr_end': 0, 'operand_end': 0, 'condition': False, 'then_uses': [], 'rhs_created': False, 'rhs_executed': True, 'drop_uses': [], 'promoted': False, 'static_storage': True, 'owner_end': 0, 'bound_temp_end': 0}
check('well formed empty obligations',solve(base),[])
check('temporary-use regression 0', solve(dict(base, **({'uses':[N],'alive':[N+1]}))), ['temporary-use'])
check('temporary-use regression 1', solve(dict(base, **({'uses':[N,N+1],'alive':[N+1,N+2]}))), ['temporary-use'])
check('argument-scope regression 0', solve(dict(base, **({'arg_end':N+1,'call_end':N}))), ['argument-scope'])
check('argument-scope regression 1', solve(dict(base, **({'arg_end':N+2,'call_end':N+1}))), ['argument-scope'])
check('let-extension regression 0', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+1}))), ['let-extension'])
check('let-extension regression 1', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+2}))), ['let-extension'])
check('assignment-no-extension regression 0', solve(dict(base, **({'assignment_extended':True}))), ['assignment-no-extension'])
check('assignment-no-extension regression 1', solve(dict(base, **({'assignment_extended':True,'block_end':N}))), ['assignment-no-extension'])
check('operand-expression regression 0', solve(dict(base, **({'operand_end':N,'expr_end':N+1}))), ['operand-expression'])
check('operand-expression regression 1', solve(dict(base, **({'operand_end':N+1,'expr_end':N+2}))), ['operand-expression'])
check('condition-escape regression 0', solve(dict(base, **({'condition':True,'then_uses':[N]}))), ['condition-escape'])
check('condition-escape regression 1', solve(dict(base, **({'condition':True,'then_uses':[N+1]}))), ['condition-escape'])
check('short-circuit-creation regression 0', solve(dict(base, **({'rhs_created':True,'rhs_executed':False}))), ['short-circuit-creation'])
check('short-circuit-creation regression 1', solve(dict(base, **({'rhs_created':True,'rhs_executed':False,'expr_end':N,'operand_end':N}))), ['short-circuit-creation'])
check('destructor-use regression 0', solve(dict(base, **({'drop_uses':[N+1],'alive':[N]}))), ['destructor-use'])
check('destructor-use regression 1', solve(dict(base, **({'drop_uses':[N,N+1],'alive':[N]}))), ['destructor-use'])
check('promotion-storage regression 0', solve(dict(base, **({'promoted':True,'static_storage':False}))), ['promotion-storage'])
check('promotion-storage regression 1', solve(dict(base, **({'promoted':True,'static_storage':False,'block_end':N}))), ['promotion-storage'])
check('bound-owner-scope regression 0', solve(dict(base, **({'bound_temp_end':N,'owner_end':N+1}))), ['bound-owner-scope'])
check('bound-owner-scope regression 1', solve(dict(base, **({'bound_temp_end':N+1,'owner_end':N+2}))), ['bound-owner-scope'])
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['uses'])<=set(d['alive']): errors.append('temporary-use')
    if d['arg_end']>d['call_end']: errors.append('argument-scope')
    if d['let_extended'] and d['temp_end']!=d['block_end']: errors.append('let-extension')
    if d['assignment_extended']: errors.append('assignment-no-extension')
    if d['operand_end']<d['expr_end']: errors.append('operand-expression')
    if d['condition'] and bool(d['then_uses']): errors.append('condition-escape')
    if d['rhs_created'] and not d['rhs_executed']: errors.append('short-circuit-creation')
    if not set(d['drop_uses'])<=set(d['alive']): errors.append('destructor-use')
    if d['promoted'] and not d['static_storage']: errors.append('promotion-storage')
    if d['bound_temp_end']+1<d['owner_end']: errors.append('bound-owner-scope')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'uses': [], 'alive': [], 'call_end': 0, 'arg_end': 0, 'let_extended': False, 'temp_end': 0, 'block_end': 0, 'assignment_extended': False, 'expr_end': 0, 'operand_end': 0, 'condition': False, 'then_uses': [], 'rhs_created': False, 'rhs_executed': True, 'drop_uses': [], 'promoted': False, 'static_storage': True, 'owner_end': 0, 'bound_temp_end': 0}
check('well formed empty obligations',solve(base),[])
check('temporary-use regression 0', solve(dict(base, **({'uses':[N],'alive':[N+1]}))), ['temporary-use'])
check('temporary-use regression 1', solve(dict(base, **({'uses':[N,N+1],'alive':[N+1,N+2]}))), ['temporary-use'])
check('argument-scope regression 0', solve(dict(base, **({'arg_end':N+1,'call_end':N}))), ['argument-scope'])
check('argument-scope regression 1', solve(dict(base, **({'arg_end':N+2,'call_end':N+1}))), ['argument-scope'])
check('let-extension regression 0', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+1}))), ['let-extension'])
check('let-extension regression 1', solve(dict(base, **({'let_extended':True,'temp_end':N,'block_end':N+2}))), ['let-extension'])
check('assignment-no-extension regression 0', solve(dict(base, **({'assignment_extended':True}))), ['assignment-no-extension'])
check('assignment-no-extension regression 1', solve(dict(base, **({'assignment_extended':True,'block_end':N}))), ['assignment-no-extension'])
check('operand-expression regression 0', solve(dict(base, **({'operand_end':N,'expr_end':N+1}))), ['operand-expression'])
check('operand-expression regression 1', solve(dict(base, **({'operand_end':N+1,'expr_end':N+2}))), ['operand-expression'])
check('condition-escape regression 0', solve(dict(base, **({'condition':True,'then_uses':[N]}))), ['condition-escape'])
check('condition-escape regression 1', solve(dict(base, **({'condition':True,'then_uses':[N+1]}))), ['condition-escape'])
check('short-circuit-creation regression 0', solve(dict(base, **({'rhs_created':True,'rhs_executed':False}))), ['short-circuit-creation'])
check('short-circuit-creation regression 1', solve(dict(base, **({'rhs_created':True,'rhs_executed':False,'expr_end':N,'operand_end':N}))), ['short-circuit-creation'])
check('destructor-use regression 0', solve(dict(base, **({'drop_uses':[N+1],'alive':[N]}))), ['destructor-use'])
check('destructor-use regression 1', solve(dict(base, **({'drop_uses':[N,N+1],'alive':[N]}))), ['destructor-use'])
check('promotion-storage regression 0', solve(dict(base, **({'promoted':True,'static_storage':False}))), ['promotion-storage'])
check('promotion-storage regression 1', solve(dict(base, **({'promoted':True,'static_storage':False,'block_end':N}))), ['promotion-storage'])
check('bound-owner-scope regression 0', solve(dict(base, **({'bound_temp_end':N,'owner_end':N+1}))), ['bound-owner-scope'])
check('bound-owner-scope regression 1', solve(dict(base, **({'bound_temp_end':N+1,'owner_end':N+2}))), ['bound-owner-scope'])
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 named owner is still dropped at its original temporary boundary.

Check temporary storage scopes using statement, block and full-expression integer boundaries. A borrowed temporary must cover use points; ordinary call arguments end at call boundary; let reference initializers may extend to block end but assignment RHS may not; operand temporaries end after enclosing expression; condition temporaries cannot leak into the then block; short-circuit RHS temporaries exist only on executed branch; a destructor observation is a use point; a reference to a promoted constant uses static storage; explicit owner binding prevents premature temporary destruction. 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('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 bool(d['parents']) and next(iter(d['parents'].values())) not in d['declared']: errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 reborrow parent is unresolved after the first child declaration.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if False: errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>2 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 short reborrow ancestry cycle is accepted as a valid loan forest.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if False: errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if len(d['child_points'])>len(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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:
Reborrow lifetime can shift beyond the parent loan while keeping equal size.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if False: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique'] and not d['parent_points']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 shared parent manufactures an exclusive child capability.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if False: errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if set(d['parent_use'])==set(d['unique_child_use']) and bool(d['parent_use']): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 unique child only suspends parent access when their use regions are identical.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if False: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if bool(d['child_place']) and bool(d['parent_place']) and d['child_place'][0]!=d['parent_place'][0]: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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 reborrow projects from a sibling of the authorized parent place.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if False: errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if len(set(d['bypassed'])&set(d['suspended']))>1: errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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:
Nested reborrow bypasses the suspended immediate parent loan.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if False: errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if set(d['sibling_a'])==set(d['sibling_b']) and bool(d['sibling_a']): errors.append('sibling-regions')
    if d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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:
Distinct sibling exclusive reborrows overlap at a shared program point.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if False: errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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['parents'].values())<=set(d['declared']): errors.append('parent-resolution')
    if any(len(x)>0 for x in d['cycles']): errors.append('lineage-cycle')
    if not set(d['child_points'])<=set(d['parent_points']): errors.append('child-region')
    if d['child_mut'] and not d['parent_unique']: errors.append('permission-inheritance')
    if bool(set(d['parent_use'])&set(d['unique_child_use'])): errors.append('parent-suspension')
    if d['child_place'][:len(d['parent_place'])]!=d['parent_place']: errors.append('place-descent')
    if bool(set(d['bypassed'])&set(d['suspended'])): errors.append('intermediate-suspension')
    if bool(set(d['sibling_a'])&set(d['sibling_b'])): errors.append('sibling-regions')
    if d['ended_child'] and len(d['ended_ancestors'])>1: errors.append('child-end-locality')
    if d['killed_parent'] and bool(d['surviving_descendants']): errors.append('parent-kill-cascade')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'parents': {}, 'declared': [], 'cycles': [], 'child_points': [], 'parent_points': [], 'child_mut': False, 'parent_unique': True, 'parent_use': [], 'unique_child_use': [], 'child_place': [], 'parent_place': [], 'bypassed': [], 'suspended': [], 'sibling_a': [], 'sibling_b': [], 'ended_child': False, 'ended_ancestors': [], 'killed_parent': False, 'surviving_descendants': []}
check('well formed empty obligations',solve(base),[])
check('parent-resolution regression 0', solve(dict(base, **({'parents':{'c':'p','d':'q'},'declared':['p']}))), ['parent-resolution'])
check('parent-resolution regression 1', solve(dict(base, **({'parents':{N:'p',N+1:'q'},'declared':['p']}))), ['parent-resolution'])
check('lineage-cycle regression 0', solve(dict(base, **({'cycles':[['a','b']]}))), ['lineage-cycle'])
check('lineage-cycle regression 1', solve(dict(base, **({'cycles':[[N]]}))), ['lineage-cycle'])
check('child-region regression 0', solve(dict(base, **({'child_points':[N],'parent_points':[N+1]}))), ['child-region'])
check('child-region regression 1', solve(dict(base, **({'child_points':[N,N+1],'parent_points':[N+1,N+2]}))), ['child-region'])
check('permission-inheritance regression 0', solve(dict(base, **({'child_mut':True,'parent_unique':False}))), ['permission-inheritance'])
check('permission-inheritance regression 1', solve(dict(base, **({'child_mut':True,'parent_unique':False,'parent_points':list(range(N))}))), ['permission-inheritance'])
check('parent-suspension regression 0', solve(dict(base, **({'parent_use':[N,N+1],'unique_child_use':[N]}))), ['parent-suspension'])
check('parent-suspension regression 1', solve(dict(base, **({'parent_use':[N],'unique_child_use':[N,N+1]}))), ['parent-suspension'])
check('place-descent regression 0', solve(dict(base, **({'child_place':['r','b'],'parent_place':['r','a']}))), ['place-descent'])
check('place-descent regression 1', solve(dict(base, **({'child_place':['r',N+1],'parent_place':['r',N]}))), ['place-descent'])
check('intermediate-suspension regression 0', solve(dict(base, **({'bypassed':['p'],'suspended':['p']}))), ['intermediate-suspension'])
check('intermediate-suspension regression 1', solve(dict(base, **({'bypassed':[N],'suspended':[N]}))), ['intermediate-suspension'])
check('sibling-regions regression 0', solve(dict(base, **({'sibling_a':[N,N+1],'sibling_b':[N+1]}))), ['sibling-regions'])
check('sibling-regions regression 1', solve(dict(base, **({'sibling_a':[N],'sibling_b':[N,N+1]}))), ['sibling-regions'])
check('child-end-locality regression 0', solve(dict(base, **({'ended_child':True,'ended_ancestors':['p']}))), ['child-end-locality'])
check('child-end-locality regression 1', solve(dict(base, **({'ended_child':True,'ended_ancestors':[N]}))), ['child-end-locality'])
check('parent-kill-cascade regression 0', solve(dict(base, **({'killed_parent':True,'surviving_descendants':['c']}))), ['parent-kill-cascade'])
check('parent-kill-cascade regression 1', solve(dict(base, **({'killed_parent':True,'surviving_descendants':[N]}))), ['parent-kill-cascade'])
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:
Ending a reborrow invalidates its still-live ancestor reference.

Check statically resolved reborrow chains. Every child has declared parent; chains acyclic; child lifetime subset of parent; mutable child requires unique parent permission; parent use cannot overlap child unique-use points; child place must descend from parent place; nested child cannot bypass suspended intermediate parent; sibling unique reborrows may not overlap points; ending a child does not end its ancestors; killing a parent kills all descendants. Descriptor supplies inferred facts and requested proof obligations. 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