arm-hyp abstract/design: object_type enum reorder

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4 · Aug 11, 2023 · 8ba1b46 · 8ba1b46
1 parent 7f490df
commit 8ba1b46
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/spec/abstract/ARM_HYP/ArchDecode_A.thy b/spec/abstract/ARM_HYP/ArchDecode_A.thy
@@ -259,12 +259,12 @@ where
 definition
   arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option" where
  "arch_data_to_obj_type n \<equiv>
-  if n = 0 then Some SmallPageObj
-  else if n = 1 then Some LargePageObj
-  else if n = 2 then Some SectionObj
-  else if n = 3 then Some SuperSectionObj
-  else if n = 4 then Some PageTableObj
-  else if n = 5 then Some PageDirectoryObj
+  if n = 0 then Some PageDirectoryObj
+  else if n = 1 then Some SmallPageObj
+  else if n = 2 then Some LargePageObj
+  else if n = 3 then Some SectionObj
+  else if n = 4 then Some SuperSectionObj
+  else if n = 5 then Some PageTableObj
   else if n = 6 then Some VCPUObj
   else None"
 

diff --git a/spec/design/skel/ARM_HYP/ArchTypes_H.thy b/spec/design/skel/ARM_HYP/ArchTypes_H.thy
@@ -34,12 +34,12 @@ interpretation Arch .
 definition
   enum_object_type: "enum_class.enum \<equiv>
     map APIObjectType (enum_class.enum :: apiobject_type list) @
-     [SmallPageObject,
+     [PageDirectoryObject,
+      SmallPageObject,
       LargePageObject,
       SectionObject,
       SuperSectionObject,
       PageTableObject,
-      PageDirectoryObject,
       VCPUObject
     ]"