Gerwin Klein

> @lsf37 What do you mean by "zero-ing"? Implicit initialization of kernel objects by Retype? Yes, `resetUntypedCap` uses `memzero` to clear memory so that Retype can assume it's all zeroes,...

> What would people think of including the name of the block or union in the name of the words field, so that you can search the code for e.g....

> re. benchmarks: I don't currently have one of every device on the seL4 benchmarks, so I'm not sure what the best way to handle that is. @nomadeel would you...

It looks like there is a bunch of work here that would still be useful, even though verification impact could be fairly high. @sorear are you planning on working more...

Yes, the style error is genuine, please replace the tabs with spaces. In the `sel4_tools` repo, there is a script `style_all.sh` that you can run on the file to make...

Nice. How hard would it be to generate a test case for that? I guess reliably triggering an IRQ when a thread is in the release queue is not exactly...

This is still on draft, so I haven't looked at it yet, but it seems that a lot of the PR checks are failing. These should work before we really...

> > This is still on draft, so I haven't looked at it yet, but it seems that a lot of the PR checks are failing. These should work before...

> I've now pushed fixes that make the kernel compile. Hopefully that's enough to give some insights? Thanks. It is, but the insights are not good -- there is way...

> Thanks for having a look! I am expecting that eventually non-CHERI builds should not change in terms of the generated binary code. I had to change the bitfield generator...