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

2015 update for DRefine

This commit is contained in:
Gerwin Klein 2015-05-13 09:52:32 +02:00
parent a979379e3a
commit f6124669fc
16 changed files with 2496 additions and 2650 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/drefine/ADT_DR.thy
View File

@ -132,7 +132,7 @@ lemma dwp_thread_set_idle:
apply (wp)
apply (rule_tac Q = "\<lambda>s. transform s = cs \<and> thread = idle_thread s"
in hoare_vcg_precond_imp)
apply (clarsimp simp:valid_def mem_def set_object_def
apply (clarsimp simp:valid_def set_object_def
put_def get_def return_def bind_def)
apply (clarsimp simp:transform_def transform_current_thread_def transform_objects_def)
apply (assumption)

178
proof/drefine/Arch_DR.thy
View File

@ -389,11 +389,11 @@ proof -
apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
apply simp
apply (drule_tac t="pda ?v" in sym, simp)
apply (drule_tac t="pda v" for v in sym, simp)
apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm del: disjCI)
apply (frule_tac p="Platform.ptrFromPAddr ?v" in pspace_alignedD, simp+)
apply (frule_tac p="Platform.ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule disjI2, rule conjI)
apply (rule_tac x="unat (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)"
in exI)
@ -421,6 +421,7 @@ proof -
apply (simp add: lookup_pt_slot_def liftE_bindE)
apply (rule corres_symb_exec_r[OF _ get_pde_sp get_pde_inv], simp_all)[1]
apply (clarsimp simp add: corres_alternate2 split: ARM_Structs_A.pde.split)
apply (rename_tac word1 set word2)
apply (rule corres_alternate1)
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp select_wp | simp)+
@ -431,11 +432,11 @@ proof -
apply (cut_tac less_kernel_base_mapping_slots[OF kb pd_aligned])
apply (drule_tac x="ucast (lookup_pd_slot pd_ptr vptr && mask pd_bits >> 2)" in bspec)
apply simp
apply (drule_tac t="pda ?v" in sym, simp)
apply (drule_tac t="pda v" for v in sym, simp)
apply (clarsimp simp: obj_at_def a_type_def del: disjCI)
apply (clarsimp split: Structures_A.kernel_object.split_asm split_if_asm
arch_kernel_obj.split_asm del: disjCI)
apply (frule_tac p="Platform.ptrFromPAddr ?v" in pspace_alignedD, simp+)
apply (frule_tac p="Platform.ptrFromPAddr v" for v in pspace_alignedD, simp+)
apply (rule map_includedI)
apply (clarsimp simp: transform_pt_slot_ref_def all_pd_pt_slots_def
opt_object_page_directory[unfolded opt_object_def]
@ -534,7 +535,7 @@ lemma shiftl_mod:
apply (subst shiftl_t2n)
apply (clarsimp simp:unat_word_ariths)
apply (subgoal_tac "2 ^ n * unat x < 2 ^ 32")
apply (clarsimp simp: mod_less)
apply (clarsimp)
apply (subst (asm) word_unat_power)
apply (drule unat_less_helper)
apply (rule_tac y="2^n * 2 ^(32-n)" in less_le_trans)
@ -568,7 +569,6 @@ proof (induct x)
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps
split del: split_if)
apply (clarsimp simp: get_asid_pool_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def
@ -624,7 +624,6 @@ next
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps
bindE_assoc
split del: split_if)
apply (clarsimp simp: get_asid_control_intent_def transform_intent_def
@ -686,7 +685,6 @@ next
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps
split del: split_if)
apply (clarsimp simp: get_page_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def
@ -708,12 +706,12 @@ next
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle label_to_flush_type_def InvocationLabels_H.isPageFlush_def
dest!: a_type_pdD)+
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))"
apply (rule_tac r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv x21 && ~~ mask pd_bits))" for I
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (case_tac r, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
@ -733,7 +731,7 @@ next
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp add: in_monad conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
@ -753,12 +751,12 @@ next
opt_object_page_directory invs_valid_idle
dest!: a_type_pdD)
apply (clarsimp simp: gets_bind_alternative corres_symb_exec_in_gets)
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv b && ~~ mask pd_bits))"
apply (rule_tac r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv b && ~~ mask pd_bits))" for I
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (case_tac r, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply (clarsimp simp add: liftE_bindE[symmetric])
@ -778,7 +776,7 @@ next
apply (wp | simp)+
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp)+
apply (clarsimp simp add: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp add: in_monad conj_disj_distribR[symmetric])
apply (simp add: conj_disj_distribR cong: conj_cong)
apply (simp add: arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def update_cap_rights_def
@ -800,7 +798,7 @@ next
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
@ -811,7 +809,7 @@ next
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
@ -822,18 +820,18 @@ next
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
apply (rule corres_from_rdonly)
apply (wp, clarsimp)
apply ( simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (simp only: Let_unfold, wp, clarsimp, rule valid_validE, wp whenE_inv, clarsimp, wp)
apply (assumption)
apply (rule validE_cases_valid, rule hoare_pre)
apply (wp | simp add: Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_inv_def)+
apply (clarsimp simp: in_monad in_alternative conj_disj_distribR[symmetric])
apply (clarsimp simp: in_monad conj_disj_distribR[symmetric])
apply (safe)
apply blast
apply (metis flush.exhaust)
@ -847,7 +845,6 @@ next
thus ?case
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps
split del: split_if)
apply (clarsimp simp: get_page_table_intent_def transform_intent_def
option_map_Some_eq2 throw_opt_def cdl_get_pt_mapped_addr_def
@ -855,26 +852,19 @@ next
transform_intent_page_table_map_def
split del: split_if
split: invocation_label.split_asm list.split_asm)
apply (simp add: transform_cap_simps throw_on_none_def transform_cap_list_def
apply (simp add: throw_on_none_def transform_cap_list_def
get_index_def split_beta alternative_refl
transform_mapping_def corres_whenE_throwError_split_rhs corres_alternate2
split: cap.split arch_cap.split option.split cdl_frame_cap_type.splits)
apply (clarsimp simp: dc_def[symmetric] liftE_bindE
gets_the_def bind_assoc transform_mapping_def
corres_symb_exec_in_gets gets_bind_alternative)
(* apply (rule_tac F="v \<noteq> None" in corres_req)
apply (clarsimp simp: neq_Nil_conv valid_cap_simps obj_at_def
opt_object_page_directory invs_valid_idle
dest!: a_type_pdD)
apply (clarsimp simp: gets_bind_alternative corres_symb_exec_in_gets
assert_opt_def)
*)
apply (rule_tac r'=dc and P'="?I" and Q'="\<lambda>rv. ?I and (\<exists>\<rhd> (lookup_pd_slot rv ab && ~~ mask pd_bits))"
in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule_tac r'=dc and P'="I" and Q'="\<lambda>rv. I and (\<exists>\<rhd> (lookup_pd_slot rv ab && ~~ mask pd_bits))"
for I in corres_alternative_throw_splitE[OF _ _ returnOk_wp[where x="()"], simplified])
apply (rule corres_from_rdonly, simp_all)[1]
apply (wp | simp)+
apply (rule hoare_strengthen_post, rule hoare_post_taut)
apply (case_tac r, auto simp add: in_monad in_alternative)[1]
apply (case_tac r, auto simp add: in_monad)[1]
apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2
check_vp_alignment_def unlessE_whenE)
apply clarsimp
@ -918,7 +908,7 @@ next
(* abandon hope, all who enter here *)
apply (simp add: Decode_D.decode_invocation_def
decode_invocation_def arch_decode_invocation_def
transform_cap_simps get_page_directory_intent_def transform_intent_def
get_page_directory_intent_def transform_intent_def
isPDFlush_def
split del: split_if)
apply (clarsimp simp: get_page_directory_intent_def transform_intent_def
@ -938,11 +928,11 @@ next
apply (clarsimp simp: whenE_def)
apply (intro conjI impI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def
Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric]
in_monad conj_disj_distribR[symmetric]
split: option.splits | rule impI conjI)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp split: option.splits, safe)
@ -951,36 +941,36 @@ next
apply (intro conjI impI)
apply (wp resolve_vaddr_inv
| simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def
translate_arch_invocation_def transform_page_dir_inv_def in_monad in_alternative
translate_arch_invocation_def in_monad
conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
@ -991,40 +981,40 @@ next
apply (intro conjI impI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (wp resolve_vaddr_inv | clarsimp simp: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (clarsimp simp: whenE_def)
apply (intro conjI impI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (clarsimp split: ArchInvocation_A.flush_type.splits)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
@ -1033,60 +1023,60 @@ next
apply (clarsimp simp: whenE_def)
apply (intro conjI impI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: flush_type_map_def transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (clarsimp split: ArchInvocation_A.flush_type.splits)
apply (metis flush.exhaust)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (metis flush.exhaust)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
apply (rule corres_from_rdonly)
apply (wp valid_validE[OF whenE_inv] | clarsimp split: option.splits | safe)+
apply (rule validE_cases_valid, rule hoare_pre, wp)
apply (clarsimp simp: whenE_def)
apply (rule_tac x="Inl undefined" in exI)
apply (wp resolve_vaddr_inv | simp add: transform_page_dir_inv_def Let_unfold arch_invocation_relation_def translate_arch_invocation_def
transform_page_dir_inv_def in_monad in_alternative conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
in_monad conj_disj_distribR[symmetric] split: option.splits | rule impI conjI allI)+
done
qed
@ -1234,14 +1224,10 @@ lemma diminished_PageTable [simp]:
apply (rule ext)
apply (case_tac c,
simp_all add: diminished_def cap_rights_update_def acap_rights_update_def mask_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, auto)
done
lemma cleanCacheRange_PoU_underlying_memory[wp]:
" \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCacheRange_PoU p f g \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>"
apply (clarsimp simp: cleanCacheRange_PoU_def, wp)
done
lemma invoke_page_table_corres:
"transform_page_table_inv ptinv' = Some ptinv \<Longrightarrow>
dcorres dc \<top> (valid_pti ptinv' and invs and valid_etcbs)
@ -1250,6 +1236,7 @@ lemma invoke_page_table_corres:
apply (clarsimp simp: transform_page_table_inv_def
split: ArchInvocation_A.page_table_invocation.split_asm
split_if_asm)
apply (rename_tac word oref attribs)
apply (clarsimp simp: is_pt_cap_def valid_pti_def make_arch_duplicate_def)
apply (rule stronger_corres_guard_imp)
apply (rule corres_split [OF _ set_cap_corres])
@ -1354,6 +1341,7 @@ lemma diminished_page_is_page:
\<Longrightarrow> \<exists>rs'. c = cap.ArchObjectCap (arch_cap.PageCap x rs' sz mp)"
apply (case_tac c,
simp_all add:diminished_def cap_rights_update_def acap_rights_update_def mask_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, (clarsimp simp:validate_vm_rights_def)+)
done
@ -1571,34 +1559,43 @@ lemma pte_check_if_mapped_corres:
"dcorres dc \<top> \<top> (return a) (pte_check_if_mapped pte)"
apply (clarsimp simp add: pte_check_if_mapped_def get_master_pte_def get_pte_def get_pt_def bind_assoc in_monad get_object_def corres_underlying_def)
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (clarsimp split: ARM_Structs_A.pte.splits)
apply (simp_all add: get_pte_def get_pt_def get_object_def in_monad bind_assoc split: kernel_object.splits arch_kernel_obj.splits)
apply clarsimp
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (auto simp: in_monad)[2]
apply clarsimp
apply (case_tac y, simp_all add: in_monad, case_tac arch_kernel_obj, simp_all add: in_monad, auto simp: in_monad)
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad, auto simp: in_monad)
done
lemma pde_check_if_mapped_corres:
"dcorres dc \<top> \<top> (return a) (pde_check_if_mapped pde)"
apply (clarsimp simp add: pde_check_if_mapped_def get_master_pde_def get_pde_def get_pd_def bind_assoc in_monad get_object_def corres_underlying_def)
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (clarsimp split: ARM_Structs_A.pde.splits)
apply (simp_all add: get_pde_def get_pd_def get_object_def in_monad bind_assoc)
apply clarsimp
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (auto simp: in_monad)[1]
apply clarsimp
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad)
apply (auto simp: in_monad)[1]
apply clarsimp
apply (case_tac y, simp_all add: in_monad, case_tac arch_kernel_obj, simp_all add: in_monad, auto simp: in_monad)
apply (case_tac y, simp_all add: in_monad)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all add: in_monad, auto simp: in_monad)
done
lemma if_invalidate_equiv_return:
@ -1609,7 +1606,6 @@ lemma if_invalidate_equiv_return:
apply clarsimp
done
lemma ct_active_not_idle_etc:
"\<lbrakk> invs s; ct_active s \<rbrakk> \<Longrightarrow> not_idle_thread (cur_thread s) s"
apply (simp add: not_idle_thread_def ct_in_state_def)
@ -1625,6 +1621,7 @@ lemma invoke_page_corres:
apply (clarsimp simp:invoke_page_def)
apply (case_tac ip')
apply (simp_all add:perform_page_invocation_def)
apply (rename_tac word cap prod sum)
apply (simp_all add:perform_page_invocation_def transform_page_inv_def)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:valid_page_inv_def)
@ -1676,6 +1673,7 @@ lemma invoke_page_corres:
apply (frule_tac v = b in valid_idle_has_null_cap,simp+)
apply (clarsimp simp:is_arch_update_def is_arch_cap_def cap_master_cap_def split:cap.split_asm)
-- "PageRemap"
apply (rename_tac sum)
apply (case_tac sum)
apply (clarsimp simp: mapM_singleton mapM_x_mapM)
apply (simp add:page_inv_duplicates_valid_def
@ -1725,42 +1723,6 @@ lemma invoke_page_corres:
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def
dest!:diminished_page_is_page)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
(*
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF _ store_pte_set_cap_corres])
apply (rule corres_dummy_return_l)
apply (rule_tac corres_split[OF _ dcorres_store_invalid_pte_tail_large_page])
apply (rule wp_to_dcorres[where Q=\<top>])
apply (wp do_machine_op_wp mapM_wp' set_cap_idle
store_pte_page_inv_entries_safe set_cap_page_inv_entries_safe
| clarsimp simp:cleanCacheRange_PoU_def)+
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:mapM_singleton mapM_x_mapM valid_page_inv_def)
apply (rule corres_guard_imp)
apply (rule corres_dummy_return_l)
apply (rule corres_split[OF _ store_pde_set_cap_corres])
apply (rule corres_dummy_return_l)
apply (rule_tac corres_split[OF _ dcorres_store_invalid_pde_tail_super_section])
apply (rule wp_to_dcorres[where Q=\<top>])
apply (wp do_machine_op_wp mapM_wp' set_cap_idle
set_cap_page_inv_entries_safe store_pde_page_inv_entries_safe
| clarsimp simp:cleanCacheRange_PoU_def valid_slots_def
)+
apply (clarsimp simp:invs_def valid_state_def
cte_wp_at_caps_of_state page_inv_duplicates_valid_def)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: valid_page_inv_def liftM_def
transform_mapping_def
split:arch_cap.splits option.splits)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at (op = x) (a,b) s \<and> s = s'" in set_cap_corres_stronger)
apply clarsimp
apply (drule cte_wp_at_eqD2, simp)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def
dest!:diminished_page_is_page)
apply (wp get_cap_cte_wp_at_rv | clarsimp)+
*)
apply (clarsimp simp:cte_wp_at_def is_arch_diminished_def is_arch_cap_def is_pt_cap_def
dest!:diminished_page_is_page)
apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def)
@ -1940,7 +1902,7 @@ proof -
apply simp
apply (rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top>]])
apply simp
apply (clarsimp simp:conj_ac
apply (clarsimp simp:conj_comms
| strengthen impI[OF invs_valid_pspace] impI[OF invs_valid_idle])+
apply (rule_tac P = "pcap = cap.UntypedCap frame pageBits idx" in hoare_gen_asm)
apply (wp max_index_upd_invs_simple set_cap_idle
@ -2077,7 +2039,7 @@ lemma invoke_arch_corres:
(arch_perform_invocation arch_invok)"
apply (clarsimp simp: arch_perform_invocation_def valid_arch_inv_def)
apply (case_tac arch_invok)
apply (simp_all add:arch_invocation_relation_def translate_arch_invocation_def arch_invocation_relation_def)
apply (simp_all add:arch_invocation_relation_def translate_arch_invocation_def)
apply (clarsimp simp:liftE_def bind_assoc)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ invoke_page_table_corres])

110
proof/drefine/CNode_DR.thy
View File

@ -44,6 +44,7 @@ lemma ex_cte_cap_to_not_idle:
apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state)
apply (drule(1) valid_global_refsD2)
apply (case_tac cap, simp_all add: cap_range_def global_refs_def)
apply (rename_tac word)
apply (clarsimp simp: valid_idle_def valid_irq_node_def st_tcb_at_def
obj_at_def is_cap_table_def)
apply (drule_tac x=word in spec, simp)
@ -58,8 +59,7 @@ definition
lemma option_return_modify_modify:
"case_option (return ()) (\<lambda>x. modify (f x))
= (\<lambda>opt. modify (case_option id f opt))"
apply (rule ext)
by (simp split: option.split add: modify_id_return)
by (auto split: option.split simp: modify_id_return)
lemma update_cdt_modify:
"update_cdt f = modify (cdt_update f)"
@ -90,7 +90,7 @@ lemma dcorres_set_untyped_cap_as_full:
(CSpace_D.set_untyped_cap_as_full (transform_cap src_cap) (transform_cap cap) (transform_cslot_ptr src))
(CSpace_A.set_untyped_cap_as_full src_cap cap src)"
apply (simp add:set_untyped_cap_as_full_def CSpace_D.set_untyped_cap_as_full_def
split del:if_splits)
split del:split_if)
apply (case_tac "is_untyped_cap src_cap \<and> is_untyped_cap cap")
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp)
@ -106,14 +106,10 @@ lemma dcorres_set_untyped_cap_as_full:
apply (simp add:valid_cap_def word_bits_def cap_aligned_def)
apply simp
apply simp
apply (rule_tac F = "is_untyped_cap src_cap
\<and> is_untyped_cap cap"
in corres_gen_asm)
apply (rule_tac F = "is_untyped_cap src_cap \<and> is_untyped_cap cap" in corres_gen_asm)
apply (clarsimp dest!:is_untyped_cap_eqD)
apply (rule set_cap_corres)
apply (clarsimp simp:transform_cap_def
free_range_of_untyped_def cap_aligned_def
max_free_index_def
apply (clarsimp simp:transform_cap_def free_range_of_untyped_def cap_aligned_def max_free_index_def
dest!:is_untyped_cap_eqD)
apply (cut_tac sz = sz in p2_less_minus)
apply simp
@ -195,20 +191,19 @@ lemma insert_cap_sibling_corres:
apply (clarsimp simp:gets_fold_into_modify dc_def[symmetric]
option_return_modify_modify modify_modify bind_assoc
cong:option.case_cong)
apply (rule_tac P=\<top> and P'="(\<lambda>s. \<not> should_be_parent_of src_capa (is_original_cap s src) cap ?orig')
apply (rule_tac P=\<top> and P'="(\<lambda>s. \<not> should_be_parent_of src_capa (is_original_cap s src) cap orig')
and cte_at src and cte_at sibling
and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))
and (\<lambda>s. cdt s sibling = None)"
and (\<lambda>s. cdt s sibling = None)" for orig'
in corres_modify)
apply (clarsimp split del: if_splits)
apply (clarsimp split del: split_if)
apply (subst if_not_P, assumption)+
apply (clarsimp simp: opt_parent_def transform_def
transform_objects_def transform_cdt_def
transform_current_thread_def
transform_asid_table_def
split: option.split)
apply (clarsimp simp: fun_upd_def[symmetric]
cong:if_cong)
apply (clarsimp simp: fun_upd_def[symmetric] cong:if_cong)
apply (subgoal_tac "inj_on transform_cslot_ptr ({src, sibling} \<union> dom (cdt s') \<union> ran (cdt s'))")
apply (subst map_lift_over_f_eq map_lift_over_upd,
erule subset_inj_on, fastforce)+
@ -224,7 +219,7 @@ lemma insert_cap_sibling_corres:
apply ((wp set_cap_caps_of_state2 get_cap_wp static_imp_wp
| simp add: swp_def cte_wp_at_caps_of_state)+)
apply (wp set_cap_idle |
simp add:set_untyped_cap_as_full_def split del:if_splits)+
simp add:set_untyped_cap_as_full_def split del: split_if)+
apply (rule_tac Q = "\<lambda>r s. cdt s sibling = None
\<and> \<not> should_be_parent_of src_capa (is_original_cap s sibling) cap (cap_insert_dest_original cap src_capa)
\<and> mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)"
@ -236,7 +231,7 @@ lemma insert_cap_sibling_corres:
apply fastforce
apply (wp get_cap_wp set_cap_idle static_imp_wp
| simp add:set_untyped_cap_as_full_def
split del:if_splits)+
split del: split_if)+
apply (rule_tac Q = "\<lambda>r s. cdt s sibling = None
\<and> (\<exists>cap. caps_of_state s src = Some cap)
\<and> \<not> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)
@ -288,17 +283,16 @@ lemma insert_cap_child_corres:
apply (rule corres_split[OF _ dcorres_set_untyped_cap_as_full])
apply (rule corres_split[OF _ set_cap_corres[OF refl refl]])
apply (rule dcorres_set_parent_helper)
apply (rule_tac P=\<top> and P'="(\<lambda>s. should_be_parent_of src_capa (?orig s) cap ?orig')
apply (rule_tac P=\<top> and P'="(\<lambda>s. should_be_parent_of src_capa (orig s) cap orig')
and cte_at src and cte_at child
and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))"
and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s))" for orig orig'
in corres_modify)
apply (clarsimp split del: if_splits)
apply (clarsimp split del: split_if)
apply (subst if_P, assumption)+
apply (clarsimp simp: opt_parent_def transform_def transform_asid_table_def
transform_objects_def transform_cdt_def
transform_current_thread_def)
apply (clarsimp simp: fun_upd_def[symmetric]
cong:if_cong)
apply (clarsimp simp: fun_upd_def[symmetric] cong:if_cong)
apply (subgoal_tac "inj_on transform_cslot_ptr ({src, child} \<union> dom (cdt s') \<union> ran (cdt s'))")
apply (subst map_lift_over_f_eq map_lift_over_upd,
erule subset_inj_on, fastforce)+
@ -309,7 +303,7 @@ lemma insert_cap_child_corres:
apply (wp set_cap_caps_of_state2 get_cap_wp static_imp_wp
| simp add: swp_def cte_wp_at_caps_of_state)+
apply (wp set_cap_idle |
simp add:set_untyped_cap_as_full_def split del:if_splits)+
simp add:set_untyped_cap_as_full_def split del:split_if)+
apply (rule_tac Q = "\<lambda>r s. not_idle_thread (fst child) s
\<and> should_be_parent_of src_capa (is_original_cap s child) cap (cap_insert_dest_original cap src_capa)
\<and> mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)"
@ -318,7 +312,7 @@ lemma insert_cap_child_corres:
apply (clarsimp simp:mdb_cte_at_def cte_wp_at_caps_of_state)
apply fastforce
apply (wp get_cap_wp set_cap_idle static_imp_wp
| simp split del:if_splits add:set_untyped_cap_as_full_def)+
| simp split del:split_if add:set_untyped_cap_as_full_def)+
apply (rule_tac Q = "\<lambda>r s. not_idle_thread (fst child) s
\<and> (\<exists>cap. caps_of_state s src = Some cap)
\<and> should_be_parent_of src_capa (is_original_cap s src) cap (cap_insert_dest_original cap src_capa)
@ -506,6 +500,7 @@ lemma cap_null_reply_case_If:
else h)"
by (simp add: is_reply_cap_def is_master_reply_cap_def split: cap.split)
(* FIXME: move *)
lemma corres_if_rhs2:
"\<lbrakk> G \<Longrightarrow> corres_underlying sr nf rvr P Q a b;
\<not> G \<Longrightarrow> corres_underlying sr nf rvr P' Q' a c \<rbrakk>
@ -1126,6 +1121,7 @@ lemma set_get_set_asid_pool:
apply (simp add: get_asid_pool_def set_asid_pool_def get_object_def bind_assoc exec_gets)
apply (case_tac "kheap xa a", simp_all)
apply (case_tac aa, simp_all)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all)
apply (simp add:set_object_def exec_gets bind_assoc exec_get exec_put)
apply (simp add: put_def)
@ -1174,6 +1170,7 @@ lemma get_set_asid_pool:
apply (simp add: get_asid_pool_def set_asid_pool_def get_object_def bind_assoc exec_gets)
apply (case_tac "kheap xa a", simp_all)
apply (case_tac aa, simp_all)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj, simp_all)
apply (simp add:exec_gets)
done
@ -1564,7 +1561,7 @@ ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
apply (frule(1) arch_obj_not_idle)
apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
apply (rule ext)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def
apply (clarsimp simp: transform_page_directory_contents_def unat_map_def
kernel_pde_mask_def ucast_nat_def transform_pde_def
split: if_splits ARM_Structs_A.pte.split_asm)
apply (clarsimp simp:)+
@ -1579,8 +1576,9 @@ ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
apply clarsimp
apply (clarsimp simp:KHeap_D.set_cap_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:update_slots_def assert_opt_def opt_cap_def slots_of_def opt_object_page_directory has_slots_def
object_slots_def split:option.splits)
apply (clarsimp simp:update_slots_def assert_opt_def opt_cap_def slots_of_def
opt_object_page_directory has_slots_def object_slots_def
split:option.splits)
apply (clarsimp simp:KHeap_D.set_object_def set_object_def simpler_modify_def get_def put_def bind_def return_def)
apply (clarsimp simp:corres_underlying_def transform_def cur_tcb_def tcb_at_def dest!:get_tcb_SomeD)
apply (clarsimp simp:transform_current_thread_def)
@ -1589,7 +1587,7 @@ ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots
apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
apply (subst transform_page_directory_contents_upd[symmetric])
apply (clarsimp simp:transform_pde_def)+
done
done
lemma dcorres_empty_pte_slot:
" dcorres dc \<top> (valid_idle and cur_tcb and (\<lambda>s. mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s)))
@ -1628,8 +1626,8 @@ lemma dcorres_empty_pte_slot:
apply clarsimp
apply (clarsimp simp:KHeap_D.set_cap_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:update_slots_def assert_opt_def opt_cap_def slots_of_def opt_object_page_table has_slots_def
object_slots_def split:option.splits)
apply (clarsimp simp:update_slots_def assert_opt_def opt_cap_def slots_of_def opt_object_page_table
has_slots_def object_slots_def split:option.splits)
apply (clarsimp simp:KHeap_D.set_object_def set_object_def simpler_modify_def get_def put_def bind_def return_def)
apply (clarsimp simp:corres_underlying_def transform_def cur_tcb_def tcb_at_def dest!:get_tcb_SomeD)
apply (clarsimp simp:transform_current_thread_def)
@ -1638,7 +1636,7 @@ lemma dcorres_empty_pte_slot:
apply (clarsimp simp: not_idle_thread_def transform_objects_def restrict_map_def map_add_def)
apply (subst transform_page_table_contents_upd[symmetric])
apply (clarsimp simp:transform_pte_def)
done
done
lemma store_pte_ct:
@ -1649,7 +1647,7 @@ lemma store_pte_ct:
apply wp
apply (rule_tac Q = "\<lambda>r s. P (cur_thread s)" in hoare_strengthen_post)
apply (wp|clarsimp)+
done
done
lemma invalidate_tlb_by_asid_dwp:
@ -1661,15 +1659,11 @@ lemma invalidate_tlb_by_asid_dwp:
apply (rule_tac Q = "\<lambda>r s. transform s = cs" in hoare_strengthen_post)
apply (simp add:load_hw_asid_def)
apply (wp|clarsimp)+
done
done
lemma page_table_mapped_dwp:
"\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> page_table_mapped aa ba w \<lbrace>\<lambda>a b. transform b = cs\<rbrace>"
apply (simp add:page_table_mapped_def)
apply (wp|wpc)+
apply (rule_tac Q ="\<lambda>r x. transform x = cs" in hoare_strengthen_post)
apply (wp|clarsimp)+
done
by (rule page_table_mapped_inv)
lemma store_pde_set_cap_corres:
"\<lbrakk>ucast (ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots \<rbrakk> \<Longrightarrow>
@ -1683,15 +1677,14 @@ lemma store_pde_set_cap_corres:
apply (frule arch_obj_not_idle)
apply simp
apply (simp add:not_idle_thread_def)
apply (clarsimp simp:set_object_def return_def get_def put_def corres_underlying_def
bind_def )
apply (clarsimp simp:set_object_def return_def get_def put_def corres_underlying_def bind_def)
apply (simp add:transform_def transform_current_thread_def)
apply (rule ext)
apply (clarsimp simp:transform_objects_def restrict_map_def map_add_def)
apply (rule ext)
apply (clarsimp simp:transform_page_directory_contents_def unat_map_def kernel_pde_mask_def )
apply (simp add:kernel_mapping_slots_def)
done
done
lemma copy_global_mappings_dwp:
"is_aligned word pd_bits\<Longrightarrow> \<lbrace>\<lambda>ps. valid_idle (ps :: det_state) \<and> transform ps = cs\<rbrace> copy_global_mappings word \<lbrace>\<lambda>r s. transform s = cs\<rbrace>"
@ -1718,7 +1711,7 @@ lemma copy_global_mappings_dwp:
apply (simp add:word_size,unat_arith)
apply (simp add:word_size)+
apply (wp|clarsimp)+
done
done
lemma opt_cap_pd_not_None:
"\<lbrakk>ko_at (ArchObj (arch_kernel_obj.PageDirectory ptx)) w s'; valid_idle s';ba<4096\<rbrakk>
@ -1743,7 +1736,7 @@ lemma transform_pde_NullCap:
apply (subst ucast_le_migrate[symmetric])
apply (simp_all add:word_size)
apply unat_arith
done
done
lemma dcorres_dummy_empty_slot_pd:
"\<lbrakk>0xF00 \<le> unat xa ; unat xa < 0x1000\<rbrakk> \<Longrightarrow> dcorres dc \<top> (valid_idle and page_directory_at w)
@ -1760,7 +1753,7 @@ lemma dcorres_dummy_empty_slot_pd:
apply (drule transform_pde_NullCap)
apply (simp add:ucast_nat_def)+
apply fastforce
done
done
lemma dcorres_dummy_empty_slot_pd_mapM_x:
"\<forall>x\<in> set ls. 0xF00 \<le> unat x \<and> unat x < 4096
@ -2223,7 +2216,7 @@ definition
where
"object_at P obj_id s \<equiv> \<exists>object. cdl_objects s obj_id = Some object \<and> P object"
(* MOVE *)
(* FIXME: MOVE *)
definition
"transform_cnode sz cn \<equiv>
if sz = 0
@ -2276,7 +2269,7 @@ lemma arch_recycle_cap_dcorres:
shows "dcorres (\<lambda>x. (\<lambda>cap'. x = transform_cap cap') \<circ> cap.ArchObjectCap)
\<top> (invs and cte_wp_at (op = (cap.ArchObjectCap arch_cap)) slot and valid_pdpt_objs and valid_etcbs)
(CSpace_D.recycle_cap is_final' (transform_cap (cap.ArchObjectCap arch_cap))) (arch_recycle_cap is_final' arch_cap)"
apply (cases arch_cap, simp_all del: transform_cap_simps)
apply (cases arch_cap; simp only:)
-- "asid pool"
apply (rule corres_guard_imp)
apply (rule dcorres_recycle_asid_pool_caps [where slot = slot, OF refl], simp, simp)
@ -2294,6 +2287,7 @@ lemma recycle_cap_idle_thread: "\<lbrace> \<lambda>s. P (idle_thread s) \<rbrace
unfolding recycle_cap_def
apply (case_tac b)
apply (wp | simp)+
apply (rename_tac option nat)
apply (case_tac option)
apply (wp get_thread_state_it dxo_wp_weak | rule hoare_drop_imps | simp)+
done
@ -2304,14 +2298,14 @@ lemma recycle_cap_corres_pre:
(CSpace_D.recycle_cap x (transform_cap cap)) (CSpace_A.recycle_cap x cap)"
apply (case_tac cap)
apply (rule corres_guard_imp)
prefer 14 (* Using an explict goal number is so incredibly brittle *)
prefer 14 -- Recycle
apply (simp add:recycle_cap_def)
apply (rule corres_guard_imp)
apply (rule arch_recycle_cap_dcorres)
apply (wp recycle_cap_invs [where slot = "(a, b)"] recycle_cap_idle_thread
apply (wp recycle_cap_invs recycle_cap_idle_thread
| strengthen valid_idle_invs_strg | fastforce)+
apply (simp_all add:recycle_cap_def CSpace_D.recycle_cap_def
split del:if_splits)
split del: split_if)
apply (rule corres_guard_imp[OF corres_free_fail [where P = \<top> and P' = \<top>]],simp+)
apply (rule corres_guard_imp)
apply (rule corres_split [where R = "\<top>\<top>" and R' = "\<top>\<top>"])
@ -2320,6 +2314,7 @@ lemma recycle_cap_corres_pre:
apply simp
apply (rule dcorres_ep_cancel_badge_sends)
apply (wp|clarsimp)+
apply (rename_tac option nat)
apply (case_tac option,simp+)
apply (simp add: get_thread_state_def)
apply (rule corres_guard_imp)
@ -2338,8 +2333,7 @@ lemma recycle_cap_corres_pre:
apply (rule conjI,simp)
apply (drule cte_wp_valid_cap)
apply fastforce
apply (clarsimp simp:get_cnode'_def
valid_cap_def obj_at_def split:Structures_A.kernel_object.splits)
apply (clarsimp simp:get_cnode'_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits)
apply (clarsimp simp:transform_cnode_def is_cap_table_def invs_valid_idle cnode_size_bits_def)
done
@ -2667,6 +2661,7 @@ lemma derive_cap_dummy:
apply simp
apply (simp add: liftME_def)
apply (clarsimp simp: arch_derive_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all split: option.splits)
apply (simp_all add: returnOk_def throwError_def)
done
@ -2706,7 +2701,7 @@ lemma dcorres_ensure_no_children:
apply (drule (1) wf_cs_nD)+
apply simp
apply clarsimp
apply (thin_tac "?P \<or> ?Q")
apply (thin_tac "P \<or> Q" for P Q)
apply (clarsimp simp: tcb_cap_cases_def tcb_cnode_index_def split: if_splits)
apply simp
done
@ -2731,6 +2726,7 @@ lemma derive_cap_dcorres:
apply simp
apply fastforce
apply (simp add: arch_derive_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: dcorres_returnOk')
apply (rule dcorres_returnOk')
apply (clarsimp simp:transform_mapping_def)
@ -2766,8 +2762,7 @@ lemma dcorres_update_cap_data:
apply (unfold CSpace_D.update_cap_data_def)
apply (simp add:gets_the_def gets_def bind_assoc)
apply (case_tac cap')
apply (simp_all add:transform_cap_def update_cap_data_def
CSpace_A.update_cap_data_def is_cap_simps Let_def)
apply (simp_all add:transform_cap_def update_cap_data_def is_cap_simps Let_def)
apply (simp add: CSpace_D.badge_update_def update_cap_badge_def
Structures_A.badge_update_def Types_D.badge_bits_def)
apply (simp add: CSpace_D.badge_update_def update_cap_badge_def
@ -2777,6 +2772,7 @@ lemma dcorres_update_cap_data:
apply (simp add:of_drop_to_bl)
apply (simp add:mask_twice)
apply (clarsimp simp:word_size opt_object_def Types_D.word_bits_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all add: arch_update_cap_data_def)
done
@ -2792,8 +2788,7 @@ lemma dcorres_update_cap_data_bind:
apply (rule dcorres_update_cap_data, simp)
apply simp
apply assumption
apply (clarsimp simp:
CSpace_D.update_cap_data_def)
apply (clarsimp simp: CSpace_D.update_cap_data_def)
apply (wp | wpc)+
apply simp
apply simp
@ -2891,7 +2886,7 @@ lemma decode_cnode_corres:
(invs and valid_cap cap' and (\<lambda>s. \<forall>e\<in>set excaps'. valid_cap (fst e) s) and valid_etcbs)
(CNode_D.decode_cnode_invocation cap slot excaps ui)
(Decode_A.decode_cnode_invocation label' args' cap' (map fst excaps'))"
apply (drule_tac s="Some ?x" in sym)
apply (drule_tac s="Some x" for x in sym)
apply (rule_tac label=label' and args=args' and exs="map fst excaps'"
in decode_cnode_cases2)
apply (clarsimp simp: transform_intent_def unlessE_whenE
@ -3251,7 +3246,6 @@ lemma decode_cnode_corres:
apply (case_tac list)
apply clarsimp
apply (simp add: transform_intent_def upto_enum_def toEnum_def fromEnum_def
enum_invocation_label
enum_invocation_label transform_cnode_index_and_depth_def
transform_intent_cnode_copy_def
transform_intent_cnode_mint_def
@ -3312,6 +3306,6 @@ lemma decode_cnode_label_not_match:
apply clarsimp
apply wp
apply (clarsimp simp: upto_enum_def fromEnum_def toEnum_def enum_invocation_label)
done
done
end

130
proof/drefine/Finalise_DR.thy
View File

@ -12,7 +12,6 @@ theory Finalise_DR
imports
KHeap_DR
"../invariant-abstract/PDPTEntries_AI"
"../../lib/Apply_Trace"
begin
declare dxo_wp_weak[wp del]
@ -201,7 +200,7 @@ lemma delete_cap_one_shrink_descendants:
apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s)
\<and> mdb_cte_at (swp (cte_wp_at (op\<noteq> cap.NullCap)) s) (cdt s)"
in hoare_vcg_precond_imp)
apply (rule_tac Q ="\<lambda>r s. (?Q r s) \<and> (mdb_cte_at (swp (cte_wp_at (op\<noteq> cap.NullCap)) s) (cdt s))" in hoare_strengthen_post)
apply (rule_tac Q ="\<lambda>r s. Q r s \<and> (mdb_cte_at (swp (cte_wp_at (op\<noteq> cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post)
apply (rule hoare_vcg_conj_lift)
apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p])
apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at (op\<noteq>cap.NullCap)) s ) xa" in hoare_vcg_precond_imp)
@ -286,14 +285,14 @@ lemma caps_of_state_transform_opt_cap_no_idle:
transform_def object_slots_def transform_objects_def
valid_irq_node_def obj_at_def is_cap_table_def
transform_tcb_def tcb_slot_defs
tcb_pending_op_slot_def tcb_cap_cases_def
bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
tcb_cap_cases_def bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
split: split_if_asm option.splits)
done
lemma transform_cap_Null [simp]:
"(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)"
apply (cases cap, simp_all)
apply (rename_tac arch_cap)
apply (case_tac arch_cap, simp_all)
done
@ -380,7 +379,7 @@ lemma finalise_ipc_cancel:
apply clarsimp
apply (rule corres_dummy_return_pr)
apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary])
apply (simp add:K_bind_def when_def dc_def[symmetric])
apply (simp add: when_def dc_def[symmetric])
apply (rule set_thread_state_corres)
apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset | clarsimp simp:not_idle_thread_def)+
apply (simp add:get_blocking_ipc_endpoint_def | wp)+
@ -703,7 +702,7 @@ lemma dcorres_delete_asid_pool:
apply (rule conjI)
prefer 2
apply (clarsimp, rule corres_alternate2)
apply (clarsimp simp: corres_return)
apply (clarsimp)
apply clarsimp
apply (rule corres_alternate1)
apply (rule dcorres_absorb_get_l)
@ -1317,9 +1316,9 @@ lemma page_directory_address_eq:
"\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits"
apply (drule large_frame_range_helper)
using mask_lower_twice[where m = 14 and n = 6 and x= ptr,symmetric]
apply (clarsimp simp:pd_bits_def pageBits_def pageBits_def)
apply (clarsimp simp:pd_bits_def pageBits_def)
using mask_lower_twice[where m = 14 and n = 6 and x= "ptr+t",symmetric]
apply (clarsimp simp:pd_bits_def pageBits_def pageBits_def)
apply (clarsimp simp:pd_bits_def pageBits_def)
apply (subgoal_tac "(ptr && ~~ mask 6) = (ptr + t && ~~ mask 6)")
apply simp
apply (frule is_aligned_neg_mask_eq)
@ -1333,9 +1332,9 @@ lemma page_table_address_eq:
"\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits"
apply (drule large_frame_range_helper)
using mask_lower_twice[where m = 10 and n = 6 and x= ptr,symmetric]
apply (clarsimp simp:pt_bits_def pageBits_def pageBits_def)
apply (clarsimp simp:pt_bits_def pageBits_def)
using mask_lower_twice[where m = 10 and n = 6 and x= "ptr+t",symmetric]
apply (clarsimp simp:pt_bits_def pageBits_def pageBits_def)
apply (clarsimp simp:pt_bits_def pageBits_def)
apply (subgoal_tac "(ptr && ~~ mask 6) = (ptr + t && ~~ mask 6)")
apply simp
apply (frule is_aligned_neg_mask_eq)
@ -1563,7 +1562,7 @@ lemma dcorres_store_invalid_pde_super_section:
and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
(delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)))
(store_pde ptr ARM_Structs_A.pde.InvalidPDE)"
apply (simp add:K_def)
apply simp
apply (rule corres_gen_asm2)
apply (rule corres_guard_imp)
apply (simp add:store_pde_def)
@ -1571,8 +1570,7 @@ lemma dcorres_store_invalid_pde_super_section:
apply (rule dcorres_delete_cap_simple_set_pde[where oid = pg_id])
apply simp
apply (wp|simp)+
apply (clarsimp simp: invs_def valid_mdb_def
valid_state_def valid_pspace_def)
apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def)
done
lemma dcorres_store_invalid_pte:
@ -1585,8 +1583,7 @@ lemma dcorres_store_invalid_pte:
apply (rule corres_symb_exec_r)
apply (rule dcorres_delete_cap_simple_set_pt[where pg_id = pg_id])
apply (wp|simp)+
apply (clarsimp simp: invs_def valid_mdb_def
valid_state_def valid_pspace_def)
apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def)
done
lemma dcorres_store_pde_non_sense:
@ -1595,8 +1592,7 @@ lemma dcorres_store_pde_non_sense:
\<and> (f (ucast (slot && mask pd_bits >> 2)) = pde)))
(return a) (store_pde slot pde)"
apply (simp add:store_pde_def)
apply (simp add:get_pd_def bind_assoc
get_object_def set_pd_def gets_def)
apply (simp add:get_pd_def bind_assoc get_object_def set_pd_def gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp add:assert_def corres_free_fail
split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
@ -1605,13 +1601,11 @@ lemma dcorres_store_pde_non_sense:
split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
apply (simp add:set_object_def put_def)
apply (rule dcorres_absorb_get_r)
apply (simp add:corres_underlying_def
return_def transform_def transform_current_thread_def)
apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def)
apply (frule page_directory_at_rev)
apply (drule(1) page_directory_not_idle[rotated])
apply (rule ext)+
apply (simp add:transform_objects_def
not_idle_thread_def obj_at_def)
apply (simp add:transform_objects_def not_idle_thread_def obj_at_def)
done
lemma dcorres_store_pte_non_sense:
@ -1620,8 +1614,7 @@ lemma dcorres_store_pte_non_sense:
\<and> (f (ucast (slot && mask pt_bits >> 2)) = pte)))
(return a) (store_pte slot pte)"
apply (simp add:store_pte_def)
apply (simp add:get_pt_def bind_assoc
get_object_def set_pt_def gets_def)
apply (simp add:get_pt_def bind_assoc get_object_def set_pt_def gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp add:assert_def corres_free_fail
split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
@ -1630,13 +1623,11 @@ lemma dcorres_store_pte_non_sense:
split:Structures_A.kernel_object.splits arch_kernel_obj.splits)
apply (simp add:set_object_def put_def)
apply (rule dcorres_absorb_get_r)
apply (simp add:corres_underlying_def
return_def transform_def transform_current_thread_def)
apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def)
apply (frule page_table_at_rev)
apply (drule(1) page_table_not_idle[rotated])
apply (rule ext)+
apply (simp add:transform_objects_def
not_idle_thread_def obj_at_def)
apply (simp add:transform_objects_def not_idle_thread_def obj_at_def)
done
lemma store_pde_non_sense_wp:
@ -1645,11 +1636,9 @@ lemma store_pde_non_sense_wp:
store_pde x ARM_Structs_A.pde.InvalidPDE
\<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s
\<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_Structs_A.pde.InvalidPDE))\<rbrace>"
apply (simp add:store_pde_def get_object_def
get_pde_def set_pd_def set_object_def)
apply (simp add:store_pde_def get_object_def get_pde_def set_pd_def set_object_def)
apply wp
apply (clarsimp simp:obj_at_def
split:Structures_A.kernel_object.splits arch_kernel_object.splits)
apply (clarsimp simp:obj_at_def split:Structures_A.kernel_object.splits arch_kernel_object.splits)
done
lemma dcorres_store_invalid_pde_tail_super_section:
@ -1805,8 +1794,8 @@ lemma dcorres_unmap_large_section:
in valid_entriesD[rotated])
apply (rule ccontr)
apply simp
apply (drule_tac x="ucast ?v" in arg_cong[where f = "ucast::(12 word\<Rightarrow>word32)"])
apply (drule_tac x="ucast ?v" in arg_cong[where f = "\<lambda>x. shiftl x 2"])
apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(12 word\<Rightarrow>word32)"])
apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"])
apply (subst (asm) ucast_ucast_len)
apply (rule shiftr_less_t2n)
apply (rule less_le_trans[OF and_mask_less'])
@ -1917,8 +1906,8 @@ lemma dcorres_unmap_large_page:
in valid_entriesD[rotated])
apply (rule ccontr)
apply simp
apply (drule_tac x="ucast ?v" in arg_cong[where f = "ucast::(word8\<Rightarrow>word32)"])
apply (drule_tac x="ucast ?v" in arg_cong[where f = "\<lambda>x. shiftl x 2"])
apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(word8\<Rightarrow>word32)"])
apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"])
apply (subst (asm) ucast_ucast_len)
apply (rule shiftr_less_t2n)
apply (rule less_le_trans[OF and_mask_less'])
@ -1986,7 +1975,7 @@ lemma mdb_cte_at_flush_page[wp]:
apply (simp add:mdb_cte_at_def)
apply (simp only: imp_conv_disj)
apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift)
done
done
crunch pd_pt_relation[wp]: flush_table "pd_pt_relation a b c"
(wp: crunch_wps simp: crunch_simps)
@ -2128,8 +2117,7 @@ lemma dcorres_find_pd_for_asid:
apply (rule dcorres_get)
apply (clarsimp simp:cdl_asid_table_transform liftE_bindE
transform_asid_table_entry_def split:option.splits)
apply (simp add:get_asid_pool_def get_object_def gets_the_def
gets_def bind_assoc get_asid_pool_def)
apply (simp add:get_asid_pool_def get_object_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_get)
apply (clarsimp simp: obj_at_def opt_object_asid_pool
assert_opt_def has_slots_def opt_cap_def slots_of_def assert_def
@ -2414,8 +2402,8 @@ prefer 2
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_pt_relation | wp_once hoare_drop_imps)+)[1]
apply (simp del: swp_apply | wp lookup_pt_slot_inv)+
apply (simp del: swp_apply
apply (simp | wp lookup_pt_slot_inv)+
apply (simp
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| safe)+
apply ((simp add:dc_def,wp)+)[3]
@ -2453,8 +2441,8 @@ prefer 2
apply (wp hoare_drop_imps)[1]
apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation])
apply fastforce
apply (simp del: swp_apply | wp lookup_pt_slot_inv)+
apply (simp del: swp_apply
apply (simp | wp lookup_pt_slot_inv)+
apply (simp
| wp lookup_pt_slot_inv hoare_drop_imps
find_pd_for_asid_kernel_mapping_help
| safe)+
@ -2484,8 +2472,8 @@ prefer 2
apply (wp do_machine_op_wp | clarsimp)+
apply (simp add: imp_conjR)
apply ((wp check_mapping_pptr_section_relation | wp_once hoare_drop_imps)+)[1]
apply (simp del: swp_apply | wp lookup_pt_slot_inv)+
apply (simp del: swp_apply
apply (simp | wp lookup_pt_slot_inv)+
apply (simp
| wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help
| safe)+
apply ((simp add:dc_def,wp)+)[2]
@ -2523,7 +2511,7 @@ prefer 2
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation])
apply clarsimp
apply (simp del: swp_apply add:is_aligned_mask[symmetric]
apply (simp add:is_aligned_mask[symmetric]
| wp lookup_pt_slot_inv hoare_drop_imps
find_pd_for_asid_kernel_mapping_help
| safe)+
@ -2623,7 +2611,7 @@ lemma dcorres_finalise_cap:
(CSpace_D.finalise_cap cdlcap final)
(CSpace_A.finalise_cap cap final)"
apply (case_tac cap)
apply (simp_all add:transform_cap_simps when_def)
apply (simp_all add: when_def)
apply clarsimp
apply (rule corres_rel_imp)
apply (rule corres_guard_imp[OF dcorres_ep_cancel_all])
@ -2655,10 +2643,11 @@ lemma dcorres_finalise_cap:
apply (clarsimp simp:transform_cap_def)
apply (wp|clarsimp)+
apply (clarsimp simp:assert_def corres_free_fail)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp_all add: transform_cap_simps arch_finalise_cap_def split:arch_cap.split_asm)
apply (simp_all add: arch_finalise_cap_def split:arch_cap.split_asm)
apply clarsimp
-- arch_cap.ASIDPoolCap
-- arch_cap.ASIDPoolCap
apply (rule corres_guard_imp)
apply (simp add:transform_asid_def)
apply (rule corres_split[OF _ dcorres_delete_asid_pool])
@ -2666,7 +2655,7 @@ lemma dcorres_finalise_cap:
apply (clarsimp simp:transform_cap_def)
apply (wp|clarsimp)+
apply (clarsimp split:option.splits | rule conjI)+
-- arch_cap.PageCap
-- arch_cap.PageCap
apply (simp add:transform_mapping_def)
apply (clarsimp simp:transform_mapping_def)
apply (rule corres_guard_imp)
@ -2675,7 +2664,7 @@ lemma dcorres_finalise_cap:
apply (clarsimp simp:transform_cap_def)
apply (wp | clarsimp )+
apply simp
--arch_cap.PageTableCap
--arch_cap.PageTableCap
apply (clarsimp simp:transform_mapping_def split:option.splits)
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp)
@ -2693,7 +2682,7 @@ lemma dcorres_finalise_cap:
apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]])
apply (clarsimp simp:transform_cap_def)
apply (wp|clarsimp split:option.splits)+
done
done
lemma dcorres_splits:
"\<lbrakk> T a \<Longrightarrow> dcorres r P (Q a) f (g a);
@ -2718,7 +2707,7 @@ where "remainder_cap final c\<equiv> case c of
lemma finalise_cap_remainder:
"\<lbrace>\<top>\<rbrace>CSpace_A.finalise_cap cap final \<lbrace>\<lambda>r s. fst (r) = (remainder_cap final cap) \<rbrace>"
apply (case_tac cap)
apply (simp_all add:CSpace_A.finalise_cap.simps remainder_cap_def)
apply (simp_all add: remainder_cap_def)
apply (wp|clarsimp)+
apply (fastforce simp:valid_def)
apply (simp|clarify)+
@ -2728,15 +2717,16 @@ lemma finalise_cap_remainder:
apply (wp|clarsimp|rule conjI)+
apply (simp add:arch_finalise_cap_def)
apply (cases final)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp_all)
apply (wp|clarsimp)+
apply (simp_all split:option.splits)
apply (wp | clarsimp | rule conjI)+
apply (case_tac arch_cap)
apply simp_all
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp)
apply (wp|clarsimp split:option.splits | rule conjI)+
done
done
lemma obj_ref_not_idle:
"\<lbrakk>valid_objs s;valid_global_refs s;cte_at slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s"
@ -2746,7 +2736,7 @@ lemma obj_ref_not_idle:
apply (drule_tac x = a in spec)
apply (drule_tac x = b in spec)
apply (clarsimp simp:cte_wp_at_def not_idle_thread_def cap_range_def global_refs_def)
done
done
lemma singleton_set_eq:
@ -2791,23 +2781,21 @@ lemma zombie_cap_has_all:
apply simp+
apply (simp add:is_zombie_def)
apply simp+
apply (case_tac cap)
apply simp_all
apply (case_tac y)
apply simp_all
apply (case_tac cap; simp)
apply (case_tac y; simp)
apply (frule_tac p = "(a,b)" in caps_of_state_valid_cap)
apply simp
apply (frule_tac p = slot in caps_of_state_valid_cap)
apply simp
apply (rename_tac word w2 w3 rights)
apply (clarsimp simp:valid_cap_def tcb_at_def dest!:get_tcb_SomeD)
apply (drule_tac p = "(interrupt_irq_node s word,[])" in caps_of_state_cteD)
apply (clarsimp simp:cte_wp_at_cases)
apply (clarsimp simp:obj_at_def is_tcb_def tcb_cap_cases_def tcb_cnode_index_def to_bl_1
split:if_splits)
apply (clarsimp simp:obj_at_def is_tcb_def tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split:if_splits)
apply (drule valid_globals_irq_node[OF _ caps_of_state_cteD])
apply simp
apply (fastforce simp:cap_range_def)
done
done
lemma monadic_trancl_steps:
"monadic_rewrite False False \<top>
@ -3452,12 +3440,12 @@ lemma opt_cap_cnode:
apply (case_tac "sz = 0")
apply (clarsimp, rule conjI)
apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD)
apply (metis (full_types) nat_to_bl_bl_to_bin nat_to_bl_id2
apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
option.inject wf_cs_nD)
(* "sz \<noteq> 0" *)
apply (clarsimp, rule conjI)
apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD)
apply (metis (full_types) nat_to_bl_bl_to_bin nat_to_bl_id2
apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2
option.inject wf_cs_nD)
done
@ -3562,6 +3550,7 @@ next
apply (clarsimp simp: remainder_cap_def valid_cap_simps
cte_wp_at_caps_of_state
split: cap.split_asm split_if_asm)
apply (rename_tac word nat option)
apply (frule valid_global_refsD2, clarsimp)
apply (clarsimp simp: CSpace_D.cap_removeable_def)
apply (subgoal_tac "\<exists>x cap. (word, b) = transform_cslot_ptr (word, x)
@ -3683,7 +3672,7 @@ next
apply (simp add: cutMon_walk_bind)
apply (rule corres_drop_cutMon_bind)
apply (rule corres_split[OF _ set_cap_corres])
apply (rule_tac P="dcorres ?r ?P ?P' ?f" in subst)
apply (rule_tac P="dcorres r P P' f" for r P P' f in subst)
apply (rule_tac f="\<lambda>_. ()" in gets_bind_ign)
apply (rule_tac r'="\<lambda>rv rv'. transform_cslot_ptr `
(case fst fin' of cap.Zombie p zb (Suc n) \<Rightarrow>
@ -3704,8 +3693,7 @@ next
prefer 2
apply (rule "2.hyps"[simplified, folded dc_def],
(assumption | simp | rule conjI refl)+)
apply (clarsimp simp del: transform_cap_simps
split: cap.split nat.split)
apply (clarsimp split: cap.split nat.split)
apply (rule corres_cutMon)
apply (simp add: cutMon_walk_bindE dc_def[symmetric])
apply (rule corres_drop_cutMon_bindE)
@ -3729,7 +3717,7 @@ next
apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap)
apply (clarsimp simp: transform_cslot_ptr_def)
apply (wp | simp)+
apply (simp add: conj_ac)
apply (simp add: conj_comms)
apply (wp replace_cap_invs final_cap_same_objrefs set_cap_cte_wp_at
hoare_vcg_const_Ball_lift set_cap_cte_cap_wp_to static_imp_wp
| erule finalise_cap_not_reply_master[simplified in_monad, simplified]
@ -3753,7 +3741,7 @@ next
apply (frule valid_global_refsD2, clarsimp+)
apply (erule disjE[where P="c = cap.NullCap \<and> P" for c P])
apply clarsimp
apply (clarsimp simp: conj_ac invs_valid_idle global_refs_def cap_range_def
apply (clarsimp simp: conj_comms invs_valid_idle global_refs_def cap_range_def
dest!: is_cap_simps' [THEN iffD1])
apply (frule trans [OF _ appropriate_Zombie, OF sym])
apply (case_tac cap,
@ -3782,7 +3770,7 @@ next
apply (simp add: finalise_slot_inner2_def[unfolded split_def])
apply (rule corres_alternate1, rule corres_alternate1, rule corres_alternate2)
apply simp
apply (rule_tac x="(?p, ?p')" in select_pick_corres)
apply (rule_tac x="(p, p')" for p p' in select_pick_corres)
apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric])
apply (rule swap_for_delete_corres)
apply (clarsimp simp: cte_wp_at_caps_of_state)

183
proof/drefine/Intent_DR.thy
View File

@ -230,7 +230,7 @@ lemma update_tcb_cxt_eq_dupdate_tcb_intent:
not_idle_thread_def transform_objects_def)
apply (rule ext, clarsimp)
apply (rule conjI)
apply (clarsimp simp:transform_objects_simps restrict_map_Some_iff)
apply (clarsimp simp:restrict_map_Some_iff)
apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def)
apply (clarsimp simp:transform_tcb_def restrict_map_def map_add_def)
done
@ -244,13 +244,13 @@ lemma duplicate_corrupt_tcb_intent:
apply (rule set_eqI)
apply clarsimp
apply (auto simp:corrupt_tcb_intent_def update_thread_def select_def gets_the_def
assert_opt_def return_def fail_def gets_def get_def assert_opt_def bind_def
return_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def opt_object_def split_def
split:option.splits cdl_object.splits)[1]
apply clarsimp
apply (rule iffI)
apply (auto simp:corrupt_tcb_intent_def update_thread_def select_def gets_the_def
assert_opt_def return_def fail_def gets_def get_def assert_opt_def bind_def
return_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def opt_object_def split_def
split:option.splits cdl_object.splits)
done
@ -270,7 +270,7 @@ lemma corres_corrupt_tcb_intent_return:
apply (clarsimp simp: corres_underlying_def)
apply (clarsimp simp: return_def corrupt_tcb_intent_def)
apply (clarsimp simp:corrupt_tcb_intent_def update_thread_def select_def gets_the_def
assert_opt_def return_def fail_def gets_def get_def assert_opt_def bind_def
return_def fail_def gets_def get_def assert_opt_def bind_def
put_def modify_def KHeap_D.set_object_def opt_object_def)
apply (clarsimp split:option.splits
simp:transform_def tcb_at_def is_tcb_def
@ -281,7 +281,7 @@ lemma corres_corrupt_tcb_intent_return:
apply (rule exI)
apply (auto simp: transform_def transform_tcb_def
transform_objects_def not_idle_thread_def is_tcb_def
tcb_at_def obj_at_def intro:exI split:cdl_object.splits)
tcb_at_def obj_at_def split:cdl_object.splits)
done
lemma dcorres_set_object_tcb:
@ -389,7 +389,7 @@ lemma dummy_corrupt_tcb_intent_corres:
apply (clarsimp simp:update_thread_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def)
apply (clarsimp simp:KHeap_D.set_object_def get_def put_def bind_def modify_def assert_def bind_def return_def)
apply (clarsimp simp:KHeap_D.set_object_def get_def put_def modify_def assert_def bind_def return_def)
apply (subst corres_singleton)
apply (clarsimp simp:dc_def)
apply (clarsimp simp:transform_def)
@ -479,7 +479,7 @@ lemma dcorres_dummy_corrupt_frame: "dcorres dc \<top> valid_etcbs
apply (rule corres_guard_imp)
apply (rule_tac P="op=(transform s')" and Q="op=s'"
and x = "\<lambda>x. transform_full_intent (machine_state s') x (the (get_tcb x s'))" in select_pick_corres)
apply (clarsimp simp:get_def put_def bind_def modify_def assert_def bind_def return_def)
apply (clarsimp simp:get_def put_def modify_def assert_def bind_def return_def)
apply (subst corres_singleton)
apply (clarsimp simp:corrupt_intents_def Let_def transform_def transform_objects_def)
apply (rule ext)
@ -923,11 +923,6 @@ lemma evalMonad_compose:
apply (clarsimp simp:bind_def)
done
lemma evalMonad_return [simp]:
"evalMonad (return x) s = Some x"
unfolding evalMonad_def
by (simp add: return_def)
lemma evalMonad_thread_get:
"evalMonad (thread_get f thread) sa = Some x \<Longrightarrow> \<exists>tcb. get_tcb thread sa = Some tcb \<and> f tcb = x"
by (clarsimp simp:thread_get_def evalMonad_def gets_def gets_the_def
@ -952,8 +947,7 @@ lemma evalMonad_loadWord:
(if x && mask 2 = 0 then
Some (word_rcat [underlying_memory ms (x + 3), underlying_memory ms (x + 2), underlying_memory ms (x + 1), underlying_memory ms x])
else None)"
by (clarsimp simp:word_zero_le loadWord_def gets_def get_def
return_def bind_def assert_def fail_def evalMonad_def)
by (clarsimp simp: loadWord_def gets_def get_def return_def bind_def assert_def fail_def evalMonad_def)
lemma weak_det_spec_lookup_ipc_buffer:
"weak_det_spec P (lookup_ipc_buffer a b)"
@ -961,11 +955,10 @@ lemma weak_det_spec_lookup_ipc_buffer:
apply (rule weak_det_spec_compose)+
apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap)
apply (case_tac ra)
apply (simp_all add:weak_det_spec_simps)
apply (case_tac arch_cap)
apply (simp_all add:weak_det_spec_simps)
done
apply (case_tac ra; simp add:weak_det_spec_simps)
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp add:weak_det_spec_simps)
done
lemma empty_when_fail_lookup_ipc_buffer:
"empty_when_fail (lookup_ipc_buffer a b)"
@ -973,11 +966,10 @@ lemma empty_when_fail_lookup_ipc_buffer:
apply (rule empty_when_fail_compose)+
apply (simp_all add: empty_when_fail_simps empty_when_fail_get_cap empty_when_fail_thread_get
weak_det_spec_simps weak_det_spec_thread_get weak_det_spec_get_cap)
apply (case_tac ra)
apply (simp_all add:empty_when_fail_simps)
apply (case_tac arch_cap)
apply (simp_all add:empty_when_fail_simps)
done
apply (case_tac ra; simp add:empty_when_fail_simps)
apply (rename_tac arch_cap)
apply (case_tac arch_cap; simp add:empty_when_fail_simps)
done
abbreviation
"\<lambda>s. ipc_frame_cte_at thread buf rights sz s \<equiv>
@ -1100,14 +1092,15 @@ lemma get_tcb_mrs_wp:
apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def)
apply (wp|wpc)+
apply (clarsimp simp:get_tcb_mrs_def Let_def)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_splits)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:split_if)
apply (clarsimp simp:get_tcb_message_info_def get_ipc_buffer_words_empty)
apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def)
apply (clarsimp simp:get_mrs_def thread_get_def gets_the_def)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_splits)
apply (clarsimp simp:Suc_leI[OF msg_registers_lt_msg_max_length] split del:split_if)
apply (wp|wpc)+
apply (rule_tac P = "tcb = obj" in hoare_gen_asm)
apply (clarsimp simp: get_tcb_mrs_def Let_def get_tcb_message_info_def Suc_leI[OF msg_registers_lt_msg_max_length] split del:if_splits)
apply (clarsimp simp: get_tcb_mrs_def Let_def get_tcb_message_info_def Suc_leI[OF msg_registers_lt_msg_max_length]
split del:split_if)
apply (rule_tac Q="\<lambda>buf_mrs s. buf_mrs =
(get_ipc_buffer_words (machine_state sa) obj ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]))"
in hoare_strengthen_post)
@ -1120,9 +1113,7 @@ done
(* Following is the proof of set_mrs *)
lemma pbfs_word_bits [simp]:
"pageBitsForSize sz < word_bits"
by (cases sz, simp_all add: word_bits_conv)
declare pbfs_less_wb' [simp]
lemma mab_le_pbfs [simp]:
"msg_align_bits \<le> pageBitsForSize sz"
@ -1563,10 +1554,12 @@ lemma store_word_corres_helper:
apply (rule conjI)
apply (clarsimp simp:restrict_map_def transform_object_def transform_tcb_def
split:cdl_object.split_asm Structures_A.kernel_object.split_asm split_if_asm)
apply (drule(1) valid_etcbs_tcb_etcb, clarsimp simp:restrict_map_def transform_object_def transform_tcb_def
apply (drule(1) valid_etcbs_tcb_etcb,
clarsimp simp:restrict_map_def transform_object_def transform_tcb_def
split:cdl_object.split_asm Structures_A.kernel_object.split_asm split_if_asm)+
defer
apply (drule(1) valid_etcbs_tcb_etcb, clarsimp simp:restrict_map_def transform_object_def transform_tcb_def
apply (drule(1) valid_etcbs_tcb_etcb,
clarsimp simp:restrict_map_def transform_object_def transform_tcb_def
split:cdl_object.split_asm Structures_A.kernel_object.split_asm split_if_asm)+
defer
apply (simp add:tcb_ipcframe_id_def split:split_if_asm)
@ -1574,13 +1567,15 @@ lemma store_word_corres_helper:
apply (frule_tac thread = thread in valid_tcb_objs)
apply (simp add: get_tcb_rev)
apply (clarsimp simp:valid_tcb_def tcb_cap_cases_def)
apply (case_tac "\<not> is_arch_page_cap (tcb_ipcframe tcb_ext)")
apply (rename_tac tcb etcb)
apply (case_tac "\<not> is_arch_page_cap (tcb_ipcframe tcb)")
apply (simp add:transform_full_intent_no_ipc_buffer)
apply (clarsimp simp del:upt.simps simp:transform_full_intent_def Let_def get_tcb_mrs_def is_arch_page_cap_def
split:cap.split_asm arch_cap.split_asm split del:if_splits)
split:cap.split_asm arch_cap.split_asm split del:split_if)
apply (rename_tac word cap_rights vmpage_size option)
apply (clarsimp simp:transform_cap_def arch_cap.split_asm simp del:upt.simps)
apply (frule_tac thread = thread and ptr = ptr and sz = sz
and ms = "machine_state s" and tcb_type = tcb_ext and b = b and s_id = s_id
and ms = "machine_state s" and tcb_type = tcb and b = b and s_id = s_id
and xs = "[Suc (length msg_registers)..<Suc msg_max_length]"
in get_ipc_buffer_words_separate_frame)
apply (erule get_tcb_rev)
@ -1593,8 +1588,8 @@ lemma store_word_corres_helper:
apply (clarsimp simp:transform_cap_def split:cap.splits arch_cap.splits)
apply (rule conjI)
apply (frule_tac thread = thread and ptr = ptr and sz = sz and ms = "machine_state s" and
tcb_type = tcb_ext and b = b and s_id = s_id
and xs = "[buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb_ext))]"
tcb_type = tcb and b = b and s_id = s_id
and xs = "[buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info tcb))]"
in get_ipc_buffer_words_separate_frame)
apply (erule get_tcb_rev)
apply ((simp add:ipc_frame_wp_at_def obj_at_def)+)[8]
@ -1602,7 +1597,7 @@ lemma store_word_corres_helper:
apply (rule_tac sz = vmpage_size and y = thread in within_page_ipc_buf)
apply (simp add:ipc_frame_wp_at_def obj_at_def ipc_buffer_wp_at_def)+
apply (simp add:msg_max_length_def msg_align_bits buffer_cptr_index_def)
apply (case_tac "(get_tcb_message_info tcb_ext)")
apply (case_tac "(get_tcb_message_info tcb)")
apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def)
apply (erule order_less_le_trans)
apply simp
@ -1611,7 +1606,7 @@ lemma store_word_corres_helper:
apply (rule word_and_le1[where a = 3])
apply ((clarsimp simp:ipc_frame_wp_at_def obj_at_def)+)[4]
apply (frule_tac thread = thread and ptr = ptr and sz = sz and ms = "machine_state s" and
tcb_type = tcb_ext and b = b and s_id = s_id
tcb_type = tcb and b = b and s_id = s_id
and xs = "[Suc (Suc (msg_max_length + msg_max_extra_caps))..<5 + (msg_max_length + msg_max_extra_caps)]"
in get_ipc_buffer_words_separate_frame)
apply (erule get_tcb_rev)
@ -1622,32 +1617,33 @@ lemma store_word_corres_helper:
apply (clarsimp simp:msg_align_bits msg_max_length_def msg_max_extra_caps_def)
apply simp+
apply (clarsimp simp: tcb_ipcframe_id_def split: cdl_object.splits option.split_asm cdl_cap.split_asm)
apply (clarsimp simp:transform_object_def split:Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm nat.splits)
apply (clarsimp simp: transform_object_def split:Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm nat.splits)
apply (rename_tac tcb)
apply (simp add:transform_tcb_def)
apply (drule sym)
apply (clarsimp simp:tcb_pending_op_slot_def restrict_map_def tcb_ipcbuffer_slot_def split:if_splits)
apply (frule(1) valid_etcbs_tcb_etcb[OF _ eq_sym_helper])
apply clarsimp
apply (subgoal_tac "(get_tcb thread s) = Some tcb_ext")
apply (subgoal_tac "(get_tcb thread s) = Some tcb")
apply (clarsimp dest!:get_tcb_SomeD)
apply (subgoal_tac "tcb_ext = the (get_tcb thread s)")
apply (subgoal_tac "tcb = the (get_tcb thread s)")
apply (subgoal_tac "etcb = the (get_etcb thread s)")
apply simp
apply (simp add: get_etcb_rev)
apply (simp add:get_tcb_rev)+
done
done
lemma select_f_store_word:
"(select_f (storeWord p w ms)) = (do assert (p && mask 2 = 0);
return ((),storeWord_ms p w ms) od)"
apply (clarsimp simp:assert_def select_f_def
storeWord_def bind_def assert_def fail_def simpler_modify_def storeWord_ms_def return_def)
done
apply (clarsimp simp: assert_def select_f_def storeWord_def bind_def fail_def simpler_modify_def
storeWord_ms_def return_def)
done
lemma select_f_get_register:
"(as_user thread (get_register register)) =
(do tcb\<leftarrow>gets_the (get_tcb thread);return (tcb_context tcb register) od)"
apply (simp add:assert_opt_def as_user_def set_object_def gets_the_def
apply (simp add: assert_opt_def as_user_def set_object_def gets_the_def
put_def select_f_def get_register_def gets_def get_def return_def bind_def)
apply (rule ext)
apply (case_tac "get_tcb thread s")
@ -1693,16 +1689,18 @@ lemma dcorres_store_word_safe:
apply (clarsimp simp del:upt.simps
simp: Let_def get_tcb_mrs_def is_arch_page_cap_def
split:cap.split_asm arch_cap.split_asm
split del:if_splits)
split del: split_if)
apply (frule valid_tcb_objs, erule get_tcb_rev)
apply (clarsimp simp:valid_tcb_def tcb_cap_cases_def valid_ipc_buffer_cap_def simp del:upt.simps)
apply (erule disjE)
apply (clarsimp simp:is_arch_cap_def split:cap.split_asm simp del:upt.simps)
apply (rename_tac tcb arch_cap)
apply (case_tac arch_cap)
apply ((simp add:get_ipc_buffer_words_def)+)[2]
apply (rename_tac word rights vmpage_size option)
apply (simp add:Suc_leI[OF msg_registers_lt_msg_max_length] del:upt.simps)
apply (frule_tac thread = thread and ptr = ptr and ms = "machine_state s'"
and tcb_type = tcb_ext and b = b
and tcb_type = tcb and b = b
and xs = "[Suc (length msg_registers)..<Suc msg_max_length]"
in get_ipc_buffer_words_helper)
apply (erule get_tcb_rev)
@ -1721,9 +1719,9 @@ lemma dcorres_store_word_safe:
apply (rule conjI)
apply (frule_tac thread = thread and ptr = ptr and ms = "machine_state s'"
and tcb_type = tcb_ext and b = b
and tcb_type = tcb and b = b
and xs = "[buffer_cptr_index..<buffer_cptr_index +
unat (mi_extra_caps (get_tcb_message_info tcb_ext))]"
unat (mi_extra_caps (get_tcb_message_info tcb))]"
in get_ipc_buffer_words_helper)
apply (erule get_tcb_rev)
apply ((simp add:ipc_frame_wp_at_def obj_at_def is_aligned_mask)+)[7]
@ -1731,7 +1729,7 @@ lemma dcorres_store_word_safe:
apply (rule_tac sz = vmpage_size and y = thread in within_page_ipc_buf)
apply (simp add:ipc_frame_wp_at_def obj_at_def ipc_buffer_wp_at_def)+
apply (simp add:msg_max_length_def msg_align_bits buffer_cptr_index_def)
apply (case_tac "(get_tcb_message_info tcb_ext)")
apply (case_tac "get_tcb_message_info tcb")
apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def)
apply (erule order_less_le_trans)
apply simp
@ -1745,7 +1743,7 @@ lemma dcorres_store_word_safe:
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def)
apply simp
apply (frule_tac thread = thread and ptr = ptr and sz = sz and ms = "machine_state s'"
and tcb_type = tcb_ext and b = b
and tcb_type = tcb and b = b
and xs = "[Suc (Suc (msg_max_length + msg_max_extra_caps))..<
5 + (msg_max_length + msg_max_extra_caps)]"
in get_ipc_buffer_words_helper)
@ -1836,7 +1834,7 @@ lemma zip_cpy_word_corres:
apply simp
using Cons.prems
apply (clarsimp simp: within_page_def in_user_frame_def)
apply (thin_tac "Ball ?S ?P")
apply (thin_tac "Ball S P" for S P)
apply (rule_tac x=sz in exI)
apply (frule (2) ipc_frame_ptr_at_frame_at)
apply (simp add: obj_at_def a_type_simps)
@ -1874,19 +1872,17 @@ lemma zip_store_word_corres:
apply (drule_tac x = list in spec)
apply simp
apply (clarsimp simp:store_word_offs_def)
apply (simp add: store_word_offs_def bind_assoc[symmetric]
state_assert_def[symmetric])
apply (simp add: store_word_offs_def bind_assoc[symmetric] state_assert_def[symmetric])
apply (rule corres_state_assert)
apply (rule_tac s_id = s_id and sz = sz in store_word_corres)
apply simp
apply (clarsimp simp: within_page_def in_user_frame_def)
apply (thin_tac "Ball ?S ?P")
apply (rule_tac x=sz in exI)
apply (frule (2) ipc_frame_ptr_at_frame_at)
apply (simp add: obj_at_def a_type_simps)
apply (wp store_word_offs_ipc_frame_wp)
apply clarsimp+
done
done
lemma ex_cte_cap_wp_to_not_idle:
"\<lbrakk> ex_cte_cap_wp_to P r s; valid_global_refs s; valid_objs s;
@ -1900,51 +1896,47 @@ lemma ex_cte_cap_wp_to_not_idle:
apply clarsimp
apply (case_tac cap)
apply (clarsimp simp:cap_range_def)+
apply (rename_tac word)
apply (clarsimp simp:valid_idle_def valid_irq_node_def)
apply (drule_tac x = word in spec)
apply (clarsimp simp:st_tcb_at_def obj_at_def is_cap_table_def)
apply (clarsimp simp:cap_range_def)+
apply (case_tac "get tcb")
apply clarsimp+
apply (rename_tac word)
apply (clarsimp simp:valid_idle_def valid_irq_node_def)
apply (drule_tac x = word in spec)
apply (clarsimp simp:st_tcb_at_def obj_at_def is_cap_table_def)
apply clarsimp+
done
lemma ex_cte_cap_to_not_idle:
"\<lbrakk>valid_global_refs s; valid_objs s; valid_idle s;ex_cte_cap_to r s;valid_irq_node s\<rbrakk>
\<Longrightarrow> not_idle_thread (fst r) s"
by (simp add: ex_cte_cap_wp_to_not_idle)
lemma pspace_aligned_set_cxt_mrs[wp]:
"\<lbrace>ko_at (TCB tcb) thread and pspace_aligned\<rbrace> KHeap_A.set_object thread (TCB (tcb\<lparr>tcb_context := t \<rparr>))\<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
apply (wp set_object_aligned)
apply (clarsimp simp:obj_at_def)
done
apply (wp set_object_aligned)
apply (clarsimp simp:obj_at_def)
done
lemma pspace_distinct_set_cxt_mrs[wp]:
"\<lbrace>ko_at (TCB tcb) thread and pspace_distinct\<rbrace> KHeap_A.set_object thread (TCB (tcb\<lparr>tcb_context := t \<rparr>))
\<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
apply (wp set_object_distinct)
apply (clarsimp simp:obj_at_def)
done
apply (wp set_object_distinct)
apply (clarsimp simp:obj_at_def)
done
lemma valid_objs_set_cxt_mrs[wp]:
"\<lbrace>ko_at (TCB tcb) thread and valid_objs\<rbrace> KHeap_A.set_object thread (TCB (tcb\<lparr>tcb_context := t \<rparr>))\<lbrace>\<lambda>rv. valid_objs\<rbrace>"
apply (wp set_object_valid_objs)
apply (clarsimp simp:obj_at_def)
apply (clarsimp simp:valid_objs_def)
apply (drule_tac x=thread in bspec)
apply (clarsimp simp:dom_def)
apply (clarsimp simp:valid_obj_def valid_tcb_def)
apply (drule_tac x="(a,aa,b)" in bspec)
apply simp
apply (clarsimp simp:tcb_cap_cases_def)
apply (erule disjE|clarsimp)+
done
apply (wp set_object_valid_objs)
apply (clarsimp simp:obj_at_def)
apply (clarsimp simp:valid_objs_def)
apply (drule_tac x=thread in bspec)
apply (clarsimp simp:dom_def)
apply (clarsimp simp:valid_obj_def valid_tcb_def)
apply (drule_tac x="(a,aa,b)" in bspec)
apply simp
apply (clarsimp simp:tcb_cap_cases_def)
apply (erule disjE|clarsimp)+
done
lemma ipc_frame_set_cxt_mrs[wp]:
"\<lbrace>ko_at (TCB tcb) thread and ipc_frame_wp_at P a\<rbrace> KHeap_A.set_object thread (TCB (tcb\<lparr>tcb_context := t \<rparr>))\<lbrace>\<lambda>rv. ipc_frame_wp_at P a\<rbrace>"
@ -1990,7 +1982,7 @@ lemma set_mrs_corres:
apply (wp set_object_valid_etcbs)
apply (simp del:upt.simps)
apply (auto dest!:get_tcb_SomeD simp:obj_at_def ipc_frame_wp_at_def)
done
done
lemma set_registers_ipc_frame_ptr_at[wp]:
"\<lbrace>ipc_frame_wp_at buf y\<rbrace>as_user thread (set_register r rv) \<lbrace>%x. ipc_frame_wp_at buf y\<rbrace>"
@ -2002,7 +1994,7 @@ lemma set_registers_ipc_frame_ptr_at[wp]:
apply (assumption)
apply wp
apply clarsimp
done
done
lemma set_registers_ipc_buffer_ptr_at[wp]:
"\<lbrace>ipc_buffer_wp_at buf y\<rbrace>as_user thread (set_register r rv) \<lbrace>%x. ipc_buffer_wp_at buf y\<rbrace>"
@ -2014,7 +2006,7 @@ lemma set_registers_ipc_buffer_ptr_at[wp]:
apply (assumption)
apply wp
apply clarsimp
done
done
lemma copy_mrs_corres:
@ -2059,7 +2051,7 @@ lemma copy_mrs_corres:
apply ((wp|clarsimp)+)[3]
apply (case_tac rv)
apply (clarsimp simp: ipc_buffer_wp_at_def obj_at_def tcb_at_def)+
done
done
lemmas transform_cap_simps [simp] = transform_cap_def [split_simps cap.split arch_cap.split]
@ -2098,12 +2090,12 @@ shows "dcorres dc \<top> P (corrupt_frame buf) g"
apply (case_tac xa)
apply (clarsimp simp:not_idle_thread_def tcb_ipcframe_id_def restrict_map_def transform_objects_def
split: split_if)
apply (clarsimp dest!:get_tcb_rev simp: transform_objects_tcb
tcb_ipcbuffer_slot_def tcb_pending_op_slot_def)
apply (clarsimp dest!:get_tcb_rev simp: transform_objects_tcb tcb_ipcbuffer_slot_def
tcb_pending_op_slot_def)
apply (clarsimp simp: tcb_ipcbuffer_slot_def tcb_ipcframe_id_def | rule conjI)+
apply (clarsimp simp:transform_def transform_object_def transform_tcb_def tcb_ipcframe_id_def
tcb_ipcbuffer_slot_def tcb_pending_op_slot_def dest!:get_tcb_SomeD)
done
done
lemma corrupt_frame_include_self':
assumes corres:"dcorres dc \<top> P (do corrupt_frame buf; corrupt_tcb_intent y od) g"
@ -2123,10 +2115,9 @@ shows "dcorres dc \<top> P (corrupt_frame buf) g"
select_def gets_the_def KHeap_D.set_object_def
bind_def gets_def get_def return_def assert_opt_def
fail_def simpler_modify_def split:option.splits)
apply (rule_tac x = "\<lambda>t. if t = y then ?T else x t" in exI)
apply (rule_tac x = "\<lambda>t. if t = y then T else x t" for T in exI)
apply (clarsimp simp:corrupt_intents_def transform_def not_idle_thread_def
restrict_map_def map_add_def opt_object_def
ipc_frame_wp_at_def obj_at_def
restrict_map_def map_add_def opt_object_def ipc_frame_wp_at_def obj_at_def
split:option.split_asm cdl_object.split_asm)
apply (rule ext)
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def tcb_ipcframe_id_def tcb_pending_op_slot_def
@ -2136,7 +2127,7 @@ shows "dcorres dc \<top> P (corrupt_frame buf) g"
apply (drule(1) valid_etcbs_tcb_etcb)
apply (fastforce simp:opt_object_def transform_tcb_def tcb_ipcframe_id_def tcb_pending_op_slot_def
tcb_ipcbuffer_slot_def)+
done
done
lemma dcorres_set_mrs:
"dcorres dc \<top>
@ -2147,7 +2138,7 @@ lemma dcorres_set_mrs:
apply (rule corrupt_frame_include_self)
apply (rule corres_guard_imp[OF set_mrs_corres])
apply clarsimp+
done
done
lemma dcorres_copy_mrs:
"valid_message_info mi \<Longrightarrow>
@ -2159,7 +2150,7 @@ lemma dcorres_copy_mrs:
apply (rule corrupt_frame_include_self)
apply (rule corres_guard_imp[OF copy_mrs_corres])
apply auto
done
done
lemma ipc_frame_ptr_at_sz_at:
"\<lbrakk>ko_at (ArchObj (DataPage sz)) obuf s; valid_objs s;ipc_frame_ptr_at obuf thread s \<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s"
@ -2170,7 +2161,7 @@ lemma ipc_frame_ptr_at_sz_at:
apply (subgoal_tac "valid_cap (tcb_ipcframe tcb) s")
apply (clarsimp simp:valid_cap_def obj_at_def a_type_def split:arch_kernel_obj.splits)
apply (clarsimp simp:valid_tcb_def tcb_cap_cases_def)
done
done
lemma dcorres_store_word_conservative:
" within_page obuf ptr sz \<Longrightarrow>
@ -2193,6 +2184,6 @@ lemma dcorres_store_word_conservative:
apply (frule ipc_frame_ptr_at_sz_at,simp+)
apply (rule corres_guard_imp[OF store_word_corres])
apply simp+
done
done
end

28
proof/drefine/Interrupt_DR.thy
View File

@ -25,7 +25,7 @@ lemma decode_irq_control_error_corres:
(* Interrupt Control Invocations *)
primrec
primrec (nonexhaustive)
translate_irq_control_invocation :: "Invocations_A.irq_control_invocation \<Rightarrow> cdl_irq_control_invocation"
where
"translate_irq_control_invocation (IRQControl irq p slot) =
@ -188,6 +188,7 @@ lemma option_get_cap_corres:
apply (clarsimp simp:assert_def corres_free_fail assert_opt_def)
apply (case_tac y)
apply (simp_all add:assert_def corres_free_fail)
apply (rename_tac "fun")
apply (case_tac "fun b")
apply (simp add:corres_free_fail)
apply clarsimp
@ -195,11 +196,12 @@ lemma option_get_cap_corres:
apply fastforce
apply (clarsimp simp: transform_cap_def)
apply (clarsimp simp:transform_tcb_slot_simp[simplified])
apply (subgoal_tac "get_tcb a x = Some tcb_ext")
apply (rename_tac tcb)
apply (subgoal_tac "get_tcb a x = Some tcb")
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:lift_simp not_idle_thread_def)
apply (clarsimp simp: get_tcb_def)
done
done
lemma maskInterrupt_underlying_memory[wp]:
"\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt a x \<lbrace>\<lambda>x ms. underlying_memory ms = m\<rbrace>"
@ -295,7 +297,7 @@ lemma handle_interrupt_corres:
apply (rule_tac R'="\<lambda>rv. (\<lambda>s. (is_aep_cap rv \<longrightarrow> aep_at (obj_ref_of rv) s)) and invs and valid_etcbs"
in corres_split[OF _ option_get_cap_corres])
apply (case_tac rv'a)
prefer 4
prefer 4
apply (simp_all add:when_def)
apply (clarsimp simp:transform_cap_def when_def is_aep_cap_def | rule conjI)+
apply (rule corres_dummy_return_l)
@ -326,13 +328,13 @@ prefer 4
apply (subgoal_tac "cdl_irq_node (transform s'b) x = (interrupt_irq_node s'b x)")
apply clarsimp
apply (rule corres_guard_imp,rule corres_dummy_return_pl)
apply (simp add: nested_bind bind_assoc)
apply (simp add: bind_assoc)
apply (rule dcorres_rhs_noop_above[OF timer_tick_dcorres])
apply (rule dcorres_symb_exec_r[OF dcorres_machine_op_noop])
apply (wp dmo_dwp hoare_TrueI| simp)+
apply (clarsimp simp:transform_def invs_def valid_state_def dest!: valid_irq_node_cte_at_irq_slot )+
apply (simp add:cte_wp_at_caps_of_state)
done
done
lemma set_irq_state_original:
"\<lbrace>\<lambda>s. P (is_original_cap s slot)\<rbrace> set_irq_state a b
@ -356,6 +358,7 @@ lemma dcorres_invoke_irq_control:
(Interrupt_A.invoke_irq_control irq_control_invocation)"
apply (case_tac irq_control_invocation)
apply (simp_all add:arch_invoke_irq_control_def corres_free_fail)
apply (rename_tac word p1 p2)
apply (clarsimp simp:liftE_def bind_assoc)
apply (rule dcorres_symb_exec_r_strong)
apply (simp add:Interrupt_D.invoke_irq_control_def)
@ -396,17 +399,14 @@ lemma dcorres_invoke_irq_control:
done
lemma op_eq_simp:"(op = y) = (\<lambda>x. x = y)"
apply (rule ext)
apply auto
done
lemma op_eq_simp: "(op = y) = (\<lambda>x. x = y)" by auto
lemma get_irq_slot_not_idle_wp:
"\<lbrace>valid_idle and valid_irq_node \<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>rv. not_idle_thread (fst rv)\<rbrace>"
apply (clarsimp simp:get_irq_slot_def)
apply (rule irq_node_image_not_idle)
apply simp+
done
done
lemma get_irq_slot_ex_cte_cap_wp_to:
"\<lbrace>\<lambda>s. valid_irq_node s \<and> (\<exists>slot. cte_wp_at (op = (cap.IRQHandlerCap w)) slot s)\<rbrace> KHeap_A.get_irq_slot w
@ -416,7 +416,7 @@ lemma get_irq_slot_ex_cte_cap_wp_to:
apply (rule exI)+
apply (erule cte_wp_at_weakenE)
apply clarsimp
done
done
crunch is_original[wp] : fast_finalise "\<lambda>s. is_original_cap s slot"
@ -431,7 +431,7 @@ lemma cap_delete_one_original:
apply wp
apply (clarsimp simp:set_cdt_def)
apply (wp dxo_wp_weak | clarsimp)+
done
done
lemma cte_wp_at_neq_slot_set_cap:
@ -439,7 +439,7 @@ lemma cte_wp_at_neq_slot_set_cap:
CSpaceAcc_A.set_cap cap.NullCap slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>"
apply (wp set_cap_cte_wp_at_cases)
apply (clarsimp simp:cte_wp_at_def)
done
done
lemma cte_wp_at_neq_slot_cap_delete_one:
"slot\<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot\<rbrace> cap_delete_one slot'

97
proof/drefine/Ipc_DR.thy
View File

@ -12,8 +12,6 @@ theory Ipc_DR
imports CNode_DR
begin
declare option.weak_case_cong[cong]
abbreviation
"thread_is_running y s \<equiv> st_tcb_at (op=Structures_A.thread_state.Running) y s"
@ -28,7 +26,7 @@ lemma set_thread_state_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> set_thread_state thread x \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:set_thread_state_def)
apply (wp set_object_cur_thread_idle_thread dxo_wp_weak | simp)+
done
done
lemma thread_set_cur_thread_idle_thread:
" \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> thread_set (tcb_fault_update Map.empty) word \<lbrace>\<lambda>xg s. P (cur_thread s) (idle_thread s)\<rbrace>"
@ -518,7 +516,7 @@ lemma dcorres_do_async_transfer:
apply (wp | clarsimp simp:not_idle_thread_def)+
apply (simp add:gets_the_def gets_def bind_assoc get_def split_def get_ipc_buffer_def tcb_at_def
exs_valid_def fail_def return_def bind_def assert_opt_def split:cdl_cap.splits)
apply (rule_tac x = "(?a,?b)" in bexI)
apply (rule_tac x = "(a,b)" for a b in bexI)
apply (rule conjI|fastforce simp:fail_def return_def split:option.splits)+
apply (clarsimp split:option.splits simp:fail_def | rule conjI)+
apply (subst opt_cap_tcb)
@ -712,6 +710,7 @@ lemma recv_async_ipc_corres:
(recv_async_ipc thread cap)
(receive_async_ipc thread cap')"
apply (clarsimp simp:receive_async_ipc_def invs_def recv_async_ipc_def corres_free_fail split:cap.splits)
apply (rename_tac word1 word2 rights)
apply (rule dcorres_expand_pfx)
apply (rule_tac Q' = "\<lambda>r. op = s' and ko_at (kernel_object.AsyncEndpoint r) word1 and valid_aep r" in corres_symb_exec_r)
apply (rule dcorres_expand_pfx)
@ -720,8 +719,8 @@ lemma recv_async_ipc_corres:
apply (rule dcorres_absorb_get_l)
apply (frule get_async_ep_pick,simp)
apply (case_tac rv)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def cap_object_simps
valid_aep_abstract_def none_is_waiting_aep_def)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def cap_object_simps valid_aep_abstract_def
none_is_waiting_aep_def)
apply (rule corres_guard_imp)
apply (rule corres_alternate1)
apply (rule corres_dummy_return_l)
@ -729,7 +728,7 @@ lemma recv_async_ipc_corres:
apply (rule corres_dummy_set_async_ep,simp)
apply (wp|simp)+
apply (clarsimp simp:st_tcb_at_def tcb_at_def obj_at_def get_tcb_rev)
(* WaitingAEP *)
(* WaitingAEP *)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def
valid_aep_abstract_def none_is_waiting_aep_def cap_object_simps)
apply (rule conjI)
@ -741,7 +740,7 @@ lemma recv_async_ipc_corres:
apply (rule corres_dummy_set_async_ep,simp+)
apply (fastforce simp:st_tcb_at_def obj_at_def get_tcb_rev)
(* Active AEP list *)
(* Active AEP list *)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def
valid_aep_abstract_def none_is_waiting_aep_def cap_object_simps)
apply (rule corres_alternate2)
@ -757,7 +756,7 @@ lemma recv_async_ipc_corres:
apply (clarsimp simp:valid_objs_valid_aep_simp valid_state_def valid_pspace_def)
apply (simp add:obj_at_def)
apply (clarsimp|wp)+
done
done
lemma send_async_ipc_corres:
"ep_id = epptr \<Longrightarrow> dcorres dc \<top> (invs and valid_etcbs)
@ -772,12 +771,13 @@ lemma send_async_ipc_corres:
apply clarsimp
apply (frule valid_objs_valid_aep_simp[rotated])
apply (simp add:valid_state_def valid_pspace_def)
apply (rename_tac async_ep s)
apply (case_tac async_ep)
apply (simp add:gets_def bind_assoc option_select_def)
apply (frule get_async_ep_pick,simp)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def valid_aep_abstract_def none_is_waiting_aep_def)
apply (rule corres_guard_imp,rule corres_dummy_set_async_ep,simp+)
(* Waiting AEP list *)
(* Waiting AEP list *)
apply (simp add:gets_def bind_assoc option_select_def)
apply (frule get_async_ep_pick,simp)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def valid_aep_abstract_def)
@ -793,12 +793,12 @@ lemma send_async_ipc_corres:
apply (drule_tac x = y in eqset_imp_iff)
apply (clarsimp simp:valid_pspace_def aep_waiting_set_def)
apply (clarsimp simp: st_tcb_at_def obj_at_def valid_aep_def split:list.splits)
(* ActiveAEP *)
(* ActiveAEP *)
apply (clarsimp simp:gets_def bind_assoc option_select_def)
apply (frule get_async_ep_pick,simp)
apply (clarsimp simp:aep_waiting_set_lift valid_state_def valid_aep_abstract_def none_is_waiting_aep_def)
apply (rule corres_guard_imp,rule corres_dummy_set_async_ep,simp+)
done
done
lemma set_thread_state_block_on_send_corres:
"dcorres dc \<top>
@ -842,13 +842,13 @@ lemma corres_setup_caller_cap:
apply (drule valid_tcb_objs)
apply (erule get_tcb_rev)
apply (simp add:valid_tcb_state_def)
done
done
lemma seq_alt_when:"(do a \<leftarrow> when c (f \<sqinter> g); h a od) = ((do a\<leftarrow>when c f ; h a od)\<sqinter> (do a\<leftarrow>when c g; h a od))"
apply (clarsimp simp:when_def)
apply (subst alternative_bind_distrib)+
apply (clarsimp simp:alternative_def)
done
apply (clarsimp simp:when_def)
apply (subst alternative_bind_distrib)+
apply (clarsimp simp:alternative_def)
done
lemma evalMonad_mapM:
assumes as:"evalMonad (mapM f ls) s = Some v"
@ -951,7 +951,7 @@ lemma dcorres_set_extra_badge:
apply (clarsimp)
apply (rule dcorres_store_word_offs_spec)
apply (drule_tac x = "buffer_cptr_index + n" and sz = sz in within_page_ipc_buf)
apply (simp add:of_nat_add)+
apply (simp)+
apply (simp add:obj_at_def cte_wp_at_cases)
apply (drule_tac t = "tcb_ipcframe obj" in sym)
apply (fastforce simp:ipc_frame_wp_at_def obj_at_def)
@ -960,10 +960,12 @@ lemma dcorres_set_extra_badge:
apply (fastforce simp:ipc_frame_wp_at_def obj_at_def)
apply (simp add:ipc_buffer_wp_at_def obj_at_def)
apply (clarsimp simp:msg_max_length_def max_ipc_words_def buffer_cptr_index_def
capTransferDataSize_def msgMaxLength_def msgMaxExtraCaps_def msgExtraCapBits_def msg_align_bits)
apply (simp add:of_nat_mult)
capTransferDataSize_def msgMaxLength_def msgMaxExtraCaps_def
msgExtraCapBits_def msg_align_bits)
apply (simp)
apply (clarsimp simp:get_ipc_buffer_def gets_the_def exs_valid_def gets_def
get_def bind_def return_def assert_opt_def fail_def split:option.splits | rule conjI)+
get_def bind_def return_def assert_opt_def fail_def
split:option.splits | rule conjI)+
apply (subgoal_tac "s = transform s'")
prefer 2
apply simp+
@ -981,7 +983,7 @@ lemma dcorres_set_extra_badge:
apply (clarsimp simp:cte_wp_at_cases obj_at_def)
apply (drule_tac t = "tcb_ipcframe obj" in sym)
apply (fastforce simp:ipc_frame_wp_at_def obj_at_def)
done
done
definition
"dest_of xs \<equiv> case xs of [] \<Rightarrow> None | [r] \<Rightarrow> Some (transform_cslot_ptr r)"
@ -1013,12 +1015,12 @@ lemma evalMonad_thread_get_eq:
apply (clarsimp simp:gets_the_def gets_def get_def bind_def return_def assert_opt_def)
apply (case_tac "get_tcb x b")
apply (clarsimp simp:return_def fail_def evalMonad_def split:option.splits)+
done
done
lemma evalMonad_lookup_ipc_buffer_wp:
assumes cte_wp:"\<And>P slot. (\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c)
\<Longrightarrow> \<lbrace>cte_wp_at (P and op\<noteq> cap.NullCap) slot\<rbrace> f \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace>"
assumes tcb_wp:"\<And>P buf t. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> f \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t \<rbrace>"
assumes tcb_wp:"\<And>buf t. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> f \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t \<rbrace>"
shows "\<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace>"
apply (simp add:valid_def lookup_ipc_buffer_def)
apply (subst evalMonad_compose)
@ -1037,6 +1039,7 @@ shows "\<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some
apply wp
apply (clarsimp simp:evalMonad_get_cap split:option.split_asm cap.split_asm)
apply (drule caps_of_state_cteD)
apply (rename_tac arch_cap)
apply (frule_tac P1 = "op = (cap.ArchObjectCap arch_cap)" in use_valid[OF _ cte_wp])
apply (clarsimp simp:is_cap_simps)
apply (erule cte_wp_at_weakenE)
@ -1049,7 +1052,7 @@ shows "\<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some
apply (case_tac arch_cap)
apply simp_all
apply (clarsimp simp:evalMonad_def return_def split:if_splits)
done
done
crunch ipc_buffer_wp_at[wp]: update_cdt "ipc_buffer_wp_at buf t"
(wp: crunch_wps simp: crunch_simps Retype_A.detype_def set_cdt_def ipc_buffer_wp_at_def ignore:clearMemory)
@ -1065,7 +1068,7 @@ lemma ipc_buffer_wp_set_cap[wp]:
apply (simp add:get_object_def gets_def get_def bind_def return_def assert_def fail_def valid_def)
apply (clarsimp split:Structures_A.kernel_object.splits simp:return_def set_object_def fail_def get_def put_def bind_def)
apply (rule conjI|clarsimp simp:ipc_buffer_wp_at_def obj_at_def)+
done
done
lemma ipc_buffer_wp_at_cap_insert_ext[wp]:
"\<lbrace>ipc_buffer_wp_at buf t \<rbrace> cap_insert_ext src_parent src_slot dest_slot src_p dest_p \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>"
@ -1221,22 +1224,18 @@ next
apply (rule hoare_pre)
apply (rule cap_insert_weak_cte_wp_at_not_null)
apply clarsimp+
apply (wp cap_insert_idle valid_irq_node_typ
hoare_vcg_ball_lift cap_insert_cte_wp_at)
apply (wp cap_insert_idle valid_irq_node_typ hoare_vcg_ball_lift cap_insert_cte_wp_at)
apply (rule validE_validE_R)
apply (wp whenE_throwError_wp)[1]
apply wp
apply (clarsimp)
apply (rule hoareE_TrueI)
apply (rule validE_R_validE)
apply (simp add:conj_ac ball_conj_distrib
split del:if_splits
del:split_paired_Ex split_paired_All split_paired_Ball split_paired_Bex
split_paired_all)
apply (simp add:conj_comms ball_conj_distrib split del:split_if)
apply (rule_tac Q' ="\<lambda>cap' s. (cap'\<noteq> cap.NullCap \<longrightarrow>(
(cte_wp_at (is_derived (cdt s) (slot_ptr, slot_idx) cap') (slot_ptr, slot_idx) s)
\<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_objs s \<and> valid_idle s
\<and> valid_mdb s \<and> ?QM s cap'))"
\<and> valid_mdb s \<and> QM s cap'))" for QM
in hoare_post_imp_R)
prefer 2
apply (subgoal_tac "r\<noteq> cap.NullCap \<longrightarrow> cte_wp_at (op \<noteq> cap.NullCap) (slot_ptr, slot_idx) s")
@ -1266,14 +1265,11 @@ next
apply (clarsimp split del: split_if)
apply (clarsimp simp: cte_wp_at_caps_of_state not_idle_thread_def)
apply (rule conjI)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def
obj_at_def is_cap_table_def)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def obj_at_def is_cap_table_def)
apply (rule conjI)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def
obj_at_def is_cap_table_def)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def obj_at_def is_cap_table_def)
apply (rule conjI)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def
obj_at_def is_cap_table_def)
apply (clarsimp simp: not_idle_thread_def valid_idle_def st_tcb_at_def obj_at_def is_cap_table_def)
apply (rule conjI)
apply (rule rev_mp[OF _ real_cte_tcb_valid])
apply simp
@ -1360,9 +1356,11 @@ lemma get_receive_slot_dcorres:
apply (simp add:tcb_slot_pending_ipc_neq[symmetric])
apply (case_tac "tcb_ipcframe obj")
apply (simp_all add:dest_of_def)
apply (rename_tac arch_cap)
apply (case_tac "arch_cap")
apply (simp_all add:dest_of_def)
apply (clarsimp simp:transform_cap_def)
apply (rename_tac word set vm opt)
apply (drule_tac x = word in spec)
apply (drule_tac x = "set" in spec)
apply (clarsimp simp:cte_wp_at_cases dest!:get_tcb_SomeD)
@ -1451,6 +1449,7 @@ lemma dcorres_dummy_corrupt_ipc_buffer:
apply simp_all
apply (rule corres_guard_imp[OF dummy_corrupt_tcb_intent_corres]
,(clarsimp simp:not_idle_thread_def tcb_at_def)+)+
apply (rename_tac arch_cap etcb)
apply (case_tac "arch_cap")
apply simp_all
apply (rule corres_guard_imp[OF dummy_corrupt_tcb_intent_corres]
@ -1609,7 +1608,7 @@ lemma dcorres_copy_mrs':
apply (rule corres_split[OF _ set_registers_corres])
apply (rule corres_symb_exec_r)+
apply (rule corres_trivial[OF corres_free_return])
apply (wp|clarsimp simp:option.cases split:option.splits)+
apply (wp|clarsimp split:option.splits)+
apply (clarsimp simp:get_ipc_buffer_def gets_the_def exs_valid_def gets_def
get_def bind_def return_def assert_opt_def fail_def split:option.splits | rule conjI)+
apply (frule(1) tcb_at_is_etcb_at, clarsimp simp: is_etcb_at_def, fold get_etcb_def)
@ -1644,7 +1643,10 @@ lemma dcorres_copy_mrs':
done
lemma opt_cap_valid_etcbs: "\<lbrakk>tcb_at ptr s; valid_etcbs s; ptr \<noteq> idle_thread s; sl \<in> tcb_abstract_slots \<or> sl = tcb_pending_op_slot\<rbrakk> \<Longrightarrow> \<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap"
lemma opt_cap_valid_etcbs:
"\<lbrakk>tcb_at ptr s; valid_etcbs s; ptr \<noteq> idle_thread s;
sl \<in> tcb_abstract_slots \<or> sl = tcb_pending_op_slot\<rbrakk> \<Longrightarrow>
\<exists>cap. opt_cap (ptr, sl) (transform s) = Some cap"
apply (clarsimp simp: tcb_at_def)
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp: opt_cap_tcb)
@ -1741,6 +1743,7 @@ shows "\<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some
apply (fastforce simp:evalMonad_def return_def)
apply (clarsimp simp:evalMonad_get_cap split:option.split_asm cap.split_asm)
apply (drule caps_of_state_cteD)
apply (rename_tac arch_cap)
apply (frule_tac P1 = "op = (cap.ArchObjectCap arch_cap)" in use_valid[OF _ cte_wp])
apply (erule cte_wp_at_weakenE)
apply clarsimp
@ -1757,7 +1760,7 @@ done
lemma ipc_buffer_wp_at_copy_mrs[wp]:
"\<lbrace>ipc_buffer_wp_at buf t \<rbrace> copy_mrs send rva recv rv (mi_length (data_to_message_info (tcb_context obj' msg_info_register)))
\<lbrace>\<lambda>r. ipc_buffer_wp_at buf t\<rbrace>"
apply (simp add:copy_mrs_def)
unfolding copy_mrs_def
apply (wp|wpc)+
apply (wp mapM_wp)
apply (simp add:store_word_offs_def ipc_buffer_wp_at_def)
@ -1769,7 +1772,8 @@ lemma ipc_buffer_wp_at_copy_mrs[wp]:
apply (wp mapM_wp)
apply fastforce
apply (clarsimp)
done
apply wp
done
lemma copy_mrs_valid_irq_node:
"\<lbrace>valid_irq_node\<rbrace> copy_mrs a b c d e
@ -2207,6 +2211,7 @@ lemma recv_sync_ipc_corres:
apply (simp add:valid_state_def)
apply simp
apply (clarsimp simp:option_select_def valid_ep_abstract_def)
apply (rename_tac list)
apply (drule_tac s = "set list" in sym)
apply (rule conjI, clarsimp dest!: not_empty_list_not_empty_set)
apply (clarsimp simp:neq_Nil_conv)
@ -2386,6 +2391,7 @@ lemma send_sync_ipc_corres:
apply (clarsimp simp:valid_ep_abstract_def split del:if_splits)
apply (subst option_select_not_empty)
apply (clarsimp simp: dest!: not_empty_list_not_empty_set)
apply (rename_tac list)
apply (drule_tac s = "set list" in sym)
apply (clarsimp simp: bind_assoc neq_Nil_conv)
apply (rule_tac P1="\<top>" and P'="op = s'a" and x1 = y
@ -2452,11 +2458,6 @@ lemma send_sync_ipc_corres:
apply fastforce
done
lemma dcorres_injection_handler_rhs:
"dcorres (dc \<oplus> r) P P' f g
\<Longrightarrow> dcorres (dc \<oplus> r) P P' f (injection_handler h g)"
by (rule KHeap_DR.dcorres_injection_handler_rhs)
lemma not_idle_thread_resolve_address_bits:
"\<lbrace>valid_global_refs and valid_objs and valid_idle and valid_irq_node and ko_at (TCB obj) thread\<rbrace>
CSpace_A.resolve_address_bits (tcb_ctable obj, blist)

288
proof/drefine/KHeap_DR.thy
View File

@ -76,9 +76,17 @@ lemma cap_table_at_cte_wp_at_length:
apply auto
done
context
begin
(* avoid spurious warning in termination proof below *)
declare CSpace_D.resolve_address_bits.simps [simp del]
termination CSpace_D.resolve_address_bits
by (relation "measure (\<lambda>(a,b,c). c)") (clarsimp simp:in_monad)+
end
crunch cdl_cdt [wp]: "KHeap_D.set_cap" "\<lambda>s. P (cdl_cdt s)"
(wp: crunch_wps select_wp simp: crunch_simps)
@ -297,8 +305,7 @@ lemma caps_of_state_transform_opt_cap:
transform_def transform_objects_def object_slots_def
valid_irq_node_def obj_at_def is_cap_table_def
transform_tcb_def tcb_slot_defs
tcb_pending_op_slot_def tcb_cap_cases_def
bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
tcb_cap_cases_def bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0
split: split_if_asm)
done
@ -331,7 +338,7 @@ lemma get_cap_no_fail:
apply (simp add:dom_def assert_opt_def corres_free_fail)
apply (simp add:assert_opt_def corres_free_fail)
apply auto
done
done
lemma get_cap_helper:
"dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at (op=cap) slot)) f (g cap)"
@ -350,6 +357,7 @@ lemma get_cap_corres:
apply (clarsimp simp:assert_def corres_free_fail assert_opt_def)
apply (case_tac y)
apply (simp_all add:assert_def corres_free_fail)
apply (rename_tac nat "fun")
apply (case_tac "fun b")
apply (simp add:corres_free_fail)
apply clarsimp
@ -362,21 +370,20 @@ lemma get_cap_corres:
done
definition
opt_cap_wp_at :: "(cdl_cap \<Rightarrow> bool) \<Rightarrow> (cdl_object_id \<times> nat) \<Rightarrow> cdl_state \<Rightarrow> bool"
where "opt_cap_wp_at P slot s \<equiv> \<exists>cap. fst (KHeap_D.get_cap slot s) = {(cap, s)} \<and> P cap"
opt_cap_wp_at :: "(cdl_cap \<Rightarrow> bool) \<Rightarrow> (cdl_object_id \<times> nat) \<Rightarrow> cdl_state \<Rightarrow> bool"
where
"opt_cap_wp_at P slot s \<equiv> \<exists>cap. fst (KHeap_D.get_cap slot s) = {(cap, s)} \<and> P cap"
lemma opt_cap_wp_at_def':
"opt_cap_wp_at P slot s = (case (opt_cap slot s) of Some a \<Rightarrow> P a | _ \<Rightarrow> False) "
apply (clarsimp simp:opt_cap_wp_at_def opt_cap_def gets_the_def gets_def get_def return_def assert_opt_def bind_def)
apply (auto simp:fail_def return_def split:option.splits)
done
done
lemma nat2p: "nat (2^(x::nat)) = 2^(x::nat)"
by (rule nat_int.Rep_inverse',simp)
thm cap_counts_def
lemma nat_to_bl_bl_to_bin:
lemma nat_to_bl_to_bin:
"nat_to_bl bits n = Some xs \<Longrightarrow> n = nat (bl_to_bin xs)"
apply (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p)
apply (subst mod_pos_pos_trivial,simp_all)
@ -395,11 +402,10 @@ shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<
apply (rule_tac x = ptr in exI)
apply (clarsimp simp:transform_objects_def restrict_map_Some_iff object_slots_def split:cdl_object.splits)
apply (frule assms)
apply (clarsimp simp:cte_wp_at_cases
transform_object_def transform_tcb_def
tcb_pending_op_slot_def
split:Structures_A.kernel_object.splits nat.splits
arch_kernel_object.splits if_splits | drule(1) valid_etcbs_tcb_etcb)+
apply (clarsimp simp: cte_wp_at_cases transform_object_def transform_tcb_def tcb_pending_op_slot_def
split: Structures_A.kernel_object.splits nat.splits
arch_kernel_object.splits if_splits
| drule(1) valid_etcbs_tcb_etcb)+
apply (clarsimp simp:cap_counts_def infer_tcb_pending_op_def split:Structures_A.thread_state.splits nat.splits)
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 4" in exI)
@ -416,19 +422,20 @@ shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<
using transform_tcb_slot_simp[simplified,symmetric]
apply (rule_tac x= "tcb_cnode_index 0" in exI)
apply (clarsimp)
apply (rename_tac arch_kernel_obj)
apply (case_tac arch_kernel_obj,simp_all)
apply (simp_all add:object_slots_def transform_object_def)
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = x2b in exI,simp add: nat_to_bl_bl_to_bin)
apply (rule_tac x = x2b in exI,simp add: nat_to_bl_to_bin)
apply (drule(1) valid_etcbs_tcb_etcb, simp)
prefer 6 (* IRQ Node *)
apply (clarsimp split: Structures_A.kernel_object.splits nat.splits option.splits)
apply (clarsimp simp:transform_cnode_contents_def option_map_join_def
split:option.splits Structures_A.kernel_object.splits nat.splits)
apply (clarsimp simp:cte_wp_at_cases well_formed_cnode_invsI transform_cslot_ptr_def split:if_splits)
apply (rule_tac x = x2a in exI,simp add: nat_to_bl_bl_to_bin)
apply (rule_tac x = x2a in exI,simp add: nat_to_bl_to_bin)
apply (frule assms)
apply ((simp_all add:Let_def cap_counts_def transform_tcb_def
split:option.splits if_splits arch_kernel_obj.splits
@ -437,13 +444,11 @@ shows "\<lbrakk>opt_cap_wp_at P slot (transform s);valid_objs s; valid_etcbs s\<
clarsimp simp: unat_map_def transform_page_table_contents_def cap_counts_def
transform_page_directory_contents_def transform_asid_pool_contents_def
transform_pte_def transform_pde_def transform_asid_pool_entry_def
split:option.splits if_splits ARM_Structs_A.pte.splits ARM_Structs_A.pde.splits
dest!:assms)+)
done
lemma eqset_imp': "A = B \<Longrightarrow> \<forall>x. ((x\<in> A) = (x\<in> B))"
by auto
lemma eqset_imp': "A = B \<Longrightarrow> \<forall>x. ((x\<in> A) = (x\<in> B))" by simp
lemma eq_singleton_set: "\<lbrakk>A = f` B; \<forall>x\<in>B. \<forall>y\<in> B. x\<noteq> y \<longrightarrow> f x\<noteq> f y \<rbrakk>\<Longrightarrow> (\<exists>a. A = {a}) = (\<exists>b. B = {b})"
apply (subgoal_tac "card A = card B")
@ -466,23 +471,21 @@ lemma final_cap_set_map:
apply (rule_tac x=ba in exI)
apply simp+
apply (erule cte_wp_at_weakenE_customised)
(*defer till the otherway around comes up*)
defer
(*defer till the otherway around comes up*)
defer
apply (clarsimp simp:image_def opt_cap_wp_at_def')
apply (drule iffD1[OF cte_wp_at_caps_of_state])
apply clarsimp
apply (frule caps_of_state_transform_opt_cap, simp)
apply clarsimp
apply (frule valid_idle_has_null_cap)
(*It is true since idle thread should not get any cap installed *)
(*It is true since idle thread should not get any cap installed *)
apply simp+
apply (thin_tac "opt_cap ?x ?y = ?Q")
apply (thin_tac "opt_cap x y = Q" for x y Q)
apply (auto simp: transform_cap_def cap_has_object_def cap_object_simps
cap_counts_def
cdl_cap_irq_def
cap_counts_def cdl_cap_irq_def
split: cap.splits arch_cap.splits split_if_asm)
done
done
lemma opt_cap_wp_at_ex_opt_cap:
"opt_cap_wp_at P p s = (\<exists>cap'. opt_cap p s = Some cap' \<and> P cap')"
@ -518,7 +521,7 @@ lemma is_final_cap_corres:
apply (case_tac cap)
apply (clarsimp simp:cap_counts_def transform_cap_def)+
apply (clarsimp split:arch_cap.splits cap.splits)
done
done
lemma dcorres_exec_is_final_cap:
assumes c: "\<And>final. dcorres r (P final) P' (f final) f'"
@ -541,11 +544,11 @@ lemma corres_dummy_set_async_ep:
apply (simp add: set_async_ep_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: corres_free_fail assert_def
split:option.splits Structures_A.kernel_object.splits)
split: option.splits Structures_A.kernel_object.splits)
apply (rule corres_free_set_object)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (subst transform_objects_update_kheap_same_caps)
apply (simp add:caps_of_object.simps a_type_def transform_objects_update_same)+
apply (simp add: a_type_def transform_objects_update_same)+
done
lemma corres_dummy_set_sync_ep:
@ -553,12 +556,12 @@ lemma corres_dummy_set_sync_ep:
apply (simp add: set_endpoint_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp: corres_free_fail assert_def
split:option.splits Structures_A.kernel_object.splits)
split: option.splits Structures_A.kernel_object.splits)
apply (rule corres_free_set_object)
apply (clarsimp simp:transform_def transform_current_thread_def)
apply (subst transform_objects_update_kheap_same_caps)
apply (simp add:caps_of_object.simps a_type_def transform_objects_update_same)+
done
apply (simp add: a_type_def transform_objects_update_same)+
done
lemma thread_set_fault_corres:
assumes r: "\<And>t. f (tcb_has_fault (t::Structures_A.tcb)) = (case (ft (tcb_fault t)) of None \<Rightarrow> False | _ \<Rightarrow> True)"
@ -570,14 +573,13 @@ lemma thread_set_fault_corres:
apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:opt_object_tcb not_idle_thread_def transform_tcb_def)
apply (rule dcorres_set_object_tcb)
apply (clarsimp simp:transform_tcb_def tcb_at_def
cong:transform_full_intent_cong
dest!:get_tcb_SomeD get_etcb_SomeD )
apply (clarsimp simp: transform_tcb_def tcb_at_def cong: transform_full_intent_cong
dest!: get_tcb_SomeD get_etcb_SomeD )
apply (cut_tac t = obj' in r)
apply (clarsimp split:option.splits)
apply ((clarsimp simp:opt_object_tcb tcb_at_def get_etcb_def dest!:get_tcb_SomeD get_etcb_SomeD)+)[3]
apply (clarsimp, drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp simp:opt_object_tcb not_idle_thread_def get_etcb_def)
done
done
lemma get_object_corres:
"ptr = ptr' \<Longrightarrow>
@ -588,8 +590,7 @@ lemma get_object_corres:
apply (rule corres_split'[OF _ _ gets_sp gets_sp, where r'=dc])
apply simp
apply (clarsimp simp: assert_def corres_free_fail split: split_if)
apply (rule_tac F="rv = Some (transform_object undefined 0 etcb' y)"
in corres_req)
apply (rule_tac F="rv = Some (transform_object undefined 0 etcb' y)" in corres_req)
apply (simp_all add: assert_opt_def)
apply (clarsimp simp: opt_object_def transform_def transform_objects_def
not_idle_thread_def obj_at_def)
@ -608,25 +609,9 @@ lemma xf_cnode_contents:
unfolding transform_cnode_contents_def
apply clarsimp
apply (frule (1) wf_cs_nD [symmetric], simp)
apply (simp add: nat_to_bl_id2 word_bits_conv option_map_join_simps
option_map_join_def)
apply (simp add: nat_to_bl_id2 word_bits_conv option_map_join_simps option_map_join_def)
done
lemma nat_to_bl_to_bin:
"\<lbrakk> well_formed_cnode_n sz cn; cn sl' = Some ocap'; nat_to_bl sz x = Some sl' \<rbrakk>
\<Longrightarrow> x = nat (bl_to_bin sl')"
unfolding nat_to_bl_def
apply (clarsimp simp: bin_bl_bin' bintrunc_mod2p)
apply (subst int_mod_eq')
apply (clarsimp simp: not_leE)
apply (drule not_leE)
apply (drule iffD2[OF zless_int])
apply (clarsimp)
apply simp
done
lemma transform_cnode_contents_upd:
"\<lbrakk>well_formed_cnode_n sz cn; cn sl' = Some ocap'\<rbrakk> \<Longrightarrow>
transform_cnode_contents sz cn(nat (bl_to_bin sl') \<mapsto> transform_cap cap') =
@ -722,7 +707,8 @@ lemma transform_full_intent_same_cap:
apply simp
apply (simp add: is_cap_simps)
apply (cases "tcb_ipcframe tcb", simp_all)
apply (simp add:transform_cap_def is_cap_simps split:cap.splits split_if_asm arch_cap.splits cong:if_weak_cong)+
apply (simp add:transform_cap_def is_cap_simps
split:cap.splits split_if_asm arch_cap.splits)+
done
lemma set_cap_corres:
@ -777,7 +763,7 @@ proof -
update_slots_def
split del: split_if)
apply (case_tac "nat (bl_to_bin sl') = tcb_ipcbuffer_slot")
apply (simp add: tcb_slot_defs tcb_pending_op_slot_def)
apply (simp add: tcb_slot_defs)
apply (clarsimp simp: bl_to_bin_tcb_cnode_index|rule conjI)+
apply (rule corres_guard_imp)
apply (rule select_pick_corres)
@ -785,8 +771,7 @@ proof -
apply (clarsimp simp: transform_tcb_def)
apply (rule conjI)
apply (rule ext)
apply (clarsimp simp: transform_tcb_def tcb_slot_defs
tcb_pending_op_slot_def)
apply (clarsimp simp: transform_tcb_def tcb_slot_defs)
apply (rule refl)
apply assumption
apply simp
@ -798,8 +783,7 @@ proof -
apply (clarsimp simp: transform_tcb_def)
apply (rule conjI)
apply (rule ext)
apply (clarsimp simp: transform_tcb_def tcb_slot_defs
tcb_pending_op_slot_def )
apply (clarsimp simp: transform_tcb_def tcb_slot_defs)
apply (erule transform_full_intent_same_cap)
apply simp
apply simp
@ -808,8 +792,7 @@ proof -
apply (rule conjI)
apply (clarsimp simp: bl_to_bin_tcb_cnode_index)
apply (rule conjI ext dcorres_set_object_tcb|simp|
clarsimp simp: transform_tcb_def tcb_slot_defs tcb_pending_op_slot_def
corres_free_fail
clarsimp simp: transform_tcb_def tcb_slot_defs corres_free_fail
cong: transform_full_intent_caps_cong_weak)+
done
qed
@ -840,16 +823,13 @@ lemma set_pending_cap_corres:
apply (frule opt_object_tcb[rotated, rotated])
apply (fastforce simp:get_tcb_def)
apply (fastforce simp:get_etcb_rev)
apply (clarsimp simp:assert_opt_def has_slots_def
transform_tcb_def object_slots_def update_slots_def)
apply (clarsimp simp:corres_underlying_def in_monad
set_object_def KHeap_D.set_object_def simpler_modify_def)
apply (clarsimp simp:assert_opt_def has_slots_def transform_tcb_def object_slots_def update_slots_def)
apply (clarsimp simp:corres_underlying_def in_monad set_object_def KHeap_D.set_object_def simpler_modify_def)
apply (simp add:transform_def transform_current_thread_def)
apply (rule ext)
apply (subst transform_objects_update_kheap_same_caps)
apply (simp add:obj_at_def transform_tcb_def
not_generates_pending_is_null)+
done
apply (simp add:obj_at_def transform_tcb_def not_generates_pending_is_null)+
done
lemma transform_scheduler_action_update[simp]: "transform (s\<lparr> scheduler_action := a \<rparr>) = transform s"
by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)
@ -866,7 +846,8 @@ lemma set_thread_state_ext_dcorres: "dcorres dc P P' (return ()) (set_thread_sta
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_symb_exec_r)
apply (clarsimp simp: corres_underlying_def when_def set_scheduler_action_def
modify_def bind_def put_def gets_def get_def return_def split: option.splits)
modify_def bind_def put_def gets_def get_def return_def
split: option.splits)
apply wp
done
@ -884,7 +865,7 @@ lemma set_thread_state_corres:
apply simp
apply (clarsimp dest!:get_tcb_SomeD simp:obj_at_def)
apply (rule hoare_TrueI)+
done
done
lemma set_cap_null_cap_corres:
"dcorres dc \<top> (valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs)
@ -913,14 +894,14 @@ lemma mdb_cte_at_cte_wp_at:
apply (case_tac slot,case_tac slot')
apply (drule spec)+
apply (auto)
done
done
lemma mdb_cte_at_cte_wp_at':
"\<lbrakk>mdb_cte_at (swp (cte_wp_at (op \<noteq> cap.NullCap)) s) (cdt s); cdt s slot = Some slot'\<rbrakk>
\<Longrightarrow>(cte_wp_at (op\<noteq> cap.NullCap) slot' s)"
apply (case_tac slot,case_tac slot')
apply (clarsimp simp:mdb_cte_at_def)
done
done
lemma transform_cdt_slot_inj_on_mdb_cte_at:
@ -1372,7 +1353,7 @@ lemma empty_slot_corres:
apply (subgoal_tac "cap \<noteq> cdl_cap.NullCap")
apply clarsimp
apply (rule dcorres_gets_all_param)
apply (rule_tac P="%a. dcorres dc ?P ?P' ?h a" in subst[OF bind_assoc[where m="gets cdt"]])
apply (rule_tac P="%a. dcorres dc P P' h a" for P P' h in subst[OF bind_assoc[where m="gets cdt"]])
apply (rule corres_split [where r'="dc"])
apply (rule corres_add_noop_lhs)
apply (rule_tac P'="\<lambda>_. valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)" in corres_underlying_split)
@ -1403,7 +1384,7 @@ lemma empty_slot_corres:
lemma valid_idle_fast_finalise[wp]:
"\<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>%r. valid_idle\<rbrace>"
apply (case_tac p)
apply (simp_all add:fast_finalise.simps)
apply (simp_all)
apply (wp,simp add:valid_state_def invs_def)
apply (rule hoare_post_imp[where Q="%r. invs"])
apply (clarsimp simp:valid_state_def invs_def,wp ep_cancel_all_invs)
@ -1413,12 +1394,11 @@ lemma valid_idle_fast_finalise[wp]:
apply clarsimp
apply wp
apply (simp add:valid_state_def invs_def)
done
done
lemma valid_irq_node_fast_finalise[wp]:
"\<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>%r. valid_irq_node\<rbrace>"
apply (case_tac p)
apply (simp_all add:fast_finalise.simps)
apply (case_tac p; simp)
apply (wp,simp add:valid_state_def invs_def)
apply (rule hoare_post_imp[where Q="%r. invs"])
apply (clarsimp simp:valid_state_def invs_def,wp ep_cancel_all_invs)
@ -1428,12 +1408,11 @@ lemma valid_irq_node_fast_finalise[wp]:
apply clarsimp
apply wp
apply (simp add:valid_state_def invs_def)
done
done
lemma invs_mdb_fast_finalise[wp]:
"\<lbrace>invs\<rbrace> IpcCancel_A.fast_finalise p q \<lbrace>%r. valid_mdb\<rbrace>"
apply (case_tac p)
apply (simp_all add:fast_finalise.simps)
apply (case_tac p; simp)
apply (wp,simp add:valid_state_def invs_def)
apply (rule hoare_post_imp[where Q="%r. invs"])
apply (clarsimp simp:valid_state_def invs_def,wp ep_cancel_all_invs)
@ -1461,7 +1440,7 @@ lemma block_lift:
apply (clarsimp simp:is_thread_blocked_on_endpoint_def transform_tcb_def infer_tcb_pending_op_def)
apply (case_tac "tcb_state tcb_type")
apply (auto)
done
done
(* Before we handle fast_finalise, we need sth form invs that can give us some preconditions of ep and aep *)
@ -1715,6 +1694,7 @@ lemma get_endpoint_pick:
apply (clarsimp simp: ep_waiting_set_send_def sym_refs_def)
apply (drule_tac x = x in spec)
apply (clarsimp simp:state_refs_of_def)
apply (rename_tac list)
apply clarsimp
apply (subgoal_tac "ko_at (Endpoint (Structures_A.endpoint.RecvEP list)) epptr s
\<and> ko_at (Endpoint (Structures_A.endpoint.RecvEP list)) p' s")
@ -1722,13 +1702,14 @@ lemma get_endpoint_pick:
apply (drule(1) sym_refs_ko_atD)+
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_def2)
apply (clarsimp simp: obj_at_def)
apply (rename_tac list p')
apply (subgoal_tac "ko_at (Endpoint (Structures_A.endpoint.SendEP list)) epptr s
\<and> ko_at (Endpoint (Structures_A.endpoint.SendEP list)) p' s")
apply (clarsimp simp: neq_Nil_conv)
apply (drule(1) sym_refs_ko_atD)+
apply (clarsimp simp: st_tcb_at_refs_of_rev st_tcb_def2)
apply (clarsimp simp:obj_at_def)
done
done
lemma get_async_ep_pick:
"\<lbrakk>kheap s epptr = Some (kernel_object.AsyncEndpoint async_ep);
@ -1771,6 +1752,7 @@ lemma get_async_ep_pick:
apply (clarsimp split:Structures_A.async_ep.splits)
apply (clarsimp simp:refs_of_def tcb_st_refs_of_def ep_q_refs_of_def aep_q_refs_of_def
split:Structures_A.kernel_object.splits)+
apply (rename_tac list p')
apply (subgoal_tac "ko_at (AsyncEndpoint (async_ep.WaitingAEP list)) epptr s
\<and> ko_at (AsyncEndpoint (async_ep.WaitingAEP list)) p' s")
apply (clarsimp simp: neq_Nil_conv)
@ -1783,7 +1765,7 @@ lemma get_async_ep_pick:
apply (clarsimp simp:aep_waiting_set_def)
apply (drule_tac x=x in spec)
apply (clarsimp simp: state_refs_of_def)
done
done
definition tcb_filter_modify ::"cdl_object_id set\<Rightarrow>(cdl_object option \<Rightarrow> cdl_object option)\<Rightarrow> unit k_monad"
where "tcb_filter_modify filter_set f \<equiv> modify
@ -1800,7 +1782,7 @@ lemma tcb_filter_modify_decompose:
apply (rule ext)
apply (clarsimp split:option.splits|rule conjI)+
apply (fastforce)
done
done
lemma set_list_modify_corres_helper:
"\<lbrakk> distinct update_list;
@ -1811,7 +1793,7 @@ lemma set_list_modify_corres_helper:
\<rbrakk> \<Longrightarrow> dcorres dc \<top> (\<lambda>s. \<forall>x\<in>(set update_list). (P x s)) (tcb_filter_modify filter_set f)
(mapM_x (\<lambda>t. f' t) update_list)"
apply simp
apply (thin_tac " filter_set = lift_func ` set update_list")
apply (thin_tac "filter_set = lift_func ` set update_list")
proof (induct update_list)
case Nil
show ?case
@ -1916,7 +1898,7 @@ lemma set_ep_exec_wp:
apply (simp add:get_object_def)
apply wp
apply (clarsimp split:Structures_A.kernel_object.splits)
done
done
lemma set_aep_exec_wp:
"\<lbrace>op = s\<rbrace> set_async_ep epptr ep \<lbrace>\<lambda>r s'. s' = update_kheap ((kheap s)(epptr \<mapsto> AsyncEndpoint ep)) s\<rbrace> "
@ -2332,9 +2314,7 @@ lemma fast_finalise_wait_aep:
apply (clarsimp simp:valid_aep_abstract_def aep_waiting_set_def)
apply (drule_tac ptr=x in valid_etcbs_tcb_etcb)
apply (auto simp: is_etcb_at_def)
done
done
lemma dcorres_ep_cancel_all:
"dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.ep_cancel_all oid)
@ -2343,6 +2323,7 @@ lemma dcorres_ep_cancel_all:
apply (clarsimp simp:get_endpoint_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits)
apply (rename_tac endpoint)
apply (case_tac endpoint)
apply (clarsimp simp:ep_cancel_all_def_alt1)
apply (rule dcorres_absorb_get_l)
@ -2362,7 +2343,7 @@ lemma dcorres_ep_cancel_all:
apply (rule corres_guard_imp)
apply (rule fast_finalise_recv_ep)
apply (simp add:obj_at_def)+
done
done
lemma dcorres_aep_cancel_all:
"dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.ep_cancel_all oid)
@ -2370,6 +2351,7 @@ lemma dcorres_aep_cancel_all:
apply (clarsimp simp: aep_cancel_all_def get_async_ep_def get_object_def bind_assoc gets_def)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_def corres_free_fail split:Structures_A.kernel_object.splits)
apply (rename_tac async_ep)
apply (case_tac async_ep)
apply (clarsimp simp:ep_cancel_all_def_alt1)
apply (rule dcorres_absorb_get_l)
@ -2405,12 +2387,9 @@ done
lemma fast_finalise_corres:
"dcorres dc \<top> (valid_state and valid_idle and valid_etcbs) (PageTableUnmap_D.fast_finalise (transform_cap rv') final)
(IpcCancel_A.fast_finalise rv' final)"
apply (case_tac rv')
apply (simp_all add:transform_cap_def)
apply (simp_all add:PageTableUnmap_D.fast_finalise_def fast_finalise.simps PageTableUnmap_D.fast_finalise.simps corres_free_fail)
apply (simp_all add:when_def)
apply (clarsimp simp:dcorres_ep_cancel_all)
apply (clarsimp simp:dcorres_aep_cancel_all)
apply (case_tac rv';
simp add: transform_cap_def corres_free_fail when_def
dcorres_ep_cancel_all dcorres_aep_cancel_all)
done
lemma cdl_cdt_transform:
@ -2452,17 +2431,17 @@ lemma set_parent_corres:
apply (clarsimp simp:cdl_cdt_transform)
apply (rule ext)
apply (clarsimp split:if_splits)
done
done
lemma set_tcb_capslot_weak_valid_mdb:
"\<lbrace>weak_valid_mdb and cte_wp_at (op=cap.NullCap) slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r s. weak_valid_mdb s\<rbrace> "
apply (simp add: weak_valid_mdb_def cte_wp_at_caps_of_state swp_def)
apply (wp set_cap_caps_of_state2)
apply (case_tac slot)
apply (clarsimp simp:valid_def set_cap_def cte_wp_at_caps_of_state weak_valid_mdb_def swp_def cte_wp_at_caps_of_state)
apply (clarsimp simp: valid_def set_cap_def cte_wp_at_caps_of_state weak_valid_mdb_def swp_def)
apply (simp only: mdb_cte_at_def)
apply fastforce
done
done
lemma get_tcb_reply_cap_wp_cte_at:
"\<lbrace>tcb_at sid and valid_objs and cte_wp_at (op\<noteq> cap.NullCap) (sid, tcb_cnode_index 2)\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
@ -2478,7 +2457,7 @@ lemma get_tcb_reply_cap_wp_cte_at:
apply (rule tcb_cap_wp_at)
apply (simp add:dom_tcb_cap_cases)+
apply (clarsimp simp:cte_wp_at_def)
done
done
lemma get_tcb_reply_cap_wp_master_cap:
"\<lbrace>tcb_at sid and valid_objs and cte_wp_at (op\<noteq> cap.NullCap) (sid,tcb_cnode_index 2) \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
@ -2492,7 +2471,7 @@ lemma get_tcb_reply_cap_wp_master_cap:
apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)
apply (wp get_cap_cte_wp_at_rv)
apply (clarsimp simp:cte_wp_at_def)+
done
done
lemma get_tcb_reply_cap_wp_original_cap:
"\<lbrace>tcb_at sid and valid_objs and cte_wp_at (op\<noteq> cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
@ -2630,7 +2609,7 @@ lemma always_empty_slot_corres:
apply (rule always_empty_slot_NullCap_corres)
apply simp
apply (rule dcorres_gets_all_param)
apply (rule_tac P="%a. dcorres dc ?P ?P' ?h a" in subst[OF bind_assoc[where m="gets cdt"]])
apply (rule_tac P="%a. dcorres dc P P' h a" for P P' h in subst[OF bind_assoc[where m="gets cdt"]])
apply (rule corres_split [where r'="dc"])
apply (rule dcorres_rhs_noop_above[OF empty_slot_ext_dcorres])
apply (rule corres_bind_ignore_ret_rhs)
@ -2677,14 +2656,14 @@ lemma delete_cap_simple_corres:
apply simp
apply (clarsimp simp:not_idle_thread_def |wp get_cap_cte_wp_at_rv)+
apply (simp add:invs_def valid_state_def valid_pspace_def)+
done
done
lemma cap_delete_one_valid_mdb[wp]:
"\<lbrace>invs and emptyable slot\<rbrace> cap_delete_one slot \<lbrace>\<lambda>yc. valid_mdb\<rbrace>"
apply (rule hoare_post_imp [where Q="%x. invs"])
apply (simp add:invs_def valid_state_def valid_pspace_def)
apply (rule delete_one_invs)
done
apply (rule hoare_post_imp [where Q="%x. invs"])
apply (simp add:invs_def valid_state_def valid_pspace_def)
apply (rule delete_one_invs)
done
lemma thread_get_corres:
"\<lbrakk>did = thread; dcorres rv \<top> P' (f tcb) (g (t tcb')) \<rbrakk>
@ -2719,7 +2698,7 @@ lemma thread_get_corresE:
apply (simp add:liftE_def bindE_def lift_def)
apply (rule thread_get_corres)
apply simp+
done
done
definition in_terminate_branch :: "bool list \<Rightarrow> cap \<Rightarrow> bool"
where "in_terminate_branch ref cap \<equiv> case cap of
@ -2750,7 +2729,7 @@ lemma resolve_address_bits_error_branch2:
apply (clarsimp | rule conjI)+
apply (clarsimp simp:whenE_def | rule conjI)+
apply auto
done
done
lemma resolve_address_bits_terminate_branch:
"\<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk>
@ -2773,8 +2752,7 @@ lemmas cap_type_simps = cap_type_def[split_simps cdl_cap.split]
lemma is_cnode_cap_transform_cap:
"Types_D.is_cnode_cap (transform_cap cap) = is_cnode_cap cap"
apply (case_tac cap)
apply (simp_all add:transform_cap_def cap_type_simps
split:cdl_cap.splits arch_cap.splits)
apply (simp_all add:transform_cap_def cap_type_simps split:cdl_cap.splits arch_cap.splits)
done
lemma cdl_resolve_address_bits_error_branch1:
@ -2795,7 +2773,7 @@ lemma branch_map_simp1:
apply simp+
apply (drule_tac cref1=ref and cref'1="of_bl ref" in iffD2[OF guard_mask_shift,rotated])
apply (simp add: word_rep_drop)+
done
done
lemma take_drop:
"replicate n k @ a = (replicate n k @ (take s a)) @ (drop s a)"
@ -2806,7 +2784,7 @@ lemma branch_map_simp2:
\<Longrightarrow> unat ((((of_bl cref)::word32) >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))"
apply (subgoal_tac "take nata (drop (length list) cref) \<le> drop (length list) cref")
apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref"])
defer
defer
apply clarsimp
apply (subgoal_tac "nata\<le> length cref - length list")
apply (drule min.absorb2[where b = nata])
@ -2824,7 +2802,7 @@ defer
apply simp
apply (simp add:word_rep_drop)
apply (rule take_drop)
done
done
lemma resolve_address_bits_error_corres:
@ -2842,36 +2820,39 @@ lemma resolve_address_bits_error_corres:
apply simp+
apply (clarsimp)
apply (simp add:transform_cap_def cap_type_simps unlessE_def)
apply (clarsimp simp :in_terminate_branch_def in_recursive_branch_def | rule conjI)+
apply (clarsimp simp :assertE_def)
apply (clarsimp simp:get_cnode_def bind_assoc get_cnode_def liftE_bindE)
apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp simp: in_terminate_branch_def in_recursive_branch_def | rule conjI)+
apply (clarsimp simp: assertE_def get_cnode_def bind_assoc liftE_bindE)
apply (clarsimp simp: valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp split:Structures_A.kernel_object.splits)
apply (rename_tac "fun")
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (rule_tac Q="\<lambda>x y. y = transform s \<and> x =
transform_object (machine_state s) oref etcb_opt
apply (rule_tac Q="\<lambda>x y. y = transform s \<and>
x = transform_object (machine_state s) oref etcb_opt
(kernel_object.CNode radix_bits fun) "
in corres_symb_exec_l)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:whenE_def branch_map_simp1 split: nat.splits|rule conjI)+
apply (drule (1) transform_objects_cnode, simp, clarsimp simp:transform_objects_cnode gets_the_def gets_def get_def
apply (drule (1) transform_objects_cnode, simp,
clarsimp simp:transform_objects_cnode gets_the_def gets_def get_def
cap_object_simps bind_def return_def valid_def exs_valid_def
assert_opt_def opt_object_def transform_def
split: nat.splits)+
apply (clarsimp simp: get_cnode_def bind_assoc get_cnode_def liftE_bindE)
apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp split:Structures_A.kernel_object.splits)
apply (clarsimp simp: get_cnode_def bind_assoc liftE_bindE)
apply (clarsimp simp: valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp split: Structures_A.kernel_object.splits)
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (rename_tac "fun")
apply (rule_tac Q="\<lambda>x y. y = (transform s) \<and> x = (transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun))" in corres_symb_exec_l)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:whenE_def branch_map_simp1|rule conjI)+
apply (drule (1) transform_objects_cnode, simp, clarsimp simp:transform_objects_cnode gets_the_def gets_def get_def
apply (drule (1) transform_objects_cnode, simp,
clarsimp simp: transform_objects_cnode gets_the_def gets_def get_def
bind_def return_def valid_def exs_valid_def cap_object_simps
assert_opt_def opt_object_def transform_def
split: nat.splits)+
done
done
lemma resolve_address_bits_terminate_corres:
"\<lbrakk>in_terminate_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap'=transform_cap cap; valid_cap cap s;valid_idle s;length ref \<le> 32;valid_objs s\<rbrakk>
@ -2883,9 +2864,10 @@ lemma resolve_address_bits_terminate_corres:
apply (clarsimp simp:unlessE_def cap_type_simps assertE_def)
apply (subgoal_tac "(of_bl ref >> radix_bits) && mask (length guard) = of_bl guard")
apply (clarsimp | rule conjI)+
apply (clarsimp simp:get_cnode_def bind_assoc get_cnode_def liftE_bindE)
apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE)
apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp split:Structures_A.kernel_object.splits)
apply (rename_tac "fun")
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (rule_tac Q="\<lambda>x y. y = (transform s) \<and> x = (transform_object (machine_state s) oref etcb_opt (kernel_object.CNode radix_bits fun))" in corres_symb_exec_l)
@ -2908,19 +2890,12 @@ lemma resolve_address_bits_terminate_corres:
apply (simp add: word_rep_drop)+
done
lemma is_cnode_cap_eq:
"Types_D.is_cnode_cap (transform_cap next_cap) =
(Structures_A.is_cnode_cap next_cap)"
by (auto simp: cap_type_simps
is_cap_simps transform_cap_def
split: cap.splits cdl_cap.splits arch_cap.splits)
lemma length_drop:
"(length cref - a) = (length (drop a cref))"
"length cref - a = length (drop a cref)"
by auto
lemma bind_eqI' :"\<lbrakk>a=b;a=b\<Longrightarrow>c=d\<rbrakk>\<Longrightarrow> (a >>= c) = (b >>= d)"
by clarsimp
by simp
lemma cdl_resolve_address_bits_eq:
"a+t\<le> length cref \<and> length cref \<le> 32\<longrightarrow>
@ -2997,7 +2972,7 @@ shows "\<lbrakk>length cref \<le> n ; length cref \<le> 32; cap = transform_cap
\<top> (valid_objs and valid_cap cap' and valid_global_refs and valid_idle and valid_etcbs)
(CSpace_D.resolve_address_bits cap (of_bl cref) (length cref)) (resolve_address_bits (cap', cref) :: ((cslot_ptr * cap_ref),det_ext) lf_monad)")
apply clarsimp
apply (thin_tac "?P ?Q")+
apply (thin_tac "P" for P)+
proof (induct n arbitrary: cref cap' cap)
case 0
show ?case
@ -3010,8 +2985,9 @@ proof (induct n arbitrary: cref cap' cap)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits)
apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits)
apply (rename_tac word list nat "fun")
apply (rule corres_guard_imp)
apply (rule_tac radix_bits = nata and guard = list and s = s' in resolve_address_bits_error_corres[where ref="[]",simplified])
apply (rule_tac radix_bits = nat and guard = list and s = s' in resolve_address_bits_error_corres[where ref="[]",simplified])
apply ((simp add:transform_cap_def in_terminate_branch_def in_recursive_branch_def valid_cap_def obj_at_def is_cap_table_def)+)[10]
done
next
@ -3034,8 +3010,9 @@ next
apply (case_tac "\<not> in_recursive_branch cref cap'")
apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits)
apply (clarsimp simp:dc_def[symmetric] is_cap_table_def split:Structures_A.kernel_object.splits cap.splits)
apply (rename_tac word list nat "fun")
apply (rule corres_guard_imp)
apply (rule_tac s=s' and radix_bits = nata and guard = list in resolve_address_bits_error_corres)
apply (rule_tac s=s' and radix_bits = nat and guard = list in resolve_address_bits_error_corres)
apply (simp_all | rule conjI)+
apply (clarsimp simp:valid_cap_def obj_at_def is_cap_table_def)
apply (clarsimp simp:gets_the_def gets_def valid_cap_def obj_at_def split:Structures_A.kernel_object.splits cap.splits)
@ -3043,16 +3020,19 @@ next
apply (subst KHeap_DR.resolve_address_bits.simps,subst resolve_address_bits_recursive_branch)
apply (clarsimp simp:cap_type_simps is_cap_simps)+
apply fastforce
apply (rename_tac word list nat "fun")
apply (simp add:cap_type_simps)
apply (simp add:in_recursive_branch_def in_terminate_branch_def unlessE_def branch_map_simp1)
apply (clarsimp simp:get_cnode_def bind_assoc get_cnode_def liftE_bindE)
apply (clarsimp simp:get_cnode_def bind_assoc liftE_bindE)
apply (rule dcorres_expand_pfx)
apply clarsimp
apply (rule_tac Q="\<lambda>x y. y = (transform s'a) \<and> x = (transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nata fun))" in corres_symb_exec_l)
apply (rule_tac Q="\<lambda>x y. y = (transform s'a) \<and> x = (transform_object (machine_state s'a) word etcb_opt (kernel_object.CNode nat fun))" in corres_symb_exec_l)
apply (rule dcorres_expand_pfx)
apply (clarsimp simp: nat_case_split)
apply (rule corres_underlying_split [where P="\<lambda>rv s. True" and
P' = "\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and valid_idle and valid_etcbs"])
apply (rule corres_underlying_split [where
P = "\<lambda>rv s. True" and
P' = "\<lambda>next_cap. valid_objs and (\<lambda>a. a \<turnstile> next_cap) and valid_global_refs and
valid_idle and valid_etcbs"])
apply (rule get_cap_corres[THEN corres_guard_imp])
apply (clarsimp simp:transform_cslot_ptr_def cap_object_simps)
apply (simp add: branch_map_simp2)
@ -3060,9 +3040,9 @@ next
apply clarsimp
apply (erule (1) cnode_not_idle)
apply (wp |simp)+
apply (clarsimp simp:cdl_resolve_address_bits_eq is_cnode_cap_eq | rule conjI)+
apply (clarsimp simp:cdl_resolve_address_bits_eq is_cnode_cap_transform_cap | rule conjI)+
apply (subst cdl_resolve_address_bits_eq)
apply (subgoal_tac "?a+?b-?a\<le> ?b")
apply (subgoal_tac "a+b-a \<le> b" for a b)
apply simp+
apply (subst length_drop)
apply (rule Suc.hyps[rule_format])
@ -3102,14 +3082,15 @@ lemma not_idle_thread_resolve_address_bits:
apply (rule validE_R_validE)
apply (rule_tac hoare_vcg_precond_impE_R)
apply (rule validE_validE_R)
apply (rule_tac Q="\<lambda>r. valid_etcbs and valid_global_refs and valid_objs and valid_idle and valid_irq_node and ex_cte_cap_to (fst r)"
apply (rule_tac Q="\<lambda>r. valid_etcbs and valid_global_refs and valid_objs and valid_idle and
valid_irq_node and ex_cte_cap_to (fst r)"
in hoare_post_impErr[where E="\<lambda>x y. True"])
apply (wp resolve_address_bits_valid_etcbs rab_cte_cap_to)
apply (simp add: ex_cte_cap_to_not_idle)+
apply (auto intro: ex_cte_cap_wp_to_not_idle)[2]
apply (clarsimp simp:ex_cte_cap_to_def)
apply (rule_tac x = thread in exI,rule_tac x = "tcb_cnode_index 0" in exI)
apply (clarsimp simp:cte_wp_at_cases obj_at_def is_cap_simps)
done
done
lemma lookup_cap_corres:
"\<lbrakk>w = of_bl blist;length blist = Types_D.word_bits\<rbrakk> \<Longrightarrow>
@ -3140,7 +3121,7 @@ lemma lookup_cap_corres:
apply (simp add:objs_valid_tcb_ctable)+
apply clarsimp
apply (clarsimp simp:not_idle_thread_def opt_cap_tcb | drule(1) valid_etcbs_get_tcb_get_etcb)+
done
done
lemma cdl_current_thread:
"(cdl_current_thread (transform s')) = transform_current_thread s'"
@ -3151,8 +3132,7 @@ lemma get_cap_get_tcb_dcorres:
(KHeap_D.get_cap (thread, tcb_cspace_slot))
(gets_the (get_tcb thread))"
apply (clarsimp simp: corres_underlying_def)
apply (clarsimp simp: gets_the_def bind_def simpler_gets_def
assert_opt_def fail_def return_def
apply (clarsimp simp: gets_the_def bind_def simpler_gets_def assert_opt_def fail_def return_def
split: option.splits)
apply (frule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
apply (drule opt_cap_tcb [where sl=tcb_cspace_slot])

4
proof/drefine/MoreCorres.thy
View File

@ -72,12 +72,12 @@ lemma corres_if_rhs:
(* Bind distributes over non-deterministic choice. *)
lemma alternative_bind_distrib: "((f \<sqinter> g) >>= h) = ((f >>= h) \<sqinter> (g >>= h))"
apply (auto simp: alternative_def bind_def split_def intro!: ext prod_eqI)
apply (auto simp: alternative_def bind_def split_def intro!: prod_eqI)
done
(* Bind distributes over non-deterministic choice. *)
lemma alternative_bind_distrib_2: "(do f; (a \<sqinter> b) od) = ((do f; a od) \<sqinter> (do f; b od))"
apply (auto simp: alternative_def bind_def split_def intro!: ext prod_eqI)
apply (auto simp: alternative_def bind_def split_def intro!: prod_eqI)
done
(* "bindE" distributes over non-deterministic choice. *)

2
proof/drefine/Refine_D.thy
View File

@ -53,7 +53,7 @@ lemma dcorres_call_kernel:
apply (clarsimp simp: invs_def valid_state_def)
apply (wp hoare_vcg_if_lift2 hoare_drop_imp he_invs
| strengthen valid_etcbs_sched valid_idle_invs_strg
| simp add: conj_ac cong: conj_cong)+
| simp add: conj_comms cong: conj_cong)+
apply (rule valid_validE2)
apply (rule hoare_vcg_conj_lift)
apply (rule he_invs)

30
proof/drefine/Schedule_DR.thy
View File

@ -254,7 +254,7 @@ lemma schedule_resume_cur_thread_dcorres_L:
apply (rule corres_either_alternate2)
apply (rule corres_guard_imp)
apply (rule corres_symb_exec_l_Ex)
apply (clarsimp simp: K_bind_def)
apply (clarsimp)
apply (rule corres_symb_exec_l_Ex)
apply (rule corres_symb_exec_l_Ex)
apply (rule corres_symb_exec_l_Ex)
@ -267,8 +267,8 @@ lemma schedule_resume_cur_thread_dcorres_L:
apply (rule switch_to_thread_idempotent_corres)
apply (clarsimp simp: corres_underlying_def fail_def)
apply (wp | simp)+
apply (fastforce simp: select_def gets_def active_tcbs_in_domain_def bind_def return_def domIff get_def fst_def
modify_def put_def change_current_domain_def)
apply (fastforce simp: select_def gets_def active_tcbs_in_domain_def bind_def return_def domIff
get_def fst_def modify_def put_def change_current_domain_def)
apply simp
apply (rule corres_guard_imp)
apply (rule dcorres_symb_exec_r)
@ -282,7 +282,6 @@ lemma schedule_resume_cur_thread_dcorres_L:
done
lemma schedule_resume_cur_thread_dcorres:
"\<And>cur cur_ts. dcorres dc \<top> (\<lambda>s. cur = cur_thread s \<and> st_tcb_at (op = cur_ts) cur s \<and> valid_etcbs s \<and> valid_sched s \<and> invs s \<and> scheduler_action s = resume_cur_thread)
Schedule_D.schedule
@ -336,7 +335,7 @@ lemma schedule_switch_thread_dcorres:
(* t \<noteq> idle_thread s *)
apply (rule stronger_corres_guard_imp)
apply (rule dcorres_symb_exec_r)
apply (clarsimp simp: guarded_switch_to_def bind_assoc nested_bind)
apply (clarsimp simp: guarded_switch_to_def bind_assoc)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_symb_exec_r)
apply (rule dcorres_rhs_noop_below_True[OF set_scheduler_action_dcorres])
@ -356,7 +355,7 @@ lemma schedule_switch_thread_dcorres:
apply fastforce
(* t = idle_thread s *)
apply (rule dcorres_symb_exec_r)
apply (clarsimp simp: guarded_switch_to_def bind_assoc nested_bind)
apply (clarsimp simp: guarded_switch_to_def bind_assoc)
apply (rule_tac Q'="\<lambda>ts s. idle ts" in dcorres_symb_exec_r)
apply (clarsimp simp: assert_def)
apply (rule conjI, clarsimp)
@ -405,7 +404,8 @@ lemma change_current_domain_dcorres: "dcorres dc \<top> \<top> change_current_do
get_def transform_def trans_state_def transform_objects_def transform_cdt_def transform_current_thread_def
transform_asid_table_def)
lemma max_set_not_empty: "\<And>x::'a::{linorder,finite}. f x \<noteq> [] \<Longrightarrow> f (Max {x. f x \<noteq> []}) \<noteq> []"
lemma max_set_not_empty:
"\<And>x::'a::{linorder,finite}. f x \<noteq> [] \<Longrightarrow> f (Max {x. f x \<noteq> []}) \<noteq> []"
apply (rule_tac S="{x. f x \<noteq> []}" in Max_prop)
apply auto
done
@ -432,7 +432,7 @@ lemma schedule_def_2:
done
lemma schedule_choose_new_thread_dcorres_fragment:
"\<And>cur_ts cur. dcorres dc \<top>
"dcorres dc \<top>
(\<lambda>s. valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread)
Schedule_D.schedule
(do dom_time \<leftarrow> gets domain_time;
@ -440,7 +440,7 @@ lemma schedule_choose_new_thread_dcorres_fragment:
y \<leftarrow> choose_thread;
set_scheduler_action resume_cur_thread
od)"
apply (clarsimp simp: guarded_switch_to_def bind_assoc nested_bind choose_thread_def)
apply (clarsimp simp: guarded_switch_to_def bind_assoc choose_thread_def)
apply (rule dcorres_symb_exec_r, rename_tac dom_t)
apply (case_tac "dom_t \<noteq> 0")
apply (clarsimp)
@ -462,7 +462,7 @@ lemma schedule_choose_new_thread_dcorres_fragment:
apply (rule_tac P'="\<lambda>s. ready_queues s (cur_domain s) = rq \<and> valid_etcbs s \<and> valid_sched_except_blocked s \<and> invs s \<and> scheduler_action s = choose_new_thread"
in stronger_corres_guard_imp)
apply (rule corres_symb_exec_l_Ex)
apply (clarsimp simp: K_bind_def)
apply (clarsimp)
apply (rule corres_symb_exec_l_Ex)
apply (rule corres_symb_exec_l_Ex)
apply (rule corres_symb_exec_l_Ex)
@ -652,8 +652,7 @@ lemma activate_thread_corres:
od | None \<Rightarrow> return ()
od)
activate_thread"
apply (simp add: activate_thread_def has_restart_cap_def
gets_def bind_assoc)
apply (simp add: activate_thread_def has_restart_cap_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_r)
apply (rule dcorres_absorb_get_l)
apply (simp add:get_thread_state_def bind_assoc thread_get_def)
@ -677,8 +676,7 @@ lemma activate_thread_corres:
apply (rule dcorres_absorb_get_l)
apply (simp add:assert_opt_def when_def)
apply (case_tac "tcb_state obj'")
apply (clarsimp simp:infer_tcb_pending_op_def
when_def st_tcb_at_def ct_in_state_def obj_at_def
apply (clarsimp simp:infer_tcb_pending_op_def when_def st_tcb_at_def ct_in_state_def obj_at_def
dest!:get_tcb_SomeD)+
apply (rule corres_guard_imp)
apply (rule dcorres_symb_exec_r)
@ -687,8 +685,8 @@ lemma activate_thread_corres:
apply simp
apply (wp dcorres_to_wp[OF as_user_setNextPC_corres,simplified])
apply (wp getRestartPC_inv as_user_inv)
apply (simp add:invs_mdb st_tcb_at_def obj_at_def invs_valid_idle
generates_pending_def not_idle_thread_def)
apply (simp add: invs_mdb st_tcb_at_def obj_at_def invs_valid_idle generates_pending_def
not_idle_thread_def)
apply (clarsimp simp:infer_tcb_pending_op_def arch_activate_idle_thread_def
when_def st_tcb_at_def ct_in_state_def obj_at_def
dest!:get_tcb_SomeD)+

14
proof/drefine/StateTranslationProofs_DR.thy
View File

@ -78,7 +78,7 @@ done
lemma msg_registers_lt_msg_max_length [simp]:
"length msg_registers < msg_max_length"
by (simp add: msg_registers_def msgRegisters_unfold msg_max_length_def )
by (simp add: msgRegisters_unfold msg_max_length_def)
lemma get_tcb_mrs_update_state :
"get_tcb_mrs ms (tcb_state_update f tcb) = get_tcb_mrs ms tcb"
@ -171,27 +171,27 @@ lemmas caps_of_state_upds = caps_of_state_update_tcb caps_of_state_update_same_c
lemma transform_cdt_kheap_update [simp]:
"transform_cdt (kheap_update f s) = transform_cdt s"
by (clarsimp simp: transform_cdt_def cong: if_cong)
by (clarsimp simp: transform_cdt_def)
lemma transform_cdt_update_machine [simp]:
"transform_cdt (update_machine ms s) = transform_cdt s "
by (clarsimp simp: transform_cdt_def cong: if_cong)
by (clarsimp simp: transform_cdt_def)
lemma transform_cdt_update_original_cap [simp]:
"transform_cdt (b\<lparr>is_original_cap := x\<rparr>) = transform_cdt b"
by (clarsimp simp: transform_cdt_def cong: if_cong)
by (clarsimp simp: transform_cdt_def)
lemma transform_asid_table_kheap_update [simp]:
"transform_asid_table (kheap_update f s) = transform_asid_table s"
by (clarsimp simp: transform_asid_table_def cong: if_cong)
by (clarsimp simp: transform_asid_table_def)
lemma transform_asid_table_update_machine [simp]:
"transform_asid_table (update_machine ms s) = transform_asid_table s "
by (clarsimp simp: transform_asid_table_def cong: if_cong)
by (clarsimp simp: transform_asid_table_def)
lemma transform_asid_table_update_original_cap [simp]:
"transform_asid_table (b\<lparr>is_original_cap := x\<rparr>) = transform_asid_table b"
by (clarsimp simp: transform_asid_table_def cong: if_cong)
by (clarsimp simp: transform_asid_table_def)
lemma transform_objects_update_kheap_same_caps:
"\<lbrakk> kh ptr = Some ko; caps_of_object ko' = caps_of_object ko; a_type ko' = a_type ko\<rbrakk> \<Longrightarrow>

3
proof/drefine/StateTranslation_D.thy
View File

@ -429,8 +429,7 @@ lemma transform_intent_isnot_UntypedIntent:
apply(unfold transform_intent_untyped_retype_def)
apply (clarsimp split: list.split, safe, simp_all)[1]
apply (clarsimp simp: transform_type_def)
apply (simp add: linorder_not_less eval_nat_numeral word_le_nat_alt
le_Suc_eq unat_arith_simps)
apply (simp add: linorder_not_less eval_nat_numeral le_Suc_eq unat_arith_simps)
apply(erule disjE)
apply(auto simp: transform_intent_def option_map_def split: invocation_label.split option.split_asm)[1]
apply (erule disjE)

180
proof/drefine/Syscall_DR.thy
View File

@ -8,14 +8,13 @@
* @TAG(NICTA_GPL)
*)
theory Syscall_DR imports
theory Syscall_DR
imports
Tcb_DR
Schedule_DR
Interrupt_DR
begin
declare option.weak_case_cong[cong]
(*
* Translate an abstract invocation into a corresponding
* CDL invocation.
@ -227,9 +226,9 @@ lemma decode_domain_corres:
(Decode_A.decode_domain_invocation label' args' excaps')"
apply (unfold Tcb_D.decode_domain_invocation_def Decode_A.decode_domain_invocation_def)
apply (unfold transform_cap_list_def)
apply (case_tac "invocation_type label'")
apply simp_all
apply (clarsimp simp: transform_intent_def option_map_def split: option.splits)+
apply (case_tac "invocation_type label'"; simp)
apply (clarsimp simp: transform_intent_def option_map_def
split: option.splits)+
defer
apply (clarsimp simp: transform_intent_def option_map_def split: option.splits)+
apply (clarsimp simp: transform_intent_domain_def)
@ -245,8 +244,7 @@ lemma decode_domain_corres:
apply (rule dcorres_whenE_throwError_abstract')
apply (rule corres_alternate2)
apply simp
apply (case_tac "fst (hd (excaps'))")
apply simp_all
apply (case_tac "fst (hd (excaps'))"; simp)
apply ((rule corres_alternate2, simp)+)[6]
apply (rule corres_alternate1)
apply (clarsimp simp: returnOk_def cdl_invocation_relation_def translate_invocation_def split: list.splits)
@ -348,7 +346,7 @@ lemma transform_type_eq_None:
apply (simp add:unat_arith_simps)
apply (clarsimp simp:arch_data_to_obj_type_def)
apply (rule conjI,arith,clarsimp)+
done
done
lemma transform_intent_untyped_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.UntypedCap w n idx\<rbrakk>
@ -356,18 +354,19 @@ lemma transform_intent_untyped_cap_None:
apply (clarsimp simp:Decode_A.decode_invocation_def)
apply wp
apply (case_tac "invocation_type label")
(* 43 subgoals *)
apply (clarsimp simp:Decode_A.decode_untyped_invocation_def unlessE_def)
apply wp
apply (clarsimp simp:transform_intent_def Decode_A.decode_untyped_invocation_def unlessE_def split del:if_splits)
apply (clarsimp simp:transform_intent_untyped_retype_def split del:if_splits)
apply (clarsimp simp:transform_intent_def Decode_A.decode_untyped_invocation_def unlessE_def split del:split_if)
apply (clarsimp simp:transform_intent_untyped_retype_def split del:split_if)
apply (case_tac "args")
apply (clarsimp,wp)[1]
apply (clarsimp split:list.split_asm split del:if_splits)
apply (clarsimp split:list.split_asm split del:split_if)
apply wp[5]
apply (clarsimp simp: transform_type_eq_None split del:if_splits split:option.splits)
apply (clarsimp simp: transform_type_eq_None split del:split_if split:option.splits)
apply (wp|clarsimp simp:whenE_def|rule conjI)+
apply (clarsimp simp: Decode_A.decode_untyped_invocation_def unlessE_def split del:if_splits,wp)+
done
apply (clarsimp simp: Decode_A.decode_untyped_invocation_def unlessE_def split del:split_if,wp)+
done
lemma transform_intent_cnode_cap_None:
"\<lbrakk>transform_intent (invocation_type label) args = None; cap = cap.CNodeCap w n list\<rbrakk>
@ -711,6 +710,7 @@ lemma perform_invocation_corres:
apply (wp | clarsimp)+
(* invoke_reply *)
apply (rename_tac word a b)
apply (clarsimp simp:invoke_reply_def)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ get_cur_thread_corres])
@ -748,6 +748,7 @@ lemma perform_invocation_corres:
(* invoke_irq *)
apply (simp add:liftE_def bindE_def)
apply (rename_tac irq_control_invocation)
apply (case_tac irq_control_invocation)
apply (rule corres_guard_imp)
apply (rule corres_split[where r'=dc])
@ -856,7 +857,7 @@ lemma get_ipc_buffer_noop:
apply (simp add:gets_the_def gets_def bind_assoc get_def split_def get_ipc_buffer_def tcb_at_def
exs_valid_def fail_def return_def bind_def assert_opt_def split:cdl_cap.splits)
apply clarsimp
apply (rule_tac x = "(the (opt_cap (t, tcb_ipcbuffer_slot) ?s),?s)" in bexI)
apply (rule_tac x = "(the (opt_cap (t, tcb_ipcbuffer_slot) s),s)" for s in bexI)
apply (rule conjI|fastforce simp:fail_def return_def split:option.splits)+
apply (clarsimp split:option.splits simp:fail_def return_def)
apply (frule(1) valid_etcbs_get_tcb_get_etcb)
@ -864,7 +865,6 @@ lemma get_ipc_buffer_noop:
done
lemma dcorres_reply_from_kernel:
(* FIXME: this is incomprehensible. fix a bit when auto-indenting is fixed? *)
"dcorres dc \<top> (invs and tcb_at oid and not_idle_thread oid and valid_etcbs) (corrupt_ipc_buffer oid True) (reply_from_kernel oid msg_rv)"
apply (simp add:reply_from_kernel_def)
apply (case_tac msg_rv)
@ -910,10 +910,10 @@ lemma dcorres_reply_from_kernel:
apply (clarsimp simp:invs_def not_idle_thread_def valid_state_def valid_pspace_def
ipc_frame_wp_at_def ipc_buffer_wp_at_def obj_at_def)
apply (clarsimp simp:cte_wp_at_cases obj_at_def)
apply (drule_tac s="cap.ArchObjectCap ?c" in sym)
apply (drule_tac s="cap.ArchObjectCap c" for c in sym)
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def)
apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases)
apply (drule_tac s="cap.ArchObjectCap ?c" in sym)
apply (drule_tac s="cap.ArchObjectCap c" for c in sym)
apply simp
apply (wp get_ipc_buffer_noop, clarsimp)
apply fastforce
@ -938,8 +938,8 @@ lemma dcorres_set_intent_error:
apply (frule ko_at_tcb_at)
apply (frule(1) tcb_at_is_etcb_at)
apply (clarsimp simp:tcb_at_def is_etcb_at_def, fold get_etcb_def)
apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def
KHeap_D.set_object_def simpler_modify_def corres_underlying_def)
apply (clarsimp simp:opt_object_tcb assert_opt_def transform_tcb_def KHeap_D.set_object_def
simpler_modify_def corres_underlying_def)
apply (simp add:transform_def return_def)
apply (rule ext)
apply (clarsimp simp:transform_objects_def transform_tcb_def
@ -960,7 +960,8 @@ lemma evalMonad_from_wp:
done
lemma empty_when_fail_get_mrs:
"empty_when_fail (get_mrs a b c)"
notes option.case_cong_weak [cong]
shows "empty_when_fail (get_mrs a b c)"
apply (clarsimp simp:get_mrs_def)
apply (rule empty_when_fail_compose)+
apply (simp add:empty_when_fail_return split:option.splits)+
@ -984,7 +985,8 @@ lemma empty_when_fail_get_mrs:
done
lemma weak_det_spec_get_mrs:
"weak_det_spec P (get_mrs a b c)"
notes option.case_cong_weak [cong]
shows "weak_det_spec P (get_mrs a b c)"
apply (clarsimp simp:get_mrs_def)
apply (rule weak_det_spec_compose)+
apply (simp add:weak_det_spec_simps split:option.splits)+
@ -1005,9 +1007,9 @@ lemma lookup_cap_and_slot_inv:
apply (simp add:validE_def)
apply (rule hoare_drop_imp)
apply (wp lookup_slot_for_thread_inv)
done
done
(* We need folloing lemma because we need to match get_mrs in abstract and cdl_intent_op in capdl after state s is fixed *)
(* We need following lemma because we need to match get_mrs in abstract and cdl_intent_op in capdl after state s is fixed *)
lemma decode_invocation_corres':
"\<lbrakk>(\<lambda>(cap, slot, extra) (slot', cap', extra', buffer).
cap = transform_cap cap' \<and> slot = transform_cslot_ptr slot' \<and> extra = transform_cap_list extra')
@ -1029,14 +1031,14 @@ lemma decode_invocation_corres':
od)
rv')"
apply (rule dcorres_expand_pfx)
apply (clarsimp split del:if_splits)
apply (clarsimp split del:split_if)
apply (rule_tac Q' ="\<lambda>r ns. ns = s
\<and> r = get_tcb_mrs (machine_state s) ctcb"
in corres_symb_exec_r)
apply (clarsimp split:option.split | rule conjI)+
apply (rule corres_guard_imp[OF decode_invocation_ep_related_branch])
apply clarsimp+
defer
defer
apply clarsimp
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp[OF decode_invocation_corres])
@ -1045,9 +1047,11 @@ defer
apply (rule dcorres_expand_pfx)
apply (rule dcorres_free_throw[OF decode_invocation_error_branch])
apply (clarsimp simp:transform_full_intent_def Let_def get_tcb_message_info_def)+
done
done
lemma reply_from_kernel_error:
notes option.case_cong_weak [cong]
shows
"\<lbrace>tcb_at oid and K (fst e \<le> mask 19 \<and> 0 < fst e = er)\<rbrace>reply_from_kernel oid e
\<lbrace>\<lambda>rv s. (\<exists>tcb. guess_error (mi_label (get_tcb_message_info tcb)) = er \<and>
ko_at (TCB tcb) oid s)\<rbrace>"
@ -1066,8 +1070,8 @@ lemma reply_from_kernel_error:
apply (rule exI)
apply (rule conjI[rotated])
apply (simp add:obj_at_def)
apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq0)
apply (simp add:shiftr_over_or_dist le_mask_iff word_neq0)
apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv)
apply (simp add:shiftr_over_or_dist le_mask_iff word_neq_0_conv)
apply (subst shiftl_shiftr_id)
apply (simp add:WordSetup.word_bits_def mask_def le_mask_iff[symmetric])+
apply unat_arith
@ -1231,13 +1235,15 @@ lemma perform_invocation_idle[wp]:
apply (case_tac i)
apply (simp_all add:not_idle_thread_def)
apply (wp invoke_cnode_idle invoke_domain_idle |clarsimp)+
apply (rename_tac irq_control_invocation)
apply (case_tac irq_control_invocation)
apply (simp_all add:invoke_irq_control.simps | wp)+
apply (simp add:arch_invoke_irq_control_def)
apply (simp_all | wp)+
apply (simp add: arch_invoke_irq_control_def)
apply (rename_tac irq_handler_invocation)
apply (case_tac irq_handler_invocation)
apply simp_all
apply (wp|simp)+
done
done
lemma msg_from_syscall_error_simp:
"fst (msg_from_syscall_error rv) \<le> mask 19"
@ -1265,7 +1271,7 @@ lemma not_master_reply_cap_lcs[wp]:
apply (simp add:cte_wp_at_def)
apply wp
apply simp
done
done
lemma not_master_reply_cap_lcs'[wp]:
"\<lbrace>valid_reply_masters and valid_objs\<rbrace> CSpace_A.lookup_cap_and_slot t ptr
@ -1278,7 +1284,7 @@ lemma not_master_reply_cap_lcs'[wp]:
apply clarsimp
apply (case_tac a)
apply (simp_all add:diminished_def mask_cap_def cap_rights_update_def)
done
done
lemma set_thread_state_ct_active:
"\<lbrace>\<lambda>s. cur_thread s = cur_thread s'\<rbrace>
@ -1286,7 +1292,7 @@ lemma set_thread_state_ct_active:
apply (simp add:set_thread_state_def)
apply (wp dxo_wp_weak
| clarsimp simp: set_object_def trans_state_def ct_in_state_def st_tcb_at_def obj_at_def)+
done
done
crunch valid_etcbs[wp]: cap_recycle valid_etcbs
(simp: unless_def ignore: without_preemption)
@ -1429,6 +1435,7 @@ lemma receive_ipc_cur_thread:
apply wp
apply clarsimp
apply (clarsimp simp:neq_Nil_conv)
apply (rename_tac list)
apply (rule_tac Q="\<lambda>r s. P (cur_thread s) \<and> tcb_at (hd list) s" in hoare_strengthen_post)
apply wp
apply (clarsimp simp:st_tcb_at_def tcb_at_def)
@ -1437,7 +1444,7 @@ lemma receive_ipc_cur_thread:
apply (wp valid_ep_get_ep2)
apply (clarsimp simp:valid_ep_def)
apply (clarsimp simp:valid_def return_def fail_def split:option.splits cap.splits)
done
done
lemma cap_delete_one_st_tcb_at_and_valid_etcbs:
"\<lbrace>st_tcb_at P t and K (\<forall>st. active st \<longrightarrow> P st) and valid_etcbs\<rbrace> cap_delete_one ptr \<lbrace>\<lambda>rv s. st_tcb_at P t s \<and> valid_etcbs s\<rbrace>"
@ -1475,13 +1482,13 @@ lemma handle_wait_corres:
\<and> (st_tcb_at active (cur_thread s') s \<and> invs s \<and> valid_etcbs s) \<and> ko_at (TCB obj') (cur_thread s') s " and R= "\<lambda>r. \<top>"
in corres_splitEE[where r'="\<lambda>x y. x = transform_cap y"])
apply (rule dcorres_expand_pfx)
apply (clarsimp split:cap.splits arch_cap.splits
simp:transform_cap_def)
apply (clarsimp split:cap.splits arch_cap.splits simp:transform_cap_def)
apply (rename_tac word1 word2 set)
apply (rule corres_guard_imp)
apply (rule_tac epptr = word1 in recv_sync_ipc_corres)
apply (simp add:cap_ep_ptr_def )+
apply (clarsimp simp:st_tcb_at_def obj_at_def dest!:get_tcb_SomeD get_etcb_SomeD)
defer(* NEED RECEIVE ASYNC IPC *)
defer(* NEED RECEIVE ASYNC IPC *)
apply (rule lookup_cap_corres, simp)
apply (simp add: Types_D.word_bits_def)
apply wp
@ -1537,6 +1544,7 @@ lemma handle_reply_corres:
in corres_split [OF _ get_cap_corres])
apply (simp add: transform_cap_def corres_fail split: cap.split)
apply (clarsimp simp: corres_fail dc_def[symmetric] split: bool.split)
apply (rename_tac word)
apply (rule corres_guard_imp)
apply (rule do_reply_transfer_corres)
apply (simp add: transform_tcb_slot_simp)
@ -1552,84 +1560,17 @@ lemma handle_reply_corres:
apply (clarsimp simp:ct_in_state_def invs_def valid_state_def st_tcb_at_def tcb_at_def obj_at_def)
done
lemma set_object_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> KHeap_A.set_object word x
\<lbrace>\<lambda>yb s. P (cur_thread s) (idle_thread s)\<rbrace>"
by (fastforce simp:set_object_def valid_def get_def put_def return_def bind_def)
lemma set_thread_state_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread (s :: det_ext state)) \<rbrace> set_thread_state thread x \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:set_thread_state_def)
apply (wp set_object_cur_thread_idle_thread)
apply simp
done
lemma thread_set_cur_thread_idle_thread:
" \<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> thread_set (tcb_fault_update Map.empty) word \<lbrace>\<lambda>xg s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:thread_set_def)
apply (wp set_object_cur_thread_idle_thread)
apply simp
done
lemma as_user_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> as_user thread x \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (clarsimp simp:as_user_def)
apply (wp set_object_cur_thread_idle_thread)+
apply (fastforce simp:set_object_def valid_def get_def put_def return_def bind_def)
apply (simp add:select_f_def)
apply (simp add:valid_def)
apply (auto|wp)+
done
lemma do_fault_transfer_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s)\<rbrace> do_fault_transfer c a e recv_buffer \<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:do_fault_transfer_def set_message_info_def)
apply (wp as_user_cur_thread_idle_thread |wpc|clarsimp)+
apply (wps | wp transfer_caps_it copy_mrs_it | simp )+
apply wpc
apply (wp | simp add:thread_get_def)+
done
lemma do_normal_transfer_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> Ipc_A.do_normal_transfer a b c d e f g h\<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:do_normal_transfer_def set_message_info_def)
apply (wp as_user_cur_thread_idle_thread |wpc|clarsimp)+
apply (wps | wp transfer_caps_it copy_mrs_it)+
apply clarsimp
done
lemma do_ipc_transfer_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread s) (idle_thread s) \<rbrace> Ipc_A.do_ipc_transfer a b c d e f\<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s)\<rbrace>"
apply (simp add:do_ipc_transfer_def)
apply (wp do_fault_transfer_cur_thread_idle_thread do_normal_transfer_cur_thread_idle_thread|wpc)+
apply (wp | simp add:thread_get_def)+
done
lemma handle_reply_cur_thread_idle_thread:
"\<lbrace>\<lambda>s. P (cur_thread (s :: det_ext state)) (idle_thread s)\<rbrace> Syscall_A.handle_reply
\<lbrace>\<lambda>rv s. P (cur_thread s) (idle_thread s) \<rbrace>"
apply (simp add:handle_reply_def)
apply (wp do_ipc_transfer_cur_thread_idle_thread|wpc)+
apply (clarsimp simp:Ipc_A.do_reply_transfer_def)
apply (wp set_thread_state_cur_thread_idle_thread|wpc)+
apply ((wps|wp cap_delete_one_it)+)[1]
apply (wp hoare_vcg_if_lift thread_set_cur_thread_idle_thread
do_ipc_transfer_cur_thread_idle_thread
set_thread_state_cur_thread_idle_thread)
apply ((wps | wp handle_fault_reply_it)+)[1]
apply wp
apply ((wps | wp cap_delete_one_it)+)[1]
apply (rule hoare_drop_imp | rule hoare_conjI | rule hoare_allI | wp)+
apply simp+
done
done
lemma handle_vm_fault_wp:
"\<lbrace>P\<rbrace> handle_vm_fault thread vmfault_type \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>"
apply (case_tac vmfault_type)
apply (simp add:handle_vm_fault.simps)
apply (simp)
apply wp
apply (clarsimp simp:do_machine_op_def getDFSR_def)
apply wp
@ -1650,7 +1591,7 @@ lemma handle_vm_fault_wp:
apply wp
apply (clarsimp simp:gets_def alternative_def select_def bind_def get_def return_def)
apply simp
apply (simp add:handle_vm_fault.simps)
apply (simp)
apply wp
apply (clarsimp simp:do_machine_op_def getIFSR_def)
apply wp
@ -1672,21 +1613,21 @@ lemma handle_vm_fault_wp:
apply (clarsimp simp:getRegister_def gets_def alternative_def select_def bind_def get_def return_def obj_at_def)
apply (simp add:get_tcb_SomeD)
apply simp
done
done
lemma get_active_irq_corres:
"dcorres (\<lambda>r r'. r' = r) \<top> \<top> get_active_irq (do_machine_op getActiveIRQ)"
apply (clarsimp simp: corres_underlying_def do_machine_op_def
select_f_def bind_def in_monad getActiveIRQ_def
return_def get_active_irq_def in_alternative select_def
return_def get_active_irq_def select_def
split: if_splits)
apply (rule_tac x="(None, transform b)" in bexI
, (simp add: in_alternative)+)
apply (rule_tac x="(Some (irq_oracle (Suc (irq_state (machine_state b)))),
transform b)" in bexI
, (simp add: in_alternative)+)
done
done
crunch valid_etcbs[wp]: "handle_reply" "valid_etcbs"
@ -1696,12 +1637,7 @@ lemma hr_ct_active_and_valid_etcbs:
"\<lbrace>invs and ct_active and valid_etcbs\<rbrace> Syscall_A.handle_reply \<lbrace>\<lambda>rv. ct_active and valid_etcbs\<rbrace>"
by (wp, simp+)
find_theorems transform valid
lemma tcb_sched_action_transform_inv[wp]:"\<lbrace>\<lambda>s. transform s = cs\<rbrace> tcb_sched_action a b \<lbrace>\<lambda>r s. transform s = cs\<rbrace>"
apply (clarsimp simp: tcb_sched_action_def)
apply (wp | simp)+
done
declare tcb_sched_action_transform[wp]
crunch transform_inv[wp]: reschedule_required "\<lambda>s. transform s = cs"
@ -1710,6 +1646,7 @@ lemma handle_event_corres:
(invs and valid_pdpt_objs and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_running s) and valid_etcbs)
(Syscall_D.handle_event ev) (Syscall_A.handle_event ev)"
apply (cases ev, simp_all add: Syscall_D.handle_event_def)
apply (rename_tac syscall)
apply (case_tac syscall)
apply (simp_all add:handle_syscall_def handle_send_def handle_call_def)
apply (rule handle_invocation_corres[THEN corres_guard_imp] | simp)+
@ -1760,9 +1697,8 @@ lemma handle_event_corres:
apply wp
apply clarsimp
apply (frule (1) ct_running_not_idle_etc)
apply (clarsimp simp:invs_def valid_state_def st_tcb_at_def
generates_pending_def obj_at_def)
apply (clarsimp simp:invs_def valid_state_def st_tcb_at_def generates_pending_def obj_at_def)
apply (wp|simp)+
done
done
end

164
proof/drefine/Tcb_DR.thy
View File

@ -69,20 +69,21 @@ lemma decode_set_ipc_buffer_translate_tcb_invocation:
apply wpc
apply (wp hoare_whenE_wp)
apply (case_tac a)
apply (simp_all add:derive_cap_def split del:if_splits)
apply (wp|clarsimp split del:if_splits)+
apply (simp_all add:derive_cap_def split del:split_if)
apply (wp|clarsimp split del:split_if)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp_all add:arch_derive_cap_def split del:if_splits)
apply (wp | clarsimp split del:if_splits)+
apply (simp_all add:arch_derive_cap_def split del: split_if)
apply (wp | clarsimp split del: split_if)+
apply (clarsimp simp:transform_mapping_def)
apply (rule hoare_pre)
apply wpc
apply (wp | clarsimp split del:if_splits)+
apply (wp | clarsimp split del: split_if)+
apply (rule hoare_pre)
apply wpc
apply wp
apply clarsimp
done
done
lemma derive_cap_translate_tcb_invocation:
"\<lbrace>op = s\<rbrace>derive_cap a b \<lbrace>\<lambda>rv. op = s\<rbrace>,\<lbrace>\<lambda>rv. \<top>\<rbrace>"
@ -90,6 +91,7 @@ lemma derive_cap_translate_tcb_invocation:
apply (case_tac b)
apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+
apply (clarsimp simp:arch_derive_cap_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:ensure_no_children_def whenE_def |wp)+
apply (clarsimp split:option.splits | rule conjI | wp)+
@ -104,13 +106,14 @@ lemma derive_cnode_cap_as_vroot:
apply (simp add:derive_cap_def is_valid_vtable_root_def)
apply (case_tac aa)
apply (clarsimp|wp)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def | wp)+
done
done
lemma derive_cnode_cap_as_croot:
"\<lbrace>op = s\<rbrace> derive_cap (b, c) a
@ -118,21 +121,22 @@ lemma derive_cnode_cap_as_croot:
apply (clarsimp simp:derive_cap_def is_cap_simps)
apply (case_tac a)
apply (clarsimp|wp)+
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def split:option.splits |wp)+
apply (intro conjI)
apply (clarsimp simp:arch_derive_cap_def | wp)+
done
done
lemma valid_vtable_root_update:
"\<lbrakk> is_valid_vtable_root (CSpace_A.update_cap_data False x aa)\<rbrakk>
\<Longrightarrow> CSpace_A.update_cap_data False x aa = aa"
apply (clarsimp simp:update_cap_data_def badge_update_def is_valid_vtable_root_def Let_def the_cnode_cap_def
split:if_splits cap.split_asm)
apply (clarsimp simp:is_arch_cap_def arch_update_cap_data_def the_arch_cap_def split:arch_cap.splits cap.split_asm)
done
apply (clarsimp simp: update_cap_data_def badge_update_def is_valid_vtable_root_def Let_def
the_cnode_cap_def is_arch_cap_def arch_update_cap_data_def the_arch_cap_def
split: split_if_asm cap.split_asm)
done
lemma decode_set_space_translate_tcb_invocation:
"\<And>s. \<lbrace>op = s\<rbrace> decode_set_space x (cap.ThreadCap t) slot' (excaps')
@ -191,7 +195,7 @@ lemma decode_set_space_translate_tcb_invocation:
apply (rule hoare_post_impErr[OF derive_cnode_cap_as_croot])
apply fastforce+
apply (wp|clarsimp)+
done
done
lemma decode_tcb_cap_label_not_match:
"\<lbrakk>\<forall>ui. Some (TcbIntent ui) \<noteq> transform_intent (invocation_type label') args'; cap' = Structures_A.ThreadCap t\<rbrakk>
@ -357,7 +361,7 @@ lemma decode_tcb_corres:
apply (clarsimp simp:throw_on_none_def get_index_def dcorres_alternative_throw | rule conjI)+
apply (rule corres_return_throw_thingy)
apply (rule decode_set_space_translate_tcb_invocation)
apply (clarsimp split del:if_splits)+
apply (clarsimp split del:split_if)+
apply (clarsimp simp:translate_tcb_invocation_def translate_tcb_invocation_thread_ctrl_buffer_def)
apply (case_tac "excaps' ! 0",simp,case_tac "excaps' ! Suc 0",simp)
apply (simp add:update_cnode_cap_data)
@ -389,16 +393,13 @@ lemma dcorres_idempotent_as_user:
dcorres dc \<top> (tcb_at u) (return q) (as_user u x)"
apply (clarsimp simp: as_user_def)
apply (clarsimp simp: corres_underlying_def bind_def split_def set_object_def return_def get_def put_def
get_tcb_def gets_the_def gets_def assert_opt_def tcb_at_def select_f_def valid_def split_def
get_tcb_def gets_the_def gets_def assert_opt_def tcb_at_def select_f_def valid_def
split: option.split Structures_A.kernel_object.split)
done
lemma transform_full_intent_kheap_update_eq:
"\<lbrakk> q \<noteq> u' \<rbrakk> \<Longrightarrow> transform_full_intent (machine_state (s\<lparr>kheap := kheap s(u' \<mapsto> x')\<rparr>)) q = transform_full_intent (machine_state s) q"
apply (rule ext)
apply (clarsimp simp: transform_full_intent_def)
done
by simp
(* Various WP rules. *)
crunch tcb_at [wp]: "IpcCancel_A.suspend" "tcb_at t" (wp: set_cap_tcb)
@ -413,7 +414,7 @@ lemma suspend_corres:
apply (rule dcorres_rhs_noop_below_True[OF tcb_sched_action_dcorres])
apply (rule set_thread_state_corres)
apply wp
apply (clarsimp simp:not_idle_thread_def conj_ac)
apply (clarsimp simp:not_idle_thread_def conj_comms)
apply wp
apply simp
apply (clarsimp simp:st_tcb_at_def not_idle_thread_def
@ -524,7 +525,7 @@ lemma restart_corres:
apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb)
apply (clarsimp simp:opt_cap_tcb not_idle_thread_def tcb_vspace_slot_def
tcb_pending_op_slot_def tcb_caller_slot_def tcb_ipcbuffer_slot_def
tcb_cspace_slot_def tcb_replycap_slot_def tcb_pending_op_slot_def)
tcb_cspace_slot_def tcb_replycap_slot_def)
apply (intro conjI impI)
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ finalise_ipc_cancel])
@ -712,8 +713,10 @@ lemma valid_idle_ep_cancel_all:
"\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.ep_cancel_all word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>"
apply (simp add:ep_cancel_all_def)
apply (wp|wpc|simp)+
apply (rename_tac list queue)
apply (rule_tac I = "(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1 and valid_idle" in mapM_x_inv_wp)
and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1
and valid_idle" in mapM_x_inv_wp)
apply clarsimp
apply (wp KHeap_DR.tcb_at_set_thread_state_wp)
apply (rule hoare_conjI)
@ -729,13 +732,15 @@ lemma valid_idle_ep_cancel_all:
apply (rule hoare_vcg_conj_lift)
apply (rule hoare_Ball_helper)
apply (wp set_endpoint_obj_at | clarsimp simp :get_ep_queue_def not_idle_thread_def)+
apply (rename_tac list queue)
apply (rule_tac I = "(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1 and valid_idle" in mapM_x_inv_wp)
and ko_at (Endpoint Structures_A.IdleEP) word1
and valid_idle" in mapM_x_inv_wp)
apply clarsimp
apply (wp KHeap_DR.tcb_at_set_thread_state_wp)
apply (rule hoare_conjI)
apply (rule_tac P="(\<lambda>s. (queue = list) \<and> (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
and valid_idle and ko_at (kernel_object.Endpoint Structures_A.endpoint.IdleEP) word1"
and valid_idle and ko_at (Endpoint Structures_A.IdleEP) word1"
in hoare_vcg_precond_imp)
apply (rule set_thread_state_ko)
apply (simp add:is_tcb_def)
@ -758,7 +763,7 @@ lemma valid_idle_ep_cancel_all:
apply (clarsimp simp:is_tcb_def valid_ep_def obj_at_def)
apply (drule(1) pending_thread_in_recv_not_idle)
apply (simp add:not_idle_thread_def obj_at_def is_ep_def)+
done
done
lemma set_aep_obj_at:
"\<lbrace>\<lambda>s. P (kernel_object.AsyncEndpoint ep)\<rbrace> set_async_ep ptr ep \<lbrace>\<lambda>rv. obj_at P ptr\<rbrace>"
@ -767,14 +772,16 @@ lemma set_aep_obj_at:
apply (simp add:get_object_def)
apply wp
apply clarsimp
done
done
lemma valid_idle_aep_cancel_all:
"\<lbrace>valid_idle and valid_state :: det_state \<Rightarrow> bool\<rbrace> IpcCancel_A.aep_cancel_all word1 \<lbrace>\<lambda>a. valid_idle\<rbrace>"
apply (simp add:aep_cancel_all_def)
apply (wp|wpc|simp)+
apply (rename_tac list)
apply (rule_tac I = "(\<lambda>s. (\<forall>a\<in> set list. tcb_at a s \<and> not_idle_thread a s))
and ko_at (kernel_object.AsyncEndpoint async_ep.IdleAEP) word1 and valid_idle" in mapM_x_inv_wp)
and ko_at (kernel_object.AsyncEndpoint async_ep.IdleAEP) word1
and valid_idle" in mapM_x_inv_wp)
apply clarsimp
apply (wp KHeap_DR.tcb_at_set_thread_state_wp)
apply (rule hoare_conjI)
@ -796,7 +803,7 @@ lemma valid_idle_aep_cancel_all:
apply (clarsimp simp:is_tcb_def valid_aep_def obj_at_def)
apply (drule(1) pending_thread_in_wait_not_idle)
apply (simp add:not_idle_thread_def obj_at_def is_aep_def)+
done
done
lemma not_idle_after_reply_ipc_cancel:
"\<lbrace>not_idle_thread obj_id' and invs :: det_state \<Rightarrow> bool \<rbrace> reply_ipc_cancel obj_id'
@ -810,8 +817,7 @@ lemma not_idle_after_reply_ipc_cancel:
apply simp
apply (rule hoare_strengthen_post[OF get_cap_idle])
apply simp
apply (case_tac capa)
apply (simp_all add:fast_finalise.simps)
apply (case_tac capa; simp)
apply (clarsimp simp:when_def | rule conjI)+
apply (wp valid_idle_ep_cancel_all valid_idle_aep_cancel_all | clarsimp)+
apply (rule hoare_strengthen_post[where Q="\<lambda>r. valid_state and valid_idle"])
@ -821,7 +827,7 @@ lemma not_idle_after_reply_ipc_cancel:
apply (rule hoare_strengthen_post)
apply (rule hoare_vcg_precond_imp[OF thread_set_invs_trivial])
apply (simp add:tcb_cap_cases_def invs_def valid_state_def)+
done
done
lemma not_idle_thread_async_ipc_cancel:
"\<lbrace>not_idle_thread obj_id' and valid_idle\<rbrace> async_ipc_cancel obj_id' word \<lbrace>\<lambda>r. valid_idle\<rbrace>"
@ -829,7 +835,7 @@ lemma not_idle_thread_async_ipc_cancel:
apply (wp valid_idle_set_thread_state|wpc)+
apply (rule hoare_strengthen_post[OF get_aep_sp])
apply (clarsimp simp:not_idle_thread_def obj_at_def is_aep_def)
done
done
lemma not_idle_after_restart [wp]:
"\<lbrace>invs and not_idle_thread obj_id' :: det_state \<Rightarrow> bool\<rbrace> Tcb_A.restart obj_id'
@ -846,7 +852,7 @@ lemma not_idle_after_restart [wp]:
apply (rule hoare_strengthen_post)
apply (wp gts_inv)
apply (clarsimp)
done
done
lemma not_idle_after_suspend [wp]:
"\<lbrace>invs and not_idle_thread obj_id' and tcb_at obj_id'\<rbrace> IpcCancel_A.suspend obj_id'
@ -855,7 +861,7 @@ lemma not_idle_after_suspend [wp]:
apply (rule hoare_vcg_precond_imp)
apply (rule suspend_invs)
apply (simp add:not_idle_thread_def invs_def valid_state_def)+
done
done
crunch valid_etcbs[wp]: "switch_if_required_to", "Tcb_A.restart" "valid_etcbs"
@ -873,14 +879,14 @@ lemma invoke_tcb_corres_copy_regs:
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split [where r'=dc])
apply (rule corres_cases [where R="d"])
apply (clarsimp simp: K_bind_def when_def)
apply (clarsimp simp: when_def)
apply (rule corres_bind_ignore_ret_rhs)
apply (rule corres_return_dc_rhs)
apply (rule invoke_tcb_corres_copy_regs_loop)
apply (clarsimp simp: when_def)
apply (rule dummy_corrupt_tcb_intent_corres)
apply (rule corres_cases [where R="c"])
apply (clarsimp simp: K_bind_def when_def)
apply (clarsimp simp: when_def)
apply (rule corres_bind_ignore_ret_rhs)
apply (rule corres_corrupt_tcb_intent_dupl)
apply (rule corres_split [where r'=dc])
@ -906,7 +912,7 @@ lemma invoke_tcb_corres_copy_regs:
apply (rule corres_alternate2)
apply (rule corres_free_return [where P="\<top>" and P'="\<top>"])
apply (wp)
apply (clarsimp simp:conj_ac)
apply (clarsimp simp:conj_comms)
apply (clarsimp simp :not_idle_thread_def | wp)+
apply (rule corres_cases [where R="a"])
apply (clarsimp simp: when_def)
@ -954,7 +960,7 @@ lemma get_cap_ex_cte_cap_wp_to:
apply (rule cte_wp_at_weakenE)
apply simp
apply (clarsimp simp:is_cap_simps)
done
done
crunch idle[wp] : cap_delete "\<lambda>s. P (idle_thread (s :: det_ext state))"
(wp: crunch_wps simp: crunch_simps)
@ -980,36 +986,41 @@ lemma dcorres_corrupt_tcb_intent_ipcbuffer_upd:
apply (clarsimp simp:transform_tcb_def)
apply (simp add: get_etcb_def)
apply (clarsimp dest!: get_tcb_SomeD get_etcb_SomeD split:option.splits)+
apply (clarsimp simp:opt_object_tcb
not_idle_thread_def dest!:get_tcb_rev get_etcb_rev)
done
apply (clarsimp simp: opt_object_tcb not_idle_thread_def dest!:get_tcb_rev get_etcb_rev)
done
lemma arch_same_obj_as_lift:
"\<lbrakk>cap_aligned a;is_arch_cap a;ca = transform_cap a;cb=transform_cap b\<rbrakk>
\<Longrightarrow> cdl_same_arch_obj_as (ca) (cb) = same_object_as a b"
apply (clarsimp simp:is_arch_cap_def split:cap.split_asm)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (case_tac arch_capa)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (clarsimp simp:cdl_same_arch_obj_as_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply ((clarsimp simp:cdl_same_arch_obj_as_def)+)[5]
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (case_tac arch_capa)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (case_tac arch_capa)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
apply (simp add:same_object_as_def)
apply (clarsimp split:cap.splits simp:cdl_same_arch_obj_as_def)
apply (case_tac arch_capa)
apply (rename_tac arch_cap)
apply (case_tac arch_cap)
apply (fastforce simp:cdl_same_arch_obj_as_def cap_aligned_def)+
done
done
lemma thread_set_valid_irq_node:
"(\<And>t getF v. (getF, v) \<in> ran tcb_cap_cases \<Longrightarrow> getF (f t) = getF t)
@ -1023,7 +1034,7 @@ lemma thread_set_valid_irq_node:
apply (clarsimp simp:obj_at_def is_cap_table_def dest!:get_tcb_SomeD)
apply (drule_tac x = irq in spec)
apply clarsimp
done
done
lemma update_ipc_buffer_valid_objs:
"\<lbrace>valid_objs and K(is_aligned a msg_align_bits)\<rbrace>
@ -1033,8 +1044,7 @@ lemma update_ipc_buffer_valid_objs:
apply (clarsimp simp:valid_tcb_def)
apply (intro conjI allI)
apply (clarsimp simp:tcb_cap_cases_def)
apply (auto simp:valid_ipc_buffer_cap_def
split:cap.splits arch_cap.splits)
apply (auto simp:valid_ipc_buffer_cap_def split:cap.splits arch_cap.splits)
done
lemma dcorres_tcb_empty_slot:
@ -1043,13 +1053,11 @@ lemma dcorres_tcb_empty_slot:
(cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and valid_pdpt_objs and valid_etcbs)
(tcb_empty_thread_slot thread idx) (cap_delete slot)"
apply (simp add:liftE_bindE tcb_empty_thread_slot_def)
apply (simp add:opt_cap_def gets_the_def
assert_opt_def gets_def bind_assoc split_def)
apply (simp add:opt_cap_def gets_the_def assert_opt_def gets_def bind_assoc split_def)
apply (rule dcorres_absorb_get_l)
apply (clarsimp simp add:cte_at_into_opt_cap)
apply (erule impE)
apply (clarsimp simp: not_idle_thread_def
dest!:invs_valid_idle)
apply (clarsimp simp: not_idle_thread_def dest!:invs_valid_idle)
apply (simp add:opt_cap_def whenE_def split_def)
apply (intro conjI impI)
apply (case_tac slot,clarsimp)
@ -1131,9 +1139,9 @@ lemma dcorres_tcb_update_ipc_buffer:
apply (clarsimp simp :emptyable_def not_idle_thread_def)+
apply (erule tcb_at_cte_at)
apply (simp add:tcb_cap_cases_def)
(* Main Part *)
(* Main Part *)
apply (clarsimp simp:tcb_update_ipc_buffer_def tcb_update_thread_slot_def transform_tcb_slot_simp[symmetric])
apply (drule_tac s="transform_cslot_ptr ?a" in sym)
apply (drule_tac s="transform_cslot_ptr a" for a in sym)
apply (clarsimp simp:check_cap_at_def)
apply (rule dcorres_expand_pfx)
apply (subst alternative_com)
@ -1160,9 +1168,12 @@ lemma dcorres_tcb_update_ipc_buffer:
apply (rule dcorres_insert_cap_combine)
apply (clarsimp+)[2]
apply (rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top>]],simp)
apply (rule_tac Q = "\<lambda>r s. cte_wp_at (op = cap.NullCap) (obj_id', tcb_cnode_index 4) s \<and> cte_wp_at (\<lambda>_. True) (ab, ba) s
\<and> valid_global_refs s \<and> valid_idle s \<and> valid_irq_node s \<and> valid_mdb s \<and> valid_objs s\<and> not_idle_thread ab s \<and> valid_etcbs s
\<and> ((is_thread_cap r \<and> obj_ref_of r = obj_id') \<longrightarrow> ex_cte_cap_wp_to (\<lambda>_. True) (obj_id', tcb_cnode_index 4) s)"
apply (rule_tac Q = "\<lambda>r s. cte_wp_at (op = cap.NullCap) (obj_id', tcb_cnode_index 4) s
\<and> cte_wp_at (\<lambda>_. True) (ab, ba) s
\<and> valid_global_refs s \<and> valid_idle s \<and> valid_irq_node s
\<and> valid_mdb s \<and> valid_objs s\<and> not_idle_thread ab s \<and> valid_etcbs s
\<and> ((is_thread_cap r \<and> obj_ref_of r = obj_id') \<longrightarrow>
ex_cte_cap_wp_to (\<lambda>_. True) (obj_id', tcb_cnode_index 4) s)"
in hoare_strengthen_post)
apply (wp get_cap_ex_cte_cap_wp_to,clarsimp)
apply (clarsimp simp:same_object_as_def)
@ -1170,7 +1181,7 @@ lemma dcorres_tcb_update_ipc_buffer:
apply (wp hoare_when_wp)
apply (rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top>]],clarsimp+)
apply (rule hoare_drop_imp,wp)
apply (clarsimp simp:conj_ac)
apply (clarsimp simp:conj_comms)
apply (wp thread_set_global_refs_triv thread_set_valid_idle)
apply (clarsimp simp:tcb_cap_cases_def)
apply (wp thread_set_valid_idle thread_set_valid_irq_node)
@ -1178,24 +1189,25 @@ lemma dcorres_tcb_update_ipc_buffer:
apply (wp thread_set_mdb)
apply (fastforce simp:tcb_cap_cases_def)
apply (simp add:not_idle_thread_def)
apply (wp thread_set_cte_at update_ipc_buffer_valid_objs
thread_set_valid_cap thread_set_cte_wp_at_trivial)
apply (wp thread_set_cte_at update_ipc_buffer_valid_objs thread_set_valid_cap thread_set_cte_wp_at_trivial)
apply (fastforce simp:tcb_cap_cases_def)
apply (simp add: transform_tcb_slot_4)
apply (rule hoare_post_impErr[OF validE_R_validE[OF hoare_True_E_R]])
apply simp+
apply (rule_tac Q = "\<lambda>r s. invs s \<and> valid_etcbs s \<and> not_idle_thread (fst a') s \<and> tcb_at obj_id' s
\<and> not_idle_thread obj_id' s \<and> not_idle_thread ab s \<and> cte_wp_at (\<lambda>_. True) (ab,ba) s \<and>
cte_wp_at (\<lambda>c. c = cap.NullCap) (obj_id', tcb_cnode_index 4) s \<and> is_aligned a msg_align_bits"
\<and> not_idle_thread obj_id' s \<and> not_idle_thread ab s \<and> cte_wp_at (\<lambda>_. True) (ab,ba) s
\<and> cte_wp_at (\<lambda>c. c = cap.NullCap) (obj_id', tcb_cnode_index 4) s \<and> is_aligned a msg_align_bits"
in hoare_post_impErr[where E="\<lambda>x. \<top>"])
apply (simp add:not_idle_thread_def)
apply (wp cap_delete_cte_at cap_delete_deletes cap_delete_valid_cap)
apply (clarsimp simp:invs_valid_objs invs_mdb invs_valid_idle)
apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def)
apply (erule cte_wp_at_weakenE,simp+)
apply (erule cte_wp_at_weakenE, erule sym)
apply simp
apply simp
apply (clarsimp simp:emptyable_def not_idle_thread_def)
apply (erule tcb_at_cte_at,clarsimp)
done
done
lemma dcorres_tcb_update_vspace_root:
"dcorres (dc \<oplus> dc) (\<top>) ( invs and valid_etcbs and tcb_at obj_id'
@ -1348,7 +1360,7 @@ lemma dcorres_tcb_update_cspace_root:
apply (simp add:transform_tcb_slot_0)
apply (simp add:validE_def,rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top> ]])
apply fastforce
apply (clarsimp simp:conj_ac)
apply (clarsimp simp:conj_comms)
apply (rule_tac Q = "\<lambda>r s. invs s \<and> valid_etcbs s \<and> not_idle_thread ba s \<and> valid_cap aaa s \<and>
not_idle_thread (fst a') s \<and> cte_wp_at (\<lambda>_. True) (ba, c) s \<and>
cte_wp_at (\<lambda>c. c = cap.NullCap) (obj_id', tcb_cnode_index 0) s \<and>
@ -1459,10 +1471,6 @@ lemma option_set_priority_corres:
apply (wp reschedule_required_transform tcb_sched_action_transform thread_set_priority_transform | simp)+
done
declare option.weak_case_cong[cong]
declare if_weak_cong[cong]
crunch valid_etcbs[wp]: set_priority "valid_etcbs"
(wp: crunch_wps simp: crunch_simps)
@ -1496,6 +1504,7 @@ crunch valid_etcbs[wp]: option_update_thread "valid_etcbs"
(wp: crunch_wps simp: crunch_simps)
lemma dcorres_thread_control:
notes option.case_cong_weak [cong]
notes case_map_option [simp del]
shows
"\<lbrakk> t' = tcb_invocation.ThreadControl obj_id' a' fault_ep' prio' croot' vroot' ipc_buffer';
@ -1548,7 +1557,7 @@ lemma dcorres_thread_control:
apply (case_tac ipc_buffer')
apply (clarsimp simp:not_idle_thread_def)+
apply wp
apply (clarsimp simp:conj_ac)
apply (clarsimp simp:conj_comms)
apply (wp cap_delete_deletes cap_delete_valid_cap)
apply (strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg)
apply (clarsimp simp:tcb_cap_cases_def)
@ -1567,7 +1576,8 @@ lemma dcorres_thread_control:
apply (wp cap_delete_cte_at cap_delete_valid_cap)
apply (rule_tac Q'="\<lambda>_. ?P" in hoare_post_imp_R[rotated])
apply (clarsimp simp:is_valid_vtable_root_def is_cnode_or_valid_arch_def
is_arch_cap_def not_idle_thread_def emptyable_def split:option.splits)
is_arch_cap_def not_idle_thread_def emptyable_def
split:option.splits)
apply (wpc|wp)+
apply (wp checked_insert_tcb_invs | clarsimp)+
apply (rule check_cap_at_stable,(simp add:not_idle_thread_def | wp)+)+
@ -1608,7 +1618,8 @@ lemma dcorres_thread_control:
apply (wp case_option_wpE)
apply (rule_tac Q="\<lambda>_. ?P" in hoare_strengthen_post[rotated])
apply (clarsimp simp:is_valid_vtable_root_def is_cnode_or_valid_arch_def
is_arch_cap_def not_idle_thread_def emptyable_def split:option.splits)
is_arch_cap_def not_idle_thread_def emptyable_def
split:option.splits)
apply (rule_tac P = "(case fault_ep' of None \<Rightarrow> True | Some bl \<Rightarrow> length bl = WordSetup.word_bits)" in hoare_gen_asm)
apply (wp out_invs_trivialT)
apply (clarsimp simp:tcb_cap_cases_def)+
@ -1630,12 +1641,11 @@ lemma invoke_tcb_corres_thread_control:
(Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (rule corres_guard_imp[OF dcorres_thread_control])
apply fastforce
apply ((clarsimp simp:conj_ac
valid_cap_aligned simp del:split_paired_All)+)[2]
apply ((clarsimp simp:conj_comms valid_cap_aligned simp del:split_paired_All)+)[2]
apply (elim conjE)
apply (subgoal_tac "\<forall>x. ex_cte_cap_to x s \<longrightarrow> not_idle_thread (fst x) s")
apply (intro conjI)
apply ((clarsimp simp del:split_paired_All split:option.splits)+)[19] (* Brittle proof. Change number? *)
apply ((clarsimp simp del:split_paired_All split:option.splits)+)[19]
apply (case_tac ipc_buffer',simp)
apply (case_tac "snd a",simp)
apply (clarsimp simp del:split_paired_All split:option.splits)
@ -1652,7 +1662,7 @@ lemma invoke_tcb_corres_thread_control:
apply clarsimp
apply (drule ex_cte_cap_wp_to_not_idle)+
apply (clarsimp simp:invs_def valid_state_def valid_pspace_def)+
done
done
lemma invoke_tcb_corres_suspend:
"\<lbrakk> t' = tcb_invocation.Suspend obj_id';

71
proof/drefine/Untyped_DR.thy
View File

@ -71,8 +71,7 @@ next
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask
del: word_neq_0_conv)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
done
have loadWord_atMostOneResult:
@ -80,8 +79,7 @@ next
apply (case_tac "is_aligned a 2")
apply (simp add: loadWord_def is_aligned_mask exec_gets)
apply (simp add: return_def)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask
del: word_neq_0_conv)
apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask)
done
have mapM_loadWord_atMostOneResult[rule_format]:
@ -288,7 +286,7 @@ lemma freeMemory_dcorres:
\<lambda>_ _. is_arch_cap or op = cap.NullCap)" in bspec)
apply (simp add: ran_tcb_cap_cases)
apply clarsimp
apply (thin_tac "case_option ?x ?y ?z")
apply (thin_tac "case_option x y z" for x y z)
apply (simp add: valid_ipc_buffer_cap_def)
apply (drule valid_page_cap_imp_valid_buf)
apply (frule_tac transform_full_intent_machine_state_eq, simp_all)
@ -299,7 +297,7 @@ lemma freeMemory_dcorres:
mask_2pm1[symmetric])
apply (erule_tac x="(p && ~~ mask (pageBitsForSize sz))" in allE)
apply clarsimp
apply (thin_tac "length ?xs = ?y")
apply (thin_tac "length xs = y" for xs y)
apply (clarsimp simp:is_aligned_neg_mask_eq)
apply (erule impE)
apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help)
@ -309,7 +307,7 @@ lemma freeMemory_dcorres:
apply simp
apply (cut_tac ptr = p and n = "pageBitsForSize sz" in word_neg_and_le)
apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help)
apply (thin_tac "?x\<noteq>?y")
apply (thin_tac "x\<noteq>y" for x y)
apply (erule notE)
apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask])
apply (rule le_refl)
@ -403,7 +401,7 @@ definition
lemma transform_empty_cnode:
"transform_cnode_contents o_bits (empty_cnode o_bits) = empty_cap_map o_bits"
apply (simp add: transform_cnode_contents_def wf_empty dom_empty_cnode)
apply (simp add: transform_cnode_contents_def dom_empty_cnode)
apply (rule ext, simp add: option_map_join_def empty_cap_map_def
nat_to_bl_def len_bin_to_bl_aux)
done
@ -420,7 +418,7 @@ lemma transform_default_tcb:
get_ipc_buffer_words_def)
apply (simp add: transform_intent_def invocation_type_def fromEnum_def
enum_invocation_label toEnum_def)
apply (simp add: fun_eq_iff tcb_slot_defs tcb_pending_op_slot_def)
apply (simp add: fun_eq_iff tcb_slot_defs)
apply (simp add: infer_tcb_pending_op_def guess_error_def default_etcb_def default_domain_def)
done
@ -449,9 +447,9 @@ lemma obj_bits_bound32:
\<Longrightarrow>obj_bits_api type us < WordSetup.word_bits"
apply (case_tac type)
apply (simp_all add:obj_bits_api_def word_bits_def slot_bits_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type)
apply (simp_all add:arch_kobj_size_def
default_arch_object_def pageBits_def)
apply (simp_all add:arch_kobj_size_def default_arch_object_def pageBits_def)
done
lemma obj_bits_bound4:
@ -459,9 +457,9 @@ lemma obj_bits_bound4:
4 \<le> obj_bits_api type us"
apply (case_tac type)
apply (simp_all add:obj_bits_api_def word_bits_def slot_bits_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type)
apply (simp_all add:arch_kobj_size_def
default_arch_object_def pageBits_def)
apply (simp_all add:arch_kobj_size_def default_arch_object_def pageBits_def)
done
lemma distinct_retype_addrs:
@ -540,7 +538,7 @@ lemma retype_transform_obj_ref_pick_id:
"type \<noteq> Structures_A.Untyped
\<Longrightarrow> map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref type us) xs)
= map (retype_transform_obj_ref type us) xs"
by (simp add:retype_transform_obj_ref_def map_map)
by (simp add:retype_transform_obj_ref_def)
lemma translate_object_type_not_untyped:
"type \<noteq> Invariants_AI.Untyped
@ -595,8 +593,8 @@ lemma retype_region_dcorres:
apply (simp add: retype_region_def Untyped_D.retype_region_def
split del: split_if)
apply (clarsimp simp:when_def generate_object_ids_def bind_assoc
split del:if_splits)
apply (simp add:retype_addrs_fold split del:if_splits)
split del:split_if)
apply (simp add:retype_addrs_fold split del:split_if)
apply (case_tac "type = Invariants_AI.Untyped")
apply (rule corres_guard_imp)
apply (simp add:translate_object_type_def)
@ -621,7 +619,6 @@ lemma retype_region_dcorres:
defer
apply clarsimp
apply (frule invs_valid_idle,clarsimp simp:valid_idle_def st_tcb_at_def obj_at_def)
apply (erule(3) pspace_no_overlapC)
apply clarsimp
apply simp
@ -629,13 +626,9 @@ lemma retype_region_dcorres:
apply wp
apply fastforce
apply simp
apply (case_tac type,
simp_all add:translate_object_type_def)
apply (case_tac type, simp_all add:translate_object_type_def)
apply (rename_tac aobject_type)
apply (case_tac aobject_type,simp_all)
done
lemma page_objects_default_object:
@ -679,7 +672,7 @@ lemma clearMemory_unused_corres_noop:
apply (subgoal_tac "y && ~~ mask (obj_bits_api ty us) = p")
apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter
split: cap.split_asm arch_cap.split_asm)
apply (cut_tac t="(?t, tcb_cnode_index 4)" and P="op = ?cap"
apply (cut_tac t="(t, tcb_cnode_index 4)" and P="op = cap" for t cap
in cte_wp_at_tcbI, simp, fastforce, simp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (drule(1) bspec)
@ -701,12 +694,6 @@ lemma clearMemory_unused_corres_noop:
apply (wp | simp)+
done
lemma word_neq0:
"(a \<noteq> (0::word32)) = ((0::word32) < a)"
apply (rule ccontr)
apply (simp add:not_less)
done
lemma dcorres_create_word_objects:
"\<lbrakk> 0 < n; ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj};
xsz = obj_bits_api ty us \<rbrakk>
@ -730,7 +717,7 @@ lemma dcorres_create_word_objects:
apply (rule corres_split[OF corres_trivial])
apply simp
apply (rule corres_mapM_to_mapM_x)
apply (rule_tac P=\<top> and P'="?P" and S = "{(x,y). y \<in> set ?M}"
apply (rule_tac P=\<top> and P'="P" and S = "{(x,y). y \<in> set M}" for P M
in corres_mapM_x[where f="\<lambda>_. return ()", OF _ _ _ refl,
simplified mapM_x_return])
apply clarsimp
@ -740,8 +727,7 @@ lemma dcorres_create_word_objects:
apply simp
apply wp
apply (wp hoare_vcg_ball_lift | simp)+
apply (clarsimp simp:zip_same retype_addrs_def ptr_add_def
image_def shiftl_t2n)
apply (clarsimp simp:zip_same retype_addrs_def ptr_add_def image_def shiftl_t2n)
apply (rule_tac x = "unat x" in bexI)
apply simp
apply clarsimp
@ -1304,7 +1290,7 @@ lemma free_range_of_untyped_pick_retype_addrs:
apply (subst group_add_class.add_diff_eq[symmetric])
apply (frule range_cover_not_zero_shift[rotated,OF _ le_refl])
apply simp
apply (thin_tac "\<not> ?P")
apply (thin_tac "\<not>P" for P)
apply (subst add.assoc[symmetric])
apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n = sz])
apply (subst add.commute[where a = "(ptr && mask sz)"])
@ -1740,7 +1726,7 @@ lemma descendants_of_empty_lift :
apply clarsimp
apply (frule transform_cdt_dom_standard)
apply (clarsimp simp:descendants_of_def)
apply (thin_tac "(a,b) = ?P")
apply (thin_tac "(a,b) = P" for P)
apply (drule(1) transform_cdt_some_rev)
apply (clarsimp simp:valid_mdb_def)
apply clarsimp
@ -1815,6 +1801,7 @@ lemma decode_untyped_corres:
unlessE_whenE
split del: split_if
split: invocation_label.split_asm)
apply (rename_tac a list w1 w2 w3 w4 w5 apiobject_type)
apply (cases excaps')
apply (simp add: get_index_def transform_cap_list_def
alternative_refl)
@ -1840,7 +1827,7 @@ lemma decode_untyped_corres:
apply auto[1]
apply (rename_tac cnode_cap cnode_cap')
apply (simp add: bindE_assoc split del: split_if)
apply (simp add: if_to_top_of_bindE is_cnode_cap_eq[symmetric]
apply (simp add: if_to_top_of_bindE is_cnode_cap_transform_cap[symmetric]
split del: split_if)
apply (rule corres_if_rhs[rotated])
apply (rule corres_trivial, simp add: alternative_refl)
@ -1866,7 +1853,7 @@ lemma decode_untyped_corres:
apply (erule is_aligned_weaken)
apply (simp add:range_cover_def)
apply (simp add:has_children_def KHeap_D.is_cdt_parent_def
descendants_of_empty_lift word_neq0)
descendants_of_empty_lift word_neq_0_conv)
apply (subst alignUp_gt_0[where x = "2 ^ sz"])
apply (rule is_aligned_weaken[where x = sz])
apply (simp add:is_aligned_def)
@ -1900,10 +1887,10 @@ lemma decode_untyped_corres:
apply (rule corres_guard_imp)
apply (rule_tac F="cap_aligned cnode_cap' \<and> is_cnode_cap cnode_cap'" in corres_gen_asm2)
apply (subgoal_tac "map (Pair (cap_object (transform_cap cnode_cap')))
[unat word4 ..< unat word4 + unat word5]
[unat w4 ..< unat w4 + unat w5]
= map (\<lambda>x. transform_cslot_ptr (obj_ref_of (cnode_cap'),
(nat_to_cref (bits_of cnode_cap') x)))
[unat word4 ..< unat word4 + unat word5]")
[unat w4 ..< unat w4 + unat w5]")
apply (simp del: map_eq_conv)
apply (simp add: mapME_x_map_simp)
apply (rule mapME_x_corres_inv)
@ -1919,7 +1906,7 @@ lemma decode_untyped_corres:
apply (rule hoare_pre)
apply (wp hoare_drop_imp | simp)+
apply fastforce
apply (clarsimp simp:is_cnode_cap_eq conj_ac split del:if_splits)
apply (clarsimp simp: conj_comms is_cnode_cap_transform_cap split del: split_if)
apply (rule validE_R_validE)
apply (rule_tac Q' = "\<lambda>a s. invs s \<and> valid_etcbs s \<and> valid_cap a s \<and> cte_wp_at (op = (cap.UntypedCap ptr sz idx)) slot' s
\<and> (Structures_A.is_cnode_cap a \<longrightarrow> not_idle_thread (obj_ref_of a) s)"
@ -1930,7 +1917,7 @@ lemma decode_untyped_corres:
in hoare_post_imp_R)
apply wp
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule_tac p = "(?x,?y)" in caps_of_state_valid[rotated])
apply (frule_tac p = "(x,y)" for x y in caps_of_state_valid[rotated])
apply simp
apply (clarsimp simp:valid_cap_def obj_at_def valid_idle_def st_tcb_at_def
is_cap_simps not_idle_thread_def is_cap_table_def dest!:invs_valid_idle)
@ -1964,7 +1951,7 @@ lemma decode_untyped_label_not_match:
apply (clarsimp simp:transform_intent_untyped_retype_def split:option.splits list.splits)
apply (simp add:Decode_A.decode_untyped_invocation_def unlessE_def)
apply wp
done
done
end