{"abstract":"Any instruction whose required operands exactly fill the stack is rejected.","category":"Bytecode virtual machines","checks":10,"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.","evaluation_group":"w2-bytecode-virtual-machines-verifier-stack-depth","failed_approach":"Checking only the resulting depth misses swap and dup_x1, which need operands without shrinking the stack.","family":"w2-bytecode-virtual-machines-verifier-stack-depth-underflow-test","id":"FA-89921","implementations":{"attempt":{"sha256":"ce254f5348a8165cc9bdf08aeebc15ea734ec49313e70b1420fc04941853e42b","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(code):\n    effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),\n               'add': (2, -1), 'ifeq': (1, -1), 'goto': (0, 0), 'return': (1, -1)}\n    def verify():\n        depth = {0: 0}\n        work = [0]\n        maxd = 0\n        while work:\n            i = work.pop()\n            op, arg = code[i]\n            need, delta = effects[op]\n            d = depth[i]\n            if d + delta < 0:\n                return ['underflow', i]\n            nd = d + delta\n            maxd = max(maxd, nd)\n            if op == 'goto':\n                succ = [arg]\n            elif op == 'ifeq':\n                succ = [i + 1, arg]\n            elif op == 'return':\n                succ = []\n            else:\n                succ = [i + 1]\n            for s in succ:\n                if s < 0 or s >= len(code):\n                    return ['falls-off', i]\n                if s in depth:\n                    if depth[s] != nd:\n                        return ['inconsistent', s]\n                else:\n                    depth[s] = nd\n                    work.append(s)\n        return ['ok', maxd]\n    try:\n        return verify()\n    except (IndexError, KeyError):\n        return ['vm-crash']\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['goto', 3], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),\n   ['inconsistent', 4]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 3]),\n  ('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),\n  ('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),\n  ('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],\n [('dup_x1 with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),\n   ['underflow', 3]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 6],\n     ['push', 5],\n     ['goto', 7],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),\n   ['underflow', 2]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),\n   ['inconsistent', 6]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 5]),\n  ('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 3]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 3])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 5]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 7],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 8],\n     ['push', 5],\n     ['goto', 9],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),\n   ['underflow', 4]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 8],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 8]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 7],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 7]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),\n   ['falls-off', 5]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 5]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 5])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 7]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 9],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 10],\n     ['push', 5],\n     ['goto', 11],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['ifeq', 7],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 6]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 10],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 10]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 9],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 9]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),\n   ['falls-off', 6]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 7]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 7])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 9]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 11],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 12],\n     ['push', 5],\n     ['goto', 13],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['ifeq', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 8]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 12],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 12]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 11],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 11]),\n  ('execution falling off the end',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 1]],),\n   ['falls-off', 9]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 9]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 9])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"589f9e3738ba8e2a82401bcd0a31afe751979cc44e1b8c8d6e6b027f8d62cc50","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(code):\n    effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),\n               'add': (2, -1), 'ifeq': (1, -1), 'goto': (0, 0), 'return': (1, -1)}\n    def verify():\n        depth = {0: 0}\n        work = [0]\n        maxd = 0\n        while work:\n            i = work.pop()\n            op, arg = code[i]\n            need, delta = effects[op]\n            d = depth[i]\n            if d <= need:\n                return ['underflow', i]\n            nd = d + delta\n            maxd = max(maxd, nd)\n            if op == 'goto':\n                succ = [arg]\n            elif op == 'ifeq':\n                succ = [i + 1, arg]\n            elif op == 'return':\n                succ = []\n            else:\n                succ = [i + 1]\n            for s in succ:\n                if s < 0 or s >= len(code):\n                    return ['falls-off', i]\n                if s in depth:\n                    if depth[s] != nd:\n                        return ['inconsistent', s]\n                else:\n                    depth[s] = nd\n                    work.append(s)\n        return ['ok', maxd]\n    try:\n        return verify()\n    except (IndexError, KeyError):\n        return ['vm-crash']\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['goto', 3], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),\n   ['inconsistent', 4]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 3]),\n  ('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),\n  ('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),\n  ('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],\n [('dup_x1 with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),\n   ['underflow', 3]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 6],\n     ['push', 5],\n     ['goto', 7],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),\n   ['underflow', 2]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),\n   ['inconsistent', 6]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 5]),\n  ('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 3]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 3])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 5]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 7],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 8],\n     ['push', 5],\n     ['goto', 9],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),\n   ['underflow', 4]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 8],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 8]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 7],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 7]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),\n   ['falls-off', 5]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 5]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 5])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 7]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 9],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 10],\n     ['push', 5],\n     ['goto', 11],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['ifeq', 7],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 6]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 10],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 10]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 9],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 9]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),\n   ['falls-off', 6]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 7]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 7])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 9]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 11],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 12],\n     ['push', 5],\n     ['goto', 13],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['ifeq', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 8]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 12],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 12]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 11],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 11]),\n  ('execution falling off the end',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 1]],),\n   ['falls-off', 9]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 9]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 9])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"fixed":{"sha256":"4c769e12927803e7ea06bc1e9250b3ea6c82c4a4a0d4a501b992a160d439a9e0","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(code):\n    effects = {'push': (0, 1), 'pop': (1, -1), 'dup': (1, 1), 'dup_x1': (2, 1), 'swap': (2, 0),\n               'add': (2, -1), 'ifeq': (1, -1), 'goto': (0, 0), 'return': (1, -1)}\n    def verify():\n        depth = {0: 0}\n        work = [0]\n        maxd = 0\n        while work:\n            i = work.pop()\n            op, arg = code[i]\n            need, delta = effects[op]\n            d = depth[i]\n            if d < need:\n                return ['underflow', i]\n            nd = d + delta\n            maxd = max(maxd, nd)\n            if op == 'goto':\n                succ = [arg]\n            elif op == 'ifeq':\n                succ = [i + 1, arg]\n            elif op == 'return':\n                succ = []\n            else:\n                succ = [i + 1]\n            for s in succ:\n                if s < 0 or s >= len(code):\n                    return ['falls-off', i]\n                if s in depth:\n                    if depth[s] != nd:\n                        return ['inconsistent', s]\n                else:\n                    depth[s] = nd\n                    work.append(s)\n        return ['ok', maxd]\n    try:\n        return verify()\n    except (IndexError, KeyError):\n        return ['vm-crash']\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[('dup_x1 with one item underflows', ([['push', 1], ['dup_x1', None], ['return', None]],), ['underflow', 1]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1], ['push', 2], ['dup_x1', None], ['add', None], ['add', None], ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['goto', 3], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 0], ['ifeq', 4], ['push', 5], ['goto', 5], ['push', 7], ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows', ([['ifeq', 1], ['push', 1], ['return', None]],), ['underflow', 0]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['push', 0], ['ifeq', 4], ['pop', None], ['return', None]],),\n   ['inconsistent', 4]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['ifeq', 3], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 3]),\n  ('execution falling off the end', ([['push', 1], ['push', 1]],), ['falls-off', 1]),\n  ('negative branch target', ([['push', 1], ['goto', -1], ['return', None]],), ['falls-off', 1]),\n  ('swap with one item underflows', ([['push', 1], ['swap', None], ['return', None]],), ['underflow', 1])],\n [('dup_x1 with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['dup_x1', None], ['return', None]],),\n   ['underflow', 3]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', 5], ['add', None], ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 6],\n     ['push', 5],\n     ['goto', 7],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['ifeq', 3], ['push', 1], ['return', None]],),\n   ['underflow', 2]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['push', 0], ['ifeq', 6], ['pop', None], ['return', None]],),\n   ['inconsistent', 6]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1], ['pop', None], ['push', 1], ['ifeq', 5], ['push', 9], ['push', 1], ['return', None]],),\n   ['inconsistent', 5]),\n  ('execution falling off the end', ([['push', 1], ['pop', None], ['push', 1]],), ['falls-off', 2]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 3]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 3])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 5]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 7],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 8],\n     ['push', 5],\n     ['goto', 9],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['ifeq', 5], ['push', 1], ['return', None]],),\n   ['underflow', 4]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 8],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 8]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 7],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 7]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['push', 1]],),\n   ['falls-off', 5]),\n  ('negative branch target',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['goto', -1], ['return', None]],),\n   ['falls-off', 5]),\n  ('swap with one item underflows',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 1], ['swap', None], ['return', None]],),\n   ['underflow', 5])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 7]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 9],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 10],\n     ['push', 5],\n     ['goto', 11],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['ifeq', 7],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 6]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 10],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 10]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 9],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 9]),\n  ('execution falling off the end',\n   ([['push', 1], ['pop', None], ['push', 2], ['pop', None], ['push', 3], ['pop', None], ['push', 1]],),\n   ['falls-off', 6]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 7]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 7])],\n [('dup_x1 with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['dup_x1', None],\n     ['return', None]],),\n   ['underflow', 9]),\n  ('dup_x1 with two items is legal',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 2],\n     ['dup_x1', None],\n     ['add', None],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 3]),\n  ('regression: dead code after goto is not verified',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', 11],\n     ['add', None],\n     ['return', None]],),\n   ['ok', 1]),\n  ('if/else arms merge at equal depth',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 0],\n     ['ifeq', 12],\n     ['push', 5],\n     ['goto', 13],\n     ['push', 7],\n     ['return', None]],),\n   ['ok', 1]),\n  ('ifeq on empty stack underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['ifeq', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['underflow', 8]),\n  ('deeper arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 0],\n     ['ifeq', 12],\n     ['pop', None],\n     ['return', None]],),\n   ['inconsistent', 12]),\n  ('shallower arm reaching merge first is inconsistent',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['ifeq', 11],\n     ['push', 9],\n     ['push', 1],\n     ['return', None]],),\n   ['inconsistent', 11]),\n  ('execution falling off the end',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['push', 1]],),\n   ['falls-off', 9]),\n  ('negative branch target',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['goto', -1],\n     ['return', None]],),\n   ['falls-off', 9]),\n  ('swap with one item underflows',\n   ([['push', 1],\n     ['pop', None],\n     ['push', 2],\n     ['pop', None],\n     ['push', 3],\n     ['pop', None],\n     ['push', 4],\n     ['pop', None],\n     ['push', 1],\n     ['swap', None],\n     ['return', None]],),\n   ['underflow', 9])]]\nfor label, args, expected in cases[N - 1]:\n    check(label, solve(*args), expected)\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"w2-bytecode-virtual-machines-verifier-stack-depth-underflow-test","generated_at":"2026-09-29T14:51:21.897955+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"Bytecode verifiers must agree exactly on stack effects and control-flow successors.","repair":"Underflow means fewer items than required: d < need.","root_cause":"The underflow comparison uses <=, treating d == need as missing an operand.","sha256":"9f158f5da3471fd8ad66cf32bf146684c4894788dfd89f284965af971145be41","title":"Stack-depth verifier: exact operand count flagged as underflow · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":39.869,"exit_code":1,"observations":[{"actual":["ok",2],"check":"dup_x1 with one item underflows","expected":["underflow",1],"passed":false},{"actual":["ok",3],"check":"dup_x1 with two items is legal","expected":["ok",3],"passed":true},{"actual":["ok",1],"check":"regression: dead code after goto is not verified","expected":["ok",1],"passed":true},{"actual":["ok",1],"check":"if/else arms merge at equal depth","expected":["ok",1],"passed":true},{"actual":["underflow",0],"check":"ifeq on empty stack underflows","expected":["underflow",0],"passed":true},{"actual":["inconsistent",4],"check":"deeper arm reaching merge first is inconsistent","expected":["inconsistent",4],"passed":true},{"actual":["inconsistent",3],"check":"shallower arm reaching merge first is inconsistent","expected":["inconsistent",3],"passed":true},{"actual":["falls-off",1],"check":"execution falling off the end","expected":["falls-off",1],"passed":true},{"actual":["falls-off",1],"check":"negative branch target","expected":["falls-off",1],"passed":true},{"actual":["ok",1],"check":"swap with one item underflows","expected":["underflow",1],"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"dup_x1 with one item underflows\", \"actual\": [\"ok\", 2], \"expected\": [\"underflow\", 1], \"passed\": false}, {\"check\": \"dup_x1 with two items is legal\", \"actual\": [\"ok\", 3], \"expected\": [\"ok\", 3], \"passed\": true}, {\"check\": \"regression: dead code after goto is not verified\", \"actual\": [\"ok\", 1], \"expected\": [\"ok\", 1], \"passed\": true}, {\"check\": \"if/else arms merge at equal depth\", \"actual\": [\"ok\", 1], \"expected\": [\"ok\", 1], \"passed\": true}, {\"check\": \"ifeq on empty stack underflows\", \"actual\": [\"underflow\", 0], \"expected\": [\"underflow\", 0], \"passed\": true}, {\"check\": \"deeper arm reaching merge first is inconsistent\", \"actual\": [\"inconsistent\", 4], \"expected\": [\"inconsistent\", 4], \"passed\": true}, {\"check\": \"shallower arm reaching merge first is inconsistent\", \"actual\": [\"inconsistent\", 3], \"expected\": [\"inconsistent\", 3], \"passed\": true}, {\"check\": \"execution falling off the end\", \"actual\": [\"falls-off\", 1], \"expected\": [\"falls-off\", 1], \"passed\": true}, {\"check\": \"negative branch target\", \"actual\": [\"falls-off\", 1], \"expected\": [\"falls-off\", 1], \"passed\": true}, {\"check\": \"swap with one item underflows\", \"actual\": [\"ok\", 1], \"expected\": [\"underflow\", 1], \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":43.812,"exit_code":1,"observations":[{"actual":["underflow",0],"check":"dup_x1 with one item underflows","expected":["underflow",1],"passed":false},{"actual":["underflow",0],"check":"dup_x1 with two items is legal","expected":["ok",3],"passed":false},{"actual":["underflow",0],"check":"regression: dead code after goto is not verified","expected":["ok",1],"passed":false},{"actual":["underflow",0],"check":"if/else arms merge at equal depth","expected":["ok",1],"passed":false},{"actual":["underflow",0],"check":"ifeq on empty stack underflows","expected":["underflow",0],"passed":true},{"actual":["underflow",0],"check":"deeper arm reaching merge first is inconsistent","expected":["inconsistent",4],"passed":false},{"actual":["underflow",0],"check":"shallower arm reaching merge first is inconsistent","expected":["inconsistent",3],"passed":false},{"actual":["underflow",0],"check":"execution falling off the end","expected":["falls-off",1],"passed":false},{"actual":["underflow",0],"check":"negative branch target","expected":["falls-off",1],"passed":false},{"actual":["underflow",0],"check":"swap with one item underflows","expected":["underflow",1],"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"dup_x1 with one item underflows\", \"actual\": [\"underflow\", 0], \"expected\": [\"underflow\", 1], \"passed\": false}, {\"check\": \"dup_x1 with two items is legal\", \"actual\": [\"underflow\", 0], \"expected\": [\"ok\", 3], \"passed\": false}, {\"check\": \"regression: dead code after goto is not verified\", \"actual\": [\"underflow\", 0], \"expected\": [\"ok\", 1], \"passed\": false}, {\"check\": \"if/else arms merge at equal depth\", \"actual\": [\"underflow\", 0], \"expected\": [\"ok\", 1], \"passed\": false}, {\"check\": \"ifeq on empty stack underflows\", \"actual\": [\"underflow\", 0], \"expected\": [\"underflow\", 0], \"passed\": true}, {\"check\": \"deeper arm reaching merge first is inconsistent\", \"actual\": [\"underflow\", 0], \"expected\": [\"inconsistent\", 4], \"passed\": false}, {\"check\": \"shallower arm reaching merge first is inconsistent\", \"actual\": [\"underflow\", 0], \"expected\": [\"inconsistent\", 3], \"passed\": false}, {\"check\": \"execution falling off the end\", \"actual\": [\"underflow\", 0], \"expected\": [\"falls-off\", 1], \"passed\": false}, {\"check\": \"negative branch target\", \"actual\": [\"underflow\", 0], \"expected\": [\"falls-off\", 1], \"passed\": false}, {\"check\": \"swap with one item underflows\", \"actual\": [\"underflow\", 0], \"expected\": [\"underflow\", 1], \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":38.858,"exit_code":0,"observations":[{"actual":["underflow",1],"check":"dup_x1 with one item underflows","expected":["underflow",1],"passed":true},{"actual":["ok",3],"check":"dup_x1 with two items is legal","expected":["ok",3],"passed":true},{"actual":["ok",1],"check":"regression: dead code after goto is not verified","expected":["ok",1],"passed":true},{"actual":["ok",1],"check":"if/else arms merge at equal depth","expected":["ok",1],"passed":true},{"actual":["underflow",0],"check":"ifeq on empty stack underflows","expected":["underflow",0],"passed":true},{"actual":["inconsistent",4],"check":"deeper arm reaching merge first is inconsistent","expected":["inconsistent",4],"passed":true},{"actual":["inconsistent",3],"check":"shallower arm reaching merge first is inconsistent","expected":["inconsistent",3],"passed":true},{"actual":["falls-off",1],"check":"execution falling off the end","expected":["falls-off",1],"passed":true},{"actual":["falls-off",1],"check":"negative branch target","expected":["falls-off",1],"passed":true},{"actual":["underflow",1],"check":"swap with one item underflows","expected":["underflow",1],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"dup_x1 with one item underflows\", \"actual\": [\"underflow\", 1], \"expected\": [\"underflow\", 1], \"passed\": true}, {\"check\": \"dup_x1 with two items is legal\", \"actual\": [\"ok\", 3], \"expected\": [\"ok\", 3], \"passed\": true}, {\"check\": \"regression: dead code after goto is not verified\", \"actual\": [\"ok\", 1], \"expected\": [\"ok\", 1], \"passed\": true}, {\"check\": \"if/else arms merge at equal depth\", \"actual\": [\"ok\", 1], \"expected\": [\"ok\", 1], \"passed\": true}, {\"check\": \"ifeq on empty stack underflows\", \"actual\": [\"underflow\", 0], \"expected\": [\"underflow\", 0], \"passed\": true}, {\"check\": \"deeper arm reaching merge first is inconsistent\", \"actual\": [\"inconsistent\", 4], \"expected\": [\"inconsistent\", 4], \"passed\": true}, {\"check\": \"shallower arm reaching merge first is inconsistent\", \"actual\": [\"inconsistent\", 3], \"expected\": [\"inconsistent\", 3], \"passed\": true}, {\"check\": \"execution falling off the end\", \"actual\": [\"falls-off\", 1], \"expected\": [\"falls-off\", 1], \"passed\": true}, {\"check\": \"negative branch target\", \"actual\": [\"falls-off\", 1], \"expected\": [\"falls-off\", 1], \"passed\": true}, {\"check\": \"swap with one item underflows\", \"actual\": [\"underflow\", 1], \"expected\": [\"underflow\", 1], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}