adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

remove explicit use of corres_rv rules 

This is now handled by the corres method

VER-737
This commit is contained in:
Daniel Matichuk 2017-05-05 11:14:02 +10:00
parent fb6cd81aa8
commit 8c7163457a
3 changed files with 30 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
proof/refine/ARM/ArchAcc_R.thy
View File

@ -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 \<oplus> 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)

58
proof/refine/ARM/CSpace1_R.thy
View File

@ -555,7 +555,6 @@ lemma getSlotCap_valid:
apply (clarsimp simp add: valid_def)
done
lemma rab_corres':
"\<lbrakk> cap_relation (fst a) c'; drop (32-bits) (to_bl cref') = snd a;
bits = length (snd a) \<rbrakk> \<Longrightarrow>
@ -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 \<open>to_bl _ = _\<close>, 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 \<open>to_bl _ = _\<close>[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

4
proof/refine/ARM/KHeap_R.thy
View File

@ -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="\<lambda>_. 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="\<lambda>_. 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]: