FA-89906 / Bytecode virtual machines / Open access
Stack-depth verifier: ifeq leaves its condition on the stack · case 01
Both branch targets are verified one slot too deep and max stack is overstated.
ROOT CAUSE
The table records ifeq with a zero delta although it consumes the condition.
VERIFIED REPAIR
ifeq requires one operand and pops it before branching.
Unsuccessful approach: Dropping the requirement lets ifeq on an empty stack verify with a negative depth.
Case contract
code is a list of [op, arg]. Stack effects (required, delta): push (0,+1), pop (1,-1), dup (1,+1), dup_x1 (2,+1), swap (2,0), add (2,-1), ifeq (1,-1; successors fallthrough and arg), goto (0,0; only arg), return (1,-1; none). Dataflow from index 0 with depth 0: report ["underflow", i], ["falls-off", i] for a successor outside the code, ["inconsistent", s] when a merge sees two depths, else ["ok", max depth]. Unreachable code is never examined.
Why this case matters
Bytecode verifiers must agree exactly on stack effects and control-flow successors.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code):
effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),
'add': (2, -1), 'ifeq': (1, 0), 'goto': (0, 0), 'return': (1, -1)}
def verify():
depth = {0: 0}
work = [0]
maxd = 0
while work:
i = work.pop()
op, arg = code[i]
need, delta = effects[op]
d = depth[i]
if d < need:
return ['underflow', i]
nd = d + delta
maxd = max(maxd, nd)
if op == 'goto':
succ = [arg]
elif op == 'ifeq':
succ = [i + 1, arg]
elif op == 'return':
succ = []
else:
succ = [i + 1]
for s in succ:
if s < 0 or s >= len(code):
return ['falls-off', i]
if s in depth:
if depth[s] != nd:
return ['inconsistent', s]
else:
depth[s] = nd
work.append(s)
return ['ok', maxd]
try:
return verify()
except (IndexError, KeyError):
return ['vm-crash']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),
('dup_x1 with two items is legal',
([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['goto', 3], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),
['inconsistent', 4]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 3]),
('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),
('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),
('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],
[('dup_x1 with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),
['underflow', 3]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 0],
['ifeq', 6],
['push', 5],
['goto', 7],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),
['underflow', 2]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),
['inconsistent', 6]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 5]),
('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 3]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 3])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 5]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['goto', 7],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 0],
['ifeq', 8],
['push', 5],
['goto', 9],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),
['underflow', 4]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 8],
['pop', None],
['return', None]],),
['inconsistent', 8]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['ifeq', 7],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 7]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),
['falls-off', 5]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 5]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 5])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 7]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', 9],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 0],
['ifeq', 10],
['push', 5],
['goto', 11],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['ifeq', 7],
['push', 1],
['return', None]],),
['underflow', 6]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 10],
['pop', None],
['return', None]],),
['inconsistent', 10]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['ifeq', 9],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 9]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),
['falls-off', 6]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 7]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 7])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 9]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', 11],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 0],
['ifeq', 12],
['push', 5],
['goto', 13],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['ifeq', 9],
['push', 1],
['return', None]],),
['underflow', 8]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 12],
['pop', None],
['return', None]],),
['inconsistent', 12]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['ifeq', 11],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 11]),
('execution falling off the end',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 1]],),
['falls-off', 9]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 9]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 9])]]
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 |
|---|---|---|---|
| dup_x1 with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
| dup_x1 with two items is legal | ['ok', 3] | ['ok', 3] | Passed |
| regression: dead code after goto is not verified | ['ok', 1] | ['ok', 1] | Passed |
| if/else arms merge at equal depth | ['ok', 2] | ['ok', 1] | Failed |
| ifeq on empty stack underflows | ['underflow', 0] | ['underflow', 0] | Passed |
| deeper arm reaching merge first is inconsistent | ['inconsistent', 4] | ['inconsistent', 4] | Passed |
| shallower arm reaching merge first is inconsistent | ['inconsistent', 3] | ['inconsistent', 3] | Passed |
| execution falling off the end | ['falls-off', 1] | ['falls-off', 1] | Passed |
| negative branch target | ['falls-off', 1] | ['falls-off', 1] | Passed |
| swap with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
SHA-256 / de7bca001cfa69b5fdb9de1c853fb27ef1312c91dfa0735e4a747226c03da0f3
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code):
effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),
'add': (2, -1), 'ifeq': (0, -1), 'goto': (0, 0), 'return': (1, -1)}
def verify():
depth = {0: 0}
work = [0]
maxd = 0
while work:
i = work.pop()
op, arg = code[i]
need, delta = effects[op]
d = depth[i]
if d < need:
return ['underflow', i]
nd = d + delta
maxd = max(maxd, nd)
if op == 'goto':
succ = [arg]
elif op == 'ifeq':
succ = [i + 1, arg]
elif op == 'return':
succ = []
else:
succ = [i + 1]
for s in succ:
if s < 0 or s >= len(code):
return ['falls-off', i]
if s in depth:
if depth[s] != nd:
return ['inconsistent', s]
else:
depth[s] = nd
work.append(s)
return ['ok', maxd]
try:
return verify()
except (IndexError, KeyError):
return ['vm-crash']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),
('dup_x1 with two items is legal',
([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['goto', 3], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),
['inconsistent', 4]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 3]),
('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),
('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),
('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],
[('dup_x1 with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),
['underflow', 3]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 0],
['ifeq', 6],
['push', 5],
['goto', 7],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),
['underflow', 2]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),
['inconsistent', 6]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 5]),
('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 3]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 3])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 5]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['goto', 7],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 0],
['ifeq', 8],
['push', 5],
['goto', 9],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),
['underflow', 4]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 8],
['pop', None],
['return', None]],),
['inconsistent', 8]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['ifeq', 7],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 7]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),
['falls-off', 5]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 5]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 5])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 7]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', 9],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 0],
['ifeq', 10],
['push', 5],
['goto', 11],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['ifeq', 7],
['push', 1],
['return', None]],),
['underflow', 6]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 10],
['pop', None],
['return', None]],),
['inconsistent', 10]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['ifeq', 9],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 9]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),
['falls-off', 6]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 7]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 7])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 9]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', 11],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 0],
['ifeq', 12],
['push', 5],
['goto', 13],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['ifeq', 9],
['push', 1],
['return', None]],),
['underflow', 8]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 12],
['pop', None],
['return', None]],),
['inconsistent', 12]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['ifeq', 11],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 11]),
('execution falling off the end',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 1]],),
['falls-off', 9]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 9]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 9])]]
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 |
|---|---|---|---|
| dup_x1 with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
| dup_x1 with two items is legal | ['ok', 3] | ['ok', 3] | Passed |
| regression: dead code after goto is not verified | ['ok', 1] | ['ok', 1] | Passed |
| if/else arms merge at equal depth | ['ok', 1] | ['ok', 1] | Passed |
| ifeq on empty stack underflows | ['underflow', 1] | ['underflow', 0] | Failed |
| deeper arm reaching merge first is inconsistent | ['inconsistent', 4] | ['inconsistent', 4] | Passed |
| shallower arm reaching merge first is inconsistent | ['inconsistent', 3] | ['inconsistent', 3] | Passed |
| execution falling off the end | ['falls-off', 1] | ['falls-off', 1] | Passed |
| negative branch target | ['falls-off', 1] | ['falls-off', 1] | Passed |
| swap with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
SHA-256 / a22df8a566033d18ebc2781f65f263c0d5a549c943f62958d82d61732bf65ecb
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(code):
effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),
'add': (2, -1), 'ifeq': (1, -1), 'goto': (0, 0), 'return': (1, -1)}
def verify():
depth = {0: 0}
work = [0]
maxd = 0
while work:
i = work.pop()
op, arg = code[i]
need, delta = effects[op]
d = depth[i]
if d < need:
return ['underflow', i]
nd = d + delta
maxd = max(maxd, nd)
if op == 'goto':
succ = [arg]
elif op == 'ifeq':
succ = [i + 1, arg]
elif op == 'return':
succ = []
else:
succ = [i + 1]
for s in succ:
if s < 0 or s >= len(code):
return ['falls-off', i]
if s in depth:
if depth[s] != nd:
return ['inconsistent', s]
else:
depth[s] = nd
work.append(s)
return ['ok', maxd]
try:
return verify()
except (IndexError, KeyError):
return ['vm-crash']
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),
('dup_x1 with two items is legal',
([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['goto', 3], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),
['inconsistent', 4]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 3]),
('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),
('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),
('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],
[('dup_x1 with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),
['underflow', 3]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 0],
['ifeq', 6],
['push', 5],
['goto', 7],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),
['underflow', 2]),
('deeper arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),
['inconsistent', 6]),
('shallower arm reaching merge first is inconsistent',
([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),
['inconsistent', 5]),
('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 3]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 3])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 5]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['goto', 7],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 0],
['ifeq', 8],
['push', 5],
['goto', 9],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),
['underflow', 4]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 8],
['pop', None],
['return', None]],),
['inconsistent', 8]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 1],
['ifeq', 7],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 7]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),
['falls-off', 5]),
('negative branch target',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),
['falls-off', 5]),
('swap with one item underflows',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),
['underflow', 5])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 7]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', 9],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 0],
['ifeq', 10],
['push', 5],
['goto', 11],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['ifeq', 7],
['push', 1],
['return', None]],),
['underflow', 6]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 10],
['pop', None],
['return', None]],),
['inconsistent', 10]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['ifeq', 9],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 9]),
('execution falling off the end',
([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),
['falls-off', 6]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 7]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 7])],
[('dup_x1 with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['dup_x1', None],
['return', None]],),
['underflow', 9]),
('dup_x1 with two items is legal',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 2],
['dup_x1', None],
['add', None],
['add', None],
['return', None]],),
['ok', 3]),
('regression: dead code after goto is not verified',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', 11],
['add', None],
['return', None]],),
['ok', 1]),
('if/else arms merge at equal depth',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 0],
['ifeq', 12],
['push', 5],
['goto', 13],
['push', 7],
['return', None]],),
['ok', 1]),
('ifeq on empty stack underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['ifeq', 9],
['push', 1],
['return', None]],),
['underflow', 8]),
('deeper arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 0],
['ifeq', 12],
['pop', None],
['return', None]],),
['inconsistent', 12]),
('shallower arm reaching merge first is inconsistent',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['ifeq', 11],
['push', 9],
['push', 1],
['return', None]],),
['inconsistent', 11]),
('execution falling off the end',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['push', 1]],),
['falls-off', 9]),
('negative branch target',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['goto', -1],
['return', None]],),
['falls-off', 9]),
('swap with one item underflows',
([['push', 1],
['pop', None],
['push', 2],
['pop', None],
['push', 3],
['pop', None],
['push', 4],
['pop', None],
['push', 1],
['swap', None],
['return', None]],),
['underflow', 9])]]
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 |
|---|---|---|---|
| dup_x1 with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
| dup_x1 with two items is legal | ['ok', 3] | ['ok', 3] | Passed |
| regression: dead code after goto is not verified | ['ok', 1] | ['ok', 1] | Passed |
| if/else arms merge at equal depth | ['ok', 1] | ['ok', 1] | Passed |
| ifeq on empty stack underflows | ['underflow', 0] | ['underflow', 0] | Passed |
| deeper arm reaching merge first is inconsistent | ['inconsistent', 4] | ['inconsistent', 4] | Passed |
| shallower arm reaching merge first is inconsistent | ['inconsistent', 3] | ['inconsistent', 3] | Passed |
| execution falling off the end | ['falls-off', 1] | ['falls-off', 1] | Passed |
| negative branch target | ['falls-off', 1] | ['falls-off', 1] | Passed |
| swap with one item underflows | ['underflow', 1] | ['underflow', 1] | Passed |
SHA-256 / 4c769e12927803e7ea06bc1e9250b3ea6c82c4a4a0d4a501b992a160d439a9e0
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.811235+00:00.
Case digest / f36c3bbf358010d9dd95cc3a12abac120259b8de16460febc9412e8824741794