aarch64 design: ExecSpec with PT types

adjusting caseconvs and pulling in the type at the right place for
sharing with ASpec.

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

spec/design/m-skel/AARCH64/MachineTypes.thy

@@ -3,7 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only
  *)
 
-chapter "RISCV 64bit Machine Types"
+chapter "AARCH64 Machine Types"
 
 theory MachineTypes
 imports
@@ -113,6 +113,7 @@ definition
                          machine_state_rest = undefined \<rparr>"
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs CONTEXT AARCH64 ONLY \
+  PT_Type \
   VMFaultType HypFaultType vmFaultTypeFSR VMPageSize pageBits ptTranslationBits \
   pageBitsForSize \
   hcrVCPU hcrNative vgicHCREN sctlrDefault sctlrEL1VM actlrDefault gicVCPUMaxNumLR \

spec/design/skel/AARCH64/ArchIntermediate_H.thy

@@ -41,16 +41,16 @@ defs Arch_createNewCaps_def:
         | SmallPageObject \<Rightarrow>
             createNewFrameCaps regionBase numObjects dev 0 ARMSmallPage
         | LargePageObject \<Rightarrow>
-            createNewFrameCaps regionBase numObjects dev (ptTranslationBits False) ARMLargePage
+            createNewFrameCaps regionBase numObjects dev (ptTranslationBits NormalPT_T) ARMLargePage
         | HugePageObject \<Rightarrow>
-            createNewFrameCaps regionBase numObjects dev (ptTranslationBits False + ptTranslationBits False) ARMHugePage
+            createNewFrameCaps regionBase numObjects dev (2 * ptTranslationBits NormalPT_T) ARMHugePage
         | VSpaceObject \<Rightarrow>
-            createNewTableCaps regionBase numObjects (ptBits True) (makeObject::pte)
-              (\<lambda>base addr. PageTableCap base True addr)
+            createNewTableCaps regionBase numObjects (ptBits VSRootPT_T) (makeObject::pte)
+              (\<lambda>base addr. PageTableCap base VSRootPT_T addr)
               (\<lambda>pts. return ())
         | PageTableObject \<Rightarrow>
-            createNewTableCaps regionBase numObjects (ptBits False) (makeObject::pte)
-              (\<lambda>base addr. PageTableCap base False addr)
+            createNewTableCaps regionBase numObjects (ptBits NormalPT_T) (makeObject::pte)
+              (\<lambda>base addr. PageTableCap base NormalPT_T addr)
               (\<lambda>pts. return ())
         | VCPUObject \<Rightarrow> (do
             addrs \<leftarrow> createObjects regionBase numObjects (injectKO (makeObject :: vcpu)) 0;

spec/design/skel/AARCH64/Hardware_H.thy

@@ -14,7 +14,7 @@ begin
 context Arch begin global_naming AARCH64_H
 
 #INCLUDE_HASKELL SEL4/Machine/Hardware/AARCH64.hs Platform=Platform.AARCH64 CONTEXT AARCH64_H \
-  NOT plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices \
+  NOT PT_Type plic_complete_claim getMemoryRegions getDeviceRegions getKernelDevices \
   loadWord storeWord storeWordVM getActiveIRQ ackInterrupt maskInterrupt \
   configureTimer resetTimer debugPrint getRestartPC setNextPC clearMemory \
   clearMemoryVM initMemory freeMemory setHardwareASID wordFromPDE wordFromPTE \

tools/haskell-translator/caseconvs

@@ -2049,26 +2049,6 @@ case \x of ((a@FrameCap {}), (b@FrameCap {})) -> ((a@PageTableCap {}), (b@PageTa
   then ->5
   else ->6
 
-case \x of cap@(PageTableCap { capPTisVSpace = True }) -> _ ->  ---> let cap = \x in
-  if isPageTableCap cap \<and> capPTisVSpace cap
-  then ->1
-  else ->2
-
-case \x of cap@(FrameCap {}) -> cap@(PageTableCap { capPTisVSpace = False }) -> cap@(PageTableCap { capPTisVSpace = True }) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->  ---> let cap = \x in
-  if isFrameCap cap
-  then ->1
-  else if isPageTableCap cap \<and> \<not> capPTisVSpace cap
-  then ->2
-  else if isPageTableCap cap \<and> capPTisVSpace cap
-  then ->3
-  else if isASIDControlCap cap
-  then ->4
-  else if isASIDPoolCap cap
-  then ->5
-  else if isVCPUCap cap
-  then ->6
-  else undefined
-
 case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@FrameCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@VCPUCap {}) ->  ---> let c = \x in
   if isPageTableCap c \<and> capPTMappedAddress c \<noteq> None
   then ->1
@@ -2084,6 +2064,26 @@ case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { c
   then ->6
   else undefined
 
+case \x of cap@(PageTableCap { capPTType = VSRootPT_T }) -> _ ->  ---> let cap = \x in
+  if isPageTableCap cap \<and> capPTType cap = VSRootPT_T
+  then ->1
+  else ->2
+
+case \x of cap@(FrameCap {}) -> cap@(PageTableCap { capPTType = NormalPT_T }) -> cap@(PageTableCap { capPTType = VSRootPT_T }) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (VCPUCap {}) ->  ---> let cap = \x in
+  if isFrameCap cap
+  then ->1
+  else if isPageTableCap cap \<and> capPTType cap = NormalPT_T
+  then ->2
+  else if isPageTableCap cap \<and> capPTType cap = VSRootPT_T
+  then ->3
+  else if isASIDControlCap cap
+  then ->4
+  else if isASIDPoolCap cap
+  then ->5
+  else if isVCPUCap cap
+  then ->6
+  else undefined
+
 case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> Arch.Types.VSpaceObject -> Arch.Types.VCPUObject ->  ---> case \x of
     APIObjectType \v0\ \<Rightarrow> ->1
   | SmallPageObject \<Rightarrow> ->2