arm+arm-hyp+riscv64 squash: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Dec 18, 2024 · de4b958 · de4b958
1 parent d818695
commit de4b958
Show file tree

Hide file tree

Showing 9 changed files with 34 additions and 27 deletions.
diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
@@ -282,11 +282,6 @@ qualify ARM_A (in Arch)
 record arch_tcb =
  tcb_context       :: user_context
 
-type_synonym arch_tcb_flag = unit
-
-definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
-  "word_from_arch_tcb_flag flag \<equiv> undefined"
-
 end_qualify
 
 context Arch begin arch_global_naming (A)

diff --git a/spec/abstract/ARM_HYP/Arch_Structs_A.thy b/spec/abstract/ARM_HYP/Arch_Structs_A.thy
@@ -12,7 +12,7 @@ chapter "ARM-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
@@ -338,11 +338,6 @@ record arch_state =
   arm_kernel_vspace :: ARM_HYP_A.arm_vspace_region_uses
   arm_us_global_pd  :: obj_ref
 
-type_synonym arch_tcb_flag = unit
-
-definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
-  "word_from_arch_tcb_flag flag \<equiv> undefined"
-
 end_qualify
 
 context Arch begin arch_global_naming (A)

diff --git a/spec/abstract/RISCV64/Arch_Structs_A.thy b/spec/abstract/RISCV64/Arch_Structs_A.thy
@@ -8,7 +8,7 @@ chapter "RISCV64-Specific Data Types"
 
 theory Arch_Structs_A
 imports
-  "ExecSpec.Arch_Structs_B"
+  ExecSpec.Arch_Structs_B
   ExceptionTypes_A
   VMRights_A
   ExecSpec.Arch_Kernel_Config_Lemmas
@@ -274,11 +274,6 @@ text \<open> Arch-specific part of a TCB: this must have at least a field for us
 record arch_tcb =
   tcb_context :: user_context
 
-type_synonym arch_tcb_flag = unit
-
-definition word_from_arch_tcb_flag :: "arch_tcb_flag \<Rightarrow> machine_word" where
-  "word_from_arch_tcb_flag flag \<equiv> undefined"
-
 end_qualify
 
 context Arch begin arch_global_naming (A)

diff --git a/spec/design/skel/ARM/ArchStructures_H.thy b/spec/design/skel/ARM/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PDET

diff --git a/spec/design/skel/ARM/Arch_Structs_B.thy b/spec/design/skel/ARM/Arch_Structs_B.thy
@@ -9,11 +9,17 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
+
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/ARM_HYP/ArchStructures_H.thy b/spec/design/skel/ARM_HYP/ArchStructures_H.thy
@@ -15,9 +15,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H decls_only NOT VPPIEventIRQ VirtTimer \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H instanceproofs NOT VPPIEventIRQ VirtTimer
-#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H bodies_only NOT makeVCPUObject \
+  NOT archTcbFlagToWord
 
 (* we define makeVCPUObject_def manually because we want a total function vgicLR *)
 defs makeVCPUObject_def:

diff --git a/spec/design/skel/ARM_HYP/Arch_Structs_B.thy b/spec/design/skel/ARM_HYP/Arch_Structs_B.thy
@@ -9,11 +9,16 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Main Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/ARM.lhs CONTEXT ARM_HYP_H ONLY ArmVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/ARM.lhs CONTEXT ARM_HYP_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 end
diff --git a/spec/design/skel/RISCV64/ArchStructures_H.thy b/spec/design/skel/RISCV64/ArchStructures_H.thy
@@ -16,9 +16,11 @@ context Arch begin arch_global_naming (H)
 #INCLUDE_SETTINGS keep_constructor=asidpool
 #INCLUDE_SETTINGS keep_constructor=arch_tcb
 
-#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H decls_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H decls_only \
+  NOT ArchTcbFlag archTcbFlagToWord
 #INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H instanceproofs
-#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H bodies_only \
+  NOT archTcbFlagToWord
 
 datatype arch_kernel_object_type =
     PTET

diff --git a/spec/design/skel/RISCV64/Arch_Structs_B.thy b/spec/design/skel/RISCV64/Arch_Structs_B.thy
@@ -9,13 +9,18 @@
 chapter "Common, Architecture-Specific Data Types"
 
 theory Arch_Structs_B
-imports Setup_Locale
+imports
+  Setup_Locale
+  Lib.HaskellLib_H
+  MachineExports
 begin
 
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Model/StateData/RISCV64.hs CONTEXT RISCV64_H ONLY RISCVVSpaceRegionUse
 
+#INCLUDE_HASKELL SEL4/Object/Structures/RISCV64.hs CONTEXT RISCV64_H ONLY ArchTcbFlag archTcbFlagToWord
+
 end
 
 end