diff --git a/proof/refine/ARM/ArchAcc_R.thy b/proof/refine/ARM/ArchAcc_R.thy index 7d03834b4..d7afaf1b2 100644 --- a/proof/refine/ARM/ArchAcc_R.thy +++ b/proof/refine/ARM/ArchAcc_R.thy @@ -1108,6 +1108,7 @@ lemma page_table_at_lift: lemmas checkPTAt_corres [corresK] = corres_stateAssert_implied_frame[OF page_table_at_lift, folded checkPTAt_def] + lemma lookup_pt_slot_corres [@lift_corres_args, corres]: "corres (lfr \ op =) (pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs @@ -1118,7 +1119,7 @@ lemma lookup_pt_slot_corres [@lift_corres_args, corres]: (lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)" unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def apply (corressimp simp: pde_relation_aligned_def lookup_failure_map_def - wp: get_pde_wp_valid getPDE_wp corres_rv_defer) + wp: get_pde_wp_valid getPDE_wp) by (auto simp: lookup_failure_map_def obj_at_def) declare in_set_zip_refl[simp] @@ -1184,7 +1185,7 @@ lemma copy_global_mappings_corres [@lift_corres_args, corres]: by (auto intro!: page_directory_pde_atI page_directory_pde_atI' simp: pde_relation_aligned_def corres_protect_def dest: align_entry_add_cong[of globalPD]) - apply wpsimp+ + apply corressimp+ apply (clarsimp simp: valid_arch_state_def obj_at_def dest!:pspace_alignedD) by (auto intro: is_aligned_weaken[of _ 14] simp: valid_arch_state'_def) diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index d64e0ca69..3249d543a 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -555,7 +555,6 @@ lemma getSlotCap_valid: apply (clarsimp simp add: valid_def) done - lemma rab_corres': "\ cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a; bits = length (snd a) \ \ @@ -621,7 +620,6 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (subst cnode_cap_case_if) apply (corressimp search: getSlotCap_corres IH wp: get_cap_wp getSlotCap_valid no_fail_stateAssert - corres_rv_defer simp: locateSlot_conv) apply (simp add: drop_postfix_eq) apply clarsimp @@ -629,30 +627,12 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply (erule valid_CNodeCapE; fastforce) subgoal premises prems for s s' x apply (insert prems) - apply (rule conjI) - apply (clarsimp split: if_splits) - apply safe[1] - apply (clarsimp simp: valid_cap_def) - apply (erule cap_table_at_cte_at) - subgoal by simp - apply (frule (1) cte_wp_valid_cap) - subgoal for cap by (cases cap; simp) - apply (simp add: caps lookup_failure_map_def) - apply (frule guard_mask_shift[where guard=guard]) - apply (intro conjI) - apply fastforce - apply clarsimp - apply (rule conjI) - apply (clarsimp simp add: objBits_simps cte_level_bits_def) - apply (erule (2) valid_CNodeCapE) - apply (erule (3) cte_map_shift') - subgoal by simp - apply (clarsimp simp add: objBits_simps cte_level_bits_def) - apply (rule conjI) - apply (erule (1) cte_map_shift; assumption?) - subgoal by simp - apply (clarsimp simp: cte_level_bits_def) - apply (intro conjI impI allI;clarsimp?) + apply (rule context_conjI) + apply (simp add: guard_mask_shift[OF \to_bl _ = _\, where guard=guard,symmetric]) + apply (simp add: caps lookup_failure_map_def) + apply (rule conjI) + apply (clarsimp split: if_splits) + apply (intro conjI impI allI;clarsimp?) apply (subst \to_bl _ = _\[symmetric]) apply (drule postfix_dropD) apply clarsimp @@ -662,14 +642,26 @@ proof (induct a arbitrary: c' cref' bits rule: resolve_address_bits'.induct) apply simp apply (subst drop_drop [symmetric]) subgoal by simp - apply (erule (1) cte_map_shift; assumption?) - apply clarsimp - subgoal by (simp add: cte_level_bits_def) - apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps) + apply (erule (2) valid_CNodeCapE) + apply (rule cap_table_at_cte_at[OF _ refl]) + apply (simp add: obj_at_def is_cap_table_def well_formed_cnode_n_def) + apply (frule (2) cte_wp_valid_cap) + apply (rule context_conjI) + apply (intro conjI impI allI;clarsimp?) + apply (clarsimp simp add: objBits_simps cte_level_bits_def) + apply (erule (2) valid_CNodeCapE) + apply (erule (3) cte_map_shift') + apply simp + apply (clarsimp simp add: objBits_simps cte_level_bits_def) + apply (erule (1) cte_map_shift; assumption?) + subgoal by simp + apply (clarsimp simp: cte_level_bits_def) + apply (rule conjI) + apply (clarsimp simp: valid_cap_def cap_table_at_gsCNodes isCap_simps) apply (rule and_mask_less_size, simp add: word_bits_def word_size cte_level_bits_def) - apply (clarsimp split: if_splits) - done - done + apply (clarsimp split: if_splits) + done + done } ultimately show ?thesis by fast diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index 92156bbcf..fa22f15d0 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -1082,7 +1082,7 @@ lemma set_ep_corres [corres]: (set_endpoint ptr e) (setEndpoint ptr e')" apply (simp add: set_endpoint_def setEndpoint_def is_ep_def[symmetric]) apply (corres_search search: set_other_obj_corres[where P="\_. True"]) - apply (correswp wp: get_object_ret get_object_wp)+ + apply (corressimp wp: get_object_ret get_object_wp)+ by (clarsimp simp: is_ep obj_at_simps) lemma set_ntfn_corres [corres]: @@ -1091,7 +1091,7 @@ lemma set_ntfn_corres [corres]: (set_notification ptr ae) (setNotification ptr ae')" apply (simp add: set_notification_def setNotification_def is_ntfn_def[symmetric]) apply (corres_search search: set_other_obj_corres[where P="\_. True"]) - apply (correswp wp: get_object_ret get_object_wp)+ + apply (corressimp wp: get_object_ret get_object_wp)+ by (clarsimp simp: is_ntfn obj_at_simps) lemma no_fail_getNotification [wp]: