FA-89946 / Bytecode virtual machines / Open access
Call frames: return resumes at the caller's own return address · case 01
Returns from nested calls jump to the grandparent's continuation or fault at top level.
ROOT CAUSE
After popping the callee, the resume pc is read from the new top frame instead of the popped frame.
VERIFIED REPAIR
Resume at the return address saved in the frame being popped.
Unsuccessful approach: Falling back only when the caller has no saved pc still picks the wrong frame for nested calls.
Case contract
Instructions: push v, load k, store k, add/sub/mul (second-from-top op top), jz t, jmp t, call t nargs nlocals, ret, halt. call pops nargs values (the first pushed becomes local 0), appends zero locals up to nlocals, records return pc = call pc + 1, and raises ["StackOverflowError", frames] when the frame count already equals max_depth. ret pops the result, discards the callee frame, pushes the result on the caller stack and resumes at the saved pc. Each executed instruction costs one fuel; running out returns ["fuel", pc]; host faults are ["vm-fault"].
Why this case matters
Frame setup and teardown decide argument binding, return values and recursion limits in every stack VM.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, max_depth, fuel):
def run():
frames = [{'locals': [0] * 4, 'stack': [], 'ret': None}]
pc = 0
for _ in range(fuel):
f = frames[-1]
ins = code[pc]
op = ins[0]
if op == 'push':
f['stack'].append(ins[1])
pc += 1
elif op == 'load':
f['stack'].append(f['locals'][ins[1]])
pc += 1
elif op == 'store':
f['locals'][ins[1]] = f['stack'].pop()
pc += 1
elif op in ('add', 'sub', 'mul'):
b = f['stack'].pop()
a = f['stack'].pop()
f['stack'].append(a + b if op == 'add' else a - b if op == 'sub' else a * b)
pc += 1
elif op == 'jz':
pc = ins[1] if f['stack'].pop() == 0 else pc + 1
elif op == 'jmp':
pc = ins[1]
elif op == 'call':
target, nargs, nlocals = ins[1], ins[2], ins[3]
if len(frames) >= max_depth:
return ['StackOverflowError', len(frames)]
args = f['stack'][len(f['stack']) - nargs:]
del f['stack'][len(f['stack']) - nargs:]
frames.append({'locals': args + [0] * (nlocals - nargs), 'stack': [], 'ret': pc + 1})
pc = target
elif op == 'ret':
value = f['stack'].pop()
frames.pop()
frames[-1]['stack'].append(value)
pc = frames[-1]['ret']
else:
return ['halt', f['stack']]
return ['fuel', pc]
try:
return run()
except (IndexError, TypeError):
return ['vm-fault']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('two-argument call binds first argument to slot 0',
([['push', 21], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [18]]),
('zero-argument call keeps caller operand stack',
([['push', 8], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [3]]),
('extra locals are zero-initialised after arguments',
([['push', 1],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [4]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 22], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [19]]),
('zero-argument call keeps caller operand stack',
([['push', 9], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [4]]),
('extra locals are zero-initialised after arguments',
([['push', 2],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [10]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 23], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [20]]),
('zero-argument call keeps caller operand stack',
([['push', 10], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [5]]),
('extra locals are zero-initialised after arguments',
([['push', 3],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [18]]),
('regression: recursive factorial',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [2]]),
('recursion depth exactly at the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['halt', [2]]),
('recursion one frame over the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
3,
500),
['StackOverflowError', 3]),
('control: fuel exhaustion',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 24], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [21]]),
('zero-argument call keeps caller operand stack',
([['push', 11], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [6]]),
('extra locals are zero-initialised after arguments',
([['push', 4],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [28]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 25], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [22]]),
('zero-argument call keeps caller operand stack',
([['push', 12], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [7]]),
('extra locals are zero-initialised after arguments',
([['push', 5],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [40]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| two-argument call binds first argument to slot 0 | ['vm-fault'] | ['halt', [18]] | Failed |
| zero-argument call keeps caller operand stack | ['vm-fault'] | ['halt', [3]] | Failed |
| extra locals are zero-initialised after arguments | ['vm-fault'] | ['halt', [4]] | Failed |
| regression: recursive factorial | ['halt', [3, 2]] | ['halt', [6]] | Failed |
| recursion depth exactly at the limit | ['halt', [3, 2]] | ['halt', [6]] | Failed |
| recursion one frame over the limit | ['StackOverflowError', 4] | ['StackOverflowError', 4] | Passed |
| control: fuel exhaustion | ['fuel', 4] | ['fuel', 4] | Passed |
SHA-256 / c10f66a0852268012416c617198d45d27f57b18a9bd4036598639e68710980e4
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, max_depth, fuel):
def run():
frames = [{'locals': [0] * 4, 'stack': [], 'ret': None}]
pc = 0
for _ in range(fuel):
f = frames[-1]
ins = code[pc]
op = ins[0]
if op == 'push':
f['stack'].append(ins[1])
pc += 1
elif op == 'load':
f['stack'].append(f['locals'][ins[1]])
pc += 1
elif op == 'store':
f['locals'][ins[1]] = f['stack'].pop()
pc += 1
elif op in ('add', 'sub', 'mul'):
b = f['stack'].pop()
a = f['stack'].pop()
f['stack'].append(a + b if op == 'add' else a - b if op == 'sub' else a * b)
pc += 1
elif op == 'jz':
pc = ins[1] if f['stack'].pop() == 0 else pc + 1
elif op == 'jmp':
pc = ins[1]
elif op == 'call':
target, nargs, nlocals = ins[1], ins[2], ins[3]
if len(frames) >= max_depth:
return ['StackOverflowError', len(frames)]
args = f['stack'][len(f['stack']) - nargs:]
del f['stack'][len(f['stack']) - nargs:]
frames.append({'locals': args + [0] * (nlocals - nargs), 'stack': [], 'ret': pc + 1})
pc = target
elif op == 'ret':
value = f['stack'].pop()
frames.pop()
frames[-1]['stack'].append(value)
pc = frames[-1]['ret'] or f['ret']
else:
return ['halt', f['stack']]
return ['fuel', pc]
try:
return run()
except (IndexError, TypeError):
return ['vm-fault']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('two-argument call binds first argument to slot 0',
([['push', 21], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [18]]),
('zero-argument call keeps caller operand stack',
([['push', 8], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [3]]),
('extra locals are zero-initialised after arguments',
([['push', 1],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [4]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 22], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [19]]),
('zero-argument call keeps caller operand stack',
([['push', 9], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [4]]),
('extra locals are zero-initialised after arguments',
([['push', 2],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [10]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 23], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [20]]),
('zero-argument call keeps caller operand stack',
([['push', 10], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [5]]),
('extra locals are zero-initialised after arguments',
([['push', 3],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [18]]),
('regression: recursive factorial',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [2]]),
('recursion depth exactly at the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['halt', [2]]),
('recursion one frame over the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
3,
500),
['StackOverflowError', 3]),
('control: fuel exhaustion',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 24], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [21]]),
('zero-argument call keeps caller operand stack',
([['push', 11], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [6]]),
('extra locals are zero-initialised after arguments',
([['push', 4],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [28]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 25], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [22]]),
('zero-argument call keeps caller operand stack',
([['push', 12], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [7]]),
('extra locals are zero-initialised after arguments',
([['push', 5],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [40]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| two-argument call binds first argument to slot 0 | ['halt', [18]] | ['halt', [18]] | Passed |
| zero-argument call keeps caller operand stack | ['halt', [3]] | ['halt', [3]] | Passed |
| extra locals are zero-initialised after arguments | ['halt', [4]] | ['halt', [4]] | Passed |
| regression: recursive factorial | ['halt', [3, 2]] | ['halt', [6]] | Failed |
| recursion depth exactly at the limit | ['halt', [3, 2]] | ['halt', [6]] | Failed |
| recursion one frame over the limit | ['StackOverflowError', 4] | ['StackOverflowError', 4] | Passed |
| control: fuel exhaustion | ['fuel', 4] | ['fuel', 4] | Passed |
SHA-256 / dd6e2a5d49530205711887b8a616d73f3ffa5b339ff68ee5dabac59277db9b07
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, max_depth, fuel):
def run():
frames = [{'locals': [0] * 4, 'stack': [], 'ret': None}]
pc = 0
for _ in range(fuel):
f = frames[-1]
ins = code[pc]
op = ins[0]
if op == 'push':
f['stack'].append(ins[1])
pc += 1
elif op == 'load':
f['stack'].append(f['locals'][ins[1]])
pc += 1
elif op == 'store':
f['locals'][ins[1]] = f['stack'].pop()
pc += 1
elif op in ('add', 'sub', 'mul'):
b = f['stack'].pop()
a = f['stack'].pop()
f['stack'].append(a + b if op == 'add' else a - b if op == 'sub' else a * b)
pc += 1
elif op == 'jz':
pc = ins[1] if f['stack'].pop() == 0 else pc + 1
elif op == 'jmp':
pc = ins[1]
elif op == 'call':
target, nargs, nlocals = ins[1], ins[2], ins[3]
if len(frames) >= max_depth:
return ['StackOverflowError', len(frames)]
args = f['stack'][len(f['stack']) - nargs:]
del f['stack'][len(f['stack']) - nargs:]
frames.append({'locals': args + [0] * (nlocals - nargs), 'stack': [], 'ret': pc + 1})
pc = target
elif op == 'ret':
value = f['stack'].pop()
frames.pop()
frames[-1]['stack'].append(value)
pc = f['ret']
else:
return ['halt', f['stack']]
return ['fuel', pc]
try:
return run()
except (IndexError, TypeError):
return ['vm-fault']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('two-argument call binds first argument to slot 0',
([['push', 21], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [18]]),
('zero-argument call keeps caller operand stack',
([['push', 8], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [3]]),
('extra locals are zero-initialised after arguments',
([['push', 1],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [4]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 22], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [19]]),
('zero-argument call keeps caller operand stack',
([['push', 9], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']], 10, 100),
['halt', [4]]),
('extra locals are zero-initialised after arguments',
([['push', 2],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [10]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 23], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [20]]),
('zero-argument call keeps caller operand stack',
([['push', 10], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [5]]),
('extra locals are zero-initialised after arguments',
([['push', 3],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [18]]),
('regression: recursive factorial',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [2]]),
('recursion depth exactly at the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['halt', [2]]),
('recursion one frame over the limit',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
3,
500),
['StackOverflowError', 3]),
('control: fuel exhaustion',
([['push', 2],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 24], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [21]]),
('zero-argument call keeps caller operand stack',
([['push', 11], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [6]]),
('extra locals are zero-initialised after arguments',
([['push', 4],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [28]]),
('regression: recursive factorial',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [6]]),
('recursion depth exactly at the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['halt', [6]]),
('recursion one frame over the limit',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
4,
500),
['StackOverflowError', 4]),
('control: fuel exhaustion',
([['push', 3],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])],
[('two-argument call binds first argument to slot 0',
([['push', 25], ['push', 3], ['call', 4, 2, 2], ['halt'], ['load', 0], ['load', 1], ['sub'], ['ret']],
10,
100),
['halt', [22]]),
('zero-argument call keeps caller operand stack',
([['push', 12], ['call', 4, 0, 1], ['sub'], ['halt'], ['load', 0], ['push', 5], ['add'], ['ret']],
10,
100),
['halt', [7]]),
('extra locals are zero-initialised after arguments',
([['push', 5],
['call', 3, 1, 2],
['halt'],
['load', 0],
['push', 3],
['add'],
['store', 1],
['load', 1],
['load', 0],
['mul'],
['ret']],
10,
100),
['halt', [40]]),
('regression: recursive factorial',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
500),
['halt', [24]]),
('recursion depth exactly at the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
6,
500),
['halt', [24]]),
('recursion one frame over the limit',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
5,
500),
['StackOverflowError', 5]),
('control: fuel exhaustion',
([['push', 4],
['call', 3, 1, 1],
['halt'],
['load', 0],
['jz', 12],
['load', 0],
['load', 0],
['push', 1],
['sub'],
['call', 3, 1, 1],
['mul'],
['ret'],
['push', 1],
['ret']],
20,
3),
['fuel', 4])]]
for label, args, expected in cases[N - 1]:
check(label, solve(*args), expected)
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)
| Boundary fixture | Actual | Expected | Outcome |
|---|---|---|---|
| two-argument call binds first argument to slot 0 | ['halt', [18]] | ['halt', [18]] | Passed |
| zero-argument call keeps caller operand stack | ['halt', [3]] | ['halt', [3]] | Passed |
| extra locals are zero-initialised after arguments | ['halt', [4]] | ['halt', [4]] | Passed |
| regression: recursive factorial | ['halt', [6]] | ['halt', [6]] | Passed |
| recursion depth exactly at the limit | ['halt', [6]] | ['halt', [6]] | Passed |
| recursion one frame over the limit | ['StackOverflowError', 4] | ['StackOverflowError', 4] | Passed |
| control: fuel exhaustion | ['fuel', 4] | ['fuel', 4] | Passed |
SHA-256 / 46e90c26af1d5cdadeb3e297f7dd35c41af9d8906abf21ecbd5c2a67744c0384
Verification & scope
A deterministic, bounded teaching model of one bytecode virtual machine mechanism with a stipulated instruction encoding; it is not a production VM and claims no conformance to any real specification. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.
Observations recorded using Python 3.12.14 at 2026-09-29T14:51:22.036323+00:00.
Case digest / 6a8809a4f1417d806839bb991cde567585259e837d44cb4b9438d1aa5876967e