BTW, it occurs to me that the following simple invariant is correct
and easy to implement on all ports:

splimp() <= spl`sched'() <= splstatclock()

The fact that there are existing implementations of spl`sched'() that
are `above' splstatclock() is not relevant, because they were written
to a different specification (per my previous mail) and should be
changed anyway.

Given this, a port does not need a splraise() function (or equivalent)
to properly implement spl`sched'().