Indan Zupancic

> Thanks for your feedback! Would it be an acceptable solution if I port my changeset to other archs and get rid of the magic 2 and 4 numbers? I...

When there are multiple parties managing virtual address space, it's good to have clear rules who uses which address range. In this case it's the linker and Microkit, but also...

First simplification that can be done: Considering legacy extensions are not supported, we can get rid of `capSBIEIDBadged` and check badge value of zero instead. Improvement is limited because we...

Problem is, how do you distinguish reply cap transfer from cap transfer by the sender? Easiest way is to steal one bit from the label and use it to mark...

Do you need actual support for parsing interrupt-multiplex or is it enough that hardware_gen.py doesn't choke on it?

To clarify, the loader should still program the registers necessary to enable the MMU before jumping to the kernel, but the kernel shouldn't assume anything about that and configure things...

Is the problem that SGI support is not enabled by default? Once the proofs have been updated, there is no reason to have a user config option for SGIs any...

> > Main comment is that I wouldn't introduce new syscalls, nor `updateCapDataLong()` , but add a new, optional argument to the existing syscalls on 32-bit platforms and make capData...

> If I'm understanding correctly, it did indeed come up before and you already fixed it as part of some work that unfortunately never quite managed to be finished. See...

Like Arm says, "the selected granule is the smallest block that can be described in the last level table". It is not the minimum page itself, so calling pages granules...