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 d['noescape'] and bool(d['body_escapes']): errors.append('noescape-proof')
    if False: 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 bool(d['body_escapes']): errors.append('noescape-proof')
    if 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:
Two actual positions map to one formal borrow capability.

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 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 False: 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)

meaning: Fixture-count band, not measured model difficulty

deps: stdlib

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

N = 1
observations = []
def solve(d):
    errors=[]
    if not set(d['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 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']): 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:
Call-local loans are released on normal return but retained on unwind.

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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:1}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:abs(sign)}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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 lifetime occurrence forgets contravariance inherited from its enclosing type.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {t[1]:0}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {t[1]:sign}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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 absent lifetime occurrence spuriously constrains the generic parameter.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1])]; signs=[sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

prompt:
A shared reference incorrectly makes its referent lifetime invariant.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[0,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Mutable reference lifetime is frozen together with its invariant payload.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,-sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Function result variance is flipped along with the argument.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1][:1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1][:-1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Variance inference omits the last tuple field.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[sign]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[]; signs=[]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Interior mutable storage contributes no invariance constraint.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[]; signs=[]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[0]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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 phantom ownership marker incorrectly freezes lifetime covariance.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[]; signs=[]
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1][:1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v if p not in out or out[p]==v else 0
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Opaque type variance records only one of its captured lifetime parameters.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

split: open-access


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

N = 1
observations = []
def solve(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=v
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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(tree):
    def walk(t,sign):
        kind=t[0]
        if kind=='var': return {t[1]:sign}
        if kind=='unused': return {}
        if kind=='ref': children=[('var',t[1]),t[2]]; signs=[sign,sign]
        elif kind=='mut': children=[('var',t[1]),t[2]]; signs=[sign,0]
        elif kind=='fn': children=[t[1],t[2]]; signs=[-sign,sign]
        elif kind=='tuple': children=t[1]; signs=[sign]*len(children)
        elif kind=='cell': children=[t[1]]; signs=[0]
        elif kind=='phantom': children=[t[1]]; signs=[sign]
        elif kind=='array': children=[t[1]]; signs=[sign]
        elif kind=='opaque': children=[('var',p) for p in t[1]]; signs=[0]*len(children)
        else: return {}
        out={}
        for child,s in zip(children,signs):
            for p,v in walk(child,s).items():
                out[p]=out.get(p,v)
        return out
    return walk(tree,1)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('variable',solve(('var','a')),{'a':1})
check('unused',solve(('unused','a')), {})
check('shared',solve(('ref','a',('var','b'))),{'a':1,'b':1})
check('mutable',solve(('mut','a',('var','b'))),{'a':1,'b':0})
check('function',solve(('fn',('var','a'),('var','b'))),{'a':-1,'b':1})
check('tuple',solve(('tuple',[('var','a'),('var','b')])),{'a':1,'b':1})
check('cell',solve(('cell',('var','a'))),{'a':0})
check('phantom',solve(('phantom',('var','a'))),{'a':1})
check('opaque',solve(('opaque',['a','b'])),{'a':0,'b':0})
check('both positions',solve(('fn',('var','a'),('var','a'))),{'a':0})
check('array',solve(('array',('var','a'),N)),{'a':1})
check('variable arity',solve(('tuple',[('var',str(i)) for i in range(N+1)])),{str(i):1 for i in range(N+1)})
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:
Repeated covariant and contravariant occurrences fail to join to invariance.

Infer lifetime parameter variance in a toy type tree. Variance signs are +1 covariant, -1 contravariant, 0 invariant; repeated different signs join to invariant. var(name); ref(lifetime,type) covariant both; mut(lifetime,type) covariant lifetime invariant payload; fn(argument,result) flips argument; tuple(list) joins; cell(type) invariant; phantom(type) covariant; array(type,length) covariant; opaque(parameters) invariant for every listed parameter; unused(name) contributes nothing. Return parameter-to-sign map.

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('bound-index-range')
    if d['after']!=[i+d['crossed'] for i in d['before']]: errors.append('capture-avoiding-shift')
    if d['fresh']<=d['caller']: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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 any(i<0 or i>d['arity'] for i in d['indices']): errors.append('bound-index-range')
    if d['after']!=[i+d['crossed'] for i in d['before']]: errors.append('capture-avoiding-shift')
    if d['fresh']<=d['caller']: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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:
The first out-of-range bound lifetime is accepted at the binder arity.

Check higher-ranked borrow instantiation using de Bruijn binder depths and universes. Bound occurrence index less than binder arity; substitutions shift free lifetimes when crossing binders; fresh universes strictly exceed caller universe; existential solutions cannot mention newer universes; universally quantified input must be checked for every listed placeholder; alpha renaming preserves equal occurrences; distinct bound parameters remain distinct; dropping a binder decrements outside indices; bound lifetimes cannot be selected as static; placeholder obligations cannot be discharged by one concrete lifetime. 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 any(i<0 or i>=d['arity'] for i in d['indices']): errors.append('bound-index-range')
    if False: errors.append('capture-avoiding-shift')
    if d['fresh']<=d['caller']: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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 any(i<0 or i>=d['arity'] for i in d['indices']): errors.append('bound-index-range')
    if len(d['after'])!=len(d['before']): errors.append('capture-avoiding-shift')
    if d['fresh']<=d['caller']: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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:
Lifetime substitution fails to shift free indices across a nested binder.

Check higher-ranked borrow instantiation using de Bruijn binder depths and universes. Bound occurrence index less than binder arity; substitutions shift free lifetimes when crossing binders; fresh universes strictly exceed caller universe; existential solutions cannot mention newer universes; universally quantified input must be checked for every listed placeholder; alpha renaming preserves equal occurrences; distinct bound parameters remain distinct; dropping a binder decrements outside indices; bound lifetimes cannot be selected as static; placeholder obligations cannot be discharged by one concrete lifetime. 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 any(i<0 or i>=d['arity'] for i in d['indices']): errors.append('bound-index-range')
    if d['after']!=[i+d['crossed'] for i in d['before']]: errors.append('capture-avoiding-shift')
    if False: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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 any(i<0 or i>=d['arity'] for i in d['indices']): errors.append('bound-index-range')
    if d['after']!=[i+d['crossed'] for i in d['before']]: errors.append('capture-avoiding-shift')
    if d['fresh']<d['caller']: errors.append('fresh-universe')
    if any(u>d['existential_universe'] for u in d['solution_universes']): errors.append('universe-leak')
    if not set(d['placeholders'])<=set(d['checked']): errors.append('universal-coverage')
    if any(d['renaming'][a]!=d['renaming'][b] for a,b in d['equal_pairs']): errors.append('alpha-equality')
    if any(d['renaming'][a]==d['renaming'][b] for a,b in d['distinct_pairs']): errors.append('alpha-distinctness')
    if d['outside_after']!=[i-1 for i in d['outside_before']]: errors.append('binder-pop')
    if bool(set(d['static_choices'])&set(d['bound'])): errors.append('static-skolem')
    if d['universal_obligation'] and d['concrete_only']: errors.append('concrete-universal')
    return errors
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
base={'indices': [], 'arity': 0, 'crossed': 0, 'before': [], 'after': [], 'fresh': 1, 'caller': 0, 'solution_universes': [], 'existential_universe': 0, 'placeholders': [], 'checked': [], 'equal_pairs': [], 'renaming': {}, 'distinct_pairs': [], 'outside_before': [], 'outside_after': [], 'static_choices': [], 'bound': [], 'universal_obligation': False, 'concrete_only': False}
check('well formed empty obligations',solve(base),[])
check('bound-index-range regression 0', solve(dict(base, **({'indices':[N],'arity':N}))), ['bound-index-range'])
check('bound-index-range regression 1', solve(dict(base, **({'indices':[N+1],'arity':N+1}))), ['bound-index-range'])
check('capture-avoiding-shift regression 0', solve(dict(base, **({'before':[N],'after':[N],'crossed':1}))), ['capture-avoiding-shift'])
check('capture-avoiding-shift regression 1', solve(dict(base, **({'before':[N,N+1],'after':[N,N+1],'crossed':2}))), ['capture-avoiding-shift'])
check('fresh-universe regression 0', solve(dict(base, **({'fresh':N,'caller':N}))), ['fresh-universe'])
check('fresh-universe regression 1', solve(dict(base, **({'fresh':N+1,'caller':N+1}))), ['fresh-universe'])
check('universe-leak regression 0', solve(dict(base, **({'solution_universes':[N+1],'existential_universe':N}))), ['universe-leak'])
check('universe-leak regression 1', solve(dict(base, **({'solution_universes':[N+2],'existential_universe':N+1}))), ['universe-leak'])
check('universal-coverage regression 0', solve(dict(base, **({'placeholders':['a','b'],'checked':['a']}))), ['universal-coverage'])
check('universal-coverage regression 1', solve(dict(base, **({'placeholders':list(range(N+1)),'checked':[0]}))), ['universal-coverage'])
check('alpha-equality regression 0', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':0,'b':1}}))), ['alpha-equality'])
check('alpha-equality regression 1', solve(dict(base, **({'equal_pairs':[('a','a'),('a','b')],'renaming':{'a':N,'b':N+1}}))), ['alpha-equality'])
check('alpha-distinctness regression 0', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':0,'b':1,'c':1}}))), ['alpha-distinctness'])
check('alpha-distinctness regression 1', solve(dict(base, **({'distinct_pairs':[('a','b'),('b','c')],'renaming':{'a':N,'b':N+1,'c':N+1}}))), ['alpha-distinctness'])
check('binder-pop regression 0', solve(dict(base, **({'outside_before':[N],'outside_after':[N]}))), ['binder-pop'])
check('binder-pop regression 1', solve(dict(base, **({'outside_before':[N+1],'outside_after':[N+1]}))), ['binder-pop'])
check('static-skolem regression 0', solve(dict(base, **({'static_choices':['a'],'bound':['a']}))), ['static-skolem'])
check('static-skolem regression 1', solve(dict(base, **({'static_choices':[N],'bound':[N]}))), ['static-skolem'])
check('concrete-universal regression 0', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':['a']}))), ['concrete-universal'])
check('concrete-universal regression 1', solve(dict(base, **({'universal_obligation':True,'concrete_only':True,'checked':[N]}))), ['concrete-universal'])
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:
Higher-ranked instantiation reuses the caller universe.

Check higher-ranked borrow instantiation using de Bruijn binder depths and universes. Bound occurrence index less than binder arity; substitutions shift free lifetimes when crossing binders; fresh universes strictly exceed caller universe; existential solutions cannot mention newer universes; universally quantified input must be checked for every listed placeholder; alpha renaming preserves equal occurrences; distinct bound parameters remain distinct; dropping a binder decrements outside indices; bound lifetimes cannot be selected as static; placeholder obligations cannot be discharged by one concrete lifetime. 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