is a bit unforgiving and really doesn't like 64-bit values.

We should possibly make wrmsr() automatically truncate the
arguments, but regardless we should just fix microcode.c.