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

arch-split: Tcb_AI.thy done

This commit is contained in:
Miki Tanaka 2016-06-29 16:21:23 +10:00
parent 89b64646ec
commit eb7f7b1564
12 changed files with 475 additions and 419 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/access-control/DomainSepInv.thy
View File

@ -1212,7 +1212,7 @@ crunch domain_sep_inv[wp]: bind_notification "domain_sep_inv irqs st"
lemma invoke_tcb_domain_sep_inv:
"\<lbrace>domain_sep_inv irqs st and
tcb_inv_wf tinv\<rbrace>
Tcb_AI.tcb_inv_wf tinv\<rbrace>
invoke_tcb tinv
\<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
apply(case_tac tinv)

2
proof/access-control/Syscall_AC.thy
View File

@ -29,7 +29,7 @@ where
\<and> aag_has_auth_to aag SyncSend epptr
| Invocations_A.InvokeNotification ep badge \<Rightarrow> aag_has_auth_to aag Notify ep
| Invocations_A.InvokeReply thread slot \<Rightarrow> is_subject aag thread \<and> is_subject aag (fst slot)
| Invocations_A.InvokeTCB i' \<Rightarrow> tcb_inv_wf i' s \<and> authorised_tcb_inv aag i'
| Invocations_A.InvokeTCB i' \<Rightarrow> Tcb_AI.tcb_inv_wf i' s \<and> authorised_tcb_inv aag i'
| Invocations_A.InvokeDomain thread slot \<Rightarrow> False
| Invocations_A.InvokeCNode i' \<Rightarrow> authorised_cnode_inv aag i' s \<and> is_subject aag (cur_thread s)
\<and> cnode_inv_auth_derivations i' s

18
proof/access-control/Tcb_AC.thy
View File

@ -222,7 +222,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma invoke_tcb_tc_respects_aag:
"\<lbrace> integrity aag X st and pas_refined aag
and einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl t sl ep priority croot vroot buf)
and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf (tcb_invocation.ThreadControl t sl ep priority croot vroot buf)
and K (authorised_tcb_inv aag (tcb_invocation.ThreadControl t sl ep priority croot vroot buf))\<rbrace>
invoke_tcb (tcb_invocation.ThreadControl t sl ep priority croot vroot buf)
\<lbrace>\<lambda>rv. integrity aag X st and pas_refined aag\<rbrace>"
@ -294,7 +294,7 @@ lemma invoke_tcb_tc_respects_aag:
lemma invoke_tcb_unbind_notification_respects:
"\<lbrace>integrity aag X st and pas_refined aag
and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t None)
and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t None)
and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t None))\<rbrace>
invoke_tcb (tcb_invocation.NotificationControl t None)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
@ -331,7 +331,7 @@ lemma bind_notification_respects:
lemma invoke_tcb_bind_notification_respects:
"\<lbrace>integrity aag X st and pas_refined aag
and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t (Some ntfn))
and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t (Some ntfn))
and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t (Some ntfn)))\<rbrace>
invoke_tcb (tcb_invocation.NotificationControl t (Some ntfn))
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
@ -343,21 +343,21 @@ lemma invoke_tcb_bind_notification_respects:
lemma invoke_tcb_ntfn_control_respects[wp]:
"\<lbrace>integrity aag X st and pas_refined aag
and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t ntfn)
and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn)
and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\<rbrace>
invoke_tcb (tcb_invocation.NotificationControl t ntfn)
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (case_tac ntfn, simp_all del: invoke_tcb.simps tcb_inv_wf.simps K_def)
apply (case_tac ntfn, simp_all del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def)
apply (wp invoke_tcb_bind_notification_respects invoke_tcb_unbind_notification_respects)
done
lemma invoke_tcb_respects:
"\<lbrace>integrity aag X st and pas_refined aag
and einvs and simple_sched_action and tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\<rbrace>
and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\<rbrace>
invoke_tcb ti
\<lbrace>\<lambda>rv. integrity aag X st\<rbrace>"
apply (cases ti, simp_all add: hoare_conjD1 [OF invoke_tcb_tc_respects_aag [simplified simp_thms]]
del: invoke_tcb.simps tcb_inv_wf.simps K_def)
del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def)
apply (safe intro!: hoare_gen_asm)
apply ((wp itr_wps mapM_x_wp' | simp add: if_apply_def2 split del: split_if
| wpc | clarsimp simp: authorised_tcb_inv_def
@ -383,7 +383,7 @@ lemma bind_notification_pas_refined[wp]:
done
lemma invoke_tcb_ntfn_control_pas_refined[wp]:
"\<lbrace>pas_refined aag and tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) and einvs and simple_sched_action
"\<lbrace>pas_refined aag and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) and einvs and simple_sched_action
and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\<rbrace>
invoke_tcb (tcb_invocation.NotificationControl t ntfn)
\<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
@ -393,7 +393,7 @@ lemma invoke_tcb_ntfn_control_pas_refined[wp]:
done
lemma invoke_tcb_pas_refined:
"\<lbrace>pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace>
"\<lbrace>pas_refined aag and Tcb_AI.tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\<rbrace>
invoke_tcb ti
\<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (cases "\<exists>t sl ep priority croot vroot buf.

4
proof/drefine/Tcb_DR.thy
View File

@ -1501,7 +1501,7 @@ lemma invoke_tcb_corres_thread_control:
"\<lbrakk> t' = tcb_invocation.ThreadControl obj_id' a' fault_ep' prio' croot' vroot' ipc_buffer';
t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc) \<top> (\<lambda>s. invs s \<and> valid_etcbs s \<and> not_idle_thread obj_id' s
\<and> valid_pdpt_objs s \<and> tcb_inv_wf t' s)
\<and> valid_pdpt_objs s \<and> Tcb_AI.tcb_inv_wf t' s)
(Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (rule corres_guard_imp[OF dcorres_thread_control])
apply fastforce
@ -1606,7 +1606,7 @@ lemmas invoke_tcb_rules = ex_nonz_cap_implies_normal_tcb
lemma invoke_tcb_corres:
"\<lbrakk> t = translate_tcb_invocation t' \<rbrakk> \<Longrightarrow>
dcorres (dc \<oplus> dc) \<top> (invs and valid_pdpt_objs and tcb_inv_wf t' and valid_etcbs)
dcorres (dc \<oplus> dc) \<top> (invs and valid_pdpt_objs and Tcb_AI.tcb_inv_wf t' and valid_etcbs)
(Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')"
apply (clarsimp)
apply (case_tac t')

2
proof/infoflow/ADT_IF.thy
View File

@ -2905,7 +2905,7 @@ lemmas bind_notification_irq_state_inv[wp] =
lemma invoke_tcb_irq_state_inv:
"\<lbrace>(\<lambda>s. irq_state_inv st s) and domain_sep_inv False sta and
tcb_inv_wf tinv and K (irq_is_recurring irq st)\<rbrace>
Tcb_AI.tcb_inv_wf tinv and K (irq_is_recurring irq st)\<rbrace>
invoke_tcb tinv
\<lbrace>\<lambda>_ s. irq_state_inv st s\<rbrace>,\<lbrace>\<lambda>_. irq_state_next st\<rbrace>"
apply(case_tac tinv)

2
proof/infoflow/FinalCaps.thy
View File

@ -3013,7 +3013,7 @@ lemma invoke_tcb_silc_inv:
static_imp_conj_wp [wp]
shows
"\<lbrace>silc_inv aag st and einvs and simple_sched_action and pas_refined aag and
tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace>
Tcb_AI.tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\<rbrace>
invoke_tcb tinv
\<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply(case_tac tinv)

2
proof/infoflow/IRQMasks_IF.thy
View File

@ -205,7 +205,7 @@ lemma checked_insert_irq_masks[wp]:
goals *)
lemma invoke_tcb_irq_masks:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and
tcb_inv_wf tinv\<rbrace>
Tcb_AI.tcb_inv_wf tinv\<rbrace>
invoke_tcb tinv
\<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>"
apply(case_tac tinv)

12
proof/infoflow/Tcb_IF.thy
View File

@ -331,7 +331,7 @@ lemma invoke_tcb_thread_preservation:
assumes thread_set_P': "\<And>f ptr. \<lbrace>invs and P\<rbrace> thread_set (tcb_fault_handler_update f) ptr \<lbrace>\<lambda>_.P\<rbrace>"
assumes P_trans[simp]: "\<And>f s. P (trans_state f s) = P s"
shows "
\<lbrace>P and invs and tcb_inv_wf (tcb_invocation.ThreadControl t sl ep prio croot vroot buf)\<rbrace>
\<lbrace>P and invs and Tcb_AI.tcb_inv_wf (tcb_invocation.ThreadControl t sl ep prio croot vroot buf)\<rbrace>
invoke_tcb (tcb_invocation.ThreadControl t sl ep prio croot vroot buf)
\<lbrace>\<lambda>rv. P\<rbrace>"
@ -431,17 +431,17 @@ lemma invoke_tcb_NotificationControl_globals_equiv:
done
lemma invoke_tcb_globals_equiv:
"\<lbrace> invs and globals_equiv st and tcb_inv_wf ti\<rbrace>
"\<lbrace> invs and globals_equiv st and Tcb_AI.tcb_inv_wf ti\<rbrace>
invoke_tcb ti
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply(case_tac ti)
prefer 4
apply (simp del: invoke_tcb.simps tcb_inv_wf.simps)
apply (simp del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps)
apply (wp invoke_tcb_thread_preservation cap_delete_globals_equiv
cap_insert_globals_equiv'' thread_set_globals_equiv
| clarsimp simp add: invs_valid_ko_at_arm split del: split_if)+
apply (simp_all del: tcb_inv_wf.simps split del: split_if)
apply (simp_all del: Tcb_AI.tcb_inv_wf.simps split del: split_if)
apply (wp | clarsimp simp: invs_valid_ko_at_arm no_cap_to_idle_thread | intro conjI impI)+
apply (rename_tac word1 word2 bool1 bool2 bool3 bool4 arm_copy_register_sets)
apply (rule_tac Q="\<lambda>_. valid_ko_at_arm and globals_equiv st and (\<lambda>s. word1 \<noteq> idle_thread s)
@ -650,7 +650,7 @@ lemma invoke_tcb_reads_respects_f:
notes validE_valid[wp del]
static_imp_wp [wp]
shows
"reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)"
"reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and Tcb_AI.tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)"
apply(case_tac ti)
apply(wp when_ev restart_reads_respects_f as_user_reads_respects_f static_imp_wp | simp)+
apply(auto intro: requiv_cur_thread_eq intro!: det_zipWithM simp: det_setRegister det_getRestartPC det_setNextPC authorised_tcb_inv_def simp: reads_equiv_f_def)[1]
@ -707,7 +707,7 @@ lemma invoke_tcb_reads_respects_f:
lemma invoke_tcb_reads_respects_f_g:
"reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti))
"reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti and (\<lambda>s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti))
(invoke_tcb ti)"
apply (rule equiv_valid_guard_imp)
apply (rule reads_respects_f_g)

354
proof/invariant-abstract/ARM/ArchTcb_AI.thy
View File

@ -12,23 +12,357 @@ theory ArchTcb_AI
imports "../Tcb_AI"
begin
context Arch begin
context Arch begin global_naming ARM
named_theorems Tcb_AI_asms
definition "Tcb_AI_dummy_const \<equiv> (1 :: nat)"
lemma Tcb_AI_trivial_result[Tcb_AI_asms]:
"Tcb_AI_dummy_const > 0"
by (simp add: Tcb_AI_dummy_const_def)
lemma activate_idle_invs[Tcb_AI_asms]:
"\<lbrace>invs and ct_idle\<rbrace>
arch_activate_idle_thread thread
\<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>"
by (simp add: arch_activate_idle_thread_def)
lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]:
"empty_fail (getRegister r)"
by (simp add: getRegister_def)
lemma same_object_also_valid: (* arch specific *)
"\<lbrakk> same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap;
cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2^asid_bits - 1);
cap_vptr cap = None; cap_asid_base cap = None \<rbrakk>
\<Longrightarrow> s \<turnstile> cap"
apply (cases cap,
(clarsimp simp: same_object_as_def is_cap_simps cap_asid_def
wellformed_cap_def wellformed_acap_def
valid_cap_def bits_of_def cap_aligned_def
split: cap.split_asm arch_cap.split_asm option.splits)+)
done
lemma same_object_obj_refs[Tcb_AI_asms]:
"\<lbrakk> same_object_as cap cap' \<rbrakk>
\<Longrightarrow> obj_refs cap = obj_refs cap'"
apply (cases cap, simp_all add: same_object_as_def)
apply ((clarsimp simp: is_cap_simps bits_of_def same_aobject_as_def
split: cap.split_asm )+)
by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp)
definition
is_cnode_or_valid_arch :: "cap \<Rightarrow> bool"
where
"is_cnode_or_valid_arch cap \<equiv>
is_cnode_cap cap
\<or> (is_arch_cap cap
\<and> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None))"
definition (* arch specific *)
"pt_pd_asid cap \<equiv> case cap of
ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
lemmas pt_pd_asid_simps [simp] = (* arch specific *)
pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split]
lemma checked_insert_is_derived: (* arch specific *)
"\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap;
obj_refs new_cap = obj_refs old_cap
\<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap
\<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk>
\<Longrightarrow> is_derived m slot new_cap old_cap"
apply (cases slot)
apply (frule same_object_as_cap_master)
apply (frule master_cap_obj_refs)
apply (frule cap_master_eq_badge_none)
apply (frule same_master_cap_same_types)
apply (simp add: is_derived_def)
apply clarsimp
apply (auto simp: is_cap_simps cap_master_cap_def
is_cnode_or_valid_arch_def vs_cap_ref_def
table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq
split: cap.split_asm arch_cap.split_asm
option.split_asm)[1]
done
lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *)
"is_cnode_or_valid_arch cap
\<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)"
by (auto simp add: is_cnode_or_valid_arch_def
is_cap_simps)
lemma checked_insert_tcb_invs[wp]: (* arch specific *)
"\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap
and tcb_cap_valid new_cap (target, ref)
and K (is_pt_cap new_cap \<or> is_pd_cap new_cap
\<longrightarrow> cap_asid new_cap \<noteq> None)
and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
\<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
check_cap_at new_cap src_slot
(check_cap_at (cap.ThreadCap target) slot
(cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: check_cap_at_def)
apply (rule hoare_pre)
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce)
apply (frule caps_of_state_valid_cap[where p=slot], fastforce)
apply (rule conjI, simp only: ex_cte_cap_wp_to_def)
apply (rule_tac x=slot in exI)
apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs)
apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps
dest!: cap_master_cap_eqDs)
apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x])
apply (erule cte_wp_atE[OF caps_of_state_cteD])
apply (fastforce simp: obj_at_def is_obj_defs)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "\<not> is_zombie new_cap")
apply (simp add: same_object_zombies same_object_obj_refs)
apply (erule(2) zombies_final_helperE)
apply fastforce
apply (fastforce simp add: cte_wp_at_caps_of_state)
apply assumption
apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps
is_valid_vtable_root_def)
apply (rule conjI)
apply (erule(1) checked_insert_is_derived, simp+)
apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps)
done
lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
assumes x: "P cap.NullCap"
shows "\<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
finalise_cap cap fin
\<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
apply (cases cap, simp_all)
apply (wp suspend_caps_of_state hoare_vcg_all_lift
| simp
| rule impI
| rule hoare_drop_imps)+
apply (clarsimp simp: ball_ran_eq x)
apply (wp delete_one_caps_of_state
| rule impI
| simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+
done
lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]:
"table_cap_ref (max_free_index_update cap) = table_cap_ref cap"
by (simp add:free_index_update_def table_cap_ref_def split:cap.splits)
interpretation Tcb_AI_1? : Tcb_AI_1
where state_ext_t = state_ext_t
and is_cnode_or_valid_arch = is_cnode_or_valid_arch
by (unfold_locales; fact Tcb_AI_asms)
lemma use_no_cap_to_obj_asid_strg: (* arch specific *)
"(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s)
\<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap
\<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s"
apply (clarsimp simp: cte_wp_at_caps_of_state
no_cap_to_obj_with_diff_ref_def
simp del: split_paired_All)
apply (frule caps_of_state_valid_cap, fastforce)
apply (erule allE)+
apply (erule (1) impE)+
apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits)
apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
done
lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]:
"\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
cap_delete slot
\<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace>"
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
| rule obj_ref_none_no_asid)+
done
lemma tc_invs[Tcb_AI_asms]:
"\<lbrace>invs and tcb_at a
and (case_option \<top> (valid_cap o fst) e)
and (case_option \<top> (valid_cap o fst) f)
and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g)
and (case_option \<top> (cte_at o snd) e)
and (case_option \<top> (cte_at o snd) f)
and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
and K (case_option True (is_cnode_cap o fst) e)
and K (case_option True (is_valid_vtable_root o fst) f)
and K (case_option True (\<lambda>v. case_option True
((swp valid_ipc_buffer_cap (fst v)
and is_arch_cap and is_cnode_or_valid_arch)
o fst) (snd v)) g)
and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
invoke_tcb (ThreadControl a sl b pr e f g)
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (simp add: split_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
| rule wp_split_const_if wp_split_const_if_R
hoare_vcg_all_lift_R
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R
hoare_vcg_R_conj
| (wp out_invs_trivial case_option_wpE cap_delete_deletes
cap_delete_valid_cap cap_insert_valid_cap out_cte_at
cap_insert_cte_at cap_delete_cte_at out_valid_cap
hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
thread_set_tcb_ipc_buffer_cap_cleared_invs
thread_set_invs_trivial[OF ball_tcb_cap_casesI]
hoare_vcg_all_lift thread_set_valid_cap out_emptyable
check_cap_inv [where P="valid_cap c" for c]
check_cap_inv [where P="tcb_cap_valid c p" for c p]
check_cap_inv[where P="cte_at p0" for p0]
check_cap_inv[where P="tcb_at p0" for p0]
thread_set_cte_at
thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]
checked_insert_no_cap_to
out_no_cap_to_trivial[OF ball_tcb_cap_casesI]
thread_set_ipc_tcb_cap_valid
static_imp_wp static_imp_conj_wp)[1]
| simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
emptyable_def
del: hoare_True_E_R
| wpc
| strengthen use_no_cap_to_obj_asid_strg
tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+)
apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified]
is_cap_simps is_valid_vtable_root_def
is_cnode_or_valid_arch_def tcb_cap_valid_def
invs_valid_objs cap_asid_def vs_cap_ref_def
split: option.split_asm
| rule conjI)+
done
lemma check_valid_ipc_buffer_inv: (* arch_specific *)
"\<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: check_valid_ipc_buffer_def whenE_def
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpcw)+
done
lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]:
"\<lbrace>\<lambda>(s::'state_ext::state_ext state). is_arch_cap cap \<and> is_cnode_or_valid_arch cap
\<and> valid_ipc_buffer_cap cap vptr
\<and> is_aligned vptr msg_align_bits
\<longrightarrow> P s\<rbrace>
check_valid_ipc_buffer vptr cap
\<lbrace>\<lambda>rv. P\<rbrace>,-"
apply (simp add: check_valid_ipc_buffer_def whenE_def
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpc)+
apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def
valid_ipc_buffer_cap_def)
done
lemma derive_no_cap_asid[wp,Tcb_AI_asms]:
"\<lbrace>(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\<Rightarrow>bool\<rbrace>
derive_cap slot cap
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-"
apply (simp add: derive_cap_def arch_derive_cap_def
cong: cap.case_cong)
apply (rule hoare_pre)
apply (wp | simp | wpc)+
apply (auto simp add: no_cap_to_obj_with_diff_ref_Null,
auto simp add: no_cap_to_obj_with_diff_ref_def
table_cap_ref_def)
done
lemma decode_set_ipc_inv[wp,Tcb_AI_asms]:
"\<lbrace>P::'state_ext::state_ext state \<Rightarrow> bool\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_set_ipc_buffer_def whenE_def
split_def
split del: split_if)
apply (rule hoare_pre, wp check_valid_ipc_buffer_inv)
apply simp
done
lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]:
"no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s"
apply (case_tac "update_cap_data P x c = NullCap")
apply (simp add: no_cap_to_obj_with_diff_ref_Null)
apply (subgoal_tac "vs_cap_ref (update_cap_data P x c)
= vs_cap_ref c")
apply (simp add: no_cap_to_obj_with_diff_ref_def
update_cap_objrefs)
apply (clarsimp simp: update_cap_data_closedform
table_cap_ref_def
arch_update_cap_data_def
split: cap.split)
apply simp
done
lemma update_cap_valid[Tcb_AI_asms]:
"valid_cap cap (s::'state_ext::state_ext state) \<Longrightarrow>
valid_cap (case capdata of
None \<Rightarrow> cap_rights_update rs cap
| Some x \<Rightarrow> update_cap_data p x
(cap_rights_update rs cap)) s"
apply (case_tac capdata, simp_all)[1]
apply (case_tac cap,
simp_all add: update_cap_data_def cap_rights_update_def
is_cap_defs Let_def split_def valid_cap_def
badge_update_def the_cnode_cap_def cap_aligned_def
arch_update_cap_data_def
split del: split_if)
apply (simp add: badge_update_def cap_rights_update_def)
apply (simp add: badge_update_def)
apply simp
apply (rename_tac arch_cap)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (case_tac arch_cap, simp_all add: acap_rights_update_def
split: option.splits prod.splits)
done
crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t"
(wp: crunch_wps simp: crunch_simps)
end
interpretation Tcb_AI?: Tcb_AI
where Tcb_AI_dummy_const = Arch.Tcb_AI_dummy_const
proof goal_cases
context begin interpretation Arch .
requalify_consts is_cnode_or_valid_arch
end
global_interpretation Tcb_AI?: Tcb_AI
where is_cnode_or_valid_arch = ARM.is_cnode_or_valid_arch
proof goal_cases
interpret Arch .
case 1 show ?case by (intro_locales; (unfold_locales, fact Tcb_AI_asms)?)
qed
case 1 show ?case
by (unfold_locales; fact Tcb_AI_asms)
qed
end

4
proof/invariant-abstract/Syscall_AI.thy
View File

@ -76,7 +76,7 @@ where
"valid_invocation (Invocations_A.InvokeUntyped i) = valid_untyped_inv i"
| "valid_invocation (Invocations_A.InvokeEndpoint w w2 b) = (ep_at w and ex_nonz_cap_to w)"
| "valid_invocation (Invocations_A.InvokeNotification w w2) = (ntfn_at w and ex_nonz_cap_to w)"
| "valid_invocation (Invocations_A.InvokeTCB i) = tcb_inv_wf i"
| "valid_invocation (Invocations_A.InvokeTCB i) = Tcb_AI.tcb_inv_wf i"
| "valid_invocation (Invocations_A.InvokeDomain thread domain) = (tcb_at thread and (\<lambda>s. thread \<noteq> idle_thread s))"
| "valid_invocation (Invocations_A.InvokeReply thread slot) =
(tcb_at thread and cte_wp_at (op = (cap.ReplyCap thread False)) slot)"
@ -521,7 +521,7 @@ lemma decode_inv_wf[wp]:
cong: cap.case_cong if_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp decode_tcb_inv_wf decode_domain_inv_wf[simplified split_def] | wpc |
apply (wp Tcb_AI.decode_tcb_inv_wf decode_domain_inv_wf[simplified split_def] | wpc |
simp add: o_def uncurry_def split_def del: is_cnode_cap.simps cte_refs.simps)+
apply (strengthen cnode_diminished_strg)
apply (clarsimp simp: valid_cap_def cte_wp_at_eq_simp is_cap_simps

490
proof/invariant-abstract/Tcb_AI.thy
View File

@ -12,13 +12,23 @@ theory Tcb_AI
imports "./$L4V_ARCH/ArchCNodeInv_AI"
begin
locale Tcb_AI begin
extend_locale
fixes Tcb_AI_dummy_const :: nat
assumes Tcb_AI_trivial_asm: "Tcb_AI_dummy_const > 0"
end
locale Tcb_AI_1 =
fixes state_ext_t :: "('state_ext::state_ext) itself"
fixes is_cnode_or_valid_arch :: "cap \<Rightarrow> bool"
assumes activate_idle_invs:
"\<And>thread. \<lbrace>(invs::'state_ext state \<Rightarrow> bool) and ct_idle\<rbrace>
arch_activate_idle_thread thread
\<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>"
assumes empty_fail_getRegister [intro!, simp]:
"\<And>r. empty_fail (getRegister r)"
assumes same_object_obj_refs:
"\<And>cap cap'. \<lbrakk> same_object_as cap cap' \<rbrakk>
\<Longrightarrow> obj_refs cap = obj_refs cap'"
assumes finalise_cap_not_cte_wp_at:
"\<And>P cap fin. P cap.NullCap \<Longrightarrow> \<lbrace>\<lambda>(s::'state_ext state). \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
finalise_cap cap fin \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
assumes table_cap_ref_max_free_index_upd[simp]: (* reodered to resolve dependency in tc_invs *)
"\<And>cap. table_cap_ref (max_free_index_update cap) = table_cap_ref cap"
lemma ct_in_state_weaken:
"\<lbrakk> ct_in_state Q s; \<And>st. Q st \<Longrightarrow> P st \<rbrakk> \<Longrightarrow> ct_in_state P s"
@ -36,16 +46,8 @@ lemma set_thread_state_ct_st:
apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma activate_idle_invs:
"\<lbrace>invs and ct_idle\<rbrace>
arch_activate_idle_thread thread
\<lbrace>\<lambda>rv. invs and ct_idle\<rbrace>"
by (simp add: arch_activate_idle_thread_def)
end
lemma activate_invs:
"\<lbrace>invs\<rbrace> activate_thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>"
lemma (in Tcb_AI_1) activate_invs:
"\<lbrace>(invs::'state_ext::state_ext state \<Rightarrow> bool)\<rbrace> activate_thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>"
apply (unfold activate_thread_def)
apply (rule hoare_seq_ext [OF _ gets_sp])
apply (rule hoare_seq_ext [OF _ gts_sp])
@ -87,7 +89,6 @@ lemma setup_reply_master_reply_master[wp]:
apply (auto simp: cte_wp_at_caps_of_state is_cap_simps)
done
lemma setup_reply_master_has_reply[wp]:
"\<lbrace>\<lambda>s. P (has_reply_cap t s)\<rbrace> setup_reply_master t' \<lbrace>\<lambda>rv s. P (has_reply_cap t s)\<rbrace>"
apply (simp add: has_reply_cap_def cte_wp_at_caps_of_state
@ -98,7 +99,6 @@ lemma setup_reply_master_has_reply[wp]:
apply auto
done
lemma setup_reply_master_nonz_cap[wp]:
"\<lbrace>ex_nonz_cap_to p\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>"
apply (simp add: setup_reply_master_def ex_nonz_cap_to_def cte_wp_at_caps_of_state)
@ -108,7 +108,6 @@ lemma setup_reply_master_nonz_cap[wp]:
apply clarsimp
done
lemma restart_invs[wp]:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace> restart t \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: restart_def)
@ -147,12 +146,6 @@ lemma copyAreaToRegs_tcb'[wp]:
"\<lbrace>tcb_at t\<rbrace> copyAreaToRegs regs a b \<lbrace>\<lambda>rv. tcb_at t\<rbrace>"
by (simp add: tcb_at_typ, wp copyAreaToRegs_typ_at)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma empty_fail_getRegister [intro!, simp]:
"empty_fail (getRegister r)"
by (simp add: getRegister_def)
end
lemma copyRegsToArea_typ_at:
"\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> copyRegsToArea regs a b \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
apply (simp add: copyRegsToArea_def)
@ -406,21 +399,6 @@ lemma out_cte_wp_at_trivialT:
done
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma same_object_also_valid:
"\<lbrakk> same_object_as cap cap'; s \<turnstile> cap'; wellformed_cap cap;
cap_asid cap = None \<or> (\<exists>asid. cap_asid cap = Some asid \<and> 0 < asid \<and> asid \<le> 2^asid_bits - 1);
cap_vptr cap = None; cap_asid_base cap = None \<rbrakk>
\<Longrightarrow> s \<turnstile> cap"
apply (cases cap,
(clarsimp simp: same_object_as_def is_cap_simps cap_asid_def
wellformed_cap_def wellformed_acap_def
valid_cap_def bits_of_def cap_aligned_def
split: cap.split_asm arch_cap.split_asm option.splits)+)
done
end
lemma same_object_as_cte_refs:
"\<lbrakk> same_object_as cap cap' \<rbrakk> \<Longrightarrow>
cte_refs cap' = cte_refs cap"
@ -436,17 +414,6 @@ lemma same_object_untyped_range:
by (cases cap, (clarsimp simp: same_object_as_def is_cap_simps)+)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma same_object_obj_refs:
"\<lbrakk> same_object_as cap cap' \<rbrakk>
\<Longrightarrow> obj_refs cap = obj_refs cap'"
apply (cases cap, simp_all add: same_object_as_def)
apply ((clarsimp simp: is_cap_simps bits_of_def
split: cap.split_asm )+)
by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp)
end
lemma same_object_zombies:
"\<lbrakk> same_object_as cap cap' \<rbrakk>
\<Longrightarrow> is_zombie cap = is_zombie cap'"
@ -463,18 +430,6 @@ lemma zombies_final_helperE:
apply (fastforce simp: cte_wp_at_caps_of_state)
done
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition
is_cnode_or_valid_arch :: "cap \<Rightarrow> bool"
where
"is_cnode_or_valid_arch cap \<equiv>
is_cnode_cap cap
\<or> (is_arch_cap cap
\<and> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None))"
end
lemma cap_badge_none_master:
"(cap_badge (cap_master_cap cap) = None)
= (cap_badge cap = None)"
@ -488,88 +443,6 @@ lemma cap_master_eq_badge_none:
apply (simp add: cap_badge_none_master)
done
context Arch begin global_naming ARM (*FIXME: arch_split*)
definition
"pt_pd_asid cap \<equiv> case cap of
ArchObjectCap (PageTableCap _ (Some (asid, _))) \<Rightarrow> Some asid
| ArchObjectCap (PageDirectoryCap _ (Some asid)) \<Rightarrow> Some asid
| _ \<Rightarrow> None"
lemmas pt_pd_asid_simps [simp] =
pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split]
lemma checked_insert_is_derived:
"\<lbrakk> same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap;
obj_refs new_cap = obj_refs old_cap
\<longrightarrow> table_cap_ref old_cap = table_cap_ref new_cap
\<and> pt_pd_asid old_cap = pt_pd_asid new_cap\<rbrakk>
\<Longrightarrow> is_derived m slot new_cap old_cap"
apply (cases slot)
apply (frule same_object_as_cap_master)
apply (frule master_cap_obj_refs)
apply (frule cap_master_eq_badge_none)
apply (frule same_master_cap_same_types)
apply (simp add: is_derived_def)
apply clarsimp
apply (auto simp: is_cap_simps cap_master_cap_def
is_cnode_or_valid_arch_def vs_cap_ref_def
table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq
split: cap.split_asm arch_cap.split_asm
option.split_asm)[1]
done
lemma is_cnode_or_valid_arch_cap_asid:
"is_cnode_or_valid_arch cap
\<Longrightarrow> (is_pt_cap cap \<longrightarrow> cap_asid cap \<noteq> None)
\<and> (is_pd_cap cap \<longrightarrow> cap_asid cap \<noteq> None)"
by (auto simp add: is_cnode_or_valid_arch_def
is_cap_simps)
lemma checked_insert_tcb_invs[wp]:
"\<lbrace>invs and cte_wp_at (\<lambda>c. c = cap.NullCap) (target, ref)
and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap
and tcb_cap_valid new_cap (target, ref)
and K (is_pt_cap new_cap \<or> is_pd_cap new_cap
\<longrightarrow> cap_asid new_cap \<noteq> None)
and (cte_wp_at (\<lambda>c. obj_refs c = obj_refs new_cap
\<longrightarrow> table_cap_ref c = table_cap_ref new_cap \<and>
pt_pd_asid c = pt_pd_asid new_cap) src_slot)\<rbrace>
check_cap_at new_cap src_slot
(check_cap_at (cap.ThreadCap target) slot
(cap_insert new_cap src_slot (target, ref))) \<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: check_cap_at_def)
apply (rule hoare_pre)
apply (wp get_cap_wp)
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce)
apply (frule caps_of_state_valid_cap[where p=slot], fastforce)
apply (rule conjI, simp only: ex_cte_cap_wp_to_def)
apply (rule_tac x=slot in exI)
apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs)
apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps
dest!: cap_master_cap_eqDs)
apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x])
apply (erule cte_wp_atE[OF caps_of_state_cteD])
apply (fastforce simp: obj_at_def is_obj_defs)
apply clarsimp
apply (rule conjI)
apply clarsimp
apply (subgoal_tac "\<not> is_zombie new_cap")
apply (simp add: same_object_zombies same_object_obj_refs)
apply (erule(2) zombies_final_helperE)
apply fastforce
apply (fastforce simp add: cte_wp_at_caps_of_state)
apply assumption
apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps
is_valid_vtable_root_def)
apply (rule conjI)
apply (erule(1) checked_insert_is_derived, simp+)
apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps)
done
end
lemma check_cap_inv2:
assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
@ -599,30 +472,13 @@ lemma thread_set_emptyable[wp]:
crunch not_cte_wp_at[wp]: unbind_maybe_notification "\<lambda>s. \<forall>cp\<in>ran (caps_of_state s). P cp"
(wp: thread_set_caps_of_state_trivial simp: tcb_cap_cases_def)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma finalise_cap_not_cte_wp_at:
assumes x: "P cap.NullCap"
shows "\<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
finalise_cap cap fin
\<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
apply (cases cap, simp_all)
apply (wp suspend_caps_of_state hoare_vcg_all_lift
| simp
| rule impI
| rule hoare_drop_imps)+
apply (clarsimp simp: ball_ran_eq x)
apply (wp delete_one_caps_of_state
| rule impI
| simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+
done
end
lemma rec_del_all_caps_in_range:
lemma (in Tcb_AI_1) rec_del_all_caps_in_range:
assumes x: "P cap.NullCap"
and y: "\<And>x n zt. P (cap.ThreadCap x) \<Longrightarrow> P (cap.Zombie x zt n)"
and z: "\<And>x y gd n zt. P (cap.CNodeCap x y gd) \<Longrightarrow> P (cap.Zombie x zt n)"
and w: "\<And>x zt zt' n m. P (cap.Zombie x zt n) \<Longrightarrow> P (cap.Zombie x zt' m)"
shows "s \<turnstile> \<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
shows "s \<turnstile> \<lbrace>\<lambda>(s::'state_ext state). \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
rec_del args
\<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>,
\<lbrace>\<lambda>e s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>"
@ -692,22 +548,6 @@ qed
abbreviation
"no_cap_to_obj_dr_emp cap \<equiv> no_cap_to_obj_with_diff_ref cap {}"
context Arch begin global_naming ARM (*FIXME: arch_split*)
lemma use_no_cap_to_obj_asid_strg:
"(cte_at p s \<and> no_cap_to_obj_dr_emp cap s \<and> valid_cap cap s \<and> invs s)
\<longrightarrow> cte_wp_at (\<lambda>c. obj_refs c = obj_refs cap
\<longrightarrow> table_cap_ref c = table_cap_ref cap \<and> pt_pd_asid c = pt_pd_asid cap) p s"
apply (clarsimp simp: cte_wp_at_caps_of_state
no_cap_to_obj_with_diff_ref_def
simp del: split_paired_All)
apply (frule caps_of_state_valid_cap, fastforce)
apply (erule allE)+
apply (erule (1) impE)+
apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits)
apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+
done
end
lemma no_cap_to_obj_with_diff_ref_ran_caps_form:
"no_cap_to_obj_dr_emp cap
= (\<lambda>s. \<forall>cp \<in> ran (caps_of_state s).
@ -717,21 +557,56 @@ lemma no_cap_to_obj_with_diff_ref_ran_caps_form:
apply auto
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma cap_delete_no_cap_to_obj_asid[wp]:
"\<lbrace>no_cap_to_obj_dr_emp cap\<rbrace>
locale Tcb_AI = Tcb_AI_1 state_ext_t is_cnode_or_valid_arch
for state_ext_t :: "('state_ext::state_ext) itself"
and is_cnode_or_valid_arch :: "cap \<Rightarrow> bool" +
assumes cap_delete_no_cap_to_obj_asid[wp]:
"\<And>cap slot. \<lbrace>(no_cap_to_obj_dr_emp cap::'state_ext state \<Rightarrow> bool)\<rbrace>
cap_delete slot
\<lbrace>\<lambda>rv. no_cap_to_obj_dr_emp cap\<rbrace>"
apply (simp add: cap_delete_def
no_cap_to_obj_with_diff_ref_ran_caps_form)
apply wp
apply simp
apply (rule use_spec)
apply (rule rec_del_all_caps_in_range)
apply (simp add: table_cap_ref_def[simplified, split_simps cap.split]
| rule obj_ref_none_no_asid)+
done
end
assumes tc_invs:
"\<And>a e f g b sl pr. \<lbrace>(invs::'state_ext state \<Rightarrow> bool) and tcb_at a
and (case_option \<top> (valid_cap o fst) e)
and (case_option \<top> (valid_cap o fst) f)
and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g)
and (case_option \<top> (cte_at o snd) e)
and (case_option \<top> (cte_at o snd) f)
and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
and K (case_option True (is_cnode_cap o fst) e)
and K (case_option True (is_valid_vtable_root o fst) f)
and K (case_option True (\<lambda>v. case_option True
((swp valid_ipc_buffer_cap (fst v)
and is_arch_cap and is_cnode_or_valid_arch)
o fst) (snd v)) g)
and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
invoke_tcb (ThreadControl a sl b pr e f g)
\<lbrace>\<lambda>rv. invs\<rbrace>"
assumes decode_set_ipc_inv[wp]:
"\<And>P args cap slot excaps. \<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>"
assumes update_cap_valid:
"\<And>cap s capdata rs p. valid_cap cap (s::'state_ext state) \<Longrightarrow>
valid_cap (case capdata of
None \<Rightarrow> cap_rights_update rs cap
| Some x \<Rightarrow> update_cap_data p x
(cap_rights_update rs cap)) s"
assumes check_valid_ipc_buffer_wp:
"\<And>cap vptr P. \<lbrace>\<lambda>(s::'state_ext state). is_arch_cap cap \<and> is_cnode_or_valid_arch cap
\<and> valid_ipc_buffer_cap cap vptr
\<and> is_aligned vptr msg_align_bits
\<longrightarrow> P s\<rbrace>
check_valid_ipc_buffer vptr cap
\<lbrace>\<lambda>rv. P\<rbrace>,-"
assumes derive_no_cap_asid[wp]:
"\<And>cap S slot. \<lbrace>(no_cap_to_obj_with_diff_ref cap S)::'state_ext state \<Rightarrow> bool\<rbrace>
derive_cap slot cap
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-"
assumes no_cap_to_obj_with_diff_ref_update_cap_data:
"\<And>c S s P x. no_cap_to_obj_with_diff_ref c S (s::'state_ext state) \<longrightarrow>
no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s"
lemma out_no_cap_to_trivial:
"(\<And>tcb v. \<forall>(getF, x)\<in>ran tcb_cap_cases. getF (f v tcb) = getF tcb)
@ -754,13 +629,8 @@ lemma thread_set_no_cap_to_trivial:
| simp)+
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma table_cap_ref_max_free_index_upd[simp]:
"table_cap_ref (max_free_index_update cap) = table_cap_ref cap"
by (simp add:free_index_update_def table_cap_ref_def split:cap.splits)
end
lemma checked_insert_no_cap_to:
lemma (in Tcb_AI_1) checked_insert_no_cap_to:
"\<lbrace>no_cap_to_obj_with_diff_ref c' {} and
no_cap_to_obj_with_diff_ref a {}\<rbrace>
check_cap_at a b (check_cap_at c d (cap_insert a b e))
@ -862,70 +732,8 @@ lemma thread_set_ipc_tcb_cap_valid:
dest!: get_tcb_SomeD)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma tc_invs:
"\<lbrace>invs and tcb_at a
and (case_option \<top> (valid_cap o fst) e)
and (case_option \<top> (valid_cap o fst) f)
and (case_option \<top> (case_option \<top> (valid_cap o fst) o snd) g)
and (case_option \<top> (cte_at o snd) e)
and (case_option \<top> (cte_at o snd) f)
and (case_option \<top> (case_option \<top> (cte_at o snd) o snd) g)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) e)
and (case_option \<top> (no_cap_to_obj_dr_emp o fst) f)
and (case_option \<top> (case_option \<top> (no_cap_to_obj_dr_emp o fst) o snd) g)
and K (case_option True (is_cnode_cap o fst) e)
and K (case_option True (is_valid_vtable_root o fst) f)
and K (case_option True (\<lambda>v. case_option True
((swp valid_ipc_buffer_cap (fst v)
and is_arch_cap and is_cnode_or_valid_arch)
o fst) (snd v)) g)
and K (case_option True (\<lambda>bl. length bl = word_bits) b)\<rbrace>
invoke_tcb (ThreadControl a sl b pr e f g)
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (rule hoare_gen_asm)+
apply (simp add: split_def cong: option.case_cong)
apply (rule hoare_vcg_precond_imp)
apply wp
apply ((simp only: simp_thms
| rule wp_split_const_if wp_split_const_if_R
hoare_vcg_all_lift_R
hoare_vcg_E_elim hoare_vcg_const_imp_lift_R
hoare_vcg_R_conj
| (wp out_invs_trivial case_option_wpE cap_delete_deletes
cap_delete_valid_cap cap_insert_valid_cap out_cte_at
cap_insert_cte_at cap_delete_cte_at out_valid_cap
hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R
thread_set_tcb_ipc_buffer_cap_cleared_invs
thread_set_invs_trivial[OF ball_tcb_cap_casesI]
hoare_vcg_all_lift thread_set_valid_cap out_emptyable
check_cap_inv [where P="valid_cap c" for c]
check_cap_inv [where P="tcb_cap_valid c p" for c p]
check_cap_inv[where P="cte_at p0" for p0]
check_cap_inv[where P="tcb_at p0" for p0]
thread_set_cte_at
thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI]
checked_insert_no_cap_to
out_no_cap_to_trivial[OF ball_tcb_cap_casesI]
thread_set_ipc_tcb_cap_valid
static_imp_wp static_imp_conj_wp)[1]
| simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified]
emptyable_def
del: hoare_True_E_R
| wpc
| strengthen use_no_cap_to_obj_asid_strg
tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"]
tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+)
apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified]
is_cap_simps is_valid_vtable_root_def
is_cnode_or_valid_arch_def tcb_cap_valid_def
invs_valid_objs cap_asid_def vs_cap_ref_def
split: option.split_asm
| rule conjI)+
done
context Tcb_AI begin
(* FIXME-NTFN *)
primrec
tcb_inv_wf :: "tcb_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
@ -1031,17 +839,17 @@ lemma bind_notification_invs:
done
lemma tcbinv_invs:
"\<lbrace>invs and tcb_inv_wf ti\<rbrace>
lemma (in Tcb_AI) tcbinv_invs:
"\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool) and tcb_inv_wf ti\<rbrace>
invoke_tcb ti
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (case_tac ti, simp_all only:)
apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs
apply ((wp_trace writereg_invs readreg_invs copyreg_invs tc_invs
| simp
| clarsimp simp: invs_def valid_state_def valid_pspace_def
dest!: idle_no_ex_cap
split: option.split
| rule conjI)+)[6]
| rule conjI)+)[6]
apply (rename_tac option)
apply (case_tac option, simp_all)
apply (rule hoare_pre)
@ -1050,7 +858,6 @@ lemma tcbinv_invs:
apply clarsimp
done
crunch typ_at[wp]: invoke_tcb "\<lambda>s. P (typ_at T p s)"
(ignore: check_cap_at setNextPC zipWithM
wp: hoare_drop_imps mapM_x_wp' check_cap_inv
@ -1094,7 +901,7 @@ lemma decode_copyreg_inv:
| wp_once | wpcw)+
done
lemma decode_readreg_wf:
lemma (in Tcb_AI) decode_readreg_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
decode_read_registers args (cap.ThreadCap t)
\<lbrace>tcb_inv_wf\<rbrace>,-"
@ -1105,7 +912,7 @@ lemma decode_readreg_wf:
apply simp
done
lemma decode_writereg_wf:
lemma (in Tcb_AI) decode_writereg_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
decode_write_registers args (cap.ThreadCap t)
\<lbrace>tcb_inv_wf\<rbrace>,-"
@ -1116,7 +923,7 @@ lemma decode_writereg_wf:
apply simp
done
lemma decode_copyreg_wf:
lemma (in Tcb_AI) decode_copyreg_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t
and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> x
\<and> (\<forall>y \<in> zobj_refs x. ex_nonz_cap_to y s))\<rbrace>
@ -1137,7 +944,8 @@ lemma OR_choice_E_weak_wp: "\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrac
apply (simp add: validE_R_def validE_def OR_choice_weak_wp)
done
lemma decode_set_priority_wf[wp]:
lemma (in Tcb_AI) decode_set_priority_wf[wp]:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t\<rbrace>
decode_set_priority args (cap.ThreadCap t) slot \<lbrace>tcb_inv_wf\<rbrace>,-"
apply (simp add: decode_set_priority_def split del: split_if)
@ -1185,34 +993,6 @@ lemma decode_set_priority_inv[wp]:
apply simp
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma check_valid_ipc_buffer_inv:
"\<lbrace>P\<rbrace> check_valid_ipc_buffer vptr cap \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: check_valid_ipc_buffer_def whenE_def
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpcw)+
done
lemma check_valid_ipc_buffer_wp:
"\<lbrace>\<lambda>s. is_arch_cap cap \<and> is_cnode_or_valid_arch cap
\<and> valid_ipc_buffer_cap cap vptr
\<and> is_aligned vptr msg_align_bits
\<longrightarrow> P s\<rbrace>
check_valid_ipc_buffer vptr cap
\<lbrace>\<lambda>rv. P\<rbrace>,-"
apply (simp add: check_valid_ipc_buffer_def whenE_def
cong: cap.case_cong arch_cap.case_cong
split del: split_if)
apply (rule hoare_pre)
apply (wp | simp split del: split_if | wpc)+
apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def
valid_ipc_buffer_cap_def)
done
end
lemma derive_is_arch[wp]:
"\<lbrace>\<lambda>s. is_arch_cap c\<rbrace> derive_cap slot c \<lbrace>\<lambda>rv s. is_arch_cap rv\<rbrace>,-"
@ -1222,23 +1002,9 @@ lemma derive_is_arch[wp]:
apply fastforce
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma derive_no_cap_asid[wp]:
"\<lbrace>no_cap_to_obj_with_diff_ref cap S\<rbrace>
derive_cap slot cap
\<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref rv S\<rbrace>,-"
apply (simp add: derive_cap_def arch_derive_cap_def
cong: cap.case_cong)
apply (rule hoare_pre)
apply (wp | simp | wpc)+
apply (auto simp add: no_cap_to_obj_with_diff_ref_Null,
auto simp add: no_cap_to_obj_with_diff_ref_def
table_cap_ref_def)
done
end
lemma decode_set_ipc_wf[wp]:
"\<lbrace>invs and tcb_at t and cte_at slot and ex_cte_cap_to slot
lemma (in Tcb_AI) decode_set_ipc_wf[wp]:
"\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool) and tcb_at t and cte_at slot and ex_cte_cap_to slot
and ex_nonz_cap_to t
and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> fst x \<and> cte_at (snd x) s
\<and> ex_cte_cap_to (snd x) s
@ -1254,7 +1020,6 @@ lemma decode_set_ipc_wf[wp]:
apply (clarsimp simp: neq_Nil_conv)
done
lemma decode_set_ipc_is_tc[wp]:
"\<lbrace>\<top>\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv s. is_thread_control rv\<rbrace>,-"
apply (rule hoare_pre)
@ -1265,16 +1030,6 @@ lemma decode_set_ipc_is_tc[wp]:
done
lemma decode_set_ipc_inv[wp]:
"\<lbrace>P\<rbrace> decode_set_ipc_buffer args cap slot excaps \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_set_ipc_buffer_def whenE_def
split_def
split del: split_if)
apply (rule hoare_pre, wp check_valid_ipc_buffer_inv)
apply simp
done
lemma slot_long_running_inv[wp]:
"\<lbrace>P\<rbrace> slot_cap_long_running_delete ptr \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: slot_cap_long_running_delete_def)
@ -1288,26 +1043,10 @@ lemma val_le_length_Cons:
apply (cases n, simp_all)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma no_cap_to_obj_with_diff_ref_update_cap_data:
"no_cap_to_obj_with_diff_ref c S s \<longrightarrow>
no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s"
apply (case_tac "update_cap_data P x c = NullCap")
apply (simp add: no_cap_to_obj_with_diff_ref_Null)
apply (subgoal_tac "vs_cap_ref (update_cap_data P x c)
= vs_cap_ref c")
apply (simp add: no_cap_to_obj_with_diff_ref_def
update_cap_objrefs)
apply (clarsimp simp: update_cap_data_closedform
table_cap_ref_def
arch_update_cap_data_def
split: cap.split)
apply simp
done
lemma decode_set_space_wf[wp]:
"\<lbrace>invs and tcb_at t and cte_at slot and ex_cte_cap_to slot
lemma (in Tcb_AI) decode_set_space_wf[wp]:
"\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool)
and tcb_at t and cte_at slot and ex_cte_cap_to slot
and ex_nonz_cap_to t
and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> fst x \<and> cte_at (snd x) s
\<and> ex_cte_cap_to (snd x) s
@ -1319,7 +1058,7 @@ lemma decode_set_space_wf[wp]:
split del: split_if)
apply (rule hoare_pre)
apply (wp derive_cap_valid_cap
| simp add: is_valid_vtable_root_def o_def
| simp add: ARM_A.is_valid_vtable_root_def o_def
split del: split_if
| rule hoare_drop_imps)+
apply (clarsimp split del: split_if simp: ball_conj_distrib
@ -1329,7 +1068,6 @@ lemma decode_set_space_wf[wp]:
del: length_greater_0_conv)
done
end
lemma decode_set_space_inv[wp]:
@ -1363,8 +1101,9 @@ lemma boring_simp[simp]:
"(if x then True else False) = x" by simp
lemma decode_tcb_conf_wf[wp]:
"\<lbrace>invs and tcb_at t and cte_at slot and ex_cte_cap_to slot
lemma (in Tcb_AI) decode_tcb_conf_wf[wp]:
"\<lbrace>(invs::('state_ext::state_ext) state\<Rightarrow>bool)
and tcb_at t and cte_at slot and ex_cte_cap_to slot
and ex_nonz_cap_to t
and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> fst x \<and> cte_at (snd x) s
\<and> ex_cte_cap_to (snd x) s
@ -1382,20 +1121,20 @@ lemma decode_tcb_conf_wf[wp]:
in hoare_post_imp_R)
apply wp
apply (clarsimp simp: is_thread_control_def2 cong: option.case_cong)
apply (wp | simp add: whenE_def split del: split_if)+
apply (wp_trace | simp add: whenE_def split del: split_if)+
apply (clarsimp simp: linorder_not_less val_le_length_Cons
del: ballI)
done
lemma decode_tcb_conf_inv[wp]:
"\<lbrace>P\<rbrace> decode_tcb_configure args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
lemma (in Tcb_AI) decode_tcb_conf_inv[wp]:
"\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_tcb_configure args cap slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
apply (clarsimp simp add: decode_tcb_configure_def Let_def whenE_def
split del: split_if)
apply (rule hoare_pre, wp)
apply simp
done
lemmas derived_cap_valid = derive_cap_valid_cap
lemma derived_cap_cnode_valid:
@ -1409,29 +1148,6 @@ lemma derived_cap_cnode_valid:
apply (clarsimp simp add: liftME_def in_monad)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma update_cap_valid:
"valid_cap cap s \<Longrightarrow>
valid_cap (case capdata of
None \<Rightarrow> cap_rights_update rs cap
| Some x \<Rightarrow> update_cap_data p x
(cap_rights_update rs cap)) s"
apply (case_tac capdata, simp_all)[1]
apply (case_tac cap,
simp_all add: update_cap_data_def cap_rights_update_def
is_cap_defs Let_def split_def valid_cap_def
badge_update_def the_cnode_cap_def cap_aligned_def
arch_update_cap_data_def
split del: split_if)
apply (simp add: badge_update_def cap_rights_update_def)
apply (simp add: badge_update_def)
apply simp
apply (rename_tac arch_cap)
using valid_validate_vm_rights[simplified valid_vm_rights_def]
apply (case_tac arch_cap, simp_all add: acap_rights_update_def
split: option.splits prod.splits)
done
end
crunch inv[wp]: decode_unbind_notification P
(simp: whenE_def)
@ -1441,8 +1157,9 @@ lemma decode_bind_notification_inv[wp]:
unfolding decode_bind_notification_def
by (rule hoare_pre) (wp get_ntfn_wp gbn_wp | wpc | clarsimp simp: whenE_def split del: split_if)+
lemma decode_tcb_inv_inv:
"\<lbrace>P\<rbrace> decode_tcb_invocation label args (cap.ThreadCap t) slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
lemma (in Tcb_AI) decode_tcb_inv_inv:
"\<lbrace>P::'state_ext state \<Rightarrow> bool\<rbrace> decode_tcb_invocation label args (cap.ThreadCap t) slot extras \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: decode_tcb_invocation_def Let_def
cong: if_cong
split del: split_if)
@ -1453,10 +1170,12 @@ lemma decode_tcb_inv_inv:
apply simp
done
lemma real_cte_at_not_tcb_at:
"real_cte_at (x, y) s \<Longrightarrow> \<not> tcb_at x s"
by (clarsimp simp: obj_at_def is_tcb is_cap_table)
context Tcb_AI begin
lemma decode_bind_notification_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t
and (\<lambda>s. \<forall>x \<in> set extras. s \<turnstile> (fst x) \<and> (\<forall>y \<in> zobj_refs (fst x). ex_nonz_cap_to y s))\<rbrace>
@ -1485,22 +1204,23 @@ lemma decode_unbind_notification_wf:
lemma decode_tcb_inv_wf:
"\<lbrace>invs and tcb_at t and ex_nonz_cap_to t
and cte_at slot and ex_cte_cap_to slot
and (\<lambda>s. \<forall>x \<in> set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x
and (\<lambda>(s::'state_ext::state_ext state). \<forall>x \<in> set extras. real_cte_at (snd x) s \<and> s \<turnstile> fst x
\<and> ex_cte_cap_to (snd x) s
\<and> (\<forall>y \<in> zobj_refs (fst x). ex_nonz_cap_to y s)
\<and> no_cap_to_obj_dr_emp (fst x) s)\<rbrace>
decode_tcb_invocation label args (cap.ThreadCap t) slot extras
\<lbrace>tcb_inv_wf\<rbrace>,-"
apply (simp add: decode_tcb_invocation_def Let_def
apply (simp add: decode_tcb_invocation_def Let_def del: tcb_inv_wf_def
cong: if_cong split del: split_if)
apply (rule hoare_vcg_precond_impE_R)
apply wpc
apply (wp decode_tcb_conf_wf decode_readreg_wf
apply (wp_trace decode_tcb_conf_wf decode_readreg_wf
decode_writereg_wf decode_copyreg_wf
decode_bind_notification_wf decode_unbind_notification_wf)
apply (clarsimp simp: real_cte_at_cte)
apply (fastforce simp: real_cte_at_not_tcb_at)
done
end
lemma out_pred_tcb_at_preserved:
"\<lbrakk> \<And>tcb x. tcb_state (f x tcb) = tcb_state tcb \<rbrakk> \<Longrightarrow>
@ -1514,10 +1234,12 @@ lemma pred_tcb_at_arch_state[simp]:
"pred_tcb_at proj P t (arch_state_update f s) = pred_tcb_at proj P t s"
by (simp add: pred_tcb_at_def obj_at_def)
(*
context begin interpretation Arch . (*FIXME: arch_split*)
crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t"
crunch pred_tcb_at: arch_switch_to_thread "pred_tcb_at proj P t"
(wp: crunch_wps simp: crunch_simps)
end
*)
lemma invoke_domain_invs:
"\<lbrace>invs\<rbrace>
@ -1551,6 +1273,7 @@ lemma decode_domain_inv_wf:
apply (erule ballE[where x="hd excs"])
apply simp+
done
lemma tcb_bound_refs_no_NTFNBound:
"(x, NTFNBound) \<notin> tcb_bound_refs a"
by (simp add: tcb_bound_refs_def split: option.splits)
@ -1602,5 +1325,4 @@ lemma unbind_notification_sym_refs[wp]:
intro!: ntfn_q_refs_no_NTFNBound)
done
end

2
proof/refine/Tcb_R.thy
View File

@ -1485,7 +1485,7 @@ where
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
corres (intr \<oplus> op =)
(einvs and simple_sched_action and tcb_inv_wf ti)
(einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti)
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"
apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)