10Verification

Narrow a byte explicitly

Read the failure before repairing it

Read lowNibble in three steps: its input is Bit#(8), its return contract is Bit#(4), and its body currently returns the input unchanged. Then inspect mkTop to see that Run will call it with 8'ha5 and display the returned nibble.

Before editing, predict the phase that fails. The source asks BSV to unify an eight-bit expression with a four-bit result, so type checking should stop before simulation rather than silently dropping a. The visible symptom is a bit-size mismatch; the root cause is an implicit narrowing conversion.

Only the return expression in lowNibble needs repair. Keep the package, function signature, mkTop, and public observation unchanged.

Reason about the minimal repair

The contract does not ask for saturation, a comparison, or a reordered nibble. It asks to discard high bits and preserve low bits. Use one explicit width operation whose meaning is exactly that policy. The destination type already tells BSV how many low bits must remain, so no new local state or control flow is needed.

Run after editing. Successful compilation proves the conversion is explicit and well typed; the displayed nibble proves that the low half of the mixed sample survives.

Observable completion contract

Completion means more than making 8'ha5 display 5:

the function still accepts Bit#(8) and returns Bit#(4);
inputs with only low bits set preserve those bits;
inputs with only high bits set return zero;
mixed inputs discard bits [7:4] and preserve bits [3:0] exactly.

A fixed result or a conversion that selects the high nibble violates at least one of these observations.

Progressive hints

Hint 1: name the violated contract

The return type is narrower than the current expression. BSV requires source code to state intentional data loss.

Hint 2: identify the retained region

The required result is the low end of the input. Check which family of bit-width operations discards high positions rather than extending or reinterpreting.

Hint 3: choose the primitive

truncate expresses an intentional narrowing and derives the retained width from its context. Apply it at the function's return expression without changing the signature.

Transfer experiment

After completing the task, temporarily change the return width to three bits and test an input whose low nibble is 1101. Predict which three bits remain. Then restore the required signature. The same repair should derive its result width from context rather than containing a four-bit-specific mask.