Gerwin Klein

Rebased and feedback so far integrated.

There is also a question about which other monads to support (e.g. error and/or reader monad), but so far most of the instances I've seen are on the plain nondet...

An alternative would be to remove the behaviour part of `DSpec` entirely, remove all of `DRefine`, and directly prove capDL separation logic properties about the parts of the kernel API...

@mbrcknl Do you anticipate needing `DSpec` behaviour for things like cap granting over IPC in your work?

@kent-mcleod shall we merge this and make an issue for the TODO above?

Have merged this now to unblock the web server test.

Hey @Furao -- is this relevant to your VM setup? Would you be able to have a look at it?