51Verification

Preserve signed packed bits

Problem

mkSignedAdapter.encode accepts an Int#(32) and sends signedCarrier(value) to foreignSignedBits, whose foreign signature carries 32 unsigned bits. The C side must receive the value's complete two's-complement bit pattern so it can reinterpret the sign itself. The editable signedCarrier returns zero, so the public run prints carrier = 00000000 for -7.

Change only the body of signedCarrier. Keep the Int#(32) input type, the Bit#(32) result type, the adapter, the foreign-function declaration, and mkTop.

Read and predict

1. Read signedCarrier's types before its body. The input type records signed meaning; the result type is a plain bit vector of the same width.
2. Follow the result into foreignSignedBits. In the default Run, a BSV stand-in with the same signature returns its argument, so the display shows exactly what would cross the C boundary.
3. Before pressing Run, write the 32-bit two's-complement pattern of -7 in hexadecimal. Predict the starter's output and the repaired output.

Make the repair

This is a change of representation, not a computation. No negation, absolute value, or extension is involved: both types are 32 bits wide, and every bit must reach the carrier unchanged. Replace only the returned expression, run again, and explain why the sign bit survives even though the carrier type is unsigned.

Completion contract

• For every Int#(32) value, the carrier equals that value's packed bits.
• Negative values, zero, and positive values all keep every bit, including the sign bit.
• The function's types and the foreign signature are unchanged.
• Special-casing the displayed -7 does not satisfy other inputs.

Progressive hints

Transfer experiment

Before changing the public driver, predict the carriers for -1, 0, and 1. Then change the driver to one of them, run, and restore -7. This checks the line between signed interpretation and bit transport.