FA-89721 / Instruction set emulation / Open access

Writes to r0 are kept · case 01

After addi r0, r0 is nonzero and later reads of r0 are wrong.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

The register write does not discard writes to r0.

VERIFIED REPAIR

Discard any write whose destination is r0.

Unsuccessful approach: Special-casing particular immediates still lets some writes to r0 through.

Case contract

Input [prog, limit]: word-indexed instructions at byte addresses 4*i: addi rt rs imm, beq/bne/beql rs rt off16, j index, nop, halt; 8 registers with r0 hardwired to 0. Branch target = branch address + 4 + (sign-extended off16 << 2). The instruction after a branch or jump (its delay slot) always executes before control transfers, except that a not-taken beql skips (annuls) its slot. j target = ((pc+4) & 0xF0000000) | (index << 2). Addresses outside the program behave as halt. Return [executed pcs, registers].

Why this case matters

Emulating MIPS-style pipelines requires executing the architectural delay slot and computing targets from the slot address.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    prog, limit = args
    r = [0] * 8
    pc = 0
    trace = []
    pending = None
    steps = 0
    while steps < limit:
        steps += 1
        ins = prog[pc // 4] if 0 <= pc // 4 < len(prog) else ['halt']
        trace.append(pc)
        op = ins[0]
        nxt = pc + 4
        if op == 'halt':
            break
        if op == 'addi':
            if True:
                r[ins[1]] = r[ins[2]] + ins[3]
        elif op in ('beq', 'bne', 'beql'):
            taken = (r[ins[1]] == r[ins[2]]) == (op != 'bne')
            off = ins[3] - 0x10000 if ins[3] & 0x8000 else ins[3]
            tgt = pc + 4 + (off << 2)
            if op == 'beql' and not taken:
                nxt = pc + 8
            else:
                pending = tgt if taken else pc + 8
        elif op == 'j':
            pending = ((pc + 4) & 0xF0000000) | (ins[1] << 2)
        if pending is not None and op not in ('beq', 'bne', 'beql', 'j'):
            nxt = pending
            pending = None
        pc = nxt
    return [trace, r]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 2], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 3], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 1], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 3], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 6, 3, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 4], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 4, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 2], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 3, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 4], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 8, 4, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 5], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 5, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 3], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 4, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 5], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 10, 5, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 6], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 6, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 4], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 5, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 6], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 12, 6, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 7], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 7, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 5], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 6, 0]])]]
for label, args, expected in fixtures[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
forward taken beq	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	Passed
backward counted loop	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	Passed
branch likely not taken annuls slot	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	Passed
branch likely taken runs slot	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	Passed
zero register and jump	`[[0, 4, 8, 12, 16, 20, 24], [8, 3, 0, 0, 9, 10, 11, 0]]`	`[[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]`	Failed
bne with nop slot	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	Passed

SHA-256 / f4820826dd05c8e21b29c0a669241fba41f27f812a0e7e9e5da758d7c78abb93

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    prog, limit = args
    r = [0] * 8
    pc = 0
    trace = []
    pending = None
    steps = 0
    while steps < limit:
        steps += 1
        ins = prog[pc // 4] if 0 <= pc // 4 < len(prog) else ['halt']
        trace.append(pc)
        op = ins[0]
        nxt = pc + 4
        if op == 'halt':
            break
        if op == 'addi':
            if ins[1] or ins[3] == 5:
                r[ins[1]] = r[ins[2]] + ins[3]
        elif op in ('beq', 'bne', 'beql'):
            taken = (r[ins[1]] == r[ins[2]]) == (op != 'bne')
            off = ins[3] - 0x10000 if ins[3] & 0x8000 else ins[3]
            tgt = pc + 4 + (off << 2)
            if op == 'beql' and not taken:
                nxt = pc + 8
            else:
                pending = tgt if taken else pc + 8
        elif op == 'j':
            pending = ((pc + 4) & 0xF0000000) | (ins[1] << 2)
        if pending is not None and op not in ('beq', 'bne', 'beql', 'j'):
            nxt = pending
            pending = None
        pc = nxt
    return [trace, r]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 2], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 3], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 1], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 3], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 6, 3, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 4], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 4, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 2], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 3, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 4], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 8, 4, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 5], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 5, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 3], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 4, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 5], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 10, 5, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 6], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 6, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 4], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 5, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 6], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 12, 6, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 7], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 7, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 5], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 6, 0]])]]
for label, args, expected in fixtures[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
forward taken beq	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	Passed
backward counted loop	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	Passed
branch likely not taken annuls slot	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	Passed
branch likely taken runs slot	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	Passed
zero register and jump	`[[0, 4, 8, 12, 16, 20, 24], [8, 3, 0, 0, 9, 10, 11, 0]]`	`[[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]`	Failed
bne with nop slot	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	Passed

SHA-256 / 4c4f137a16e1d25564808ce8aa34205976aada7a3e8cc6d63c3948e859582bef

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(*args):
    prog, limit = args
    r = [0] * 8
    pc = 0
    trace = []
    pending = None
    steps = 0
    while steps < limit:
        steps += 1
        ins = prog[pc // 4] if 0 <= pc // 4 < len(prog) else ['halt']
        trace.append(pc)
        op = ins[0]
        nxt = pc + 4
        if op == 'halt':
            break
        if op == 'addi':
            if ins[1]:
                r[ins[1]] = r[ins[2]] + ins[3]
        elif op in ('beq', 'bne', 'beql'):
            taken = (r[ins[1]] == r[ins[2]]) == (op != 'bne')
            off = ins[3] - 0x10000 if ins[3] & 0x8000 else ins[3]
            tgt = pc + 4 + (off << 2)
            if op == 'beql' and not taken:
                nxt = pc + 8
            else:
                pending = tgt if taken else pc + 8
        elif op == 'j':
            pending = ((pc + 4) & 0xF0000000) | (ins[1] << 2)
        if pending is not None and op not in ('beq', 'bne', 'beql', 'j'):
            nxt = pending
            pending = None
        pc = nxt
    return [trace, r]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
fixtures = [[('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 2], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 3], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 1], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 3], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 6, 3, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 4], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 4, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 2], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 3, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 4], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 8, 4, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 5], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 5, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 3], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 4, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 5], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 10, 5, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 6], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 6, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 4], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 5, 0]])], [('forward taken beq', [[['addi', 1, 0, 3], ['beq', 0, 0, 2], ['addi', 2, 2, 1], ['addi', 3, 0, 9], ['halt']], 40], [[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]), ('backward counted loop', [[['addi', 1, 0, 6], ['addi', 2, 2, 2], ['addi', 1, 1, -1], ['bne', 1, 0, 65533], ['addi', 3, 3, 1], ['halt']], 60], [[0, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 12, 6, 0, 0, 0, 0]]), ('branch likely not taken annuls slot', [[['addi', 1, 0, 1], ['beql', 1, 0, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['halt']], 40], [[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]), ('branch likely taken runs slot', [[['addi', 1, 0, 1], ['beql', 1, 1, 2], ['addi', 2, 0, 7], ['addi', 3, 0, 4], ['addi', 4, 0, 5], ['halt']], 40], [[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]), ('zero register and jump', [[['addi', 1, 0, 7], ['addi', 0, 1, 5], ['addi', 4, 0, 1], ['j', 5], ['addi', 5, 4, 1], ['addi', 6, 0, 3], ['halt']], 40], [[0, 4, 8, 12, 16, 20, 24], [0, 7, 0, 0, 1, 2, 3, 0]]), ('bne with nop slot', [[['addi', 1, 0, 1], ['bne', 1, 0, 3], ['nop'], ['addi', 7, 0, 1], ['halt'], ['addi', 6, 1, 5], ['halt']], 40], [[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 6, 0]])]]
for label, args, expected in fixtures[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
forward taken beq	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	`[[0, 4, 8, 16], [0, 3, 1, 0, 0, 0, 0, 0]]`	Passed
backward counted loop	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	`[[0, 4, 8, 12, 16, 4, 8, 12, 16, 20], [0, 0, 4, 2, 0, 0, 0, 0]]`	Passed
branch likely not taken annuls slot	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	`[[0, 4, 12, 16], [0, 1, 0, 4, 0, 0, 0, 0]]`	Passed
branch likely taken runs slot	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	`[[0, 4, 8, 16, 20], [0, 1, 7, 0, 5, 0, 0, 0]]`	Passed
zero register and jump	`[[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]`	`[[0, 4, 8, 12, 16, 20, 24], [0, 3, 0, 0, 1, 2, 3, 0]]`	Passed
bne with nop slot	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	`[[0, 4, 8, 20, 24], [0, 1, 0, 0, 0, 0, 2, 0]]`	Passed

SHA-256 / 1e2caedfb6642996cdeaf03ff48831d82f9e03b7a79d8a46d93687fbea5e8790

Verification & scope

A deterministic bounded teaching model of one emulator rule; the instruction semantics are a stipulated contract inspired by common ISAs and are not a claim of cycle-exact or architectural conformance. 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:19.972686+00:00.

Case digest / e24c0184c3bbaab595cbb13c48511a130e5ffcca6dfbcac62fbd30e0db1dc07e