From ce27e67d47e462d3cec3bb117bfe39b873f365e7 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Wed, 12 Jun 2024 09:51:48 +1000 Subject: [PATCH] proof: update for removed hoare_gets Signed-off-by: Corey Lewis --- proof/drefine/Syscall_DR.thy | 6 +++--- proof/infoflow/ARM/ArchArch_IF.thy | 7 ++++--- proof/infoflow/InfoFlow_IF.thy | 3 ++- proof/infoflow/RISCV64/ArchArch_IF.thy | 5 +++-- proof/refine/AARCH64/Retype_R.thy | 27 +++++++++++++------------- proof/refine/AARCH64/Schedule_R.thy | 2 +- proof/refine/ARM/Retype_R.thy | 25 +++++++++++------------- proof/refine/ARM/Schedule_R.thy | 2 +- proof/refine/ARM_HYP/Retype_R.thy | 13 +++++++------ proof/refine/ARM_HYP/Schedule_R.thy | 2 +- proof/refine/RISCV64/Retype_R.thy | 23 ++++++++++------------ proof/refine/RISCV64/Schedule_R.thy | 2 +- proof/refine/X64/Retype_R.thy | 9 +++------ proof/refine/X64/Schedule_R.thy | 2 +- 14 files changed, 62 insertions(+), 66 deletions(-) diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index 36d0ab599f..e8f9877fc9 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -1645,9 +1645,9 @@ lemma handle_event_corres: apply wp[1] apply clarsimp apply (frule (1) ct_running_not_idle_etc) - apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def gets_def get_def - valid_fault_def - split: Structures_A.thread_state.splits)+ + apply (fastforce simp: st_tcb_at_def obj_at_def generates_pending_def valid_fault_def + split: Structures_A.thread_state.splits) + apply wpsimp+ apply (rule corres_symb_exec_r[OF handle_fault_corres]) apply wp[1] apply clarsimp diff --git a/proof/infoflow/ARM/ArchArch_IF.thy b/proof/infoflow/ARM/ArchArch_IF.thy index f75758f73e..f0eb76ce4a 100644 --- a/proof/infoflow/ARM/ArchArch_IF.thy +++ b/proof/infoflow/ARM/ArchArch_IF.thy @@ -804,9 +804,10 @@ lemma arm_asid_table_update_reads_respects: apply (rule modify_ev2) apply clarsimp apply (drule (1) is_subject_kheap_eq[rotated]) - apply (auto simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def - intro!: equiv_asids_arm_asid_table_update) - done + apply (fastforce simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def + intro!: equiv_asids_arm_asid_table_update) + apply wpsimp + done lemma perform_asid_control_invocation_reads_respects: notes K_bind_ev[wp del] diff --git a/proof/infoflow/InfoFlow_IF.thy b/proof/infoflow/InfoFlow_IF.thy index 2de302236b..05a68a466b 100644 --- a/proof/infoflow/InfoFlow_IF.thy +++ b/proof/infoflow/InfoFlow_IF.thy @@ -957,8 +957,9 @@ lemma do_machine_op_rev: apply (clarsimp simp: select_f_def equiv_valid_2_def) apply (insert equiv_dmo, clarsimp simp: equiv_valid_def2 equiv_valid_2_def)[1] apply blast - apply (wp select_f_inv)+ + apply (wpsimp wp: select_f_inv)+ apply (fastforce simp: select_f_def dest: state_unchanged[OF mo_inv])+ + apply wpsimp done end diff --git a/proof/infoflow/RISCV64/ArchArch_IF.thy b/proof/infoflow/RISCV64/ArchArch_IF.thy index ea5d9ff546..7ac7890e19 100644 --- a/proof/infoflow/RISCV64/ArchArch_IF.thy +++ b/proof/infoflow/RISCV64/ArchArch_IF.thy @@ -425,8 +425,9 @@ lemma riscv_asid_table_update_reads_respects: apply (rule modify_ev2) apply clarsimp apply (drule (1) is_subject_kheap_eq[rotated]) - apply (auto simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def - intro!: equiv_asids_riscv_asid_table_update) + apply (fastforce simp: reads_equiv_def2 affects_equiv_def2 states_equiv_for_def equiv_for_def + intro!: equiv_asids_riscv_asid_table_update) + apply wpsimp done lemma perform_asid_control_invocation_reads_respects: diff --git a/proof/refine/AARCH64/Retype_R.thy b/proof/refine/AARCH64/Retype_R.thy index d581599880..9d642869eb 100644 --- a/proof/refine/AARCH64/Retype_R.thy +++ b/proof/refine/AARCH64/Retype_R.thy @@ -4296,20 +4296,21 @@ lemma createNewCaps_idle'[wp]: split del: if_split) apply (cases ty, simp_all add: Arch_createNewCaps_def split del: if_split) - apply (rename_tac apiobject_type) - apply (case_tac apiobject_type, simp_all split del: if_split)[1] - apply (wp, simp) + apply (rename_tac apiobject_type) + apply (case_tac apiobject_type, simp_all split del: if_split)[1] + apply wpsimp + (* The following step does not use wpsimp to avoid clarsimp_no_cond, which for some reason + leads to a failed proof state. If this could be fixed then the inclusion of + classic_wp_pre could also be removed. *) including classic_wp_pre - apply (wp mapM_x_wp' - createObjects_idle' - threadSet_idle' - | simp add: projectKO_opt_tcb projectKO_opt_cte mult_2 - makeObject_cte makeObject_tcb archObjSize_def - tcb_cte_cases_def objBitsKO_def APIType_capBits_def - objBits_def createObjects_def cteSizeBits_def - | simp add: field_simps - | intro conjI impI - | fastforce simp: curDomain_def)+ + apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' + | simp add: projectKO_opt_tcb projectKO_opt_cte mult_2 + makeObject_cte makeObject_tcb archObjSize_def + tcb_cte_cases_def objBitsKO_def APIType_capBits_def + objBits_def createObjects_def cteSizeBits_def + | simp add: field_simps + | intro conjI impI + | clarsimp simp: curDomain_def)+ done crunch createNewCaps diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index 861220f007..0f31f50b4b 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -2124,7 +2124,7 @@ lemma schedule_corres: tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp del: gets_wp | strengthen valid_objs'_valid_tcbs')+ - apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) + apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong) apply (wp gets_wp)+ (* abstract final subgoal *) diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy index 88dcf8f9d6..cd24cc2b06 100644 --- a/proof/refine/ARM/Retype_R.thy +++ b/proof/refine/ARM/Retype_R.thy @@ -4277,20 +4277,17 @@ lemma createNewCaps_idle'[wp]: split del: if_split) apply (cases ty, simp_all add: Arch_createNewCaps_def split del: if_split) - apply (rename_tac apiobject_type) - apply (case_tac apiobject_type, simp_all split del: if_split)[1] - apply (wp, simp) - including classic_wp_pre - apply (wp mapM_x_wp' - createObjects_idle' - threadSet_idle' - | simp add: projectKO_opt_tcb projectKO_opt_cte - makeObject_cte makeObject_tcb archObjSize_def - tcb_cte_cases_def objBitsKO_def APIType_capBits_def - ptBits_def pdBits_def pageBits_def objBits_def - createObjects_def pteBits_def pdeBits_def - | intro conjI impI - | fastforce simp: curDomain_def)+ + apply (rename_tac apiobject_type) + apply (case_tac apiobject_type, simp_all split del: if_split)[1] + apply wpsimp + apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle' + | simp add: projectKO_opt_tcb projectKO_opt_cte + makeObject_cte makeObject_tcb archObjSize_def + tcb_cte_cases_def objBitsKO_def APIType_capBits_def + ptBits_def pdBits_def pageBits_def objBits_def + createObjects_def pteBits_def pdeBits_def + | intro conjI impI + | clarsimp simp: curDomain_def)+ done crunch createNewCaps diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index cecfe69535..ef40db58db 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -1910,7 +1910,7 @@ lemma schedule_corres: tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp del: gets_wp | strengthen valid_objs'_valid_tcbs')+ - apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) + apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong) apply (wp gets_wp)+ (* abstract final subgoal *) diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index 959dc75883..82698e8920 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -4351,18 +4351,19 @@ lemma createNewCaps_idle'[wp]: split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] - apply (wp, simp) - including classic_wp_pre - apply (wp mapM_x_wp' - createObjects_idle' - threadSet_idle' + apply wpsimp + (* The following step does not use wpsimp to avoid clarsimp_no_cond, which for some reason + leads to a failed proof state. If this could be fixed then the inclusion of + classic_wp_pre could also be removed. *) + including classic_wp_pre + apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' | simp add: projectKO_opt_tcb projectKO_opt_cte makeObject_cte makeObject_tcb archObjSize_def tcb_cte_cases_def objBitsKO_def APIType_capBits_def vspace_bits_defs objBits_def createObjects_def | intro conjI impI - | fastforce simp: curDomain_def)+ + | clarsimp simp: curDomain_def)+ done crunch createNewCaps diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index defefbbea1..ee340f2f7e 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -2109,7 +2109,7 @@ lemma schedule_corres: tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp del: gets_wp | strengthen valid_objs'_valid_tcbs' invs_valid_pspace')+ - apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) + apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong) apply (wp gets_wp)+ (* abstract final subgoal *) diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy index e8aeee022e..1efd013312 100644 --- a/proof/refine/RISCV64/Retype_R.thy +++ b/proof/refine/RISCV64/Retype_R.thy @@ -4223,19 +4223,16 @@ lemma createNewCaps_idle'[wp]: split del: if_split) apply (cases ty, simp_all add: Arch_createNewCaps_def split del: if_split) - apply (rename_tac apiobject_type) - apply (case_tac apiobject_type, simp_all split del: if_split)[1] - apply (wp, simp) - including classic_wp_pre - apply (wp mapM_x_wp' - createObjects_idle' - threadSet_idle' - | simp add: projectKO_opt_tcb projectKO_opt_cte - makeObject_cte makeObject_tcb archObjSize_def - tcb_cte_cases_def objBitsKO_def APIType_capBits_def - objBits_def createObjects_def bit_simps cteSizeBits_def - | intro conjI impI - | fastforce simp: curDomain_def)+ + apply (rename_tac apiobject_type) + apply (case_tac apiobject_type, simp_all split del: if_split)[1] + apply wpsimp + apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle' + | simp add: projectKO_opt_tcb projectKO_opt_cte + makeObject_cte makeObject_tcb archObjSize_def + tcb_cte_cases_def objBitsKO_def APIType_capBits_def + objBits_def createObjects_def bit_simps cteSizeBits_def + | intro conjI impI + | clarsimp simp: curDomain_def)+ done crunch createNewCaps diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index b2d12a3948..822ea514a9 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -1967,7 +1967,7 @@ lemma schedule_corres: tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp del: gets_wp | strengthen valid_objs'_valid_tcbs')+ - apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) + apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong) apply (wp gets_wp)+ (* abstract final subgoal *) diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index 0eeff644d2..b20f6dbf23 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -4396,17 +4396,14 @@ lemma createNewCaps_idle'[wp]: split del: if_split) apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] - apply (wp, simp) - including classic_wp_pre - apply (wp mapM_x_wp' - createObjects_idle' - threadSet_idle' + apply wpsimp + apply (wpsimp wp: mapM_x_wp' createObjects_idle' threadSet_idle' | simp add: projectKO_opt_tcb projectKO_opt_cte makeObject_cte makeObject_tcb archObjSize_def tcb_cte_cases_def objBitsKO_def APIType_capBits_def objBits_def createObjects_def bit_simps | intro conjI impI - | fastforce simp: curDomain_def)+ + | clarsimp simp: curDomain_def)+ done crunch createNewCaps diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index c0f16b3bdc..fb37c1c16b 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -1911,7 +1911,7 @@ lemma schedule_corres: tcbSchedEnqueue_invs'_not_ResumeCurrentThread thread_get_wp del: gets_wp | strengthen valid_objs'_valid_tcbs')+ - apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong del: hoare_gets) + apply (clarsimp simp: conj_ac if_apply_def2 cong: imp_cong conj_cong) apply (wp gets_wp)+ (* abstract final subgoal *)