Would any of seL4's guarantees be compromised if a Translate method were added to page directory objects (for mapping a virtual address to the underlying physical address, without exposing the intermediate page capabilities)?