FA-90151 / Bytecode virtual machines / Open access
Branch relaxation: single relaxation pass · case 01
A branch pushed out of range by another branch widening stays short and wraps.
ROOT CAUSE
Relaxation stops after the first pass even when widening changed addresses.
VERIFIED REPAIR
Repeat address assignment until no branch is widened (bounded by the number of instructions).
Unsuccessful approach: Allowing a second pass still misses cascades that need three rounds.
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 off < -128 or off > 127:
long_form.add(i)
changed = True
if not changed or rounds >= 1:
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.w', 127]], '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': 131} | {'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', 126]], 'size': 260} | {'branches': [[1, 'jmp', 127], [130, 'jz.w', 128]], 'size': 262} | Failed |
| wide conditional branch is four bytes | {'branches': [[0, 'jz.w', 199], [203, 'jmp', -2]], 'size': 205} | {'branches': [[0, 'jz.w', 201], [205, 'jmp', -2]], 'size': 207} | Failed |
| 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 / 320783401a76eb54dd52478ca597d671c9b2afbedb01984c8851aaaf4a9904f6
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 > 127:
long_form.add(i)
changed = True
if not changed or rounds >= 2:
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.w', 126], [130, 'jmp.w', 128]], 'size': 262} | {'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.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 / ecdfad005bc2efd574dfa3e0d876f1c3119661ca839e286f89dae85b9e0acbef
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.994906+00:00.
Case digest / 84a59ef1fdb6b5c7b524eb11261f20a8e02521656ec7e7b532559871b58d8231