FA-90146 / Bytecode virtual machines / Open access
Branch relaxation: displacement -128 considered out of range · case 01
Backward branches of exactly -128 bytes are widened, growing code for no reason.
ROOT CAUSE
The fit test uses abs(off) > 127, which rejects the valid minimum -128.
VERIFIED REPAIR
Short displacements are valid from -128 to 127 inclusive.
Unsuccessful approach: Accepting +128 lets a forward branch overflow its 8-bit field.
Case contract
Assemble ["label", name], ["data", nbytes], ["jmp", label], ["jz", label]. Branches start in the short form (2 bytes, signed 8-bit displacement from the end of the instruction, valid -128..127). A short branch whose displacement does not fit is widened (jmp.w 3 bytes, jz.w 4 bytes) and addresses are recomputed until no branch changes (branches never shrink). Report duplicate or undefined labels; otherwise return each branch as [address, mnemonic, displacement from its own end] and the total size.
Why this case matters
Variable-length branch encodings need fixpoint relaxation to produce correct displacements.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(prog):
labels_seen = set()
for ins in prog:
if ins[0] == 'label':
if ins[1] in labels_seen:
return ['duplicate-label', ins[1]]
labels_seen.add(ins[1])
for ins in prog:
if ins[0] in ('jmp', 'jz') and ins[1] not in labels_seen:
return ['undefined-label', ins[1]]
long_form = set()
def size(i, ins):
if i in long_form:
return 4 if ins[0] == 'jz' else 3
return 2
rounds = 0
while True:
rounds += 1
addr = 0
addrs = []
where = {}
for i, ins in enumerate(prog):
addrs.append(addr)
if ins[0] == 'label':
where[ins[1]] = addr
elif ins[0] == 'data':
addr += ins[1]
else:
addr += size(i, ins)
changed = False
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz') and i not in long_form:
off = where[ins[1]] - (addrs[i] + 2)
if abs(off) > 127:
long_form.add(i)
changed = True
if not changed or rounds > len(prog):
break
out = []
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz'):
suffix = '.w' if i in long_form else ''
out.append([addrs[i], ins[0] + suffix, where[ins[1]] - (addrs[i] + size(i, ins))])
return {'branches': out, 'size': addr}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: three-step widening cascade',
([['data', 1],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 1], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132}),
('forward branch just around the short limit',
([['data', 1], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 201], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 1], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5}),
('duplicate label', ([['label', 'a'], ['data', 1], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 1]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 2],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[2, 'jmp.w', 129], [15, 'jz.w', 128], [134, 'jmp.w', 128]], 'size': 266}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 2], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [130, 'jmp.w', -133]], 'size': 133}),
('forward branch just around the short limit',
([['data', 2], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[2, 'jmp', 127], [131, 'jz.w', 128]], 'size': 263}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 202], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 202], [206, 'jmp', -2]], 'size': 208}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 2], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [4, 'jmp', -4]], 'size': 6}),
('duplicate label', ([['label', 'a'], ['data', 2], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 2]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 3],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[3, 'jmp.w', 129], [16, 'jz.w', 128], [135, 'jmp.w', 128]], 'size': 267}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 3], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [131, 'jmp.w', -134]], 'size': 134}),
('forward branch just around the short limit',
([['data', 3], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[3, 'jmp', 127], [132, 'jz.w', 128]], 'size': 264}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 203], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 203], [207, 'jmp', -2]], 'size': 209}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 3], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [5, 'jmp', -5]], 'size': 7}),
('duplicate label', ([['label', 'a'], ['data', 3], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 3]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 4],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[4, 'jmp.w', 129], [17, 'jz.w', 128], [136, 'jmp.w', 128]], 'size': 268}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 4], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [132, 'jmp.w', -135]], 'size': 135}),
('forward branch just around the short limit',
([['data', 4], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[4, 'jmp', 127], [133, 'jz.w', 128]], 'size': 265}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 204], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 204], [208, 'jmp', -2]], 'size': 210}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 4], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [6, 'jmp', -6]], 'size': 8}),
('duplicate label', ([['label', 'a'], ['data', 4], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 4]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 5],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[5, 'jmp.w', 129], [18, 'jz.w', 128], [137, 'jmp.w', 128]], 'size': 269}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 5], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [133, 'jmp.w', -136]], 'size': 136}),
('forward branch just around the short limit',
([['data', 5], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[5, 'jmp', 127], [134, 'jz.w', 128]], 'size': 266}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 205], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 205], [209, 'jmp', -2]], 'size': 211}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 5], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [7, 'jmp', -7]], 'size': 9}),
('duplicate label', ([['label', 'a'], ['data', 5], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 5]],), ['undefined-label', 'nowhere'])]]
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: three-step widening cascade | {'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265} | {'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265} | Passed |
| backward branch exactly -128 stays short | {'branches': [[126, 'jz.w', -130], [131, 'jmp.w', -134]], 'size': 134} | {'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132} | Failed |
| forward branch just around the short limit | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | Passed |
| wide conditional branch is four bytes | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | Passed |
| short branches to adjacent labels | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | Passed |
| duplicate label | ['duplicate-label', 'a'] | ['duplicate-label', 'a'] | Passed |
| undefined label | ['undefined-label', 'nowhere'] | ['undefined-label', 'nowhere'] | Passed |
SHA-256 / 0d0050b095048f4429dfc66544f91c5f5b0e87213f611410e72539b9b75521cb
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(prog):
labels_seen = set()
for ins in prog:
if ins[0] == 'label':
if ins[1] in labels_seen:
return ['duplicate-label', ins[1]]
labels_seen.add(ins[1])
for ins in prog:
if ins[0] in ('jmp', 'jz') and ins[1] not in labels_seen:
return ['undefined-label', ins[1]]
long_form = set()
def size(i, ins):
if i in long_form:
return 4 if ins[0] == 'jz' else 3
return 2
rounds = 0
while True:
rounds += 1
addr = 0
addrs = []
where = {}
for i, ins in enumerate(prog):
addrs.append(addr)
if ins[0] == 'label':
where[ins[1]] = addr
elif ins[0] == 'data':
addr += ins[1]
else:
addr += size(i, ins)
changed = False
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz') and i not in long_form:
off = where[ins[1]] - (addrs[i] + 2)
if off < -128 or off > 128:
long_form.add(i)
changed = True
if not changed or rounds > len(prog):
break
out = []
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz'):
suffix = '.w' if i in long_form else ''
out.append([addrs[i], ins[0] + suffix, where[ins[1]] - (addrs[i] + size(i, ins))])
return {'branches': out, 'size': addr}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: three-step widening cascade',
([['data', 1],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 1], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132}),
('forward branch just around the short limit',
([['data', 1], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 201], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 1], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5}),
('duplicate label', ([['label', 'a'], ['data', 1], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 1]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 2],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[2, 'jmp.w', 129], [15, 'jz.w', 128], [134, 'jmp.w', 128]], 'size': 266}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 2], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [130, 'jmp.w', -133]], 'size': 133}),
('forward branch just around the short limit',
([['data', 2], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[2, 'jmp', 127], [131, 'jz.w', 128]], 'size': 263}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 202], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 202], [206, 'jmp', -2]], 'size': 208}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 2], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [4, 'jmp', -4]], 'size': 6}),
('duplicate label', ([['label', 'a'], ['data', 2], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 2]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 3],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[3, 'jmp.w', 129], [16, 'jz.w', 128], [135, 'jmp.w', 128]], 'size': 267}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 3], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [131, 'jmp.w', -134]], 'size': 134}),
('forward branch just around the short limit',
([['data', 3], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[3, 'jmp', 127], [132, 'jz.w', 128]], 'size': 264}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 203], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 203], [207, 'jmp', -2]], 'size': 209}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 3], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [5, 'jmp', -5]], 'size': 7}),
('duplicate label', ([['label', 'a'], ['data', 3], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 3]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 4],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[4, 'jmp.w', 129], [17, 'jz.w', 128], [136, 'jmp.w', 128]], 'size': 268}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 4], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [132, 'jmp.w', -135]], 'size': 135}),
('forward branch just around the short limit',
([['data', 4], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[4, 'jmp', 127], [133, 'jz.w', 128]], 'size': 265}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 204], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 204], [208, 'jmp', -2]], 'size': 210}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 4], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [6, 'jmp', -6]], 'size': 8}),
('duplicate label', ([['label', 'a'], ['data', 4], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 4]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 5],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[5, 'jmp.w', 129], [18, 'jz.w', 128], [137, 'jmp.w', 128]], 'size': 269}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 5], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [133, 'jmp.w', -136]], 'size': 136}),
('forward branch just around the short limit',
([['data', 5], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[5, 'jmp', 127], [134, 'jz.w', 128]], 'size': 266}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 205], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 205], [209, 'jmp', -2]], 'size': 211}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 5], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [7, 'jmp', -7]], 'size': 9}),
('duplicate label', ([['label', 'a'], ['data', 5], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 5]],), ['undefined-label', 'nowhere'])]]
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: three-step widening cascade | {'branches': [[1, 'jmp', 127], [13, 'jz', 127], [130, 'jmp', 128]], 'size': 261} | {'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265} | Failed |
| backward branch exactly -128 stays short | {'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132} | {'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132} | Passed |
| forward branch just around the short limit | {'branches': [[1, 'jmp', 127], [130, 'jz', 128]], 'size': 260} | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | Failed |
| wide conditional branch is four bytes | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | Passed |
| short branches to adjacent labels | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | Passed |
| duplicate label | ['duplicate-label', 'a'] | ['duplicate-label', 'a'] | Passed |
| undefined label | ['undefined-label', 'nowhere'] | ['undefined-label', 'nowhere'] | Passed |
SHA-256 / e1b1a93e55f528ed9e5ea0380f9a559923f6dfbadba41faf43f11feca379758f
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(prog):
labels_seen = set()
for ins in prog:
if ins[0] == 'label':
if ins[1] in labels_seen:
return ['duplicate-label', ins[1]]
labels_seen.add(ins[1])
for ins in prog:
if ins[0] in ('jmp', 'jz') and ins[1] not in labels_seen:
return ['undefined-label', ins[1]]
long_form = set()
def size(i, ins):
if i in long_form:
return 4 if ins[0] == 'jz' else 3
return 2
rounds = 0
while True:
rounds += 1
addr = 0
addrs = []
where = {}
for i, ins in enumerate(prog):
addrs.append(addr)
if ins[0] == 'label':
where[ins[1]] = addr
elif ins[0] == 'data':
addr += ins[1]
else:
addr += size(i, ins)
changed = False
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz') and i not in long_form:
off = where[ins[1]] - (addrs[i] + 2)
if off < -128 or off > 127:
long_form.add(i)
changed = True
if not changed or rounds > len(prog):
break
out = []
for i, ins in enumerate(prog):
if ins[0] in ('jmp', 'jz'):
suffix = '.w' if i in long_form else ''
out.append([addrs[i], ins[0] + suffix, where[ins[1]] - (addrs[i] + size(i, ins))])
return {'branches': out, 'size': addr}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
cases = [[('regression: three-step widening cascade',
([['data', 1],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 1], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132}),
('forward branch just around the short limit',
([['data', 1], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 201], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 1], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5}),
('duplicate label', ([['label', 'a'], ['data', 1], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 1]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 2],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[2, 'jmp.w', 129], [15, 'jz.w', 128], [134, 'jmp.w', 128]], 'size': 266}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 2], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [130, 'jmp.w', -133]], 'size': 133}),
('forward branch just around the short limit',
([['data', 2], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[2, 'jmp', 127], [131, 'jz.w', 128]], 'size': 263}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 202], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 202], [206, 'jmp', -2]], 'size': 208}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 2], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [4, 'jmp', -4]], 'size': 6}),
('duplicate label', ([['label', 'a'], ['data', 2], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 2]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 3],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[3, 'jmp.w', 129], [16, 'jz.w', 128], [135, 'jmp.w', 128]], 'size': 267}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 3], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [131, 'jmp.w', -134]], 'size': 134}),
('forward branch just around the short limit',
([['data', 3], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[3, 'jmp', 127], [132, 'jz.w', 128]], 'size': 264}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 203], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 203], [207, 'jmp', -2]], 'size': 209}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 3], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [5, 'jmp', -5]], 'size': 7}),
('duplicate label', ([['label', 'a'], ['data', 3], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 3]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 4],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[4, 'jmp.w', 129], [17, 'jz.w', 128], [136, 'jmp.w', 128]], 'size': 268}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 4], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [132, 'jmp.w', -135]], 'size': 135}),
('forward branch just around the short limit',
([['data', 4], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[4, 'jmp', 127], [133, 'jz.w', 128]], 'size': 265}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 204], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 204], [208, 'jmp', -2]], 'size': 210}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 4], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [6, 'jmp', -6]], 'size': 8}),
('duplicate label', ([['label', 'a'], ['data', 4], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 4]],), ['undefined-label', 'nowhere'])],
[('regression: three-step widening cascade',
([['data', 5],
['jmp', 'A'],
['data', 10],
['jz', 'B'],
['data', 115],
['label', 'A'],
['jmp', 'C'],
['data', 10],
['label', 'B'],
['data', 118],
['label', 'C'],
['data', 1]],),
{'branches': [[5, 'jmp.w', 129], [18, 'jz.w', 128], [137, 'jmp.w', 128]], 'size': 269}),
('backward branch exactly -128 stays short',
([['label', 'top'], ['data', 126], ['jz', 'top'], ['data', 5], ['jmp', 'top']],),
{'branches': [[126, 'jz', -128], [133, 'jmp.w', -136]], 'size': 136}),
('forward branch just around the short limit',
([['data', 5], ['jmp', 'e'], ['data', 127], ['label', 'e'], ['jz', 'f'], ['data', 128], ['label', 'f']],),
{'branches': [[5, 'jmp', 127], [134, 'jz.w', 128]], 'size': 266}),
('wide conditional branch is four bytes',
([['jz', 'x'], ['data', 205], ['label', 'x'], ['jmp', 'x']],),
{'branches': [[0, 'jz.w', 205], [209, 'jmp', -2]], 'size': 211}),
('short branches to adjacent labels',
([['jz', 'a'], ['label', 'a'], ['data', 5], ['jmp', 'a']],),
{'branches': [[0, 'jz', 0], [7, 'jmp', -7]], 'size': 9}),
('duplicate label', ([['label', 'a'], ['data', 5], ['label', 'a']],), ['duplicate-label', 'a']),
('undefined label', ([['jmp', 'nowhere'], ['data', 5]],), ['undefined-label', 'nowhere'])]]
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: three-step widening cascade | {'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265} | {'branches': [[1, 'jmp.w', 129], [14, 'jz.w', 128], [133, 'jmp.w', 128]], 'size': 265} | Passed |
| backward branch exactly -128 stays short | {'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132} | {'branches': [[126, 'jz', -128], [129, 'jmp.w', -132]], 'size': 132} | Passed |
| forward branch just around the short limit | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | Passed |
| wide conditional branch is four bytes | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | Passed |
| short branches to adjacent labels | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | {'branches': [[0, 'jz', 0], [3, 'jmp', -3]], 'size': 5} | Passed |
| duplicate label | ['duplicate-label', 'a'] | ['duplicate-label', 'a'] | Passed |
| undefined label | ['undefined-label', 'nowhere'] | ['undefined-label', 'nowhere'] | Passed |
SHA-256 / 5a4b39057fb8f9e7546d6e8ccf83030c6152d4ff3e885d18e02aaf74ad35f1c5
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:23.954014+00:00.
Case digest / b68c762e88916d9704d58036bf88068935254ed8346760a980536ae3f7006984