diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index 01509a33f..4ef13b5bf 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -223,30 +223,15 @@ lemma reachable_pg_cap_cdt_update[simp]: lemma replaceable_cdt_update[simp]: "replaceable (cdt_update f s) = replaceable s" - by (clarsimp simp: replaceable_def tcb_cap_valid_def intro!: ext) - - -lemma valid_pspace_cdt_update[simp]: - "valid_pspace (cdt_update f s) = valid_pspace s" - by (fastforce elim!: valid_pspace_eqI) - - -lemma ifunsafe_cdt_update[simp]: - "if_unsafe_then_cap (cdt_update f s) = if_unsafe_then_cap s" - by (fastforce elim!: ifunsafe_pspaceI) - + by (fastforce simp: replaceable_def tcb_cap_valid_def) lemma reachable_pg_cap_is_original_cap_update[simp]: "reachable_pg_cap x (is_original_cap_update f s) = reachable_pg_cap x s" by (simp add: reachable_pg_cap_def) - lemma replaceable_revokable_update[simp]: "replaceable (is_original_cap_update f s) = replaceable s" - by (clarsimp intro!: ext - simp: replaceable_def is_final_cap'_def2 - tcb_cap_valid_def) - + by (fastforce simp: replaceable_def is_final_cap'_def2 tcb_cap_valid_def) lemma zombies_final_cdt_update[simp]: "zombies_final (cdt_update f s) = zombies_final s" @@ -297,19 +282,11 @@ proof - by (clarsimp simp: st_tcb_def2) qed -lemma tcb_cap_valid_more_update[simp]: - "tcb_cap_valid cap sl (trans_state f s) = tcb_cap_valid cap sl s" - by (simp add: tcb_cap_valid_def) - lemma reachable_pg_cap_update[simp]: "reachable_pg_cap cap' (trans_state f s) = reachable_pg_cap cap' s" by (simp add:reachable_pg_cap_def vs_lookup_pages_def vs_lookup_pages1_def obj_at_def) -lemma reachable_pg_cap_exst_update[simp]: - "reachable_pg_cap cap' (trans_state f s) = reachable_pg_cap cap' s" - by (simp add:reachable_pg_cap_def) - lemma replaceable_more_update[simp]: "replaceable (trans_state f s) sl cap cap' = replaceable s sl cap cap'" by (simp add: replaceable_def) @@ -446,8 +423,6 @@ lemma empty_slot_final_cap_at: crunch st_tcb_at[wp]: empty_slot "st_tcb_at P t" -declare if_cong[cong] - lemma set_cap_revokable_update: "((),s') \ fst (set_cap c p s) \ ((),is_original_cap_update f s') \ fst (set_cap c p (is_original_cap_update f s))" @@ -678,7 +653,7 @@ lemma finalise_cap_cases1: \ cap_irqs (fst rv) = cap_irqs cap \ fst_cte_ptrs (fst rv) = fst_cte_ptrs cap \ vs_cap_ref cap = None\" - apply (cases cap, simp_all split del: split_if) + apply (cases cap, simp_all split del: split_if cong: if_cong) apply (wp suspend_final_cap[where sl=slot] deleting_irq_handler_final[where slot=slot] | simp add: o_def is_cap_simps fst_cte_ptrs_def @@ -731,7 +706,11 @@ crunch typ_at[wp]: arch_finalise_cap "\s. P (typ_at T p s)" (wp: crunch_wps simp: crunch_simps unless_def assertE_def ignore: maskInterrupt ) +context +begin +declare if_cong[cong] crunch typ_at[wp]: finalise_cap "\s. P (typ_at T p s)" +end lemma valid_cap_Null_ext: "valid_cap cap.NullCap = \" @@ -743,16 +722,12 @@ lemma finalise_cap_new_valid_cap[wp]: apply (wp suspend_valid_cap | simp add: o_def valid_cap_def cap_aligned_def valid_cap_Null_ext - del: hoare_post_taut - (* removing hoare_post_taut so wp doesn't include - completely random irrelevant wp lemmas in the proof *) - split del: if_splits + split del: split_if | clarsimp | rule conjI)+ apply (simp add: arch_finalise_cap_def) apply (rule hoare_pre) apply (wp|simp add: o_def valid_cap_def cap_aligned_def - del: hoare_post_taut - split del: if_splits|clarsimp|wpc)+ + split del: split_if|clarsimp|wpc)+ done lemma invs_arm_asid_table_unmap: @@ -1154,7 +1129,6 @@ lemma finalise_cap_replaceable: can_fast_finalise_def obj_irq_refs_subset vs_cap_ref_def - is_pt_cap_def is_pd_cap_def valid_ipc_buffer_cap_def dest!: tcb_cap_valid_NullCapD split: Structures_A.thread_state.split_asm @@ -1175,8 +1149,7 @@ lemma finalise_cap_replaceable: apply (clarsimp simp: replaceable_def reachable_pg_cap_def o_def cap_range_def valid_arch_state_def ran_tcb_cap_cases is_cap_simps - obj_irq_refs_subset - vs_cap_ref_def is_pt_cap_def is_pd_cap_def)+ + obj_irq_refs_subset vs_cap_ref_def)+ apply (fastforce split: option.splits vmpage_size.splits) done @@ -1545,9 +1518,6 @@ lemma finalise_cap_fast_Null: done -declare empty_fail_clearMemory[simp] - - lemma tcb_cap_valid_pagetable: "tcb_cap_valid (cap.ArchObjectCap (arch_cap.PageTableCap word (Some v))) slot = tcb_cap_valid (cap.ArchObjectCap (arch_cap.PageTableCap word None)) slot" @@ -1936,7 +1906,7 @@ lemma store_pde_pde_wp_at: \\_. pde_wp_at (\pde. pde = x) (p && ~~ mask pd_bits) (ucast (p && mask pd_bits >> 2))\" apply (wp - | simp add: store_pde_def set_pd_def set_pd_def set_object_def get_object_def + | simp add: store_pde_def set_pd_def set_object_def get_object_def obj_at_def pde_wp_at_def)+ done @@ -1946,7 +1916,7 @@ lemma store_pde_pde_wp_at2: store_pde p' ARM_Structs_A.pde.InvalidPDE \\_. pde_wp_at (\pde. pde = ARM_Structs_A.pde.InvalidPDE) ptr slot\" apply (wp - | simp add: store_pde_def set_pd_def set_pd_def set_object_def get_object_def + | simp add: store_pde_def set_pd_def set_object_def get_object_def obj_at_def pde_wp_at_def | clarsimp)+ done @@ -2020,7 +1990,7 @@ lemma pd_shifting_again5: apply simp apply (cut_tac x="ucast ae :: word32" and n=2 in shiftl_shiftr_id) apply ((simp add: word_bits_def less_le_trans[OF ucast_less])+)[2] - apply (simp add:ucast_bl word_bl.Rep_inverse) + apply (simp add:ucast_bl) apply (subst word_rep_drop) apply simp done @@ -2323,7 +2293,6 @@ lemma mapM_x_swp_store_invalid_pde_invs: lemma arch_cap_recycle_replaceable: notes split_if [split del] - and hoare_post_taut [simp del] and arch_reset_mem_mapping.simps [simp del] shows "\cte_wp_at (op = (cap.ArchObjectCap cap)) slot and invs @@ -2475,7 +2444,6 @@ lemma gts_wp: done lemma cap_recycle_replaceable: - notes hoare_post_taut [simp del] shows "\invs and cte_wp_at (op = cap) slot and zombies_final and valid_objs and K (cap \ cap.NullCap) and (\s. is_final = is_final_cap' cap s)\ @@ -2504,8 +2472,7 @@ lemma cap_recycle_replaceable: -- "last imp goal" apply (simp add: replaceable_or_arch_update_same) apply (cases cap, simp_all add: is_cap_simps) - apply (clarsimp simp: is_cap_simps obj_irq_refs_subset is_pt_cap_def is_pd_cap_def - vs_cap_ref_def cap_range_def + apply (clarsimp simp: is_cap_simps obj_irq_refs_subset vs_cap_ref_def cap_range_def cong: rev_conj_cong) apply (frule(1) zombies_finalD [OF caps_of_state_cteD], clarsimp simp: is_cap_simps) apply (clarsimp simp: cte_wp_at_caps_of_state) @@ -2576,21 +2543,6 @@ lemma set_asid_pool_obj_at_ptr: done -lemma zombies_final_arch [simp]: - "zombies_final (arch_state_update f s) = zombies_final s" - by (simp add: zombies_final_def is_final_cap'_def) - - -lemma state_refs_of_arch [simp]: - "state_refs_of (arch_state_update f s) = state_refs_of s" - by (simp add: state_refs_of_def) - - -lemma valid_global_refs_table [simp]: - "valid_global_refs (s\arch_state := arch_state s\arm_asid_table := arm_asid_table'\\) = valid_global_refs s" - by (simp add: valid_global_refs_def global_refs_def) - - lemma valid_arch_state_table_strg: "valid_arch_state s \ asid_pool_at p s \ Some p \ arm_asid_table (arch_state s) ` (dom (arm_asid_table (arch_state s)) - {x}) \ @@ -2934,7 +2886,6 @@ lemma arch_recycle_cap_invs: store_pte_typ_at static_imp_wp | simp add: fun_upd_def[symmetric] cte_wp_at_caps_of_state valid_cap_simps - split del: split_if | wpc)+) apply (case_tac slot) apply clarsimp @@ -2957,7 +2908,7 @@ lemma arch_recycle_cap_invs: apply simp+ apply (clarsimp simp: valid_cap_simps) apply (clarsimp simp: is_cap_simps valid_cap_simps mask_def asid_bits_def - vmsz_aligned_def upto_enum_step_def pt_bits_def pageBits_def is_cap_simps + vmsz_aligned_def upto_enum_step_def pt_bits_def pageBits_def image_image word32_shift_by_2 split: split_if_asm) apply (erule order_le_less_trans, simp)+ apply (rule_tac x=a in exI, rule_tac x=b in exI) @@ -3204,9 +3155,7 @@ lemma arch_recycle_cap_valid[wp]: in hoare_post_imp) apply (erule conjE) apply (erule disjE) - apply ((clarsimp simp: arch_reset_mem_mapping.simps - valid_cap_def cap_aligned_def - | rename_tac arch_cap, case_tac arch_cap)+)[2] + apply ((clarsimp simp: valid_cap_def cap_aligned_def | case_tac arch_cap)+)[2] apply (simp add: arch_recycle_cap_def) apply (intro conjI impI) apply (wp unmap_page_table_valid_cap invalidate_tlb_by_asid_valid_cap @@ -3247,8 +3196,7 @@ lemma recycle_cap_valid[wp]: lemma recycle_cap_cases: - notes hoare_post_taut [simp del] - and split_if [split del] + notes split_if [split del] shows "\\\ recycle_cap is_final cap \\rv s. rv = cap diff --git a/proof/invariant-abstract/KHeap_AI.thy b/proof/invariant-abstract/KHeap_AI.thy index fa094a263..ea3455aa5 100644 --- a/proof/invariant-abstract/KHeap_AI.thy +++ b/proof/invariant-abstract/KHeap_AI.thy @@ -218,23 +218,9 @@ lemma set_cdt_inv: done -lemma cte_wp_at_cdt [simp]: - "cte_wp_at P p (cdt_update f s) = cte_wp_at P p s" - by (clarsimp simp add: cte_wp_at_cases) - - -lemma obj_at_cdt [simp]: - "obj_at P p (cdt_update f s) = obj_at P p s" - by (clarsimp simp add: obj_at_def) - - -lemma valid_cap_cdt [simp]: - "cdt_update f s \ cap = s \ cap" - apply (cases cap) - apply (simp_all add: valid_cap_def valid_untyped_def split_def - cong: arch_cap.case_cong - split: option.split sum.split) - done +lemmas cte_wp_at_cdt = cdt_update.cte_wp_at_update +lemmas obj_at_cdt = cdt_update.obj_at_update +lemmas valid_cap_cdt = cdt_update.valid_cap_update lemma set_object_at_obj3: @@ -493,9 +479,7 @@ lemma set_ep_refs_of[wp]: apply (simp add: set_endpoint_def set_object_def) apply (rule hoare_seq_ext [OF _ get_object_sp]) apply wp - apply (clarsimp simp: state_refs_of_def - elim!: rsubst[where P=P] - intro!: ext) + apply (fastforce simp: state_refs_of_def elim!: rsubst[where P=P]) done @@ -1096,9 +1080,7 @@ lemma ep_redux_simps: = (set xs \ {EPRecv})" "aep_q_refs_of (case xs of [] \ Structures_A.IdleAEP | y # ys \ Structures_A.WaitingAEP (y # ys)) = (set xs \ {AEPAsync})" - by (fastforce split: list.splits - simp: valid_ep_def valid_aep_def - intro!: ext)+ + by (fastforce split: list.splits simp: valid_ep_def valid_aep_def)+ crunch it[wp]: set_async_ep "\s. P (idle_thread s)" @@ -1608,7 +1590,7 @@ lemma set_object_valid_kernel_mappings: apply wp apply (clarsimp simp: valid_kernel_mappings_def elim!: ranE split: split_if_asm) - apply (fastforce intro: ranI) + apply fastforce done @@ -2108,8 +2090,7 @@ lemma as_user_arch_obj: lemma tcb_cap_valid_caps_of_stateD: - "\P. \ caps_of_state s p = Some cap; valid_objs s \ \ - tcb_cap_valid cap p s" + "\ caps_of_state s p = Some cap; valid_objs s \ \ tcb_cap_valid cap p s" apply (rule cte_wp_tcb_cap_valid) apply (simp add: cte_wp_at_caps_of_state) apply assumption