Should we reduce DSpec to sys-init operations only?

[lsf37]

Currently DSpec has capDL behaviour for most operations in the kernel, including granting caps via IPC and other operations that the system initialiser does not use. Although we had more plans for capDL than that, the only current use for DSpec is the system initialiser and it seems unlikely that more will materialise, because user-level reasoning with actual kernel behaviour is more useful directly on the ASpec level.

One way to reduce proof size and maintenance overhead would be to replace specified behaviour in DSpec for these operations with non-determinism instead so that any ASpec behaviour will still refine DSpec by trivial refinement, essentially removing that refinement proof. As a consequence, one would no longer be able to reason about such kernel invocations on the capDL level -- but if the system initialiser is the only use case, we never have to.

We should investigate how much of the refinement proof in DRefine that would eliminate (= how many kernel invocations have a capDL specification, but are not used in the initialiser, and how much proof in DRefine those invocations correspond to).

We should also investigate if there are any other use cases or planned system initialiser extensions that would need such behaviour before we remove any.

[lsf37]

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 that are used by the initialiser. This would essentially fuse the refinement proof with the capDL-api proofs.

This would have the advantage that state that is currently invisible to the initialiser proof, such as TCB priorities, becomes accessible in that proof, because the full ASpec state is accessible.

The downside of this alternative is that it is a much larger proof change.

[lsf37]

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

[corlewis]

One thing to keep in mind is that I remember some parts of the DSpec state and its behaviour being added to make sure that it accurately represented all of the access authorities granted by corresponding ASpec states and to allow the Dpolicy proof to be completed, even though they weren't directly needed for the system initialiser.