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 d['two_phase'] and not d['auto_receiver']: errors.append('eligible-auto-borrow')
    if False: 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']: errors.append('eligible-auto-borrow')
    if d['activation_point']+1<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:
Receiver reservation activates before the last argument evaluation step.

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 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 False: 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']: 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'] and d['activated']: 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 canceled method call leaves its unactivated reservation live.

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 False: errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 bool(d['body_reads']) and d['body_reads'][0] not in d['reads']: errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 callee summary omits a later borrowed read effect.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if False: errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not d['writes'] and bool(d['body_writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 callee write summary loses one mutated borrowed parameter.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if False: errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if set(d['body_moves']).isdisjoint(d['moves']) and bool(d['body_moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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:
Moving one actual is hidden by another correctly summarized move.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if False: errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not d['escapes'] and bool(d['body_escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 borrow retained by the callee is omitted from its escape summary.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if False: errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not d['unique_actuals'] and bool(d['writes']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 write effect is instantiated on an actual without exclusive permission.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if False: errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not d['return_origins'] and bool(d['body_return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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:
Return alias summary chooses one of multiple parameter origins.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if False: errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not d['retained'] and bool(d['actual_refs']): errors.append('unknown-retention')
    if d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 unresolved call releases some actual borrows without a proven summary.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if False: errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 not set(d['body_reads'])<=set(d['reads']): errors.append('read-summary')
    if not set(d['body_writes'])<=set(d['writes']): errors.append('write-summary')
    if not set(d['body_moves'])<=set(d['moves']): errors.append('move-summary')
    if not set(d['body_escapes'])<=set(d['escapes']): errors.append('escape-summary')
    if not set(d['writes'])<=set(d['unique_actuals']): errors.append('unique-actual')
    if not set(d['body_return_origins'])<=set(d['return_origins']): errors.append('return-origin-summary')
    if d['unknown'] and not set(d['actual_refs'])<=set(d['retained']): errors.append('unknown-retention')
    if d['noescape'] and len(d['body_escapes'])>1: errors.append('noescape-proof')
    if len(d['mapping'])!=len(set(d['mapping'])) or set(d['mapping'])!=set(d['formals']): errors.append('formal-map-bijection')
    if not set(d['call_loans'])<=set(d['released_normal']) or not set(d['call_loans'])<=set(d['released_unwind']): errors.append('unwind-release')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'body_reads': [], 'reads': [], 'body_writes': [], 'writes': [], 'body_moves': [], 'moves': [], 'body_escapes': [], 'escapes': [], 'unique_actuals': [], 'return_origins': [], 'body_return_origins': [], 'unknown': False, 'actual_refs': [], 'retained': [], 'noescape': False, 'mapping': [], 'formals': [], 'call_loans': [], 'released_normal': [], 'released_unwind': []}
check('well formed empty obligations',solve(base),[])
check('read-summary regression 0', solve(dict(base, **({'body_reads':['a','b'],'reads':['a']}))), ['read-summary'])
check('read-summary regression 1', solve(dict(base, **({'body_reads':[N,N+1],'reads':[N]}))), ['read-summary'])
check('write-summary regression 0', solve(dict(base, **({'body_writes':['a','b'],'writes':['a'],'unique_actuals':['a']}))), ['write-summary'])
check('write-summary regression 1', solve(dict(base, **({'body_writes':[N,N+1],'writes':[N],'unique_actuals':[N]}))), ['write-summary'])
check('move-summary regression 0', solve(dict(base, **({'body_moves':['a','b'],'moves':['a']}))), ['move-summary'])
check('move-summary regression 1', solve(dict(base, **({'body_moves':[N,N+1],'moves':[N]}))), ['move-summary'])
check('escape-summary regression 0', solve(dict(base, **({'body_escapes':['a','b'],'escapes':['a']}))), ['escape-summary'])
check('escape-summary regression 1', solve(dict(base, **({'body_escapes':[N,N+1],'escapes':[N]}))), ['escape-summary'])
check('unique-actual regression 0', solve(dict(base, **({'writes':['a','b'],'unique_actuals':['a']}))), ['unique-actual'])
check('unique-actual regression 1', solve(dict(base, **({'writes':[N],'unique_actuals':[N+1]}))), ['unique-actual'])
check('return-origin-summary regression 0', solve(dict(base, **({'body_return_origins':['a','b'],'return_origins':['a']}))), ['return-origin-summary'])
check('return-origin-summary regression 1', solve(dict(base, **({'body_return_origins':[N,N+1],'return_origins':[N]}))), ['return-origin-summary'])
check('unknown-retention regression 0', solve(dict(base, **({'unknown':True,'actual_refs':['a','b'],'retained':['a']}))), ['unknown-retention'])
check('unknown-retention regression 1', solve(dict(base, **({'unknown':True,'actual_refs':[N,N+1],'retained':[N]}))), ['unknown-retention'])
check('noescape-proof regression 0', solve(dict(base, **({'noescape':True,'body_escapes':['r'],'escapes':['r']}))), ['noescape-proof'])
check('noescape-proof regression 1', solve(dict(base, **({'noescape':True,'body_escapes':[N],'escapes':[N]}))), ['noescape-proof'])
check('formal-map-bijection regression 0', solve(dict(base, **({'mapping':['a','a'],'formals':['a']}))), ['formal-map-bijection'])
check('formal-map-bijection regression 1', solve(dict(base, **({'mapping':[N,N],'formals':[N]}))), ['formal-map-bijection'])
check('unwind-release regression 0', solve(dict(base, **({'call_loans':['r'],'released_normal':['r']}))), ['unwind-release'])
check('unwind-release regression 1', solve(dict(base, **({'call_loans':[N],'released_normal':[N]}))), ['unwind-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 noescape contract tolerates one escaping borrowed argument.

Validate a callee borrow effect summary against observed static body effects. Reads, writes, moves and escapes are separate effect sets; writes require unique actuals; a returned alias must list every possible argument origin; unknown callees conservatively retain actual references; a noescape assertion excludes body escapes; argument-to-formal mapping must be a bijection over expected formals; normal and unwind exits both release declared call-local loans. 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