> Is there some hideously complicated reason we can't add up the sizes, and 
> _then_ set VM_MAX_KERNEL_ADDRESS?

Hm.  At first glance, this would seem likely to break DDB.