refine+crefine: update for arch_requalify design spec updates

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
seL4 · Aug 19, 2024 · e00f7b4 · e00f7b4
1 parent 723a7b6
commit e00f7b4
Show file tree

Hide file tree

Showing 16 changed files with 34 additions and 34 deletions.
diff --git a/proof/crefine/AARCH64/Invoke_C.thy b/proof/crefine/AARCH64/Invoke_C.thy
@@ -2812,10 +2812,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)

diff --git a/proof/crefine/AARCH64/Retype_C.thy b/proof/crefine/AARCH64/Retype_C.thy
@@ -5047,7 +5047,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -5070,14 +5070,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory

diff --git a/proof/crefine/ARM/Invoke_C.thy b/proof/crefine/ARM/Invoke_C.thy
@@ -2623,10 +2623,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)

diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy
@@ -4350,7 +4350,7 @@ lemma placeNewObject_user_data:
 
 
 definition
-  createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4373,14 +4373,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory

diff --git a/proof/crefine/ARM_HYP/Invoke_C.thy b/proof/crefine/ARM_HYP/Invoke_C.thy
@@ -2828,10 +2828,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)

diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy
@@ -4919,7 +4919,7 @@ lemma placeNewObject_user_data:
 
 
 definition
-  createObject_hs_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4942,14 +4942,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "word32 \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "word32 \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory

diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy
@@ -2774,10 +2774,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)

diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy
@@ -4796,7 +4796,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -4819,14 +4819,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory

diff --git a/proof/crefine/X64/Invoke_C.thy b/proof/crefine/X64/Invoke_C.thy
@@ -2800,10 +2800,10 @@ lemma ctes_of_ex_cte_cap_to':
 
 
 lemma Arch_isFrameType_spec:
-  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::ArchTypes_H.object_type)\<rbrace>
+  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. unat \<acute>type \<le> fromEnum (maxBound::object_type)\<rbrace>
              Call Arch_isFrameType_'proc
   \<lbrace> \<acute>ret__unsigned_long =
-     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::ArchTypes_H.object_type))\<rbrace>"
+     from_bool (isFrameType ((toEnum (unat \<^bsup>s\<^esup> type))::object_type))\<rbrace>"
   apply vcg
   apply (simp add: toEnum_object_type_to_H)
   apply (frule object_type_from_to_H)

diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy
@@ -5628,7 +5628,7 @@ lemma placeNewObject_user_data:
   done
 
 definition
-  createObject_hs_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
+  createObject_hs_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> kernel_state \<Rightarrow> bool"
 where
   "createObject_hs_preconds regionBase newType userSize d \<equiv>
      (invs' and pspace_no_overlap' regionBase (getObjectSize newType userSize)
@@ -5651,14 +5651,14 @@ abbreviation
 
 (* these preconds actually used throughout the proof *)
 abbreviation(input)
-  createObject_c_preconds1 :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds1 :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds1 regionBase newType userSize deviceMemory \<equiv>
     {s. region_actually_is_dev_bytes regionBase (2 ^ getObjectSize newType userSize) deviceMemory s}"
 
 (* these preconds used at start of proof *)
 definition
-  createObject_c_preconds :: "machine_word \<Rightarrow> ArchTypes_H.object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
+  createObject_c_preconds :: "machine_word \<Rightarrow> object_type \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> (globals myvars) set"
 where
   "createObject_c_preconds regionBase newType userSize deviceMemory \<equiv>
   (createObject_c_preconds1 regionBase newType userSize deviceMemory

diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy
@@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"

diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy
@@ -526,7 +526,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"

diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy
@@ -1797,11 +1797,11 @@ lemma invokeIRQControl_no_orphans [wp]:
   apply (wp | clarsimp)+
   done
 
-lemma invokeIRQHandler_no_orphans [wp]:
+lemma arch_invokeIRQHandler_no_orphans[wp]:
   "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
-   invokeIRQHandler i
+   ARM_H.invokeIRQHandler i
    \<lbrace> \<lambda>reply s. no_orphans s \<rbrace>"
-  apply (cases i, simp_all add: invokeIRQHandler_def)
+  apply (cases i, simp_all add: ARM_H.invokeIRQHandler_def)
     apply (wp | clarsimp | fastforce)+
   done
 
@@ -1939,7 +1939,7 @@ lemma setDomain_no_orphans [wp]:
   apply (fastforce simp: tcb_at_typ_at'  is_active_tcb_ptr_runnable')
   done
 
-crunch InterruptDecls_H.invokeIRQHandler
+crunch invokeIRQHandler
   for no_orphans[wp]: no_orphans
 
 lemma performInvocation_no_orphans [wp]:

diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy
@@ -536,7 +536,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"

diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy
@@ -534,7 +534,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"

diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy
@@ -535,7 +535,7 @@ crunch InterruptDecls_H.invokeIRQHandler
   for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
 
 lemmas invokeIRQHandler_typ_ats[wp] =
-  typ_at_lifts [OF InterruptDecls_H_invokeIRQHandler_typ_at']
+  typ_at_lifts [OF invokeIRQHandler_typ_at']
 
 crunch setDomain
   for tcb_at'[wp]: "tcb_at' tptr"