haskell+design: archMDBAssertions in cteInsert

Introduce the name and assertion "archMDBAssertions" in cteInsert so
that specific architectures can make additional MDB assumptions (e.g.
IOControlPortCap uniqueness in X64).

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

spec/design/skel/CNode_H.thy

@@ -31,6 +31,7 @@ where
   p s"
 by auto
 
-#INCLUDE_HASKELL SEL4/Object/CNode.lhs bodies_only NOT finaliseSlot cteRevoke cteDeleteOne noReplyCapsFor
+#INCLUDE_HASKELL SEL4/Object/CNode.lhs bodies_only NOT finaliseSlot cteRevoke \
+  cteDeleteOne noReplyCapsFor archMDBAssertions
 
 end

spec/haskell/src/SEL4/Object/CNode.lhs

@@ -231,6 +231,15 @@ The following functions define the operations that can be performed by a CNode i
 
 \subsubsection{Inserting New Capabilities}
 
+\begin{impdetails}
+
+Arch assertions for the refinement proof. Content is defined in Isabelle.
+
+> archMDBAssertions :: KernelState -> Bool
+> archMDBAssertions _ = error "defined in Isabelle"
+
+\end{impdetails}
+
 > setUntypedCapAsFull :: Capability -> Capability -> PPtr CTE -> Kernel ()
 > setUntypedCapAsFull srcCap newCap srcSlot = do
 >         if (isUntypedCap srcCap && isUntypedCap newCap &&
@@ -242,6 +251,12 @@ Insertion of new capabilities copied from existing capabilities is performed by
 > cteInsert :: Capability -> PPtr CTE -> PPtr CTE -> Kernel ()
 > cteInsert newCap srcSlot destSlot = do
 
+\begin{impdetails}
+
+>         stateAssert archMDBAssertions "architecture dependent MDB assertions must hold"
+
+\end{impdetails}
+
 First, fetch the capability table entry for the source.
 
 >         srcCTE <- getCTE srcSlot