design: fix ExecSpec for other architectures

Include the new ArchPSpace_H file, which on the other (non-AArch64)
architectures will only contain an empty placeholder function.

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

spec/design/skel/ARM/ArchPSpace_H.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+(* Arch-specific ghost update functions for physical memory *)
+
+theory ArchPSpace_H
+imports
+  ObjectInstances_H
+begin
+
+context Arch begin global_naming ARM_H
+
+#INCLUDE_HASKELL SEL4/Model/PSpace/ARM.hs
+
+end (* context Arch *)
+
+end

spec/design/skel/ARM_HYP/ArchPSpace_H.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+(* Arch-specific ghost update functions for physical memory *)
+
+theory ArchPSpace_H
+imports
+  ObjectInstances_H
+begin
+
+context Arch begin global_naming ARM_HYP_H
+
+#INCLUDE_HASKELL SEL4/Model/PSpace/ARM.hs
+
+end (* context Arch *)
+
+end

spec/design/skel/RISCV64/ArchPSpace_H.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+(* Arch-specific ghost update functions for physical memory *)
+
+theory ArchPSpace_H
+imports
+  ObjectInstances_H
+begin
+
+context Arch begin global_naming RISCV64_H
+
+#INCLUDE_HASKELL SEL4/Model/PSpace/RISCV64.hs
+
+end (* context Arch *)
+
+end

spec/design/skel/X64/ArchPSpace_H.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+(* Arch-specific ghost update functions for physical memory *)
+
+theory ArchPSpace_H
+imports
+  ObjectInstances_H
+begin
+
+context Arch begin global_naming X64_H
+
+#INCLUDE_HASKELL SEL4/Model/PSpace/X64.hs
+
+end (* context Arch *)
+
+end