capDL-tool, capdl-loader-app: Add support for binding notifications for TCBs

[nspin]

This will be required by Microkit.

[lsf37]

This might have verification impact for the system initialiser. @corlewis do we need to do anything special in the tools or is this just excluded in spec wellformedness for sys-init?

Do you think it would be hard to add to the sys-init proofs?

[lsf37]

The code changes as such look good to me.

[corlewis]

This might have verification impact for the system initialiser. @corlewis do we need to do anything special in the tools or is this just excluded in spec wellformedness for sys-init?

Do you think it would be hard to add to the sys-init proofs?

Bound notifications are currently excluded by wellformedness, so there won't be any immediate issues with sys-init.

There's two parts to adding it to the verified system initialiser, creating a wp rule for seL4_TCB_BindNotification, and updating the specification and correctness proof. The second part shouldn't be too hard, but while I don't have any experience with the capDL-api proofs, my guess is that the first could be difficult.

[corlewis]

The capDL-tool will need some changes in PrintIsabelle.hs so that it produces output that is consistent with the verification capDL specification. In particular, the verification specification doesn't know about the MCS caps that can be in a TCBs CNode, and so its equivalent to tcbBoundNotificationSlot is set to 6 instead of 8. We'll need to do this translation somewhere in PrintIsabelle.hs.

[corlewis]

The capDL-tool will need some changes in PrintIsabelle.hs so that it produces output that is consistent with the verification capDL specification. In particular, the verification specification doesn't know about the MCS caps that can be in a TCBs CNode, and so its equivalent to tcbBoundNotificationSlot is set to 6 instead of 8. We'll need to do this translation somewhere in PrintIsabelle.hs.

Hmm, I guess that an easier alternative would be to update the verification specification's TCB slots instead. I don't think that that would affect any of the proofs and we could leave a comment there explaining the unexpected ordering.

That would probably be more maintainable as well. I might give that a go to make sure that there aren't any proof impacts that I'm missing. I'll report back once I've done an initial pass.

[corlewis]

Hmm, I guess that an easier alternative would be to update the verification specification's TCB slots instead. I don't think that that would affect any of the proofs and we could leave a comment there explaining the unexpected ordering.

That would probably be more maintainable as well. I might give that a go to make sure that there aren't any proof impacts that I'm missing. I'll report back once I've done an initial pass.

The proof update was a little bit more involved than I was first guessing, but it wasn't too bad. See seL4/l4v#716.

However, while this is still the easiest way forwards at the moment, I've changed my mind and now think the best maintainability would be to do the translation in capDL-tool. That would keep all of the changes in one place and not lead to needing to know to make a change to l4v after making a change to the TCB cap slots here in capdl.

I'm happy to go with what we have here though, and leave that for the future if/when we make further changes to the cap slots.

[lsf37]

@corlewis I'd be fine with merging seL4/l4v#716 and this PR here. It's relatively rare that we update these slots, so it shouldn't be too much of maintenance burden.