arm+arm_hyp+aarch64 crefine: fix name of setThreadState_tcbContext

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Mar 27, 2024 · 21014ea · 21014ea
1 parent 79456ff
commit 21014ea
Show file tree

Hide file tree

Showing 6 changed files with 15 additions and 15 deletions.
diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy
@@ -54,7 +54,7 @@ lemma setCTE_tcbContext:
   apply (rule setObject_cte_obj_at_tcb', simp_all)
   done
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 

diff --git a/proof/crefine/AARCH64/Fastpath_Equiv.thy b/proof/crefine/AARCH64/Fastpath_Equiv.thy
@@ -49,7 +49,7 @@ lemma setCTE_tcbContext:
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 
@@ -1697,7 +1697,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
                                           fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]
                                | wps)+)[3]
                     apply (simp cong: rev_conj_cong)
-                    apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply]
+                    apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply]
                                       setThreadState_oa_queued user_getreg_rv
                                       setThreadState_no_sch_change setThreadState_obj_at_unchanged
                                       sts_st_tcb_at'_cases sts_bound_tcb_at'

diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy
@@ -54,7 +54,7 @@ lemma setCTE_tcbContext:
   apply (rule setObject_cte_obj_at_tcb', simp_all)
   done
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 

diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy
@@ -49,7 +49,7 @@ lemma setCTE_tcbContext:
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 
@@ -1558,7 +1558,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
                                           fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]
                                | wps)+)[3]
                     apply (simp cong: rev_conj_cong)
-                    apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply]
+                    apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply]
                                       setThreadState_oa_queued user_getreg_rv
                                       setThreadState_no_sch_change setThreadState_obj_at_unchanged
                                       sts_st_tcb_at'_cases sts_bound_tcb_at'

diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy
@@ -54,7 +54,7 @@ lemma setCTE_tcbContext:
   apply (rule setObject_cte_obj_at_tcb', simp_all)
   done
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 

diff --git a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy
@@ -49,7 +49,7 @@ lemma setCTE_tcbContext:
 
 context begin interpretation Arch . (*FIXME: arch_split*)
 
-lemma seThreadState_tcbContext:
+lemma setThreadState_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     setThreadState a b
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"
@@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext:
 declare comp_apply [simp del]
 crunch tcbContext[wp]: deleteCallerCap "obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t"
   (wp: setEndpoint_obj_at_tcb' setBoundNotification_tcbContext
-       setNotification_tcb crunch_wps seThreadState_tcbContext
+       setNotification_tcb crunch_wps setThreadState_tcbContext
    simp: crunch_simps unless_def)
 declare comp_apply [simp]
 
@@ -1561,7 +1561,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres:
                                           fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]
                                | wps)+)[3]
                     apply (simp cong: rev_conj_cong)
-                    apply (wpsimp wp: seThreadState_tcbContext[simplified comp_apply]
+                    apply (wpsimp wp: setThreadState_tcbContext[simplified comp_apply]
                                       setThreadState_oa_queued user_getreg_rv
                                       setThreadState_no_sch_change setThreadState_obj_at_unchanged
                                       sts_st_tcb_at'_cases sts_bound_tcb_at'