corlewis
commented
1 month ago I'm seeing changes to the manual in the corresponding seL4 PR, and some of those descriptions look to originally have been copied from our Haskell spec comments. However, this PR does not change any Haskell or abstract comments, which seems suspicious. Either we never added/changed them for MCS (also not great), or it feels like something should get updated. Thoughts?
Hmm, I haven't done an exhaustive search but I can't see any equivalent comments in the specifications.
This commit is the corresponding specification and proof updates for https://github.com/seL4/seL4/pull/945, the second alternative described in https://github.com/seL4/rfcs/blob/main/src/active/0130-mcs-grant-reply.md.
The updates to the specifications, abstract invariants and refine proofs are complete. As crefine for MCS is still in progress, I have only updated it as needed to maintain its current state. In particular, this means that I have not proven refinement to the C code for the changes made to
receiveIPC, since that would require first updating that proof for all of the other unrelated MCS content.receiveIPCis a relatively complicated function, so this could be a significant amount of work and should probably be done separately.Test with: https://github.com/seL4/seL4/pull/945