FA-89951 / Bytecode virtual machines / Open access
Call frames: return value pushed beneath caller operands · case 01
Expressions that use a call result with pending operands compute with swapped operands.
ROOT CAUSE
The result is inserted at the bottom of the caller operand stack.
VERIFIED REPAIR
Push the result on top of the caller operand stack.
Unsuccessful approach: Appending to the popped callee frame loses the result entirely.
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'].insert(0, 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]] | Failed |
| 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 / 0505dca3c7e968ec46ab610b34cb8c8fedf0e1cffae0302977ad95ffc7f3e769
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()
f['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', []] | ['halt', [18]] | Failed |
| zero-argument call keeps caller operand stack | ['vm-fault'] | ['halt', [3]] | Failed |
| extra locals are zero-initialised after arguments | ['halt', []] | ['halt', [4]] | Failed |
| regression: recursive factorial | ['vm-fault'] | ['halt', [6]] | Failed |
| recursion depth exactly at the limit | ['vm-fault'] | ['halt', [6]] | Failed |
| recursion one frame over the limit | ['StackOverflowError', 4] | ['StackOverflowError', 4] | Passed |
| control: fuel exhaustion | ['fuel', 4] | ['fuel', 4] | Passed |
SHA-256 / bdf0eb2090e36d4eaba87b36ea989971771576c33a11ae0fa3db0c6d7695e3e9
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.076708+00:00.
Case digest / d66e623c0b2efd0c610a6f0c8dc06b87194a9078a298cca9689f46734dd83269