27Verification

Repair a hand-written Bits instance

Problem

The protocol assigns Idle to 01, Start to 10, and Stop to 11. pack implements that contract, but the starter's unpack table does not reverse it. The code compiles because Bits#(Command, 2) proves conversion types and widths, not agreement between case arms.

Edit only unpack's decoding behavior. Keep the enum, pack, instance header, helper functions, and mkTop structure intact.

Read and predict before editing

Read Command and the instance header, then compare every pack arm with the unpack arms as two directions of one protocol table. Finally trace mkTop: its first display observes an encoding and its second observes one decoding.

Before editing, predict both observations. Encoding Stop produces 11, but decoding 01 currently produces Start instead of Idle. Run the starter to confirm that one direction is correct and the other is not. This is a semantic simulation failure, not a missing-instance compile error.

Make the minimum repair

Reverse the existing encoding relation rather than inventing another ordering. Assigned codes must decode to their original labels, while unassigned 00 must decode to Idle. Do not change an encoding arm or width declaration.

After the edit, Run must still show 11 for Stop, while decoding 01 must identify Idle. Also reason through all three semantic values to check unpack(pack(value)) == value, and through all four bit patterns. The unused 00 normalizes to Idle, so packing that decoded value yields 01.

Completion requires correct decoding, all round trips, the fallback, and unchanged encoding. Fixing only the displayed 01 case is incomplete.

Progressive hints

Transfer experiment

Temporarily change only the decoded input observed by mkTop from 01 to 10. Predict Start, run once, and restore it. This distinguishes a repaired protocol relation from a special case for the original sample.