From 827ee5e86cb0d0f6293078bce0c78cf9bf429487 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 6 Dec 2023 12:25:58 +1100 Subject: [PATCH] arm+arm_hyp+aarch64 crefine: fix name of setThreadState_tcbContext Signed-off-by: Corey Lewis --- proof/crefine/AARCH64/Fastpath_C.thy | 4 ++-- proof/crefine/AARCH64/Fastpath_Equiv.thy | 6 +++--- 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 +++--- 6 files changed, 15 insertions(+), 15 deletions(-) diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index fb21546507..132cbee167 100644 --- 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: "\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/AARCH64/Fastpath_Equiv.thy b/proof/crefine/AARCH64/Fastpath_Equiv.thy index 0cb9028902..b005190e93 100644 --- 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: "\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] @@ -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 index 09be1b557b..cd2f746a82 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 e39857801f..e4fedded83 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] @@ -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 index 3660f4cc75..117979ae1a 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 2ade2f9356..7bfd4520e8 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] @@ -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'