FA-89861 / Bytecode virtual machines / Open access
Relative-jump VM: fuel limit allows one extra instruction · case 01
A program given exactly one unit too little fuel still halts normally.
ROOT CAUSE
The budget test uses steps > fuel, so fuel + 1 instructions execute.
VERIFIED REPAIR
Stop before executing when the executed-instruction count has reached fuel.
Unsuccessful approach: Comparing against fuel - 1 now stops a program that has exactly enough fuel.
Case contract
Flat int bytecode, byte addressed: 0 HALT, 1 PUSH imm, 2 ADD, 3 SUB (second-from-top minus top), 4 JMP rel, 5 JZ rel (pops condition, branches when it is 0), 6 DUP, 7 SWAP, 8 PRINT (pop to out). Relative displacements are measured from the address after the one-byte operand. Every executed instruction including HALT costs one unit of fuel; with fuel exhausted report status fuel. Return status, pc, printed values and stack; stack underflow, bad pc and bad opcode are statuses.
Why this case matters
Branch displacement bases, operand order and fuel accounting are classic interpreter-loop defects.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, fuel):
def run():
pc = 0
stack = []
out = []
steps = 0
while True:
if pc < 0 or pc >= len(code):
return {'status': 'badpc', 'pc': pc, 'out': out, 'stack': stack}
if steps > fuel:
return {'status': 'fuel', 'pc': pc, 'out': out, 'stack': stack}
steps += 1
op = code[pc]
if op == 0:
return {'status': 'halt', 'pc': pc, 'out': out, 'stack': stack}
need = {1: 0, 2: 2, 3: 2, 4: 0, 5: 1, 6: 1, 7: 2, 8: 1}.get(op)
if need is None:
return {'status': 'badop', 'pc': pc, 'out': out, 'stack': stack}
if len(stack) < need:
return {'status': 'underflow', 'pc': pc, 'out': out, 'stack': stack}
if op == 1:
stack.append(code[pc + 1])
pc += 2
elif op == 2 or op == 3:
b = stack.pop()
a = stack.pop()
stack.append(a + b if op == 2 else a - b)
pc += 1
elif op == 4:
pc += 2 + code[pc + 1]
elif op == 5:
c = stack.pop()
pc = pc + 2 + code[pc + 1] if c == 0 else pc + 2
elif op == 6:
stack.append(stack[-1])
pc += 1
elif op == 7:
stack[-1], stack[-2] = stack[-2], stack[-1]
pc += 1
else:
out.append(stack.pop())
pc += 1
try:
return run()
except IndexError:
return {'status': 'trap'}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: countdown loop prints n..1',
([1, 2, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 3, 1, 2, 7, 3, 8, 0], 50),
{'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -1, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 1, 8, 0], 3), {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 1, 8, 0], 2),
{'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 1, 6, 2, 8, 0], 20),
{'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 6, 0], 10),
{'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 3, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 6, 1, 2, 7, 3, 8, 0], 50),
{'out': [-4], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -2, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 2, 8, 0], 3), {'out': [2], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 2, 8, 0], 2),
{'out': [2], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 2, 6, 2, 8, 0], 20),
{'out': [4], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 7, 0], 10),
{'out': [], 'pc': 9, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 4, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 9, 1, 2, 7, 3, 8, 0], 50),
{'out': [-7], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -3, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 3, 8, 0], 3), {'out': [3], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 3, 8, 0], 2),
{'out': [3], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 3, 6, 2, 8, 0], 20),
{'out': [6], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 8, 0], 10),
{'out': [], 'pc': 10, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 5, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 12, 1, 2, 7, 3, 8, 0], 50),
{'out': [-10], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -4, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 4, 8, 0], 3), {'out': [4], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 4, 8, 0], 2),
{'out': [4], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 4, 6, 2, 8, 0], 20),
{'out': [8], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 9, 0], 10),
{'out': [], 'pc': 11, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 6, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [6, 5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 15, 1, 2, 7, 3, 8, 0], 50),
{'out': [-13], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -5, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 5, 8, 0], 3), {'out': [5], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 5, 8, 0], 2),
{'out': [5], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 5, 6, 2, 8, 0], 20),
{'out': [10], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 10, 0], 10),
{'out': [], 'pc': 12, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})]]
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 |
|---|---|---|---|
| regression: countdown loop prints n..1 | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | Passed |
| swap then subtract uses swapped order | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | Passed |
| jz on negative value falls through | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | Passed |
| fuel exactly sufficient halts | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | Passed |
| fuel one short reports exhaustion | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'} | Failed |
| dup on empty stack underflows | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | Passed |
| dup with one item doubles | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | Passed |
| forward jump beyond code is badpc | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | Passed |
| control: unknown opcode | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | Passed |
SHA-256 / 2289856736de8f3a5313cb49f41255a51464f27eea4e1220e33c0dfc2c8c1fd5
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, fuel):
def run():
pc = 0
stack = []
out = []
steps = 0
while True:
if pc < 0 or pc >= len(code):
return {'status': 'badpc', 'pc': pc, 'out': out, 'stack': stack}
if steps >= fuel - 1:
return {'status': 'fuel', 'pc': pc, 'out': out, 'stack': stack}
steps += 1
op = code[pc]
if op == 0:
return {'status': 'halt', 'pc': pc, 'out': out, 'stack': stack}
need = {1: 0, 2: 2, 3: 2, 4: 0, 5: 1, 6: 1, 7: 2, 8: 1}.get(op)
if need is None:
return {'status': 'badop', 'pc': pc, 'out': out, 'stack': stack}
if len(stack) < need:
return {'status': 'underflow', 'pc': pc, 'out': out, 'stack': stack}
if op == 1:
stack.append(code[pc + 1])
pc += 2
elif op == 2 or op == 3:
b = stack.pop()
a = stack.pop()
stack.append(a + b if op == 2 else a - b)
pc += 1
elif op == 4:
pc += 2 + code[pc + 1]
elif op == 5:
c = stack.pop()
pc = pc + 2 + code[pc + 1] if c == 0 else pc + 2
elif op == 6:
stack.append(stack[-1])
pc += 1
elif op == 7:
stack[-1], stack[-2] = stack[-2], stack[-1]
pc += 1
else:
out.append(stack.pop())
pc += 1
try:
return run()
except IndexError:
return {'status': 'trap'}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: countdown loop prints n..1',
([1, 2, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 3, 1, 2, 7, 3, 8, 0], 50),
{'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -1, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 1, 8, 0], 3), {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 1, 8, 0], 2),
{'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 1, 6, 2, 8, 0], 20),
{'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 6, 0], 10),
{'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 3, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 6, 1, 2, 7, 3, 8, 0], 50),
{'out': [-4], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -2, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 2, 8, 0], 3), {'out': [2], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 2, 8, 0], 2),
{'out': [2], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 2, 6, 2, 8, 0], 20),
{'out': [4], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 7, 0], 10),
{'out': [], 'pc': 9, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 4, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 9, 1, 2, 7, 3, 8, 0], 50),
{'out': [-7], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -3, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 3, 8, 0], 3), {'out': [3], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 3, 8, 0], 2),
{'out': [3], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 3, 6, 2, 8, 0], 20),
{'out': [6], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 8, 0], 10),
{'out': [], 'pc': 10, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 5, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 12, 1, 2, 7, 3, 8, 0], 50),
{'out': [-10], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -4, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 4, 8, 0], 3), {'out': [4], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 4, 8, 0], 2),
{'out': [4], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 4, 6, 2, 8, 0], 20),
{'out': [8], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 9, 0], 10),
{'out': [], 'pc': 11, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 6, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [6, 5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 15, 1, 2, 7, 3, 8, 0], 50),
{'out': [-13], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -5, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 5, 8, 0], 3), {'out': [5], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 5, 8, 0], 2),
{'out': [5], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 5, 6, 2, 8, 0], 20),
{'out': [10], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 10, 0], 10),
{'out': [], 'pc': 12, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})]]
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 |
|---|---|---|---|
| regression: countdown loop prints n..1 | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | Passed |
| swap then subtract uses swapped order | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | Passed |
| jz on negative value falls through | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | Passed |
| fuel exactly sufficient halts | {'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | Failed |
| fuel one short reports exhaustion | {'out': [], 'pc': 2, 'stack': [1], 'status': 'fuel'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'} | Failed |
| dup on empty stack underflows | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | Passed |
| dup with one item doubles | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | Passed |
| forward jump beyond code is badpc | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | Passed |
| control: unknown opcode | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | Passed |
SHA-256 / 17972bd9839ab10a7182861400a05e33d4866648e5aea5acb3356af18399b802
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code, fuel):
def run():
pc = 0
stack = []
out = []
steps = 0
while True:
if pc < 0 or pc >= len(code):
return {'status': 'badpc', 'pc': pc, 'out': out, 'stack': stack}
if steps >= fuel:
return {'status': 'fuel', 'pc': pc, 'out': out, 'stack': stack}
steps += 1
op = code[pc]
if op == 0:
return {'status': 'halt', 'pc': pc, 'out': out, 'stack': stack}
need = {1: 0, 2: 2, 3: 2, 4: 0, 5: 1, 6: 1, 7: 2, 8: 1}.get(op)
if need is None:
return {'status': 'badop', 'pc': pc, 'out': out, 'stack': stack}
if len(stack) < need:
return {'status': 'underflow', 'pc': pc, 'out': out, 'stack': stack}
if op == 1:
stack.append(code[pc + 1])
pc += 2
elif op == 2 or op == 3:
b = stack.pop()
a = stack.pop()
stack.append(a + b if op == 2 else a - b)
pc += 1
elif op == 4:
pc += 2 + code[pc + 1]
elif op == 5:
c = stack.pop()
pc = pc + 2 + code[pc + 1] if c == 0 else pc + 2
elif op == 6:
stack.append(stack[-1])
pc += 1
elif op == 7:
stack[-1], stack[-2] = stack[-2], stack[-1]
pc += 1
else:
out.append(stack.pop())
pc += 1
try:
return run()
except IndexError:
return {'status': 'trap'}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: countdown loop prints n..1',
([1, 2, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 3, 1, 2, 7, 3, 8, 0], 50),
{'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -1, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 1, 8, 0], 3), {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 1, 8, 0], 2),
{'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 1, 6, 2, 8, 0], 20),
{'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 6, 0], 10),
{'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 3, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 6, 1, 2, 7, 3, 8, 0], 50),
{'out': [-4], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -2, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 2, 8, 0], 3), {'out': [2], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 2, 8, 0], 2),
{'out': [2], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 2, 6, 2, 8, 0], 20),
{'out': [4], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 7, 0], 10),
{'out': [], 'pc': 9, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 4, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 9, 1, 2, 7, 3, 8, 0], 50),
{'out': [-7], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -3, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 3, 8, 0], 3), {'out': [3], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 3, 8, 0], 2),
{'out': [3], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 3, 6, 2, 8, 0], 20),
{'out': [6], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 8, 0], 10),
{'out': [], 'pc': 10, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 5, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 12, 1, 2, 7, 3, 8, 0], 50),
{'out': [-10], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -4, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 4, 8, 0], 3), {'out': [4], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 4, 8, 0], 2),
{'out': [4], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 4, 6, 2, 8, 0], 20),
{'out': [8], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 9, 0], 10),
{'out': [], 'pc': 11, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})],
[('regression: countdown loop prints n..1',
([1, 6, 6, 5, 7, 6, 8, 1, 1, 3, 4, -10, 0], 200),
{'out': [6, 5, 4, 3, 2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'}),
('swap then subtract uses swapped order',
([1, 15, 1, 2, 7, 3, 8, 0], 50),
{'out': [-13], 'pc': 7, 'stack': [], 'status': 'halt'}),
('jz on negative value falls through',
([1, -5, 5, 2, 1, 99, 0], 50),
{'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'}),
('fuel exactly sufficient halts', ([1, 5, 8, 0], 3), {'out': [5], 'pc': 3, 'stack': [], 'status': 'halt'}),
('fuel one short reports exhaustion',
([1, 5, 8, 0], 2),
{'out': [5], 'pc': 3, 'stack': [], 'status': 'fuel'}),
('dup on empty stack underflows', ([6, 0], 10), {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'}),
('dup with one item doubles',
([1, 5, 6, 2, 8, 0], 20),
{'out': [10], 'pc': 5, 'stack': [], 'status': 'halt'}),
('forward jump beyond code is badpc',
([4, 10, 0], 10),
{'out': [], 'pc': 12, 'stack': [], 'status': 'badpc'}),
('control: unknown opcode', ([1, 1, 42, 0], 10), {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'})]]
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 |
|---|---|---|---|
| regression: countdown loop prints n..1 | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | {'out': [2, 1], 'pc': 12, 'stack': [0], 'status': 'halt'} | Passed |
| swap then subtract uses swapped order | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | {'out': [-1], 'pc': 7, 'stack': [], 'status': 'halt'} | Passed |
| jz on negative value falls through | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | {'out': [], 'pc': 6, 'stack': [99], 'status': 'halt'} | Passed |
| fuel exactly sufficient halts | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'halt'} | Passed |
| fuel one short reports exhaustion | {'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'} | {'out': [1], 'pc': 3, 'stack': [], 'status': 'fuel'} | Passed |
| dup on empty stack underflows | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | {'out': [], 'pc': 0, 'stack': [], 'status': 'underflow'} | Passed |
| dup with one item doubles | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | {'out': [2], 'pc': 5, 'stack': [], 'status': 'halt'} | Passed |
| forward jump beyond code is badpc | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | {'out': [], 'pc': 8, 'stack': [], 'status': 'badpc'} | Passed |
| control: unknown opcode | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | {'out': [], 'pc': 2, 'stack': [1], 'status': 'badop'} | Passed |
SHA-256 / 252077e75c46b098017d71f7ea790287fc878e93a4bbee24738d1a2f71b27d80
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.277109+00:00.
Case digest / 5c9572eb6ea79ae0b8b3dcaa60e4a2061bc11707b4992dac7e778dc8a75f67ac