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 d['ended_child'] and bool(d['ended_ancestors']): errors.append('child-end-locality')
    if False: 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 bool(d['ended_ancestors']): errors.append('child-end-locality')
    if d['killed_parent'] and len(d['surviving_descendants'])>1: 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:
Killing an origin leaves a descendant loan statically usable.

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 False: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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 d['activated'] and not d['reserved'] and d['activation_id'] is None: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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:
Activation accepts an identified loan with no reservation event.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if False: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates'] and not d['reserved']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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 reservation on one branch is assumed to dominate activation after a join.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if False: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id'] is None: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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:
Activation upgrades a different loan than the reserved receiver.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if False: errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if len(d['reserved_writes'])>1: errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

prompt:
An unactivated reservation is usable as a mutable reference.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if False: errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and len(d['shared_at_activation'])>1: errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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 argument loan remains live when the receiver reservation activates.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if False: errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if set(d['storage_dead'])==set(d['reservation_points']) and bool(d['storage_dead']): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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:
Reservation liveness crosses destruction of the receiver storage.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if False: errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])>2 and len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
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:
One path activates the same two-phase loan twice.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.

split: open-access


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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if False: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

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

N = 1
observations = []
def solve(d):
    errors=[]
    if d['activated'] and not d['reserved']: errors.append('reservation-required')
    if d['activated'] and not d['dominates']: errors.append('reservation-dominance')
    if d['activated'] and d['reservation_id']!=d['activation_id']: errors.append('activation-identity')
    if bool(d['reserved_writes']): errors.append('reserved-write')
    if d['activated'] and bool(d['shared_at_activation']): errors.append('activation-shared-conflict')
    if bool(set(d['storage_dead'])&set(d['reservation_points'])): errors.append('reservation-storage')
    if len(d['activations'])!=len(set(d['activations'])): errors.append('single-activation')
    if d['two_phase'] and not d['auto_receiver'] and d['activated']: errors.append('eligible-auto-borrow')
    if d['activation_point']<d['argument_end']: errors.append('argument-before-activation')
    if d['canceled'] and d['reservation_live']: errors.append('cancellation-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'activated': False, 'reserved': False, 'dominates': True, 'reservation_id': None, 'activation_id': None, 'reserved_writes': [], 'shared_at_activation': [], 'storage_dead': [], 'reservation_points': [], 'activations': [], 'auto_receiver': True, 'two_phase': False, 'argument_end': 0, 'activation_point': 0, 'canceled': False, 'reservation_live': False}
check('well formed empty obligations',solve(base),[])
check('reservation-required regression 0', solve(dict(base, **({'activated':True,'activation_id':'a','reservation_id':'a'}))), ['reservation-required'])
check('reservation-required regression 1', solve(dict(base, **({'activated':True,'activation_id':N,'reservation_id':N}))), ['reservation-required'])
check('reservation-dominance regression 0', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False}))), ['reservation-dominance'])
check('reservation-dominance regression 1', solve(dict(base, **({'activated':True,'reserved':True,'dominates':False,'activation_point':N}))), ['reservation-dominance'])
check('activation-identity regression 0', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':'a','activation_id':'b'}))), ['activation-identity'])
check('activation-identity regression 1', solve(dict(base, **({'activated':True,'reserved':True,'reservation_id':N,'activation_id':N+1}))), ['activation-identity'])
check('reserved-write regression 0', solve(dict(base, **({'reserved_writes':[N]}))), ['reserved-write'])
check('reserved-write regression 1', solve(dict(base, **({'reserved_writes':[N+1]}))), ['reserved-write'])
check('activation-shared-conflict regression 0', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':['r']}))), ['activation-shared-conflict'])
check('activation-shared-conflict regression 1', solve(dict(base, **({'activated':True,'reserved':True,'shared_at_activation':[N]}))), ['activation-shared-conflict'])
check('reservation-storage regression 0', solve(dict(base, **({'storage_dead':[N],'reservation_points':[N,N+1]}))), ['reservation-storage'])
check('reservation-storage regression 1', solve(dict(base, **({'storage_dead':[N,N+1],'reservation_points':[N]}))), ['reservation-storage'])
check('single-activation regression 0', solve(dict(base, **({'activations':['r','r']}))), ['single-activation'])
check('single-activation regression 1', solve(dict(base, **({'activations':[N,N]}))), ['single-activation'])
check('eligible-auto-borrow regression 0', solve(dict(base, **({'two_phase':True,'auto_receiver':False}))), ['eligible-auto-borrow'])
check('eligible-auto-borrow regression 1', solve(dict(base, **({'two_phase':True,'auto_receiver':False,'argument_end':0,'activation_point':N}))), ['eligible-auto-borrow'])
check('argument-before-activation regression 0', solve(dict(base, **({'activation_point':N,'argument_end':N+1}))), ['argument-before-activation'])
check('argument-before-activation regression 1', solve(dict(base, **({'activation_point':N+1,'argument_end':N+2}))), ['argument-before-activation'])
check('cancellation-release regression 0', solve(dict(base, **({'canceled':True,'reservation_live':True}))), ['cancellation-release'])
check('cancellation-release regression 1', solve(dict(base, **({'canceled':True,'reservation_live':True,'activation_point':N}))), ['cancellation-release'])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

prompt:
An explicit mutable borrow receives receiver-only reservation semantics.

Validate reservation/activation facts of a toy two-phase mutable loan. Activation requires prior reservation, dominance and same loan identity. Reserved loan cannot be written through. Shared reads may exist during reservation but not activation. Reservation cannot cross storage death. Activation occurs at most once per path. Only compiler-generated method receiver auto-borrows may be two-phase. Argument evaluation must complete before activation. Canceled calls must release reservations. 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