Formally prove claims about the interrupt executor and benchmark it

[fg-cfh]

We'd like to make a few claims about the interrupt executor that we cannot formally prove yet. It would be nice if someone could help us to prove claims roughly along the following lines:

• The only required safety condition is that sub-tasks run at higher priority than the nesting context (i.e. the executor doesn't trigger UB when used from safe code as long as those criteria are being respected)
• The executor can be safely nested, e.g. main -> swi1 (mac) -> swi0 (drv_svc) -> radio/timer/rtc
• Resources shared between the scheduling context and the interrupt context are protected from races via lockless atomics and SRP. We can capture shared resources along the call hierarchy in async blocks or poll_fn() closures w/o explicit locking.
• If we align the call hierarchy with task priority then variable visibility will automatically enforce SRP resource sharing restrictions.
• The hierarchical approach allows us to allocate tasks on the stack and spawn them inline w/o top-level static declarations or macros. This amounts to dynamically "re-programming" the interrupt handler based on context. The result is simplified interrupt handler development and improved encapsulation. As typestate provides very narrow execution context, our interrupt handlers are trivial compared to the classic centralistic state machine.
• "State-specific" handlers execute faster because we don't need to check lots of logic conditions until reaching the execution path that is actually requested.
• We get lower latency and less-to-no jitter if compared to dropping down to the main application executor.

Additionally:

• It would be nice if we could turn the interface into a safe interface by introducing appropriate compile time (or at least runtime) checks.
• It would be nice if we could compare our resource sharing approach with RTIC and identify feature gaps. Can we close those gaps and achieve feature parity with RTIC?
• We could do a benchmark against Nordic's official interrupt handler.