Gerwin Klein

> I'm curious if it is even be possible to host CHERI aware applications without large changes to the kernel object APIs. I think of how FPU extensions are added...

It looks a bit weird to just declare these as globals, but that is what `gic_common.h` does [here](https://github.com/seL4/seL4/blob/85aa104eb4d527bc9f0aac28f3e9c3a84eed1d7a/include/arch/arm/arch/machine/gic_common.h#L58).

You're right, the global does look strange, because we are getting a constant in Isabelle there, which we usually wouldn't. I'll investigate more next week. The problem is only that...

> Why not just: > > ``` > #define irqInvalid 255U > ``` Because we need the value to have a symbolic name in the verification if we want to...

> > Because we need the value to have a symbolic name in the verification if we want to keep the proof generic. If it's a `#define`, the proof only...

From @Xaphiosis: > Hang on, if we make it a global variable instead of an enum, we don't get a constant out of the C parser. Turns out that is...

> Does this mean we should re-open #1349 which uses "static const" (so that the compilers are better at inlining/realising it's a constant since it's not externally visible?) Good point....

> > Does this mean we should re-open #1349 which uses "static const" (so that the compilers are better at inlining/realising it's a constant since it's not externally visible?) >...

This might be mostly unrelated to the printing, but it would be good to trace how this could have any influence at all on behaviour after boot. It could be...

@mktnk3 any insight from the verification side how `seL4 failed assertion 'refill_ready(thread->tcbSchedContext)' at /github/workspace/kernel/src/kernel/thread.c:447 in function switchToThread` could be happening directly or very soon after boot? It looks like this...