FA-89931 / Bytecode virtual machines / Open access
Call frames: zero-argument call clears the caller stack · case 01
After calling a function with no arguments the caller loses all pending operands and faults.
ROOT CAUSE
Negative slicing with -nargs becomes [-0:] which is the whole list when nargs is 0.
VERIFIED REPAIR
Delete from len(stack) - nargs so that zero arguments removes nothing.
Unsuccessful approach: Slicing to [:-nargs] has the same -0 trap and empties the stack for zero-arity 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'][-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 | ['vm-fault'] | ['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 / b52bee78840b8e42adf753100fb5becb1a959095475527636656817021288e0a
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:]
f['stack'] = 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 | ['vm-fault'] | ['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 / d3699a77eed2633ab4940c981befb206a2244ac5628f52c683e11337244a23e2
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:21.943816+00:00.
Case digest / 41f65b61525404921f559e363bcc3e3b9353a93a4d8a2ce533aa28dbce560497