From c9acf883eb3efc713117ff51f3998807255c470c Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 6 Dec 2023 12:25:58 +1100 Subject: [PATCH] arm+arm_hyp crefine: fix name of setThreadState_tcbContext Signed-off-by: Corey Lewis --- proof/crefine/ARM/Fastpath_C.thy | 4 ++-- proof/crefine/ARM/Fastpath_Equiv.thy | 6 +++--- proof/crefine/ARM_HYP/Fastpath_C.thy | 4 ++-- proof/crefine/ARM_HYP/Fastpath_Equiv.thy | 6 +++--- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index 09be1b557bd..cd2f746a82d 100644 --- 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: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\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 index fcb1e1e8e75..5dd9d418f9a 100644 --- 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: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\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] @@ -1554,7 +1554,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 index 3660f4cc754..117979ae1ae 100644 --- 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: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -73,7 +73,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\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 index 9a015a7f923..dfa300b437e 100644 --- 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: "\obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\ setThreadState a b \\_. obj_at' (\tcb. P ((atcbContextGet o tcbArch) tcb)) t\" @@ -68,7 +68,7 @@ lemma setBoundNotification_tcbContext: declare comp_apply [simp del] crunch tcbContext[wp]: deleteCallerCap "obj_at' (\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] @@ -1557,7 +1557,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'