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

Isabelle2018: DRefine

This commit is contained in:
Gerwin Klein 2018-06-24 09:47:21 +02:00
parent a7782f4af4
commit 1e8a7505ef
11 changed files with 75 additions and 90 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
proof/drefine/Arch_DR.thy
View File

@ -1117,7 +1117,7 @@ lemma set_cap_opt_cap':
split del:if_split cong: if_cong bind_cong;
wpsimp wp: select_wp)
apply (safe elim!:rsubst[where P=P] intro!: ext)
apply (clarsimp simp:opt_cap_def slots_of_def opt_object_def object_slots_def)+
apply (clarsimp simp:opt_cap_def slots_of_def opt_object_def object_slots_def)+
done
lemma set_cap_opt_cap:
@ -1213,7 +1213,7 @@ lemma invoke_page_table_corres:
corres_split[OF _ corres_alternate1[OF dcorres_clear_object_caps_pt]])
apply (rule dcorres_symb_exec_r)
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at ((=xb)) (a,b) s \<and>
apply (rule_tac P="\<lambda>y s. cte_wp_at ((=) xb) (a,b) s \<and>
caps_of_state s' = caps_of_state s" in set_cap_corres_stronger)
apply (clarsimp simp:cte_wp_at_caps_of_state)
apply (clarsimp simp:is_arch_diminished_def transform_mapping_def update_map_data_def)
@ -1652,7 +1652,7 @@ lemma invoke_page_corres:
apply (rule corres_guard_imp)
apply (rule corres_split[OF _ dcorres_unmap_page])
apply (rule corres_split[OF _ get_cap_corres])
apply (rule_tac P="\<lambda>y s. cte_wp_at ((=x)) (a,b) s \<and>
apply (rule_tac P="\<lambda>y s. cte_wp_at ((=) x) (a,b) s \<and>
caps_of_state s' = caps_of_state s"
in set_cap_corres_stronger)
apply (clarsimp simp:cte_wp_at_caps_of_state)
@ -1808,7 +1808,7 @@ proof -
apply (clarsimp simp: valid_cap_simps cap_aligned_def)
apply (drule ex_cte_cap_to_not_idle,
auto simp: not_idle_thread_def)[1]
apply (subst safe_parent_is_parent[where m=empty],
apply (subst safe_parent_is_parent[where m=Map.empty],
auto simp: safe_parent_for_def
is_physical_def arch_is_physical_def)[1]
apply (case_tac cref,clarsimp)

12
proof/drefine/Corres_D.thy
View File

@ -29,7 +29,7 @@ lemma select_ext_select[simp]: "select_ext a S = (select S :: ('b, unit) s_monad
return_def bind_def fail_def image_def
split: if_split_asm)
lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f OR g)"
lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f \<sqinter> g)"
apply (rule ext, rename_tac s)
apply (clarsimp simp: OR_choice_def alternative_def get_def select_def return_def bind_def
select_f_def mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def
@ -166,7 +166,7 @@ using assms
by (fastforce simp:corres_underlying_def)
lemma dcorres_absorb_get_l:
assumes "!!s'. \<lbrakk> P (transform s');P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=s')) (f (transform s')) g"
assumes "!!s'. \<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g"
shows "dcorres rv P P' (do t\<leftarrow> get; f t od) g"
apply (rule corres_symb_exec_l [where Q="%x. P and ((=) x)"])
apply (rule dcorres_expand_pfx)
@ -178,7 +178,7 @@ lemma dcorres_absorb_get_l:
lemma dcorres_expand_get_l:
assumes "dcorres rv P P' (do t\<leftarrow>get; f t od) g"
shows "\<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow>
dcorres rv ((=) (transform s')) ((=s')) (f (transform s')) g"
dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g"
using assms
by (simp add:get_def corres_underlying_def bind_def)
@ -216,7 +216,7 @@ lemma dcorres_get:
\<Longrightarrow> dcorres r ((=) s) ((=) s') (f s) (f' s')"
shows "dcorres r P P' (do s\<leftarrow>get;f s od) (do s'\<leftarrow> get; f' s' od)"
apply (rule dcorres_expand_pfx)
apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and P="%x. (=s)" and P'="%x. (=s')" in corres_underlying_split)
apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and P="%x. (=) s" and P'="%x. (=) s'" in corres_underlying_split)
apply (clarsimp simp: corres_underlying_def get_def)
apply wp+
apply (drule A)
@ -239,8 +239,8 @@ lemma dcorres_gets_the:
apply (clarsimp split:option.splits simp:corres_free_fail)
apply (subgoal_tac "\<exists>obj. g x \<noteq> None")
apply (clarsimp split:option.splits)
apply (rule_tac Q="(=)(transform xa)" and Q'="(=xa)" in corres_guard_imp)
apply (simp add:A)+
apply (rule_tac Q="(=)(transform xa)" and Q'="(=) xa" in corres_guard_imp)
apply (simp add: A)+
using B
apply (wp|clarsimp)+
done

4
proof/drefine/Finalise_DR.thy
View File

@ -444,7 +444,7 @@ lemma finalise_cancel_ipc:
tcb_at_cte_at_2[unfolded tcb_at_def])
apply (simp add:cancel_signal_def)
apply (rule corres_guard_imp)
apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=s')" in corres_symb_exec_r)
apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=) s'" in corres_symb_exec_r)
apply (rule corres_symb_exec_r)
apply (rule corres_dummy_return_pl)
apply (rule corres_split[ OF _ corres_dummy_set_notification])
@ -2616,7 +2616,7 @@ lemma prepare_thread_delete_dcorres: "dcorres dc P P' (CSpace_D.prepare_thread_d
lemma dcorres_finalise_cap:
"cdlcap = transform_cap cap \<Longrightarrow>
dcorres (\<lambda>r r'. fst r = transform_cap (fst r'))
\<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=cap)) slot and valid_etcbs)
\<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=) cap) slot and valid_etcbs)
(CSpace_D.finalise_cap cdlcap final)
(CSpace_A.finalise_cap cap final)"
apply (case_tac cap)

12
proof/drefine/Intent_DR.thy
View File

@ -316,7 +316,7 @@ lemma set_cxt_none_det_intent_corres:
(KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set cxt) obj')))"
apply (clarsimp simp:bind_assoc opt_object_def corrupt_tcb_intent_def get_thread_def gets_def gets_the_def)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=s')"
apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
and x="transform_full_intent (machine_state (update_kheap ((kheap s')(y\<mapsto>(TCB (tcb_arch_update (arch_tcb_context_set cxt) obj')))) s'))
y (tcb_arch_update (arch_tcb_context_set cxt) obj')"
in select_pick_corres)
@ -383,7 +383,7 @@ lemma dummy_corrupt_tcb_intent_corres:
apply (clarsimp simp:tcb_at_def)
apply (drule(1) valid_etcbs_get_tcb_get_etcb, clarsimp)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=s')"
apply (rule_tac P="(=)(transform s')" and Q="(=) s'"
and x = "transform_full_intent (machine_state s') y tcb" in select_pick_corres)
apply (clarsimp simp:update_thread_def gets_the_def gets_def bind_assoc)
apply (rule dcorres_absorb_get_l)
@ -476,7 +476,7 @@ lemma dcorres_dummy_corrupt_frame: "dcorres dc \<top> valid_etcbs
apply (simp add:corrupt_frame_def)
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp)
apply (rule_tac P="(=)(transform s')" and Q="(=s')"
apply (rule_tac P="(=)(transform s')" and Q="(=) 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 modify_def assert_def bind_def return_def)
apply (subst corres_singleton)
@ -1194,13 +1194,13 @@ lemma get_ipc_buffer_words_empty_list[simp]:
lemma evalMonad_mapM:
"\<lbrakk>\<forall>r\<in>(set ls). evalMonad (f r) sa = evalMonad (g r) sb;
\<And>s r. \<lbrace>(=s\<rbrace>f) r\<lbrace>\<lambda>r. (=) s\<rbrace>;
\<And>s r. \<lbrace>(=s\<rbrace>g) r\<lbrace>\<lambda>r. (=) s\<rbrace>;
\<And>s r. \<lbrace>(=) s\<rbrace> f r\<lbrace>\<lambda>r. (=) s\<rbrace>;
\<And>s r. \<lbrace>(=) s\<rbrace> g r\<lbrace>\<lambda>r. (=) s\<rbrace>;
\<And>r. empty_when_fail (f r);
\<And>r. empty_when_fail (g r);
\<And>r P. weak_det_spec P (f r);
\<And>r P. weak_det_spec P (g r)\<rbrakk>
\<Longrightarrow> evalMonad (mapM f ls) sa= evalMonad (mapM g ls) sb"
\<Longrightarrow> evalMonad (mapM f ls) sa = evalMonad (mapM g ls) sb"
proof(induct ls)
case Nil
show ?case by (clarsimp simp:mapM_def sequence_def)

2
proof/drefine/Interrupt_DR.thy
View File

@ -287,7 +287,7 @@ lemma handle_interrupt_corres:
apply (clarsimp split:irq_state.splits simp:corres_free_fail | rule conjI)+
apply (simp add:Interrupt_D.handle_interrupt_def bind_assoc)
apply (rule corres_guard_imp)
apply (rule_tac Q'="(=s')" in corres_split[OF _ dcorres_get_irq_slot])
apply (rule_tac Q'="(=) s'" in corres_split[OF _ dcorres_get_irq_slot])
apply (rule_tac R'="\<lambda>rv. (\<lambda>s. (is_ntfn_cap rv \<longrightarrow> ntfn_at (obj_ref_of rv) s)) and invs and valid_etcbs"
in corres_split[OF _ option_get_cap_corres])
apply (case_tac rv'a)

4
proof/drefine/Ipc_DR.thy
View File

@ -15,7 +15,7 @@ begin
context begin interpretation Arch . (*FIXME: arch_split*)
abbreviation
"thread_is_running y s \<equiv> st_tcb_at ((=Structures_A.thread_state.Running)) y s"
"thread_is_running y s \<equiv> st_tcb_at ((=) Structures_A.Running) y s"
lemmas [wp] = abs_typ_at_lifts[OF set_simple_ko_typ_at]
@ -2823,7 +2823,7 @@ lemma send_fault_ipc_corres:
apply (simp add:Endpoint_D.send_fault_ipc_def Ipc_A.send_fault_ipc_def)
apply (rule dcorres_expand_pfx)
apply (rule corres_guard_imp)
apply (rule_tac P'="(=s')" in thread_get_corresE[where tcb' = tcb and etcb'=etcb])
apply (rule_tac P'="(=) s'" in thread_get_corresE[where tcb' = tcb and etcb'=etcb])
apply simp_all
prefer 2
apply (rule conjI)

111
proof/drefine/KHeap_DR.thy
View File

@ -22,51 +22,46 @@ lemma nat_bl_to_bin_surj:
using n_less_equal_power_2[where n=n, folded of_nat_less_iff, simplified]
apply (rule_tac x="bin_to_bl n (int n)" in exI)
apply (simp only: bin_bl_bin bintrunc_mod2p)
apply (simp add: int_mod_eq')
apply simp
done
lemma
transform_tcb_slot_0:
lemma transform_tcb_slot_0:
"transform_cslot_ptr (a, tcb_cnode_index 0) = (a,tcb_cspace_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_cspace_slot_def)
apply (simp add: tcb_cnode_index_def bl_to_bin_def)
done
done
lemma
transform_tcb_slot_1:
lemma transform_tcb_slot_1:
"transform_cslot_ptr (a,tcb_cnode_index 1) = (a,tcb_vspace_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_vspace_slot_def)
apply (simp add: tcb_cnode_index_def)
done
done
lemma
transform_tcb_slot_2:
lemma transform_tcb_slot_2:
"transform_cslot_ptr (a,tcb_cnode_index 2) = (a,tcb_replycap_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_replycap_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
done
lemma
transform_tcb_slot_3:
lemma transform_tcb_slot_3:
"transform_cslot_ptr (a,tcb_cnode_index 3) = (a,tcb_caller_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_caller_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
done
lemma
transform_tcb_slot_4:
lemma transform_tcb_slot_4:
"transform_cslot_ptr (a,tcb_cnode_index 4) = (a,tcb_ipcbuffer_slot)"
apply (clarsimp simp:transform_cslot_ptr_def)
apply (unfold tcb_ipcbuffer_slot_def)
apply (simp add: tcb_cnode_index_def)
apply (simp add:bl_to_bin_def)
done
done
lemmas transform_tcb_slot_simp =
transform_tcb_slot_0 transform_tcb_slot_1
@ -76,10 +71,7 @@ lemmas transform_tcb_slot_simp =
lemma cap_table_at_cte_wp_at_length:
"\<lbrakk> cap_table_at n p s; cte_wp_at P (p, p') s \<rbrakk>
\<Longrightarrow> length p' = n"
apply (clarsimp simp: cte_wp_at_cases obj_at_def is_cap_table
well_formed_cnode_n_def length_set_helper)
apply auto
done
by (auto simp: cte_wp_at_cases obj_at_def is_cap_table well_formed_cnode_n_def length_set_helper)
context
begin
@ -248,10 +240,10 @@ lemma get_cur_thread_corres:
(gets_the cdl_current_thread)
(gets cur_thread)"
apply (simp add:gets_the_def gets_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def)
apply (simp add:corres_underlying_def not_idle_thread_def)
apply (rule dcorres_absorb_get_l)
apply (rule dcorres_absorb_get_r)
apply (clarsimp simp:assert_opt_def transform_def transform_current_thread_def)
apply (simp add:corres_underlying_def not_idle_thread_def)
done
lemma not_in_dom_dest:
@ -266,18 +258,17 @@ lemma nat_to_bl_dest:
"b\<in>Collect (%x. length x= n)\<Longrightarrow> nat_to_bl n (nat (bl_to_bin b)) = Some b"
apply (unfold nat_to_bl_def)
apply (subgoal_tac "0 \<le> bl_to_bin b")
apply (subst nat_0_le)
apply (subst nat_0_le)
apply simp
apply (subgoal_tac "length b = n")
apply (subgoal_tac "length b = n")
apply (erule subst[where s="length b" and t=n])
apply (subst bl_bin_bl)
apply (simp add: not_le)
apply (simp add: nat_less_iff[OF bl_to_bin_ge0])
apply (clarsimp simp: bl_to_bin_lt2p)
apply clarsimp
apply clarsimp
apply (simp add:not_less)
apply (rule bl_to_bin_ge0)
done
done
lemma bl_to_bin_tcb_cnode_index_le0:
"n < 8 \<Longrightarrow> (bl_to_bin (tcb_cnode_index n) \<le> 0) = (n = 0)"
@ -346,7 +337,7 @@ lemma get_cap_no_fail:
done
lemma get_cap_helper:
"dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=cap)) slot)) f (g cap)"
"dcorres r P (P') f (get_cap slot >>= g) \<Longrightarrow> dcorres r P (P' and (cte_wp_at ((=) cap) slot)) f (g cap)"
by (clarsimp simp:bind_def corres_underlying_def cte_wp_at_def)
lemma get_cap_corres:
@ -390,11 +381,7 @@ lemma nat2p: "nat (2^(x::nat)) = 2^(x::nat)"
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)
apply (rule iffD1[OF zless_nat_eq_int_zless])
apply (simp add:nat2p)
done
by (clarsimp simp:nat_to_bl_def bin_bl_bin' bintrunc_mod2p)
lemma cap_counts_inv:
assumes "\<And>cap. P cap\<Longrightarrow> cap_counts cap"
@ -2728,7 +2715,7 @@ lemma set_parent_corres:
done
lemma set_tcb_capslot_weak_valid_mdb:
"\<lbrace>weak_valid_mdb and cte_wp_at ((=cap.NullCap)) slot\<rbrace> set_cap cap slot \<lbrace>\<lambda>r s. weak_valid_mdb s\<rbrace> "
"\<lbrace>weak_valid_mdb and cte_wp_at ((=) 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)
@ -2742,7 +2729,7 @@ lemma get_tcb_reply_cap_wp_cte_at:
\<lbrace>\<lambda>rv. cte_wp_at ((\<noteq>) cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2)\<rbrace>"
apply (rule hoare_post_imp
[where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply simp+
@ -2756,51 +2743,51 @@ lemma get_tcb_reply_cap_wp_master_cap:
\<lbrace>\<lambda>rv s. (is_master_reply_cap rv) \<rbrace>"
apply (rule hoare_post_imp
[where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply simp+
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)+
apply (clarsimp simp:cte_wp_at_def)+
done
lemma get_tcb_reply_cap_wp_original_cap:
"\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
\<lbrace>\<lambda>rv s. is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrace>"
apply (rule hoare_post_imp
apply (rule hoare_post_imp
[where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb
and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
apply clarsimp
apply (subgoal_tac "is_master_reply_cap r \<and> obj_ref_of r = sid")
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply simp+
apply (clarsimp simp:valid_mdb_def reply_master_revocable_def)
apply (drule_tac x = "obj_ref_of r" in spec)
apply (drule_tac x = "tcb_cnode_index 2" in spec)
apply (drule_tac x = r in spec)
apply (drule iffD1[OF cte_wp_at_caps_of_state])+
apply clarsimp
apply (clarsimp simp:valid_mdb_def reply_master_revocable_def)
apply (drule_tac x = "obj_ref_of r" in spec)
apply (drule_tac x = "tcb_cnode_index 2" in spec)
apply (drule_tac x = r in spec)
apply (drule iffD1[OF cte_wp_at_caps_of_state])+
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
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
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
lemma get_tcb_reply_cap_wp_obj_ref:
"\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
\<lbrace>\<lambda>rv s. (obj_ref_of rv = sid) \<rbrace>"
apply (rule hoare_post_imp
apply (rule hoare_post_imp
[where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2)
and tcb_at sid and valid_objs and cte_wp_at ((=r)) (sid,tcb_cnode_index 2)"])
and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"])
apply clarsimp
apply (frule cte_wp_tcb_cap_valid)
apply simp+
apply simp+
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
apply (wp get_cap_cte_wp_at_rv)
apply (clarsimp simp:cte_wp_at_def)+
done
lemma tcb_reply_cap_cte_wp_at:
"\<lbrakk>valid_objs s;st_tcb_at (\<lambda>r. \<not> inactive r \<and> \<not> idle r) sid s\<rbrakk>
@ -3104,7 +3091,7 @@ lemma resolve_address_bits_error_corres:
\<not> in_recursive_branch ref cap;
cap = cap.CNodeCap oref radix_bits guard;
valid_cap cap s;valid_idle s;length ref \<le> 32;valid_objs s\<rbrakk>
\<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. (fst r) = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=s))
\<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. (fst r) = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=) s)
( CSpace_D.resolve_address_bits (cap') (of_bl ref) (length ref) )
( CSpace_A.resolve_address_bits (cap,ref) )"
apply (subst KHeap_DR.resolve_address_bits.simps)
@ -3148,7 +3135,7 @@ lemma resolve_address_bits_error_corres:
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>
\<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=s))
\<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. fst r = transform_cslot_ptr (fst r') \<and> snd r = length (snd r'))) \<top> ((=) s)
( CSpace_D.resolve_address_bits cap' (of_bl ref) (length ref) )
( CSpace_A.resolve_address_bits (cap,ref) )"
apply (subst KHeap_DR.resolve_address_bits.simps,frule resolve_address_bits_terminate_branch[where 'a=det_ext],fastforce)
@ -3364,8 +3351,6 @@ lemma dcorres_injection_handler_rhs:
apply (clarsimp simp:throwError_def return_def corres_underlying_def)+
done
crunch valid_etcbs[wp]: resolve_address_bits "valid_etcbs"
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 and valid_etcbs\<rbrace>
CSpace_A.resolve_address_bits (tcb_ctable obj, blist)

2
proof/drefine/Lemmas_D.thy
View File

@ -17,7 +17,7 @@
theory Lemmas_D
imports
Include_D
"DBaseRefine.Include_D"
MoreHOL
MoreCorres
"ExecSpec.InvocationLabels_H"

6
proof/drefine/StateTranslationProofs_DR.thy
View File

@ -119,7 +119,7 @@ lemma transform_full_intent_cong:
by (simp add: transform_full_intent_def get_tcb_message_info_def get_tcb_mrs_def Suc_le_eq get_ipc_buffer_words_def)
lemma caps_of_state_eq_lift:
"\<forall>cap. cte_wp_at ((=cap)) p s = cte_wp_at ((=cap)) p s' \<Longrightarrow> caps_of_state s p = caps_of_state s' p"
"\<forall>cap. cte_wp_at ((=) cap) p s = cte_wp_at ((=) cap) p s' \<Longrightarrow> caps_of_state s p = caps_of_state s' p"
apply (simp add:cte_wp_at_def caps_of_state_def)
done
@ -134,9 +134,9 @@ lemma caps_of_state_irrelavent_simp:
fun
caps_of_object :: "kernel_object \<Rightarrow> (bool list \<rightharpoonup> cap)"
where
"caps_of_object (Structures_A.CNode sz c) = (if well_formed_cnode_n sz c then c else empty)"
"caps_of_object (Structures_A.CNode sz c) = (if well_formed_cnode_n sz c then c else Map.empty)"
| "caps_of_object (Structures_A.TCB t) = (\<lambda>n. option_map (\<lambda>(f, _). f t) (tcb_cap_cases n))"
| "caps_of_object _ = empty"
| "caps_of_object _ = Map.empty"
lemma caps_of_state_def2:
"caps_of_state s = (\<lambda>ptr. case (option_map caps_of_object (kheap s (fst ptr))) of

2
proof/drefine/Syscall_DR.thy
View File

@ -258,7 +258,7 @@ lemma decode_domain_corres:
lemma decode_domain_cap_label_not_match:
"\<lbrakk>\<forall>ui. Some (DomainIntent ui) \<noteq> transform_intent (invocation_type label') args'\<rbrakk>
\<Longrightarrow> \<lbrace>(=s\<rbrace>Decode_A.decode_domain_invocation) label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=s\<rbrace>)"
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_domain_invocation label' args' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
apply (case_tac "invocation_type label' = DomainSetSet")
apply (clarsimp simp: Decode_A.decode_domain_invocation_def transform_intent_def)+
apply (clarsimp simp: transform_intent_domain_def split: option.splits list.splits)

2
proof/drefine/Tcb_DR.thy
View File

@ -190,7 +190,7 @@ lemma decode_set_space_translate_tcb_invocation:
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>
\<Longrightarrow> \<lbrace>(=s\<rbrace>Decode_A.decode_tcb_invocation) label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=s\<rbrace>)"
\<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_tcb_invocation label' args' cap' slot' excaps' \<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
apply (simp add:Decode_A.decode_tcb_invocation_def)
apply (case_tac "invocation_type label'")
apply (simp_all add:transform_intent_def)