From a084de49939202c04a5e0f2045150bde02828bf0 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Mon, 14 Aug 2023 21:08:23 +1000 Subject: [PATCH] refine: update for changes to nondet monad Signed-off-by: Corey Lewis --- proof/refine/AARCH64/Schedule_R.thy | 2 +- proof/refine/ARM/Schedule_R.thy | 2 +- proof/refine/ARM_HYP/Schedule_R.thy | 2 +- proof/refine/RISCV64/Schedule_R.thy | 2 +- proof/refine/X64/Schedule_R.thy | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index 0ade5d66ca..ff63a9b42a 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -2314,7 +2314,7 @@ lemma schedule_invs': apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 - | wp hoare_disjI2[where Q="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] + | wp hoare_disjI2[where R="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] | strengthen invs'_invs_no_cicd diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 02921fc419..8622fbfcf9 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -2153,7 +2153,7 @@ lemma schedule_invs': apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 - | wp hoare_disjI2[where Q="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] + | wp hoare_disjI2[where R="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] | strengthen invs'_invs_no_cicd diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 9076942689..8be4b8e1e1 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -2279,7 +2279,7 @@ lemma schedule_invs': apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 - | wp hoare_disjI2[where Q="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] + | wp hoare_disjI2[where R="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] | strengthen invs'_invs_no_cicd diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 4bc496808b..800d5399b9 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -2141,7 +2141,7 @@ lemma schedule_invs': apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 - | wp hoare_disjI2[where Q="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] + | wp hoare_disjI2[where R="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] | strengthen invs'_invs_no_cicd diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index a248f01710..b1eb3a6820 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -2144,7 +2144,7 @@ lemma schedule_invs': apply (wpsimp wp: scheduleChooseNewThread_invs' ssa_invs' chooseThread_invs_no_cicd' setSchedulerAction_invs' setSchedulerAction_direct switchToThread_tcb_in_cur_domain' switchToThread_ct_not_queued_2 - | wp hoare_disjI2[where Q="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] + | wp hoare_disjI2[where R="\_ s. tcb_in_cur_domain' (ksCurThread s) s"] | wp hoare_drop_imp[where f="isHighestPrio d p" for d p] | simp only: obj_at'_activatable_st_tcb_at'[simplified comp_def] | strengthen invs'_invs_no_cicd