36Verification

Reject the boundary opcode

Problem

decodeSmall should accept an instruction whose upper nibble is 1010 only when its four-bit payload is below ten, and return that payload. Every other instruction returns zero. The literal pattern is correct, but the filter after it also lets the boundary value ten through. In the public run, the payload 10 line shows 10 where the contract requires 0.

Fix the filter only. Keep the 8'b1010_???? pattern, the default arm and its position, the function signature, and mkTop. Do not replace pattern matching with a bit mask.

Read and predict

1. Read the first arm in two parts: the pattern before &&&, then the filter after it.
2. Read the default arm. It handles every instruction the first arm rejects, whether the pattern or the filter rejected it.
3. Read the three calls in mkTop: payload nine, payload ten, and an instruction with a different prefix.

Before pressing Run, predict all three lines for the starter. Payload nine gives 9, payload ten gives 10, and the other prefix gives 0. Only the middle line is wrong. Also predict payload eleven: it already falls through to default.

Make the repair

The defect sits at exactly one point of the range: the comparison accepts equality. Change only the comparison in the filter so that ten fails it, then run again. The middle line must now show 0 while the other two lines stay the same. Explain which arm produced each of the three results.

Completion contract

• Instructions with prefix 1010 and payload zero through nine return their payload, including payload zero.
• Payloads ten through fifteen with that prefix return zero.
• Every other prefix returns zero, whatever its low nibble.
• Arm order is unchanged, so the filtered arm is still tried before default.
• The contract covers all 256 instruction values, not only the three printed ones; state the accepted range as a rule rather than excluding one sample.

Progressive hints

Transfer experiment

On paper, move the default arm above the filtered arm. Predict all three outputs and explain why the filtered arm becomes unreachable.