Gerwin Klein

I'm not convinced. This complicates the boot code, which is not verified, so it needs extra strong scrutiny, and supporting seL4 in virtualised environments is creating temptation for using it...

Can you please provide motivation for the change in the description so the we can figure out in the future why we did this? The C proofs all seem to...

This might actually not be needed. It's used to prove the `align_td` lemma underneath, which should still be true, and then the `ptr_inverse_safe` lemma which I have no idea what...

Right, I forgot to update RISCV64 and X64 for the new `init_arch_objs` parameter. Will add.

Now done. The two additional commits should probably be squashed into the first two.

> I think this is not that bad, and the performance improvement on the seL4 side is definitely good. Could I ask why x64 and RISCV are having such an...

(rebased on current master)