We discussed this a little here, but I think PC should be a virtaddr rather than xlenbits like it currently is.
PC
virtaddr
xlenbits