fix for riscv32.

We're now using gcc netbsd-stdint.h instead of our own definitions, so
match those with the format types

XXX wrong for 32bit.
XXX unclear if changing the fast types was the right call

Provide defines for the 64bit case.

New files for Userland support of UCB RISC-V (both 32-bit and 64-bit)