From 954b42cdd974d8399458cf91dbe2ff531274e037 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 4 Apr 2022 18:45:06 +1000 Subject: [PATCH] refine: speed up CSpace1_R+CSpace_R proofs Three main thrusts: - speed up the `updateMDB_the_lot` chain by using more targeted proof methods - drastically reduce goal size by removing unused assumptions when that becomes possible (this is the largest overall speed win) - use `subgoal` to unblock interactive proof progress Signed-off-by: Gerwin Klein --- proof/refine/ARM/CSpace1_R.thy | 79 +++++-- proof/refine/ARM/CSpace_R.thy | 116 ++++++---- proof/refine/ARM_HYP/CSpace1_R.thy | 148 ++++++++----- proof/refine/ARM_HYP/CSpace_R.thy | 142 +++++++----- proof/refine/RISCV64/CSpace1_R.thy | 77 +++++-- proof/refine/RISCV64/CSpace_R.thy | 104 ++++++--- proof/refine/X64/CSpace1_R.thy | 338 +++++++++++++++-------------- proof/refine/X64/CSpace_I.thy | 3 +- proof/refine/X64/CSpace_R.thy | 151 +++++++------ proof/refine/X64/KHeap_R.thy | 38 ++-- 10 files changed, 721 insertions(+), 475 deletions(-) diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index 3eae7bfd6..38928b195 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -6565,13 +6565,22 @@ lemma cteSwap_corres: | rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+ apply (simp cong: option.case_cong) apply (drule updateCap_stuff, elim conjE, erule(1) impE) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule in_getCTE, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) + apply (drule (2) updateMDB_the_lot') + apply (erule (1) impE, assumption) + apply (fastforce simp only: no_0_modify_map) + apply assumption + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule in_getCTE, elim conjE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (simp only: pspace_relations_def refl) + apply (rule conjI, rule TrueI)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ @@ -6582,7 +6591,8 @@ lemma cteSwap_corres: apply (thin_tac "ksDomSchedule t = p" for t p)+ apply (thin_tac "ksCurDomain t = p" for t p)+ apply (thin_tac "ksDomainTime t = p" for t p)+ - apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong) + apply (simp only: simp_thms no_0_modify_map) + apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong) apply (thin_tac "ctes_of x = y" for x y)+ apply (case_tac cte1) apply (rename_tac src_cap src_node) @@ -6603,24 +6613,49 @@ lemma cteSwap_corres: apply (erule weak_derived_sym') apply (erule weak_derived_sym') apply assumption - apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def) + subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv ARM.data_at_def) + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_list t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "ekheap t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "pspace_relation s s'" for s s')+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ + apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ apply(subst conj_assoc[symmetric]) apply (rule conjI) prefer 2 apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at simp del: split_paired_All) apply (drule set_cap_caps_of_state_monad)+ - apply (thin_tac "pspace_relation s t" for s t)+ apply (simp del: split_paired_All split: if_split) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule(1) mdb_swap.revokable) apply (erule_tac x="dest" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (clarsimp simp del: split_paired_All) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) @@ -6629,19 +6664,19 @@ lemma cteSwap_corres: apply (simp del: split_paired_All) apply (erule_tac x="src" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (drule caps_of_state_cte_at)+ apply (erule (5) cte_map_inj) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule (1) mdb_swap.revokable) apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 - apply (clarsimp simp: null_filter_def split: if_splits) + subgoal by (clarsimp simp: null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_map (aa,bb) \ cte_map src") apply (subgoal_tac "cte_map (aa,bb) \ cte_map dest") - apply (clarsimp simp del: split_paired_All) + subgoal by (clarsimp simp del: split_paired_All) apply (drule caps_of_state_cte_at)+ apply (drule null_filter_caps_of_stateD)+ apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) @@ -6650,7 +6685,7 @@ lemma cteSwap_corres: apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) apply (subgoal_tac "no_loops (ctes_of b)") prefer 2 - apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) + subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a") prefer 2 apply (erule mdb_swap_abs.intro) @@ -6660,7 +6695,7 @@ lemma cteSwap_corres: apply assumption apply (frule mdb_swap_abs''.intro) apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro) - apply (simp add: mdb_swap_abs'_axioms_def) + subgoal by (simp add: mdb_swap_abs'_axioms_def) apply (thin_tac "modify_map m f p p' = t" for m f p p' t) apply(rule conjI) apply (simp add: cdt_relation_def del: split_paired_All) @@ -6712,7 +6747,7 @@ lemma cteSwap_corres: apply (erule (3) inj_on_descendants_cte_map) apply (rule subset_refl) apply clarsimp - apply auto[1] + subgoal by auto apply clarsimp apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) @@ -6891,9 +6926,7 @@ lemma cteSwap_corres: apply(rule cte_at_next_slot') apply(simp_all)[9] apply(erule cte_wp_at_weakenE, simp) - apply(rule cte_at_next_slot) - apply(simp_all) - done + by (rule cte_at_next_slot; simp) lemma capSwapForDelete_corres: diff --git a/proof/refine/ARM/CSpace_R.thy b/proof/refine/ARM/CSpace_R.thy index 955f8601e..ea131e9ba 100644 --- a/proof/refine/ARM/CSpace_R.thy +++ b/proof/refine/ARM/CSpace_R.thy @@ -101,7 +101,7 @@ lemma src_no_parent [iff]: lemma no_0_n: "no_0 n" by (simp add: n_def no_0) lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n) -lemma next_neq_dest [simp]: +lemma next_neq_dest [iff]: "mdbNext src_node \ dest" using dlist src dest prev dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def) @@ -201,26 +201,10 @@ proof - thus ?thesis by (simp add: m'_def) qed -lemma [iff]: +lemma dest_not_parent [iff]: "m \ dest parentOf c = False" using dest by (simp add: parentOf_def) -lemma [iff]: - "mdbNext src_node \ dest" -proof - assume "mdbNext src_node = dest" - moreover have "dest \ 0" .. - ultimately - have "mdbPrev old_dest_node = src" - using src dest dlist - by (fastforce elim: valid_dlistEn) - with prev - show False by (simp add: src_0) -qed - -lemmas no_loops_simps [simp] = - no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops] - lemma dest_source [iff]: "(m \ dest \ x) = (x = 0)" using dest nxt by (simp add: next_unfold') @@ -883,10 +867,12 @@ lemma cteMove_corres: apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule updateCap_stuff, elim conjE, erule (1) impE) - apply (drule updateCap_stuff, clarsimp) + apply (drule updateCap_stuff) apply (subgoal_tac "pspace_distinct' b \ pspace_aligned' b") prefer 2 - subgoal by fastforce + apply (elim valid_pspaceE' conjE) + apply (rule conjI; assumption) + apply (simp only: ) apply (thin_tac "ctes_of t = s" for t s)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ @@ -895,7 +881,7 @@ lemma cteMove_corres: apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "\p. cte_at p ta = cte_at p a") prefer 2 - apply (simp add: set_cap_cte_eq) + subgoal by (simp add: set_cap_cte_eq) apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All) apply (subgoal_tac "cte_at ptr' a") prefer 2 @@ -909,6 +895,36 @@ lemma cteMove_corres: apply (clarsimp simp: pspace_relations_def) apply (rule conjI) apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "ghost_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (subst conj_assoc[symmetric]) apply (rule conjI) defer @@ -986,7 +1002,7 @@ lemma cteMove_corres: apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) = cte_map ` descendants_of (aa, bb) (cdt a)") prefer 2 - apply (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def del: split_paired_All) apply simp apply (rule conjI) apply clarsimp @@ -997,8 +1013,8 @@ lemma cteMove_corres: apply fastforce apply fastforce apply (rule subset_refl) - apply simp - apply simp + subgoal by simp + subgoal by simp apply clarsimp apply (drule (1) cte_map_inj_eq) apply (erule descendants_of_cte_at) @@ -1017,7 +1033,7 @@ lemma cteMove_corres: apply(intro allI impI) apply(rule mdb_move_abs'.next_slot) apply(simp, fastforce, simp) - apply(fastforce split: option.splits) + subgoal by(fastforce split: option.splits) apply(case_tac "ctes_of b (cte_map (aa, bb))") subgoal by (clarsimp simp: modify_map_def split: if_split_asm) apply(case_tac ab) @@ -4755,12 +4771,41 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (clarsimp simp: pspace_relations_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 @@ -4770,11 +4815,6 @@ lemma cteInsert_simple_corres: prefer 2 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) - apply (thin_tac "ksMachineState t = p" for t p)+ - apply (thin_tac "ksCurThread t = p" for t p)+ - apply (thin_tac "ksIdleThread t = p" for t p)+ - apply (thin_tac "ksReadyQueues t = p" for t p)+ - apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True") prefer 2 apply (subst should_be_parent_of_masked_as_full[symmetric]) @@ -4783,7 +4823,6 @@ lemma cteInsert_simple_corres: apply (subst conj_assoc[symmetric]) apply (rule conjI) defer - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (simp split: if_split) @@ -4798,7 +4837,7 @@ lemma cteInsert_simple_corres: apply (subst same_region_as_relation [symmetric]) prefer 3 apply (rule safe_parent_same_region) - apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full) + apply (simp add: cte_wp_at_caps_of_state) apply assumption apply assumption apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) @@ -4835,9 +4874,6 @@ lemma cteInsert_simple_corres: apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for t s)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -4845,7 +4881,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") prefer 2 - subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full) + subgoal by (fastforce simp: cte_wp_at_def) apply (erule conjE) apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index a9b8edbec..c26c7e54b 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -2460,15 +2460,15 @@ lemma updateCap_corres: apply (unfold cdt_list_relation_def)[1] apply (intro allI impI) apply (erule_tac x=c in allE) - apply (auto elim!: modify_map_casesE)[1] + subgoal by (auto elim!: modify_map_casesE)[1] apply (unfold revokable_relation_def)[1] apply (drule set_cap_caps_of_state_monad) apply (simp add: cte_wp_at_caps_of_state del: split_paired_All) apply (intro allI impI) apply (erule_tac x=c in allE) apply (erule impE[where P="\y. v = Some y" for v]) - apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm) - apply (auto elim!: modify_map_casesE del: disjE)[1] + subgoal by (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm) + subgoal by (auto elim!: modify_map_casesE del: disjE)[1] apply (case_tac "ctes_of b (cte_map slot)") apply (simp add: modify_map_None) apply (simp add: modify_map_apply) @@ -2477,7 +2477,7 @@ lemma updateCap_corres: apply (rule use_update_ztc_one [OF descendants_of_update_ztc]) apply simp apply assumption - apply (auto simp: is_cap_simps isCap_simps)[1] + subgoal by (auto simp: is_cap_simps isCap_simps)[1] apply (frule(3) is_final_untyped_ptrs [OF _ _ not_sym], clarsimp+) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (simp add: is_cap_simps, elim disjE exE, simp_all)[1] @@ -2862,9 +2862,8 @@ lemma capBadge_ordering_relation: "\ cap_relation c c'; cap_relation d d' \ \ ((capBadge c', capBadge d') \ capBadge_ordering f) = ((cap_badge c, cap_badge d) \ capBadge_ordering f)" - apply (cases c) - apply (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits) - done + by (cases c) + (auto simp add: cap_badge_def capBadge_ordering_def split: cap.splits) lemma is_reply_cap_relation: "cap_relation c c' \ is_reply_cap c = (isReplyCap c' \ \ capReplyMaster c')" @@ -5238,34 +5237,52 @@ lemma cteInsert_corres: apply (clarsimp simp: put_def state_relation_def) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 - apply (clarsimp simp: valid_mdb'_def - valid_mdb_ctes_def no_0_def) + subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (subgoal_tac "cte_map src \ 0") prefer 2 - apply (clarsimp simp: valid_mdb'_def - valid_mdb_ctes_def no_0_def) + subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (thin_tac "ksMachineState t = p" for p t)+ apply (thin_tac "ksCurThread t = p" for p t)+ apply (thin_tac "ksIdleThread t = p" for p t)+ apply (thin_tac "ksReadyQueues t = p" for p t)+ apply (thin_tac "ksSchedulerAction t = p" for p t)+ apply (clarsimp simp: pspace_relations_def) - apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (rule conjI) defer apply(rule conjI) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -5550,7 +5567,6 @@ lemma cteInsert_corres: apply(simp_all)[2] apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def split: if_split) apply (rule conjI) @@ -5605,9 +5621,6 @@ lemma cteInsert_corres: apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -5641,7 +5654,7 @@ lemma cteInsert_corres: apply (subgoal_tac "descendants_of dest (cdt a) = {}") prefer 2 apply (drule mdb_insert.dest_no_descendants) - subgoal by (fastforce simp add: cdt_relation_def simp del: split_paired_All) + subgoal by (fastforce simp add: cdt_relation_def) apply (subgoal_tac "mdb_insert_abs (cdt a) src dest") prefer 2 apply (erule mdb_insert_abs.intro) @@ -5676,7 +5689,7 @@ lemma cteInsert_corres: dest!:cap_master_cap_eqDs) apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node") prefer 2 - apply (simp add: revokable_relation_def del: split_paired_All) + apply (simp add: revokable_relation_def) apply (erule_tac x=src in allE) apply (erule impE) apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state cap_master_cap_simps @@ -5690,7 +5703,7 @@ lemma cteInsert_corres: prefer 2 apply assumption apply (simp_all)[6] - apply (simp add: cdt_relation_def split: if_split del: split_paired_All) + apply (simp add: cdt_relation_def split: if_split) apply clarsimp apply (drule (5) cte_map_inj)+ apply simp @@ -5718,7 +5731,7 @@ lemma cteInsert_corres: dest!:cap_master_cap_eqDs) apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node") subgoal by simp - apply (simp add: revokable_relation_def del: split_paired_All) + apply (simp add: revokable_relation_def) apply (erule_tac x=src in allE) apply (erule impE) apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits) @@ -5728,9 +5741,9 @@ lemma cteInsert_corres: apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at) apply (rule conjI) apply (clarsimp simp: descendants_of_eq') - subgoal by (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def) apply (clarsimp simp: descendants_of_eq') - subgoal by (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def) done @@ -6734,13 +6747,22 @@ lemma cteSwap_corres: | rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+ apply (simp cong: option.case_cong) apply (drule updateCap_stuff, elim conjE, erule(1) impE) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule in_getCTE, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) + apply (drule (2) updateMDB_the_lot') + apply (erule (1) impE, assumption) + apply (fastforce simp only: no_0_modify_map) + apply assumption + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule in_getCTE, elim conjE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (simp only: pspace_relations_def refl) + apply (rule conjI, rule TrueI)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ @@ -6751,7 +6773,8 @@ lemma cteSwap_corres: apply (thin_tac "ksDomSchedule t = p" for t p)+ apply (thin_tac "ksCurDomain t = p" for t p)+ apply (thin_tac "ksDomainTime t = p" for t p)+ - apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong) + apply (simp only: simp_thms no_0_modify_map) + apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong) apply (thin_tac "ctes_of x = y" for x y)+ apply (case_tac cte1) apply (rename_tac src_cap src_node) @@ -6772,23 +6795,48 @@ lemma cteSwap_corres: apply (erule weak_derived_sym') apply (erule weak_derived_sym') apply assumption - apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv ARM_HYP.data_at_def) + subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv ARM_HYP.data_at_def) + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_list t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "ekheap t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "pspace_relation s s'" for s s')+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ + apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ apply(subst conj_assoc[symmetric]) apply (rule conjI) prefer 2 apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at simp del: split_paired_All) apply (drule set_cap_caps_of_state_monad)+ - apply (thin_tac "pspace_relation s t" for s t)+ apply (simp del: split_paired_All split: if_split) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule(1) mdb_swap.revokable) apply (erule_tac x="dest" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) apply simp apply (clarsimp simp del: split_paired_All) apply (rule conjI) @@ -6798,19 +6846,19 @@ lemma cteSwap_corres: apply (simp del: split_paired_All) apply (erule_tac x="src" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (drule caps_of_state_cte_at)+ apply (erule (5) cte_map_inj) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule (1) mdb_swap.revokable) apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 - apply (clarsimp simp: null_filter_def split: if_splits) + subgoal by (clarsimp simp: null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_map (aa,bb) \ cte_map src") apply (subgoal_tac "cte_map (aa,bb) \ cte_map dest") - apply (clarsimp simp del: split_paired_All) + subgoal by (clarsimp simp del: split_paired_All) apply (drule caps_of_state_cte_at)+ apply (drule null_filter_caps_of_stateD)+ apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) @@ -6819,7 +6867,7 @@ lemma cteSwap_corres: apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) apply (subgoal_tac "no_loops (ctes_of b)") prefer 2 - apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) + subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a") prefer 2 apply (erule mdb_swap_abs.intro) @@ -6829,7 +6877,7 @@ lemma cteSwap_corres: apply assumption apply (frule mdb_swap_abs''.intro) apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro) - apply (simp add: mdb_swap_abs'_axioms_def) + subgoal by (simp add: mdb_swap_abs'_axioms_def) apply (thin_tac "modify_map m f p p' = t" for m f p p' t) apply(rule conjI) apply (simp add: cdt_relation_def del: split_paired_All) @@ -6881,7 +6929,7 @@ lemma cteSwap_corres: apply (erule (3) inj_on_descendants_cte_map) apply (rule subset_refl) apply clarsimp - apply auto[1] + subgoal by auto apply clarsimp apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) @@ -7060,9 +7108,7 @@ lemma cteSwap_corres: apply(rule cte_at_next_slot') apply(simp_all)[9] apply(erule cte_wp_at_weakenE, simp) - apply(rule cte_at_next_slot) - apply(simp_all) - done + by (rule cte_at_next_slot; simp) lemma capSwapForDelete_corres: diff --git a/proof/refine/ARM_HYP/CSpace_R.thy b/proof/refine/ARM_HYP/CSpace_R.thy index 011389a33..33a3bccb9 100644 --- a/proof/refine/ARM_HYP/CSpace_R.thy +++ b/proof/refine/ARM_HYP/CSpace_R.thy @@ -101,7 +101,7 @@ lemma src_no_parent [iff]: lemma no_0_n: "no_0 n" by (simp add: n_def no_0) lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n) -lemma next_neq_dest [simp]: +lemma next_neq_dest [iff]: "mdbNext src_node \ dest" using dlist src dest prev dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def) @@ -201,26 +201,10 @@ proof - thus ?thesis by (simp add: m'_def) qed -lemma [iff]: +lemma dest_not_parent [iff]: "m \ dest parentOf c = False" using dest by (simp add: parentOf_def) -lemma [iff]: - "mdbNext src_node \ dest" -proof - assume "mdbNext src_node = dest" - moreover have "dest \ 0" .. - ultimately - have "mdbPrev old_dest_node = src" - using src dest dlist - by (fastforce elim: valid_dlistEn) - with prev - show False by (simp add: src_0) -qed - -lemmas no_loops_simps [simp] = - no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops] - lemma dest_source [iff]: "(m \ dest \ x) = (x = 0)" using dest nxt by (simp add: next_unfold') @@ -883,10 +867,12 @@ lemma cteMove_corres: apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule updateCap_stuff, elim conjE, erule (1) impE) - apply (drule updateCap_stuff, clarsimp) + apply (drule updateCap_stuff) apply (subgoal_tac "pspace_distinct' b \ pspace_aligned' b") prefer 2 - subgoal by fastforce + apply (elim valid_pspaceE' conjE) + apply (rule conjI; assumption) + apply (simp only: ) apply (thin_tac "ctes_of t = s" for t s)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ @@ -895,7 +881,7 @@ lemma cteMove_corres: apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "\p. cte_at p ta = cte_at p a") prefer 2 - apply (simp add: set_cap_cte_eq) + subgoal by (simp add: set_cap_cte_eq) apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All) apply (subgoal_tac "cte_at ptr' a") prefer 2 @@ -908,7 +894,37 @@ lemma cteMove_corres: apply fastforce apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "ghost_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (subst conj_assoc[symmetric]) apply (rule conjI) defer @@ -946,7 +962,7 @@ lemma cteMove_corres: apply fastforce apply fastforce apply fastforce - apply clarsimp + subgoal by clarsimp subgoal by (simp add: null_filter_def split: if_splits) apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node") prefer 2 @@ -970,8 +986,8 @@ lemma cteMove_corres: apply (rule mdb_move_abs.intro) apply fastforce apply (fastforce elim!: cte_wp_at_weakenE) - apply simp - apply simp + subgoal by simp + subgoal by simp apply (case_tac "(aa,bb) = ptr", simp) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr") prefer 2 @@ -986,7 +1002,7 @@ lemma cteMove_corres: apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) = cte_map ` descendants_of (aa, bb) (cdt a)") prefer 2 - apply (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def del: split_paired_All) apply simp apply (rule conjI) apply clarsimp @@ -997,8 +1013,8 @@ lemma cteMove_corres: apply fastforce apply fastforce apply (rule subset_refl) - apply simp - apply simp + subgoal by simp + subgoal by simp apply clarsimp apply (drule (1) cte_map_inj_eq) apply (erule descendants_of_cte_at) @@ -1017,7 +1033,7 @@ lemma cteMove_corres: apply(intro allI impI) apply(rule mdb_move_abs'.next_slot) apply(simp, fastforce, simp) - apply(fastforce split: option.splits) + subgoal by(fastforce split: option.splits) apply(case_tac "ctes_of b (cte_map (aa, bb))") subgoal by (clarsimp simp: modify_map_def split: if_split_asm) apply(case_tac ab) @@ -4812,12 +4828,41 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (clarsimp simp: pspace_relations_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 @@ -4827,11 +4872,6 @@ lemma cteInsert_simple_corres: prefer 2 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) - apply (thin_tac "ksMachineState t = p" for t p)+ - apply (thin_tac "ksCurThread t = p" for t p)+ - apply (thin_tac "ksIdleThread t = p" for t p)+ - apply (thin_tac "ksReadyQueues t = p" for t p)+ - apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (revokable src_cap c) = True") prefer 2 apply (subst should_be_parent_of_masked_as_full[symmetric]) @@ -4840,7 +4880,6 @@ lemma cteInsert_simple_corres: apply (subst conj_assoc[symmetric]) apply (rule conjI) defer - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (simp split: if_split) @@ -4855,7 +4894,7 @@ lemma cteInsert_simple_corres: apply (subst same_region_as_relation [symmetric]) prefer 3 apply (rule safe_parent_same_region) - apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full) + apply (simp add: cte_wp_at_caps_of_state) apply assumption apply assumption apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) @@ -4892,9 +4931,6 @@ lemma cteInsert_simple_corres: apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for t s)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -4902,7 +4938,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") prefer 2 - subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full) + subgoal by (fastforce simp: cte_wp_at_def) apply (erule conjE) apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node @@ -4971,8 +5007,7 @@ lemma cteInsert_simple_corres: apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) apply(clarsimp) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) apply(erule_tac x="fst src" in allE) apply(erule_tac x="snd src" in allE) apply(fastforce) @@ -4982,12 +5017,10 @@ lemma cteInsert_simple_corres: apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[5] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -4997,12 +5030,9 @@ lemma cteInsert_simple_corres: apply(erule_tac x=aa in allE) apply(erule_tac x=bb in allE) apply(fastforce) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) by(fastforce) declare if_split [split] diff --git a/proof/refine/RISCV64/CSpace1_R.thy b/proof/refine/RISCV64/CSpace1_R.thy index d8141312c..232594b59 100644 --- a/proof/refine/RISCV64/CSpace1_R.thy +++ b/proof/refine/RISCV64/CSpace1_R.thy @@ -6694,13 +6694,22 @@ lemma cteSwap_corres: | rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+ apply (simp cong: option.case_cong) apply (drule updateCap_stuff, elim conjE, erule(1) impE) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule in_getCTE, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) + apply (drule (2) updateMDB_the_lot') + apply (erule (1) impE, assumption) + apply (fastforce simp only: no_0_modify_map) + apply assumption + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule in_getCTE, elim conjE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (simp only: pspace_relations_def refl) + apply (rule conjI, rule TrueI)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ @@ -6711,7 +6720,8 @@ lemma cteSwap_corres: apply (thin_tac "ksDomSchedule t = p" for t p)+ apply (thin_tac "ksCurDomain t = p" for t p)+ apply (thin_tac "ksDomainTime t = p" for t p)+ - apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong) + apply (simp only: simp_thms no_0_modify_map) + apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong) apply (thin_tac "ctes_of x = y" for x y)+ apply (case_tac cte1) apply (rename_tac src_cap src_node) @@ -6732,23 +6742,48 @@ lemma cteSwap_corres: apply (erule weak_derived_sym') apply (erule weak_derived_sym') apply assumption - apply (clarsimp simp: pspace_relations_def) + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_list t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "ekheap t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "pspace_relation s s'" for s s')+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ + apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv RISCV64.data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv RISCV64.data_at_def) apply(subst conj_assoc[symmetric]) apply (rule conjI) prefer 2 apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at simp del: split_paired_All) apply (drule set_cap_caps_of_state_monad)+ - apply (thin_tac "pspace_relation s t" for s t)+ apply (simp del: split_paired_All split: if_split) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule(1) mdb_swap.revokable) apply (erule_tac x="dest" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) apply simp apply (clarsimp simp del: split_paired_All) apply (rule conjI) @@ -6758,19 +6793,19 @@ lemma cteSwap_corres: apply (simp del: split_paired_All) apply (erule_tac x="src" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (drule caps_of_state_cte_at)+ apply (erule (5) cte_map_inj) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule (1) mdb_swap.revokable) apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 - apply (clarsimp simp: null_filter_def split: if_splits) + subgoal by (clarsimp simp: null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_map (aa,bb) \ cte_map src") apply (subgoal_tac "cte_map (aa,bb) \ cte_map dest") - apply (clarsimp simp del: split_paired_All) + subgoal by (clarsimp simp del: split_paired_All) apply (drule caps_of_state_cte_at)+ apply (drule null_filter_caps_of_stateD)+ apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) @@ -6779,7 +6814,7 @@ lemma cteSwap_corres: apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) apply (subgoal_tac "no_loops (ctes_of b)") prefer 2 - apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) + subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a") prefer 2 apply (erule mdb_swap_abs.intro) @@ -6789,7 +6824,7 @@ lemma cteSwap_corres: apply assumption apply (frule mdb_swap_abs''.intro) apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro) - apply (simp add: mdb_swap_abs'_axioms_def) + subgoal by (simp add: mdb_swap_abs'_axioms_def) apply (thin_tac "modify_map m f p p' = t" for m f p p' t) apply(rule conjI) apply (simp add: cdt_relation_def del: split_paired_All) @@ -6841,7 +6876,7 @@ lemma cteSwap_corres: apply (erule (3) inj_on_descendants_cte_map) apply (rule subset_refl) apply clarsimp - apply auto[1] + subgoal by auto apply clarsimp apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) @@ -7020,9 +7055,7 @@ lemma cteSwap_corres: apply(rule cte_at_next_slot') apply(simp_all)[9] apply(erule cte_wp_at_weakenE, simp) - apply(rule cte_at_next_slot) - apply(simp_all) - done + by (rule cte_at_next_slot; simp) lemma capSwapForDelete_corres: diff --git a/proof/refine/RISCV64/CSpace_R.thy b/proof/refine/RISCV64/CSpace_R.thy index b96cb0b42..5ccdc5084 100644 --- a/proof/refine/RISCV64/CSpace_R.thy +++ b/proof/refine/RISCV64/CSpace_R.thy @@ -893,7 +893,31 @@ lemma cteMove_corres: apply fastforce apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "ghost_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (subst conj_assoc[symmetric]) apply (rule conjI) defer @@ -945,7 +969,7 @@ lemma cteMove_corres: apply (simp add: nullPointer_def) apply (simp add: nullPointer_def) apply (erule weak_derived_sym') - apply clarsimp + subgoal by clarsimp apply assumption apply (rule conjI) apply (simp (no_asm) add: cdt_relation_def) @@ -955,14 +979,14 @@ lemma cteMove_corres: apply (rule mdb_move_abs.intro) apply fastforce apply (fastforce elim!: cte_wp_at_weakenE) - apply simp - apply simp + subgoal by simp + subgoal by simp apply (case_tac "(aa,bb) = ptr", simp) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) apply (case_tac "(aa,bb) = ptr'") - apply (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def del: split_paired_All) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr'") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) @@ -982,7 +1006,7 @@ lemma cteMove_corres: apply fastforce apply fastforce apply (rule subset_refl) - apply simp + subgoal by simp apply simp apply clarsimp apply (drule (1) cte_map_inj_eq) @@ -991,9 +1015,8 @@ lemma cteMove_corres: apply fastforce apply fastforce apply fastforce - subgoal by clarsimp + subgoal by simp apply(clarsimp simp: cdt_list_relation_def) - apply(subst next_slot_eq2) apply(simp split: option.splits) apply(intro conjI impI) @@ -1002,7 +1025,7 @@ lemma cteMove_corres: apply(intro allI impI) apply(rule mdb_move_abs'.next_slot) apply(simp, fastforce, simp) - apply(fastforce split: option.splits) + subgoal by (fastforce split: option.splits) apply(case_tac "ctes_of b (cte_map (aa, bb))") subgoal by (clarsimp simp: modify_map_def split: if_split_asm) apply(case_tac ab) @@ -4764,12 +4787,41 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 @@ -4779,11 +4831,6 @@ lemma cteInsert_simple_corres: prefer 2 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) - apply (thin_tac "ksMachineState t = p" for t p)+ - apply (thin_tac "ksCurThread t = p" for t p)+ - apply (thin_tac "ksIdleThread t = p" for t p)+ - apply (thin_tac "ksReadyQueues t = p" for t p)+ - apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (is_cap_revocable c src_cap) = True") prefer 2 apply (subst should_be_parent_of_masked_as_full[symmetric]) @@ -4792,7 +4839,6 @@ lemma cteInsert_simple_corres: apply (subst conj_assoc[symmetric]) apply (rule conjI) defer - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (simp split: if_split) @@ -4844,9 +4890,6 @@ lemma cteInsert_simple_corres: apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for t s)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -4884,7 +4927,7 @@ lemma cteInsert_simple_corres: apply (frule set_cap_caps_of_state_monad) apply (subgoal_tac "cte_at (aa,bb) a") prefer 2 - apply (clarsimp simp: cte_wp_at_caps_of_state split: if_split_asm) + subgoal by (clarsimp simp: cte_wp_at_caps_of_state split: if_split_asm) apply (simp add: descendants_of_eq' cdt_relation_def split: if_split del: split_paired_All) apply clarsimp apply (drule (5) cte_map_inj)+ @@ -4934,12 +4977,10 @@ lemma cteInsert_simple_corres: apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[5] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -4949,12 +4990,9 @@ lemma cteInsert_simple_corres: apply(erule_tac x=aa in allE) apply(erule_tac x=bb in allE) apply(fastforce) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) by(fastforce) declare if_split [split] diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy index 59e18f7d7..ac8f89cac 100644 --- a/proof/refine/X64/CSpace1_R.thy +++ b/proof/refine/X64/CSpace1_R.thy @@ -2461,15 +2461,15 @@ lemma updateCap_corres: apply (unfold cdt_list_relation_def)[1] apply (intro allI impI) apply (erule_tac x=c in allE) - apply (auto elim!: modify_map_casesE)[1] + subgoal by (auto elim!: modify_map_casesE)[1] apply (unfold revokable_relation_def)[1] apply (drule set_cap_caps_of_state_monad) apply (simp add: cte_wp_at_caps_of_state del: split_paired_All) apply (intro allI impI) apply (erule_tac x=c in allE) apply (erule impE[where P="\y. v = Some y" for v]) - apply (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm) - apply (auto elim!: modify_map_casesE del: disjE)[1] (* slow *) + subgoal by (clarsimp simp: null_filter_def is_zombie_def split: if_split_asm) + subgoal by (auto elim!: modify_map_casesE del: disjE)[1] (* slow *) apply (case_tac "ctes_of b (cte_map slot)") apply (simp add: modify_map_None) apply (simp add: modify_map_apply) @@ -2478,10 +2478,10 @@ lemma updateCap_corres: apply (rule use_update_ztc_one [OF descendants_of_update_ztc]) apply simp apply assumption - apply (auto simp: is_cap_simps isCap_simps)[1] + subgoal by (auto simp: is_cap_simps isCap_simps)[1] apply (frule(3) is_final_untyped_ptrs [OF _ _ not_sym], clarsimp+) apply (clarsimp simp: cte_wp_at_caps_of_state) - apply (simp add: is_cap_simps, elim disjE exE, simp_all)[1] + subgoal by (simp add: is_cap_simps, elim disjE exE, simp_all)[1] apply (simp add: eq_commute) apply (drule cte_wp_at_norm, clarsimp) apply (drule(1) pspace_relation_ctes_ofI, clarsimp+) @@ -2492,15 +2492,10 @@ lemma updateCap_corres: apply clarsimp apply (drule cte_wp_at_norm, clarsimp) apply (drule(1) pspace_relation_ctes_ofI, clarsimp+) - apply (simp add: is_cap_simps, elim disjE exE, simp_all add: isCap_simps)[1] + subgoal by (simp add: is_cap_simps, elim disjE exE, simp_all add: isCap_simps)[1] apply clarsimp done -lemma exst_set_cap: - "(x,s') \ fst (set_cap p c s) \ exst s' = exst s" - by (clarsimp simp: set_cap_def in_monad split_def get_object_def set_object_def - split: if_split_asm Structures_A.kernel_object.splits) - lemma updateMDB_eqs: assumes "(x, s'') \ fst (updateMDB p f s')" shows "ksMachineState s'' = ksMachineState s' \ @@ -2551,8 +2546,8 @@ lemma updateMDB_pspace_relation: apply (subst map_upd_triv[symmetric, where t="kheap s"], assumption) apply (erule(2) pspace_relation_update_tcbs) apply (case_tac tcba) - apply (simp add: tcb_cte_cases_def tcb_relation_def del: diff_neg_mask - split: if_split_asm) + subgoal by (simp add: tcb_cte_cases_def tcb_relation_def del: diff_neg_mask + split: if_split_asm) apply (clarsimp simp: cte_wp_at_cases') apply (erule disjE) apply (rule pspace_dom_relatedE, assumption+) @@ -2580,8 +2575,7 @@ lemma updateMDB_ekheap_relation: apply (drule(1) updateObject_cte_is_tcb_or_cte[OF _ refl, rotated]) apply (drule_tac P="(=) s'" in use_valid [OF _ getCTE_sp], rule refl) apply (drule bspec, erule domI) - apply (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm) - done + by (clarsimp simp: tcb_cte_cases_def lookupAround2_char1 split: if_split_asm) lemma updateMDB_pspace_relations: assumes "(x, s'') \ fst (updateMDB p f s')" @@ -2645,24 +2639,17 @@ lemma is_cap_revocable_eq: "\ cap_relation c c'; cap_relation src_cap src_cap'; sameRegionAs src_cap' c'; is_untyped_cap src_cap \ \ is_ep_cap c \ \ is_ntfn_cap c\ \ is_cap_revocable c src_cap = isCapRevocable c' src_cap'" - apply (clarsimp simp: isCap_simps objBits_simps bit_simps arch_is_cap_revocable_def - bits_of_def is_cap_revocable_def Retype_H.isCapRevocable_def - sameRegionAs_def3 isCapRevocable_def - split: cap_relation_split_asm arch_cap.split_asm) - done + by (clarsimp simp: isCap_simps objBits_simps bit_simps arch_is_cap_revocable_def + bits_of_def is_cap_revocable_def Retype_H.isCapRevocable_def + sameRegionAs_def3 isCapRevocable_def + split: cap_relation_split_asm arch_cap.split_asm) lemma isMDBParentOf_prev_update [simp]: "isMDBParentOf (cteMDBNode_update (mdbPrev_update f) cte) cte' = isMDBParentOf cte cte'" "isMDBParentOf cte (cteMDBNode_update (mdbPrev_update f) cte') = isMDBParentOf cte cte'" - apply (cases cte) - apply (cases cte') - apply (simp add: isMDBParentOf_def) - apply (cases cte) - apply (cases cte') - apply (clarsimp simp: isMDBParentOf_def) - done + by (cases cte, cases cte', simp add: isMDBParentOf_def)+ lemma prev_update_subtree [simp]: "modify_map m' x (cteMDBNode_update (mdbPrev_update f)) \ a \ b = m' \ a \ b" @@ -2905,32 +2892,25 @@ lemma is_derived_eq: apply (clarsimp simp: is_derived_def is_derived'_def badge_derived'_def) apply (rule conjI) apply (clarsimp simp: is_cap_simps isCap_simps) - apply (cases c, auto simp: isCap_simps cap_master_cap_def capMasterCap_def)[1] - apply (simp add:vsCapRef_def) - apply (simp add:vs_cap_ref_def) + subgoal by (cases c, auto simp: isCap_simps cap_master_cap_def capMasterCap_def vsCapRef_def + vs_cap_ref_def)[1] apply (case_tac "isIRQControlCap d'") apply (frule(1) master_cap_relation) - apply (clarsimp simp: isCap_simps cap_master_cap_def - is_zombie_def is_reply_cap_def is_master_reply_cap_def - split: cap_relation_split_asm arch_cap.split_asm)[1] + subgoal by (clarsimp simp: isCap_simps cap_master_cap_def + is_zombie_def is_reply_cap_def is_master_reply_cap_def + split: cap_relation_split_asm arch_cap.split_asm)[1] apply (case_tac "isIOPortControlCap' d'") apply (frule(1) master_cap_relation) - apply (clarsimp simp: isCap_simps cap_master_cap_def is_cap_simps is_zombie_def - split: cap_relation_split_asm arch_cap.split_asm) + subgoal by (clarsimp simp: isCap_simps cap_master_cap_def is_cap_simps is_zombie_def + split: cap_relation_split_asm arch_cap.split_asm) apply (frule(1) master_cap_relation) apply (frule(1) cap_badge_relation) apply (frule cap_asid_cap_relation) apply (frule(1) capBadge_ordering_relation) - apply (case_tac d) - apply (simp_all add: isCap_simps is_cap_simps cap_master_cap_def - vs_cap_ref_def vsCapRef_def capMasterCap_def - split: cap_relation_split_asm arch_cap.split_asm) - apply fastforce - apply ((auto split:arch_cap.splits arch_capability.splits option.splits)[7]) - apply (clarsimp split:option.splits arch_cap.splits arch_capability.splits) - apply (intro conjI|clarsimp)+ - apply fastforce - done + by (case_tac d; simp add: isCap_simps is_cap_simps cap_master_cap_def + vs_cap_ref_def vsCapRef_def capMasterCap_def + split: cap_relation_split_asm arch_cap.split_asm) + (auto split:arch_cap.splits arch_capability.splits option.splits) (* slow *) end locale masterCap = @@ -4752,7 +4732,7 @@ lemma updateCap_cte_wp_at': updateCap ptr cap \\rv s. Q (cte_wp_at' P' p s)\" apply (simp add:updateCap_def cte_wp_at_ctes_of) apply (wp setCTE_ctes_of_wp getCTE_wp) - apply (clarsimp simp: cte_wp_at_ctes_of split del: if_split) + apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte, auto split: if_split) done @@ -5327,34 +5307,55 @@ lemma cteInsert_corres: apply (clarsimp simp: put_def state_relation_def) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def - prev_update_modify_mdb_relation) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 - apply (clarsimp simp: valid_mdb'_def - valid_mdb_ctes_def no_0_def) + subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (subgoal_tac "cte_map src \ 0") prefer 2 - apply (clarsimp simp: valid_mdb'_def - valid_mdb_ctes_def no_0_def) + subgoal by (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (thin_tac "ksMachineState t = p" for p t)+ apply (thin_tac "ksCurThread t = p" for p t)+ apply (thin_tac "ksIdleThread t = p" for p t)+ apply (thin_tac "ksReadyQueues t = p" for p t)+ apply (thin_tac "ksSchedulerAction t = p" for p t)+ apply (clarsimp simp: pspace_relations_def) - apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_list t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "ekheap t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "pspace_relation s s'" for s s')+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ + apply (thin_tac "sched_act_relation s s'" for s s')+ + apply (thin_tac "ready_queues_relation s s'" for s s')+ + apply (thin_tac "ghost_relation p s s'" for p s s')+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ + apply (thin_tac "ctes_of s = t" for s t)+ + apply (thin_tac "machine_state t = s" for s t)+ apply (rule conjI) defer apply(rule conjI) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -5416,7 +5417,7 @@ lemma cteInsert_corres: apply(case_tac "ca=src") apply(simp) apply(clarsimp simp: modify_map_def) - apply(fastforce split: if_split_asm) + subgoal by(fastforce split: if_split_asm) apply(case_tac "ca = dest") apply(simp) apply(rule impI) @@ -5426,8 +5427,7 @@ lemma cteInsert_corres: subgoal by(simp) subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def) subgoal by(clarsimp) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + subgoal by(drule cte_map_inj_eq'; simp) apply(erule_tac x=src in allE)+ subgoal by(fastforce) apply(simp) @@ -5438,8 +5438,7 @@ lemma cteInsert_corres: apply(simp_all)[4] apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') subgoal by(simp) subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -5448,12 +5447,9 @@ lemma cteInsert_corres: apply(case_tac z) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) @@ -5472,20 +5468,17 @@ lemma cteInsert_corres: subgoal by(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) subgoal by(clarsimp) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) apply(erule_tac x=src in allE)+ subgoal by(fastforce) apply(simp) apply(rule impI) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[4] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') subgoal by(simp) subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -5494,17 +5487,15 @@ lemma cteInsert_corres: apply(case_tac z) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) apply(subgoal_tac "mdb_insert_sib (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') - src_node (cte_map dest) capability.NullCap dest_node c'") + src_node (cte_map dest) capability.NullCap + dest_node c'") prefer 2 apply(simp add: mdb_insert_sib_def) apply(rule mdb_insert_sib_axioms.intro) @@ -5517,8 +5508,7 @@ lemma cteInsert_corres: apply simp apply (subst (asm) is_cap_revocable_eq, assumption, assumption) apply (rule derived_sameRegionAs) - apply (subst is_derived_eq[symmetric], assumption, - assumption, assumption, assumption, assumption) + apply (subst is_derived_eq[symmetric]; assumption) apply assumption subgoal by (clarsimp simp: cte_wp_at_def is_derived_def is_cap_simps cap_master_cap_simps dest!:cap_master_cap_eqDs) @@ -5566,12 +5556,10 @@ lemma cteInsert_corres: apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[4] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -5617,12 +5605,10 @@ lemma cteInsert_corres: apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[4] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') subgoal by(simp) subgoal by(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -5631,15 +5617,11 @@ lemma cteInsert_corres: apply(case_tac z) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] - apply(drule cte_map_inj_eq') - apply(simp_all)[2] + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) + apply(drule cte_map_inj_eq'; simp) apply(erule_tac x="(aa, bb)" in allE)+ subgoal by(fastforce) - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def split: if_split) apply (rule conjI) @@ -5684,19 +5666,15 @@ lemma cteInsert_corres: apply (erule (5) cte_map_inj) (* FIXME *) - apply (rule setUntypedCapAsFull_corres) - apply simp+ + apply (rule setUntypedCapAsFull_corres; simp) apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb - set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap - setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ + set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap + setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -5730,7 +5708,7 @@ lemma cteInsert_corres: apply (subgoal_tac "descendants_of dest (cdt a) = {}") prefer 2 apply (drule mdb_insert.dest_no_descendants) - subgoal by (fastforce simp add: cdt_relation_def simp del: split_paired_All) + subgoal by (fastforce simp add: cdt_relation_def) apply (subgoal_tac "mdb_insert_abs (cdt a) src dest") prefer 2 apply (erule mdb_insert_abs.intro) @@ -5743,8 +5721,7 @@ lemma cteInsert_corres: apply (intro impI allI) apply (unfold const_def) apply (frule(4) iffD1[OF is_derived_eq]) - apply (drule_tac src_cap' = src_cap' in - maskedAsFull_revokable[where a = c',symmetric]) + apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable[where a = c',symmetric]) apply simp apply (subst mdb_insert_child.descendants) apply (rule mdb_insert_child.intro) @@ -5765,11 +5742,11 @@ lemma cteInsert_corres: dest!:cap_master_cap_eqDs) apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node") prefer 2 - apply (simp add: revokable_relation_def del: split_paired_All) + apply (simp add: revokable_relation_def) apply (erule_tac x=src in allE) apply (erule impE) apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state cap_master_cap_simps - split: if_splits dest!:cap_master_cap_eqDs) + split: if_splits dest!:cap_master_cap_eqDs) subgoal by (clarsimp simp: masked_as_full_def is_cap_simps free_index_update_def split: if_splits) subgoal by simp subgoal by clarsimp @@ -5779,7 +5756,7 @@ lemma cteInsert_corres: prefer 2 apply assumption apply (simp_all)[6] - apply (simp add: cdt_relation_def split: if_split del: split_paired_All) + apply (simp add: cdt_relation_def split: if_split) apply clarsimp apply (drule (5) cte_map_inj)+ apply simp @@ -5807,7 +5784,7 @@ lemma cteInsert_corres: dest!:cap_master_cap_eqDs) apply (subgoal_tac "is_original_cap a src = mdbRevocable src_node") subgoal by simp - apply (simp add: revokable_relation_def del: split_paired_All) + apply (simp add: revokable_relation_def) apply (erule_tac x=src in allE) apply (erule impE) apply (clarsimp simp: null_filter_def cte_wp_at_caps_of_state split: if_splits) @@ -5817,9 +5794,9 @@ lemma cteInsert_corres: apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at) apply (rule conjI) apply (clarsimp simp: descendants_of_eq') - subgoal by (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def) apply (clarsimp simp: descendants_of_eq') - subgoal by (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def) done @@ -6823,13 +6800,22 @@ lemma cteSwap_corres: | rule refl | clarsimp simp: put_def simp del: fun_upd_apply )+ apply (simp cong: option.case_cong) apply (drule updateCap_stuff, elim conjE, erule(1) impE) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule in_getCTE, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) - apply (drule (2) updateMDB_the_lot', fastforce, fastforce, simp, clarsimp) + apply (drule (2) updateMDB_the_lot') + apply (erule (1) impE, assumption) + apply (fastforce simp only: no_0_modify_map) + apply assumption + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (drule in_getCTE, elim conjE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (elim conjE TrueE, simp only:) + apply (drule (2) updateMDB_the_lot', fastforce, simp only: no_0_modify_map, assumption) + apply (simp only: pspace_relations_def refl) + apply (rule conjI, rule TrueI)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ apply (thin_tac "ksReadyQueues t = p" for t p)+ @@ -6840,7 +6826,28 @@ lemma cteSwap_corres: apply (thin_tac "ksDomSchedule t = p" for t p)+ apply (thin_tac "ksCurDomain t = p" for t p)+ apply (thin_tac "ksDomainTime t = p" for t p)+ - apply (clarsimp simp: cte_wp_at_ctes_of in_set_cap_cte_at_swp cong: if_cong) + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_list t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "ekheap t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "interrupt_state_relation n s s'" for n s s')+ + apply (thin_tac "(s,s') \ arch_state_relation" for s s')+ + apply (thin_tac "sched_act_relation s s'" for s s')+ + apply (thin_tac "ready_queues_relation s s'" for s s')+ + apply (simp only: simp_thms no_0_modify_map) + apply (clarsimp simp: cte_wp_at_ctes_of cong: if_cong) apply (thin_tac "ctes_of x = y" for x y)+ apply (case_tac cte1) apply (rename_tac src_cap src_node) @@ -6861,24 +6868,39 @@ lemma cteSwap_corres: apply (erule weak_derived_sym') apply (erule weak_derived_sym') apply assumption - apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def) + subgoal by (simp only: simp_thms ghost_relation_typ_at set_cap_a_type_inv X64.data_at_def) + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ekheap_relation e p" for e p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "pspace_relation s t" for s t)+ + apply (thin_tac "ghost_relation h s t" for h s t)+ apply(subst conj_assoc[symmetric]) apply (rule conjI) prefer 2 apply (clarsimp simp add: revokable_relation_def in_set_cap_cte_at simp del: split_paired_All) apply (drule set_cap_caps_of_state_monad)+ - apply (thin_tac "pspace_relation s t" for s t)+ apply (simp del: split_paired_All split: if_split) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule(1) mdb_swap.revokable) apply (erule_tac x="dest" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (clarsimp simp del: split_paired_All) apply (rule conjI) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) @@ -6887,19 +6909,19 @@ lemma cteSwap_corres: apply (simp del: split_paired_All) apply (erule_tac x="src" in allE) apply (erule impE) - apply (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) - apply simp + subgoal by (clarsimp simp: null_filter_def weak_derived_Null split: if_splits) + subgoal by simp apply (drule caps_of_state_cte_at)+ apply (erule (5) cte_map_inj) apply (clarsimp simp: cte_wp_at_caps_of_state simp del: split_paired_All) apply (drule (1) mdb_swap.revokable) apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \ None") prefer 2 - apply (clarsimp simp: null_filter_def split: if_splits) + subgoal by (clarsimp simp: null_filter_def split: if_splits) apply clarsimp apply (subgoal_tac "cte_map (aa,bb) \ cte_map src") apply (subgoal_tac "cte_map (aa,bb) \ cte_map dest") - apply (clarsimp simp del: split_paired_All) + subgoal by (clarsimp simp del: split_paired_All) apply (drule caps_of_state_cte_at)+ apply (drule null_filter_caps_of_stateD)+ apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) @@ -6908,7 +6930,7 @@ lemma cteSwap_corres: apply (erule cte_map_inj, erule cte_wp_cte_at, assumption+) apply (subgoal_tac "no_loops (ctes_of b)") prefer 2 - apply (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) + subgoal by (simp add: valid_mdb_ctes_def mdb_chain_0_no_loops) apply (subgoal_tac "mdb_swap_abs (cdt a) src dest a") prefer 2 apply (erule mdb_swap_abs.intro) @@ -6918,7 +6940,7 @@ lemma cteSwap_corres: apply assumption apply (frule mdb_swap_abs''.intro) apply (drule_tac t="cdt_list (a)" in mdb_swap_abs'.intro) - apply (simp add: mdb_swap_abs'_axioms_def) + subgoal by (simp add: mdb_swap_abs'_axioms_def) apply (thin_tac "modify_map m f p p' = t" for m f p p' t) apply(rule conjI) apply (simp add: cdt_relation_def del: split_paired_All) @@ -6962,7 +6984,7 @@ lemma cteSwap_corres: apply (erule cte_wp_at_weakenE, rule TrueI) apply (erule (1) descendants_of_cte_at) apply assumption+ - apply simp + subgoal by simp apply (subst insert_minus_eq, assumption) apply clarsimp apply (subst insert_minus_eq [where x="cte_map dest"], assumption) @@ -6970,7 +6992,7 @@ lemma cteSwap_corres: apply (erule (3) inj_on_descendants_cte_map) apply (rule subset_refl) apply clarsimp - apply auto[1] + subgoal by auto apply clarsimp apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) @@ -7062,12 +7084,10 @@ lemma cteSwap_corres: cte_map (aa, bb) = mdbPrev src_node") apply(clarsimp) apply(rule conjI) - apply(rule cte_map_inj) - apply(simp_all)[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(rule conjI) - apply(rule cte_map_inj) - apply(simp_all)[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(frule mdb_swap.m_exists) apply(simp) @@ -7076,8 +7096,7 @@ lemma cteSwap_corres: apply(clarsimp) apply(simp add: valid_mdb'_def) apply(clarsimp) - apply(rule cte_at_next_slot) - apply(simp_all)[4] + subgoal by (rule cte_at_next_slot; simp) apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a) = Some dest") apply(simp) apply(erule_tac x=aa in allE, erule_tac x=bb in allE) @@ -7090,12 +7109,10 @@ lemma cteSwap_corres: apply(clarsimp) apply(clarsimp simp: mdb_swap.prev_dest_src) apply(rule conjI) - apply(rule cte_map_inj) - apply(simp_all)[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(rule conjI) - apply(rule cte_map_inj) - apply(simp_all)[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(frule mdb_swap.m_exists) apply(simp) @@ -7104,8 +7121,7 @@ lemma cteSwap_corres: apply(clarsimp) apply(simp add: valid_mdb'_def) apply(clarsimp) - apply(rule cte_at_next_slot) - apply(simp_all)[4] + subgoal by (rule cte_at_next_slot; simp) apply(simp) apply(case_tac "next_slot (aa, bb) (cdt_list (a)) (cdt a)") apply(simp) @@ -7119,12 +7135,10 @@ lemma cteSwap_corres: cte_map (aa, bb) \ mdbPrev dest_node") apply(clarsimp) apply(rule conjI) - apply(rule cte_map_inj) - apply(simp_all)[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(rule conjI) - apply(rule cte_map_inj) - apply simp_all[6] + apply(rule cte_map_inj; simp?) apply(erule cte_wp_at_weakenE, simp) apply(rule conjI) apply(frule mdb_swap.m_exists) @@ -7134,9 +7148,8 @@ lemma cteSwap_corres: subgoal by (clarsimp) apply(simp add: valid_mdb'_def) apply(clarsimp) - apply(drule cte_map_inj_eq) - apply(rule cte_at_next_slot') - apply(simp_all)[9] + apply(drule cte_map_inj_eq; simp?) + subgoal by (rule cte_at_next_slot'; simp) apply(erule cte_wp_at_weakenE, simp) apply(frule mdb_swap.m_exists) apply(simp) @@ -7145,13 +7158,10 @@ lemma cteSwap_corres: apply(clarsimp) apply(simp add: valid_mdb'_def) apply(clarsimp) - apply(drule cte_map_inj_eq) - apply(rule cte_at_next_slot') - apply(simp_all)[9] - apply(erule cte_wp_at_weakenE, simp) - apply(rule cte_at_next_slot) - apply(simp_all) - done + apply(drule cte_map_inj_eq; simp?) + subgoal by (rule cte_at_next_slot'; simp) + apply(erule cte_wp_at_weakenE, simp) + by (rule cte_at_next_slot; simp) lemma capSwapForDelete_corres: diff --git a/proof/refine/X64/CSpace_I.thy b/proof/refine/X64/CSpace_I.thy index faac6a05d..6ab6bace0 100644 --- a/proof/refine/X64/CSpace_I.thy +++ b/proof/refine/X64/CSpace_I.thy @@ -776,8 +776,7 @@ lemma sameObjectAs_def2: split del: if_split cong: if_cong) apply (simp add: capRange_def isCap_simps split del: if_split) - apply fastforce - done + by fastforce lemmas sameRegionAs_def3 = sameRegionAs_def2 [simplified capClass_Master capRange_Master isCap_Master] diff --git a/proof/refine/X64/CSpace_R.thy b/proof/refine/X64/CSpace_R.thy index d1fc74152..b44d18e45 100644 --- a/proof/refine/X64/CSpace_R.thy +++ b/proof/refine/X64/CSpace_R.thy @@ -101,7 +101,7 @@ lemma src_no_parent [iff]: lemma no_0_n: "no_0 n" by (simp add: n_def no_0) lemma no_0': "no_0 m'" by (simp add: m'_def no_0_n) -lemma next_neq_dest [simp]: +lemma next_neq_dest [iff]: "mdbNext src_node \ dest" using dlist src dest prev dest_0 no_0 by (fastforce simp add: valid_dlist_def no_0_def Let_def) @@ -201,26 +201,10 @@ proof - thus ?thesis by (simp add: m'_def) qed -lemma [iff]: +lemma dest_not_parent [iff]: "m \ dest parentOf c = False" using dest by (simp add: parentOf_def) -lemma [iff]: - "mdbNext src_node \ dest" -proof - assume "mdbNext src_node = dest" - moreover have "dest \ 0" .. - ultimately - have "mdbPrev old_dest_node = src" - using src dest dlist - by (fastforce elim: valid_dlistEn) - with prev - show False by (simp add: src_0) -qed - -lemmas no_loops_simps [simp] = - no_loops_direct_simp [OF no_loops] no_loops_trancl_simp [OF no_loops] - lemma dest_source [iff]: "(m \ dest \ x) = (x = 0)" using dest nxt by (simp add: next_unfold') @@ -884,10 +868,12 @@ lemma cteMove_corres: apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule (4) updateMDB_the_lot, elim conjE) apply (drule updateCap_stuff, elim conjE, erule (1) impE) - apply (drule updateCap_stuff, clarsimp) + apply (drule updateCap_stuff) apply (subgoal_tac "pspace_distinct' b \ pspace_aligned' b") prefer 2 - subgoal by fastforce + apply (elim valid_pspaceE' conjE) + apply (rule conjI; assumption) + apply (simp only: ) apply (thin_tac "ctes_of t = s" for t s)+ apply (thin_tac "ksMachineState t = p" for t p)+ apply (thin_tac "ksCurThread t = p" for t p)+ @@ -896,7 +882,7 @@ lemma cteMove_corres: apply (thin_tac "ksSchedulerAction t = p" for t p)+ apply (subgoal_tac "\p. cte_at p ta = cte_at p a") prefer 2 - apply (simp add: set_cap_cte_eq) + subgoal by (simp add: set_cap_cte_eq) apply (clarsimp simp add: swp_def cte_wp_at_ctes_of simp del: split_paired_All) apply (subgoal_tac "cte_at ptr' a") prefer 2 @@ -909,7 +895,37 @@ lemma cteMove_corres: apply fastforce apply (clarsimp simp: pspace_relations_def) apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "ghost_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (subst conj_assoc[symmetric]) apply (rule conjI) defer @@ -947,7 +963,7 @@ lemma cteMove_corres: apply fastforce apply fastforce apply fastforce - apply clarsimp + subgoal by clarsimp subgoal by (simp add: null_filter_def split: if_splits) (*long *) apply (subgoal_tac "mdb_move (ctes_of b) (cte_map ptr) src_cap src_node (cte_map ptr') cap' old_dest_node") prefer 2 @@ -972,13 +988,13 @@ lemma cteMove_corres: apply fastforce apply (fastforce elim!: cte_wp_at_weakenE) apply simp - apply simp + subgoal by simp apply (case_tac "(aa,bb) = ptr", simp) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) apply (case_tac "(aa,bb) = ptr'") - apply (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def del: split_paired_All) apply (subgoal_tac "cte_map (aa,bb) \ cte_map ptr'") prefer 2 apply (erule (2) cte_map_inj, fastforce, fastforce, fastforce) @@ -987,7 +1003,7 @@ lemma cteMove_corres: apply (subgoal_tac "descendants_of' (cte_map (aa, bb)) (ctes_of b) = cte_map ` descendants_of (aa, bb) (cdt a)") prefer 2 - apply (simp add: cdt_relation_def del: split_paired_All) + subgoal by (simp add: cdt_relation_def del: split_paired_All) apply simp apply (rule conjI) apply clarsimp @@ -998,8 +1014,8 @@ lemma cteMove_corres: apply fastforce apply fastforce apply (rule subset_refl) - apply simp - apply simp + subgoal by simp + subgoal by simp apply clarsimp apply (drule (1) cte_map_inj_eq) apply (erule descendants_of_cte_at) @@ -1018,7 +1034,7 @@ lemma cteMove_corres: apply(intro allI impI) apply(rule mdb_move_abs'.next_slot) apply(simp, fastforce, simp) - apply(fastforce split: option.splits) + subgoal by(fastforce split: option.splits) apply(case_tac "ctes_of b (cte_map (aa, bb))") subgoal by (clarsimp simp: modify_map_def split: if_split_asm) apply(case_tac ab) @@ -5004,12 +5020,41 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: put_def state_relation_def simp del: fun_upd_apply) apply (drule updateCap_stuff) apply clarsimp - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) - apply (drule (3) updateMDB_the_lot', simp, simp, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) + apply (drule (3) updateMDB_the_lot', simp only: no_0_modify_map, simp only:, elim conjE) apply (clarsimp simp: pspace_relations_def) + apply (thin_tac "gsCNodes t = p" for t p)+ + apply (thin_tac "ksMachineState t = p" for t p)+ + apply (thin_tac "ksCurThread t = p" for t p)+ + apply (thin_tac "ksWorkUnitsCompleted t = p" for t p)+ + apply (thin_tac "ksIdleThread t = p" for t p)+ + apply (thin_tac "ksReadyQueues t = p" for t p)+ + apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (thin_tac "cur_thread t = p" for t p)+ + apply (thin_tac "domain_index t = p" for t p)+ + apply (thin_tac "domain_time t = p" for t p)+ + apply (thin_tac "cur_domain t = p" for t p)+ + apply (thin_tac "scheduler_action t = p" for t p)+ + apply (thin_tac "ready_queues t = p" for t p)+ + apply (thin_tac "idle_thread t = p" for t p)+ + apply (thin_tac "machine_state t = p" for t p)+ + apply (thin_tac "work_units_completed t = p" for t p)+ + apply (thin_tac "ksArchState t = p" for t p)+ + apply (thin_tac "gsUserPages t = p" for t p)+ + apply (thin_tac "ksCurDomain t = p" for t p)+ + apply (thin_tac "ksInterruptState t = p" for t p)+ + apply (thin_tac "ksDomScheduleIdx t = p" for t p)+ + apply (thin_tac "ksDomainTime t = p" for t p)+ + apply (thin_tac "ksDomSchedule t = p" for t p)+ + apply (thin_tac "ctes_of t = p" for t p)+ + apply (thin_tac "ekheap_relation t p" for t p)+ + apply (thin_tac "pspace_relation t p" for t p)+ + apply (thin_tac "interrupt_state_relation s t p" for s t p)+ + apply (thin_tac "sched_act_relation t p" for t p)+ + apply (thin_tac "ready_queues_relation t p" for t p)+ apply (rule conjI) - apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) + subgoal by (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv data_at_def) apply (clarsimp simp: cte_wp_at_ctes_of nullPointer_def prev_update_modify_mdb_relation) apply (subgoal_tac "cte_map dest \ 0") prefer 2 @@ -5017,13 +5062,7 @@ lemma cteInsert_simple_corres: valid_mdb_ctes_def no_0_def) apply (subgoal_tac "cte_map src \ 0") prefer 2 - apply (clarsimp simp: valid_mdb'_def - valid_mdb_ctes_def no_0_def) - apply (thin_tac "ksMachineState t = p" for t p)+ - apply (thin_tac "ksCurThread t = p" for t p)+ - apply (thin_tac "ksIdleThread t = p" for t p)+ - apply (thin_tac "ksReadyQueues t = p" for t p)+ - apply (thin_tac "ksSchedulerAction t = p" for t p)+ + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def no_0_def) apply (subgoal_tac "should_be_parent_of src_cap (is_original_cap a src) c (is_cap_revocable c src_cap) = True") prefer 2 apply (subst should_be_parent_of_masked_as_full[symmetric]) @@ -5032,7 +5071,6 @@ lemma cteInsert_simple_corres: apply (subst conj_assoc[symmetric]) apply (rule conjI) defer - apply (thin_tac "ctes_of t = t'" for t t')+ apply (clarsimp simp: modify_map_apply) apply (clarsimp simp: revokable_relation_def simp del: fun_upd_apply) apply (simp split: if_split) @@ -5047,7 +5085,7 @@ lemma cteInsert_simple_corres: apply (subst same_region_as_relation [symmetric]) prefer 3 apply (rule safe_parent_same_region) - apply (simp add: cte_wp_at_caps_of_state safe_parent_for_masked_as_full) + apply (simp add: cte_wp_at_caps_of_state) apply assumption apply assumption apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) @@ -5076,17 +5114,14 @@ lemma cteInsert_simple_corres: apply (rule setUntypedCapAsFull_corres) apply simp+ apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_valid_list - set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap - setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ + set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap + setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) - apply (thin_tac "ctes_of s = t" for s t)+ - apply (thin_tac "pspace_relation s t" for s t)+ - apply (thin_tac "machine_state t = s" for t s)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) apply (case_tac "rv'") @@ -5094,7 +5129,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") prefer 2 - subgoal by (fastforce simp: cte_wp_at_def safe_parent_for_masked_as_full) + subgoal by (fastforce simp: cte_wp_at_def) apply (erule conjE) apply (subgoal_tac "mdb_insert (ctes_of b) (cte_map src) (maskedAsFull src_cap' c') src_node @@ -5163,8 +5198,7 @@ lemma cteInsert_simple_corres: apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) apply(clarsimp) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by(drule cte_map_inj_eq; simp) apply(erule_tac x="fst src" in allE) apply(erule_tac x="snd src" in allE) apply(fastforce) @@ -5174,12 +5208,10 @@ lemma cteInsert_simple_corres: apply(simp) apply(subgoal_tac "cte_at ca a") prefer 2 - apply(rule cte_at_next_slot) - apply(simp_all)[5] + subgoal by (rule cte_at_next_slot; simp) apply(clarsimp simp: modify_map_def const_def) apply(simp split: if_split_asm) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) apply(drule_tac p="cte_map src" in valid_mdbD1') apply(simp) apply(simp add: valid_mdb'_def valid_mdb_ctes_def) @@ -5189,12 +5221,9 @@ lemma cteInsert_simple_corres: apply(erule_tac x=aa in allE) apply(erule_tac x=bb in allE) apply(fastforce) - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] - apply(drule cte_map_inj_eq) - apply(simp_all)[6] + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) + subgoal by (drule cte_map_inj_eq; simp) by(fastforce) declare if_split [split] @@ -5310,7 +5339,7 @@ lemma n_direct_eq': "n' \ p \ p' = (if p = src then p' = dest else if p = dest then m \ src \ p' else m \ p \ p')" - by (simp add: n'_def mdb_next_modify n_direct_eq) + by (simp add: n'_def n_direct_eq) lemma dest_no_next_p: "m p = Some cte \ mdbNext (cteMDBNode cte) \ dest" diff --git a/proof/refine/X64/KHeap_R.thy b/proof/refine/X64/KHeap_R.thy index 430574fda..689169999 100644 --- a/proof/refine/X64/KHeap_R.thy +++ b/proof/refine/X64/KHeap_R.thy @@ -786,10 +786,7 @@ lemma tcb_cte_cases_change: "tcb_cte_cases x = Some (getF, setF) \ (\getF. (\setF. tcb_cte_cases y = Some (getF, setF)) \ getF (setF f tcb) \ getF tcb) = (x = y \ f (getF tcb) \ getF tcb)" - apply (rule iffI) - apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) - apply (clarsimp simp: tcb_cte_cases_def split: if_split_asm) - done + by (rule iffI; clarsimp simp: tcb_cte_cases_def split: if_split_asm) (* long *) lemma cte_level_bits_nonzero [simp]: "0 < cte_level_bits" by (simp add: cte_level_bits_def) @@ -924,13 +921,12 @@ lemma obj_relation_cut_same_type: \ (\sz sz'. a_type ko = AArch (ADeviceData sz) \ a_type ko' = AArch (ADeviceData sz'))" apply (rule ccontr) apply (simp add: obj_relation_cuts_def2 a_type_def) - apply (auto simp: other_obj_relation_def cte_relation_def - pte_relation_def pde_relation_def - pdpte_relation_def pml4e_relation_def - split: Structures_A.kernel_object.split_asm if_split_asm - Structures_H.kernel_object.split_asm - X64_A.arch_kernel_obj.split_asm) - done + by (auto simp: other_obj_relation_def cte_relation_def + pte_relation_def pde_relation_def + pdpte_relation_def pml4e_relation_def + split: Structures_A.kernel_object.split_asm if_split_asm + Structures_H.kernel_object.split_asm + X64_A.arch_kernel_obj.split_asm) definition exst_same :: "Structures_H.tcb \ Structures_H.tcb \ bool" where @@ -977,7 +973,7 @@ lemma setObject_other_corres: apply (erule_tac x=ptr in allE)+ apply (clarsimp simp: obj_at_def a_type_def split: Structures_A.kernel_object.splits if_split_asm) - apply (simp split: arch_kernel_obj.splits if_splits) + subgoal by (simp split: arch_kernel_obj.splits if_splits) apply (fold fun_upd_def) apply (simp only: pspace_relation_def pspace_dom_update dom_fun_upd2 simp_thms) apply (elim conjE) @@ -996,10 +992,8 @@ lemma setObject_other_corres: apply (insert t, clarsimp simp: is_other_obj_relation_type_CapTable a_type_def) apply (erule disjE) - apply (insert t, - clarsimp simp: is_other_obj_relation_type_UserData a_type_def) - apply (insert t, - clarsimp simp: is_other_obj_relation_type_DeviceData a_type_def) + apply (insert t, clarsimp simp: is_other_obj_relation_type_UserData a_type_def) + apply (insert t, clarsimp simp: is_other_obj_relation_type_DeviceData a_type_def) apply (simp only: ekheap_relation_def) apply (rule ballI, drule(1) bspec) apply (drule domD) @@ -1011,15 +1005,15 @@ lemma setObject_other_corres: apply (case_tac ob; simp_all add: a_type_def other_obj_relation_def etcb_relation_def is_other_obj_relation_type t exst_same_def) - apply (clarsimp simp: is_other_obj_relation_type t exst_same_def - split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits - X64_A.arch_kernel_obj.splits)+ - done + by (clarsimp simp: is_other_obj_relation_type t exst_same_def + split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits + X64_A.arch_kernel_obj.splits)+ lemmas obj_at_simps = obj_at_def obj_at'_def projectKOs map_to_ctes_upd_other is_other_obj_relation_type_def a_type_def objBits_simps other_obj_relation_def archObjSize_def pageBits_def + lemma setEndpoint_corres: "ep_relation e e' \ corres dc (ep_at ptr) (ep_at' ptr) @@ -1073,8 +1067,7 @@ lemma getNotification_corres: lemma setObject_ko_wp_at: fixes v :: "'a :: pspace_storable" - assumes R: "\ko s x y n. (updateObject v ko p y n s) - = (updateObject_default v ko p y n s)" + assumes R: "\ko s y n. (updateObject v ko p y n s) = (updateObject_default v ko p y n s)" assumes n: "\v' :: 'a. objBits v' = n" assumes m: "(1 :: machine_word) < 2 ^ n" shows "\\s. obj_at' (\x :: 'a. True) p s \ @@ -2172,7 +2165,6 @@ lemma doMachineOp_invs_bits[wp]: | wp cur_tcb_lift sch_act_wf_lift tcb_in_cur_domain'_lift | fastforce elim: state_refs_of'_pspaceI)+ -crunch cte_wp_at'[wp]: doMachineOp "\s. P (cte_wp_at' P' p s)" crunch obj_at'[wp]: doMachineOp "\s. P (obj_at' P' p s)" crunch it[wp]: doMachineOp "\s. P (ksIdleThread s)"