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

arm InfoFlow: fixes for the backports from arm-hyp

This commit is contained in:
Miki Tanaka 2017-05-25 21:51:59 +10:00 committed by Alejandro Gomez-Londono
parent 93eed88af7
commit c21127eb0f
13 changed files with 223 additions and 97 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

79
proof/infoflow/ADT_IF.thy
View File

@ -927,8 +927,9 @@ lemma kernel_entry_if_invs:
"\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. invs\<rbrace>"
apply( simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2
| wp static_imp_wp thread_set_invs_trivial)+
unfolding kernel_entry_if_def
apply (wpsimp wp: thread_set_invs_trivial static_imp_wp
simp: arch_tcb_update_aux2 tcb_cap_cases_def)+
done
lemma idle_equiv_as_globals_equiv: "arm_global_pd (arch_state s) \<noteq> idle_thread s \<Longrightarrow> idle_equiv st s =
@ -1035,10 +1036,11 @@ lemma kernel_entry_silc_inv[wp]: "\<lbrace>silc_inv aag st and einvs and simple_
(\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and
domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace>
kernel_entry_if ev tc \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>"
apply (simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2
| wp static_imp_wp handle_event_silc_inv thread_set_silc_inv_trivial
unfolding kernel_entry_if_def
apply (wpsimp simp: tcb_cap_cases_def arch_tcb_update_aux2
wp: static_imp_wp handle_event_silc_inv thread_set_silc_inv_trivial
thread_set_invs_trivial thread_set_not_state_valid_sched thread_set_pas_refined
| rule hoare_vcg_conj_lift hoare_convert_imp)+
| rule hoare_vcg_conj_lift hoare_convert_imp)+
apply force
done
@ -1048,8 +1050,9 @@ lemma kernel_entry_pas_refined[wp]: "\<lbrace>pas_refined aag and guarded_pas_do
(\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and
(\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if ev tc \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>"
apply (simp add: kernel_entry_if_def tcb_cap_cases_def schact_is_rct_def arch_tcb_update_aux2
| wp static_imp_wp handle_event_pas_refined
unfolding kernel_entry_if_def
apply (wpsimp simp: tcb_cap_cases_def schact_is_rct_def arch_tcb_update_aux2 tcb_arch_ref_def
wp: static_imp_wp handle_event_pas_refined
thread_set_pas_refined guarded_pas_domain_lift
thread_set_invs_trivial thread_set_not_state_valid_sched)+
apply force
@ -1059,10 +1062,10 @@ lemma kernel_entry_if_domain_sep_inv:
"\<lbrace>domain_sep_inv irqs st and einvs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
apply( simp add: kernel_entry_if_def arch_tcb_update_aux2
| wp static_imp_wp handle_event_domain_sep_inv
thread_set_invs_trivial thread_set_not_state_valid_sched
| simp add: tcb_cap_cases_def)+
unfolding kernel_entry_if_def
apply( wpsimp simp: tcb_cap_cases_def arch_tcb_update_aux2 tcb_arch_ref_def
wp: handle_event_domain_sep_inv static_imp_wp
thread_set_invs_trivial thread_set_not_state_valid_sched)+
done
lemma kernel_entry_if_guarded_pas_domain:
@ -1078,21 +1081,20 @@ lemma kernel_entry_if_valid_sched:
(\<lambda>s. (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> scheduler_action s = resume_cur_thread)\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply(simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2
| wp static_imp_wp handle_event_valid_sched thread_set_invs_trivial
thread_set_not_state_valid_sched hoare_vcg_disj_lift
thread_set_no_change_tcb_state ct_in_state_thread_state_lift)+
apply(clarsimp)
apply(wpsimp simp: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2 tcb_arch_ref_def
wp: handle_event_valid_sched thread_set_invs_trivial hoare_vcg_disj_lift
thread_set_no_change_tcb_state ct_in_state_thread_state_lift
thread_set_not_state_valid_sched static_imp_wp)+
done
lemma kernel_entry_if_irq_masks:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\<rbrace>
kernel_entry_if e tc
\<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>"
apply( simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2
apply( simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2 tcb_arch_ref_def
| wp handle_event_irq_masks thread_set_invs_trivial)+
by fastforce
crunch valid_list[wp]: kernel_entry_if "valid_list"
definition
@ -1110,7 +1112,7 @@ text {*
definition
handle_preemption_if :: "user_context \<Rightarrow> (user_context,det_ext) s_monad" where
"handle_preemption_if tc \<equiv> do
irq \<leftarrow> do_machine_op getActiveIRQ;
irq \<leftarrow> do_machine_op (getActiveIRQ False);
when (irq \<noteq> None) $ handle_interrupt (the irq);
return tc
od"
@ -1146,9 +1148,17 @@ crunch idle_thread[wp]: handle_preemption_if "\<lambda>s. P (idle_thread s)"
lemma handle_preemption_if_guarded_pas_domain[wp]: "\<lbrace>guarded_pas_domain aag\<rbrace> handle_preemption_if tc \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>"
by (rule guarded_pas_domain_lift; wp)
crunch valid_sched[wp]: handle_preemption_if "valid_sched"
(*
crunch valid_sched[wp]: handle_interrupt "valid_sched"
(wp: crunch_wps simp: crunch_simps ignore: getActiveIRQ)
*)
lemma handle_preemption_if_valid_sched[wp]:
"\<lbrace>valid_sched and invs and (\<lambda>s. irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s)\<rbrace>
handle_preemption_if irq \<lbrace>\<lambda>_. valid_sched\<rbrace>"
apply (wpsimp simp: handle_preemption_if_def non_kernel_IRQs_def)+
apply (wpsimp wp: hoare_drop_imp hoare_vcg_if_lift2)+
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma handle_preemption_if_irq_masks:
@ -1362,7 +1372,7 @@ definition
check_active_irq_if :: "user_context \<Rightarrow> (irq option \<times> user_context, ('z :: state_ext)) s_monad"
where
"check_active_irq_if tc \<equiv>
do irq \<leftarrow> do_machine_op getActiveIRQ;
do irq \<leftarrow> do_machine_op (getActiveIRQ True);
return (irq, tc)
od"
@ -2074,9 +2084,9 @@ lemma kernel_entry_if_valid_pdpt_objs[wp]:
"\<lbrace>valid_pdpt_objs and invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s)\<rbrace>kernel_entry_if e tc \<lbrace>\<lambda>s. valid_pdpt_objs\<rbrace>"
apply (case_tac "e = Interrupt")
apply (simp add: kernel_entry_if_def)
apply (wp|wpc|simp)+
apply (simp add: kernel_entry_if_def tcb_cap_cases_def arch_tcb_update_aux2
| wp static_imp_wp thread_set_invs_trivial)+
apply (wp|wpc|simp add: kernel_entry_if_def)+
apply (wpsimp simp: tcb_cap_cases_def arch_tcb_update_aux2
wp: static_imp_wp thread_set_invs_trivial)+
done
lemma kernel_entry_if_det_inv':
@ -2180,7 +2190,7 @@ lemma invs_if_Step_ADT_A_if:
apply (wp handle_preemption_if_invs
handle_preemption_if_domain_sep_inv
handle_preemption_if_domain_time_sched_action[OF num_domains_sanity]
handle_preemption_if_det_inv ct_idle_lift| simp)+
handle_preemption_if_det_inv ct_idle_lift| simp add: non_kernel_IRQs_def)+
apply(simp add: kernel_schedule_if_def | elim exE conjE)+
apply(erule use_valid)
apply((wp schedule_if_ct_running_or_ct_idle
@ -2431,14 +2441,14 @@ lemma next_irq_state_Suc':
done
lemma getActiveIRQ_None:
"(None,s') \<in> fst (do_machine_op getActiveIRQ s) \<Longrightarrow>
"(None,s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) \<Longrightarrow>
irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = None"
apply(erule use_valid)
apply(wp dmo_getActiveIRQ_wp)
by simp
lemma getActiveIRQ_Some:
"(Some i,s') \<in> fst (do_machine_op getActiveIRQ s) \<Longrightarrow>
"(Some i,s') \<in> fst (do_machine_op (getActiveIRQ in_kernel) s) \<Longrightarrow>
irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s)) = Some i"
apply(erule use_valid)
apply(wp dmo_getActiveIRQ_wp)
@ -2986,7 +2996,7 @@ lemma handle_event_irq_state_inv:
apply(case_tac syscall)
apply ((simp add: handle_send_def handle_call_def
| wp handle_invocation_irq_state_inv)+)[1]
apply((simp | wp_trace add: irq_state_inv_triv hy_inv
apply((simp | wp add: irq_state_inv_triv hy_inv
| blast | (elim conjE, (intro conjI | assumption)+))+)[1]
apply ((simp add: handle_send_def handle_call_def
| wp handle_invocation_irq_state_inv)+)[2]
@ -3048,7 +3058,8 @@ lemma kernel_entry_if_next_irq_state_of_state:
apply(clarsimp simp: irq_state_inv_def)
apply (simp add: arch_tcb_update_aux2)
apply(erule_tac f="thread_set (tcb_arch_update (arch_tcb_context_set uc)) t" in use_valid)
apply(wp irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"] | simp add: tcb_cap_cases_def)+
apply(wpsimp wp: irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"]
simp: tcb_cap_cases_def tcb_arch_ref_def)+
apply(erule use_valid)
apply (wp | simp )+
apply(simp add: irq_state_inv_def)
@ -3066,7 +3077,9 @@ lemma kernel_entry_if_next_irq_state_of_state_next:
apply (simp add: irq_state_next_def)
apply (simp add: arch_tcb_update_aux2)
apply(erule_tac f="thread_set (tcb_arch_update (arch_tcb_context_set uc)) t" in use_valid)
apply(wp irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"] | simp add: tcb_cap_cases_def)+
apply(wpsimp wp: irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv
thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"]
simp: tcb_cap_cases_def tcb_arch_ref_def)+
apply(erule use_valid)
apply (wp | simp )+
apply(simp add: irq_state_inv_def)
@ -3084,7 +3097,9 @@ lemma kernel_entry_if_irq_measure:
apply simp
apply (simp add: arch_tcb_update_aux2)
apply(erule_tac f="thread_set (tcb_arch_update (arch_tcb_context_set uc)) t" in use_valid)
apply(wp irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"] | simp add: tcb_cap_cases_def)+
apply(wpsimp wp: irq_measure_if_inv'[where Q="\<top>"] irq_state_inv_triv
thread_set_invs_trivial irq_is_recurring_triv[where Q="\<top>"]
simp: tcb_cap_cases_def arch_tcb_update_aux2 tcb_arch_ref_def)+
apply(erule use_valid)
apply (wp | simp )+
apply(simp add: irq_measure_if_inv_def)

112
proof/infoflow/Arch_IF.thy
View File

@ -302,7 +302,7 @@ lemma find_pd_for_asid_reads_respects:
done
lemma find_pd_for_asid_assert_reads_respects:
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_arch_objs and
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and
K (is_subject_asid aag asid))
(find_pd_for_asid_assert asid)"
unfolding find_pd_for_asid_assert_def catch_def
@ -705,7 +705,7 @@ lemma flush_table_reads_respects:
lemma page_table_mapped_reads_respects:
"reads_respects aag l
(pas_refined aag and pspace_aligned
and valid_arch_objs and K (is_subject_asid aag asid))
and valid_vspace_objs and K (is_subject_asid aag asid))
(page_table_mapped asid vaddr pt)"
unfolding page_table_mapped_def catch_def fun_app_def
apply(wp get_pde_rev | wpc | simp)+
@ -714,7 +714,7 @@ lemma page_table_mapped_reads_respects:
lemma unmap_page_table_reads_respects:
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_arch_objs and K (is_subject_asid aag asid))
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid))
(unmap_page_table asid vaddr pt)"
unfolding unmap_page_table_def fun_app_def page_table_mapped_def
apply(wp find_pd_for_asid_pd_slot_authorised
@ -725,7 +725,7 @@ lemma unmap_page_table_reads_respects:
lemma perform_page_table_invocation_reads_respects:
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_arch_objs and K (authorised_page_table_inv aag pti))
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_page_table_inv aag pti))
(perform_page_table_invocation pti)"
unfolding perform_page_table_invocation_def fun_app_def cleanCacheRange_PoU_def
apply(rule equiv_valid_guard_imp)
@ -795,7 +795,7 @@ lemma flush_page_reads_respects:
(* clagged some help from unmap_page_respects in Arch_AC *)
lemma unmap_page_reads_respects:
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_arch_objs and K (is_subject_asid aag asid \<and> vptr < kernel_base)) (unmap_page pgsz asid vptr pptr)"
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (is_subject_asid aag asid \<and> vptr < kernel_base)) (unmap_page pgsz asid vptr pptr)"
unfolding unmap_page_def catch_def fun_app_def cleanCacheRange_PoU_def
apply (simp add: unmap_page_def swp_def cong: vmpage_size.case_cong)
apply(wp dmo_mol_reads_respects dmo_cacheRangeOp_reads_respects
@ -1050,7 +1050,7 @@ lemma set_mrs_reads_respects:
done
lemma perform_page_invocation_reads_respects:
"reads_respects aag l (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_arch_objs and pspace_aligned and is_subject aag \<circ> cur_thread) (perform_page_invocation pgi)"
"reads_respects aag l (pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread) (perform_page_invocation pgi)"
unfolding perform_page_invocation_def fun_app_def when_def cleanCacheRange_PoU_def
apply(rule equiv_valid_guard_imp)
apply wpc
@ -1179,7 +1179,7 @@ lemma perform_asid_pool_invocation_reads_respects:
done
lemma arch_perform_invocation_reads_respects:
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_arch_objs and K (authorised_arch_inv aag ai) and valid_arch_inv ai and is_subject aag \<circ> cur_thread)
"reads_respects aag l (pas_refined aag and pspace_aligned and valid_vspace_objs and K (authorised_arch_inv aag ai) and valid_arch_inv ai and is_subject aag \<circ> cur_thread)
(arch_perform_invocation ai)"
unfolding arch_perform_invocation_def fun_app_def
apply(wp perform_page_table_invocation_reads_respects perform_page_directory_invocation_reads_respects perform_page_invocation_reads_respects perform_asid_control_invocation_reads_respects perform_asid_pool_invocation_reads_respects | wpc)+
@ -1659,7 +1659,7 @@ lemma hoare_add_postE : "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda> r. P r\<rbrace
done
lemma find_pd_for_asid_not_arm_global_pd:
"\<lbrace>pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup
and valid_global_refs and valid_arch_state\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>rv s. lookup_pd_slot rv vptr && ~~ mask pd_bits \<noteq> arm_global_pd (arch_state s)\<rbrace>, -"
@ -1677,7 +1677,7 @@ lemma find_pd_for_asid_not_arm_global_pd:
done
lemma find_pd_for_asid_not_arm_global_pd_large_page:
"\<lbrace>pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup
and valid_global_refs and valid_arch_state\<rbrace>
find_pd_for_asid asid
\<lbrace>\<lambda>rv s.
@ -1702,7 +1702,7 @@ done
declare dmo_mol_globals_equiv[wp]
lemma unmap_page_table_globals_equiv:
"\<lbrace>pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup
"\<lbrace>pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup
and valid_global_refs and valid_arch_state and globals_equiv st\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv. globals_equiv st\<rbrace>"
unfolding unmap_page_table_def page_table_mapped_def including no_pre
apply(wp store_pde_globals_equiv | wpc | simp add: cleanByVA_PoU_def)+
@ -1818,7 +1818,7 @@ definition authorised_for_globals_page_table_inv ::
lemma perform_page_table_invocation_globals_equiv:
"\<lbrace>valid_global_refs and valid_global_objs and valid_arch_state and
globals_equiv st and pspace_aligned and valid_arch_objs and
globals_equiv st and pspace_aligned and valid_vspace_objs and
valid_vs_lookup and valid_kernel_mappings and authorised_for_globals_page_table_inv pti\<rbrace>
perform_page_table_invocation pti \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding perform_page_table_invocation_def cleanCacheRange_PoU_def
@ -1895,7 +1895,7 @@ crunch valid_ko_at_arm[wp]: flush_page "valid_ko_at_arm"
(wp: crunch_wps simp: crunch_simps)
lemma unmap_page_globals_equiv:
"\<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_arch_objs
"\<lbrace>globals_equiv st and valid_arch_state and pspace_aligned and valid_vspace_objs
and valid_global_objs and valid_vs_lookup and valid_global_refs \<rbrace> unmap_page pgsz asid vptr pptr
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding unmap_page_def cleanCacheRange_PoU_def including no_pre
@ -2039,7 +2039,7 @@ crunch valid_ko_at_arm[wp]: set_mrs valid_ko_at_arm
lemma perform_page_invocation_globals_equiv:
"\<lbrace>authorised_for_globals_page_inv pgi and valid_page_inv pgi and globals_equiv st
and valid_arch_state and pspace_aligned and valid_arch_objs and valid_global_objs
and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_objs
and valid_vs_lookup and valid_global_refs and ct_active and valid_idle\<rbrace>
perform_page_invocation pgi
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
@ -2253,7 +2253,7 @@ lemma arch_perform_invocation_globals_equiv:
done
lemma find_pd_for_asid_authority3:
"\<lbrace>\<lambda>s. \<forall>pd. (pspace_aligned s \<and> valid_arch_objs s \<longrightarrow> is_aligned pd pd_bits)
"\<lbrace>\<lambda>s. \<forall>pd. (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits)
\<and> (\<exists>\<rhd> pd) s
\<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, -"
(is "\<lbrace>?P\<rbrace> ?f \<lbrace>Q\<rbrace>,-")
@ -2290,7 +2290,7 @@ lemma decode_arch_invocation_authorised_for_globals:
apply(rule hoare_drop_imps)
apply((wp hoare_TrueI hoare_vcg_all_lift hoare_drop_imps | wpc | simp)+)[3]
apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def
neq_Nil_conv invs_psp_aligned invs_arch_objs cli_no_irqs)
neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs)
apply (drule diminished_cte_wp_at_valid_cap, clarsimp+)
apply (cases cap, simp_all)
-- "PageCap"
@ -2360,10 +2360,44 @@ lemma valid_arch_objs_arm_asid_table_unmap:
apply (clarsimp simp: valid_state_def valid_arch_objs_unmap_strg)
done
lemma valid_vspace_objs_arm_asid_table_unmap:
"valid_vspace_objs s
\<and> tab = arm_asid_table (arch_state s)
\<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
apply (clarsimp simp: valid_state_def valid_vspace_objs_unmap_strg)
done
crunch valid_arch_objs[wp]: set_vm_root "valid_arch_objs"
crunch valid_arch_objs[wp]: invalidate_asid_entry "valid_arch_objs"
crunch valid_arch_objs[wp]: flush_space "valid_arch_objs"
lemma invalidate_hw_asid_vspace_objs [wp]:
"\<lbrace>valid_vspace_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (wpsimp simp: invalidate_hw_asid_entry_def valid_vspace_objs_arch_update)+
apply assumption
apply wpsimp+
done
crunch vspace_objs[wp]: invalidate_asid valid_vspace_objs
(simp: valid_vspace_objs_arch_update)
lemma find_free_hw_asid_vspace_objs[wp]:
"find_free_hw_asid \<lbrace> valid_vspace_objs \<rbrace>"
by (wpsimp simp: find_free_hw_asid_def valid_vspace_objs_arch_update
wp: hoare_drop_imp | simp)+
crunch vspace_objs[wp]: arm_context_switch "valid_vspace_objs"
(simp: valid_vspace_objs_arch_update)
lemmas arm_context_switch_valid_vspace_objs_aux =
hoare_drop_imp[of valid_vspace_objs "arm_context_switch _ _" "\<lambda>_ s. valid_vspace_objs s"
, OF arm_context_switch_vspace_objs]
crunch valid_vspace_objs [wp]: set_vm_root valid_vspace_objs
(simp: crunch_simps valid_vspace_objs_arch_update wp: arm_context_switch_valid_vspace_objs_aux)
crunch valid_vspace_objs[wp]: invalidate_asid_entry "valid_vspace_objs"
crunch valid_vspace_objs[wp]: flush_space "valid_vspace_objs"
lemma delete_asid_pool_valid_arch_obsj[wp]:
"\<lbrace>valid_arch_objs\<rbrace>
delete_asid_pool base pptr
@ -2374,15 +2408,29 @@ lemma delete_asid_pool_valid_arch_obsj[wp]:
apply (wpsimp wp: mapM_wp')+
done
lemma delete_asid_pool_valid_vspace_objs[wp]:
"\<lbrace>valid_vspace_objs\<rbrace>
delete_asid_pool base pptr
\<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_asid_pool_def
apply (wp modify_wp)
apply (strengthen valid_vspace_objs_arm_asid_table_unmap)
apply (wpsimp wp: mapM_wp')+
done
crunch pspace_aligned[wp]: cap_swap_for_delete, set_cap, empty_slot "pspace_aligned" (ignore: empty_slot_ext wp: dxo_wp_weak)
crunch pspace_aligned[wp]: finalise_cap "pspace_aligned"
(wp: mapM_x_wp' select_wp hoare_vcg_if_lift2 hoare_drop_imps modify_wp mapM_wp' dxo_wp_weak
simp: unless_def crunch_simps arch_update.pspace_aligned_update
ignore: tcb_sched_action reschedule_required)
crunch valid_arch_objs[wp]: cap_swap_for_delete "valid_arch_objs"
crunch valid_arch_objs[wp]: empty_slot "valid_arch_objs"
crunch valid_vspace_objs[wp]: cap_swap_for_delete "valid_vspace_objs"
crunch valid_vspace_objs[wp]: empty_slot_ext "valid_vspace_objs"
(*
crunch valid_vspace_objs[wp]: empty_slot "valid_arch_objs"
(wp: crunch_wps simp: crunch_simps ignore: )
*)
lemma set_asid_pool_arch_objs_unmap'':
"\<lbrace>(valid_arch_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_arch_objs\<rbrace>"
apply (rule hoare_gen_asm)
@ -2390,6 +2438,13 @@ lemma set_asid_pool_arch_objs_unmap'':
apply (rule set_asid_pool_arch_objs_unmap)
done
lemma set_asid_pool_vspace_objs_unmap'':
"\<lbrace>(valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\<rbrace> set_asid_pool p f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
apply (rule hoare_gen_asm)
apply simp
apply (rule set_asid_pool_vspace_objs_unmap)
done
lemma restrict_eq_asn_none: "f(N := None) = f |` {s. s \<noteq> N}" by auto
lemma delete_asid_valid_arch_objs[wp]:
@ -2399,8 +2454,27 @@ lemma delete_asid_valid_arch_objs[wp]:
apply (fastforce simp: restrict_eq_asn_none)
done
crunch valid_arch_objs[wp]: finalise_cap "valid_arch_objs"
(wp: mapM_wp' mapM_x_wp' select_wp hoare_vcg_if_lift2 dxo_wp_weak hoare_drop_imps store_pde_arch_objs_unmap
lemma delete_asid_valid_vspace_objs[wp]:
"\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> delete_asid a b \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
unfolding delete_asid_def
apply (wpsimp wp: set_asid_pool_vspace_objs_unmap'')
apply (fastforce simp: restrict_eq_asn_none)
done
lemma store_pte_valid_vspace_objs[wp]:
"\<lbrace>valid_vspace_objs and valid_pte pte\<rbrace>
store_pte p pte
\<lbrace>\<lambda>_. (valid_vspace_objs)\<rbrace>"
unfolding store_pte_def
apply wp
apply clarsimp
apply (unfold valid_vspace_objs_def)
apply (erule_tac x="p && ~~ mask pt_bits" in allE)
apply auto
done
crunch valid_vspace_objs[wp]: finalise_cap "valid_vspace_objs"
(wp: mapM_wp' mapM_x_wp' select_wp hoare_vcg_if_lift2 dxo_wp_weak hoare_drop_imps store_pde_vspace_objs_unmap
simp: crunch_simps pde_ref_def unless_def
ignore: tcb_sched_action reschedule_required)

18
proof/infoflow/CNode_IF.thy
View File

@ -352,7 +352,7 @@ lemma set_cap_globals_equiv:
unfolding set_cap_def
apply(simp only: split_def)
apply(wp set_object_globals_equiv hoare_vcg_all_lift get_object_wp | wpc | simp)+
apply(fastforce simp: valid_global_objs_def valid_ao_at_def obj_at_def is_tcb_def)+
apply(fastforce simp: valid_global_objs_def valid_vso_at_def obj_at_def is_tcb_def)+
done
@ -646,7 +646,7 @@ lemma preemption_point_def2:
rv \<leftarrow> liftE work_units_limit_reached;
if rv then doE
liftE reset_work_units;
liftE (do_machine_op getActiveIRQ) >>=E
liftE (do_machine_op (getActiveIRQ True)) >>=E
case_option (returnOk ()) (throwError \<circ> Interrupted)
odE else returnOk()
odE"
@ -675,13 +675,13 @@ definition irq_is_recurring :: "irq \<Rightarrow> ('z::state_ext) state \<Righta
lemma dmo_getActiveIRQ_wp:
"\<lbrace>\<lambda>s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) (s\<lparr>machine_state := (machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>)\<rparr>)\<rbrace> do_machine_op getActiveIRQ \<lbrace>P\<rbrace>"
apply(simp add: do_machine_op_def getActiveIRQ_def)
"\<lbrace>\<lambda>s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) (s\<lparr>machine_state := (machine_state s\<lparr>irq_state := irq_state (machine_state s) + 1\<rparr>)\<rparr>)\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>P\<rbrace>"
apply(simp add: do_machine_op_def getActiveIRQ_def non_kernel_IRQs_def)
apply(wp modify_wp | wpc)+
apply clarsimp
apply(erule use_valid)
apply (wp modify_wp)
apply(auto simp: irq_at_def)
apply(auto simp: irq_at_def Let_def split: if_splits)
done
lemma only_timer_irqs:
@ -697,7 +697,7 @@ lemma only_timer_irqs:
lemma dmo_getActiveIRQ_only_timer:
"\<lbrace>domain_sep_inv False st and valid_irq_states\<rbrace>
do_machine_op getActiveIRQ
do_machine_op (getActiveIRQ in_kernel)
\<lbrace>\<lambda>rv s. (\<forall>x. rv = Some x \<longrightarrow> interrupt_states s x = IRQTimer)\<rbrace>"
apply(wp dmo_getActiveIRQ_wp)
apply clarsimp
@ -904,7 +904,7 @@ lemma equiv_valid_inv_conj_lift:
lemma dmo_getActiveIRQ_reads_respects:
notes gets_ev[wp del]
shows
"reads_respects aag l (invs and only_timer_irq_inv irq st) (do_machine_op getActiveIRQ)"
"reads_respects aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel))"
apply(rule use_spec_ev)
apply(rule do_machine_op_spec_reads_respects')
apply(simp add: getActiveIRQ_def)
@ -916,13 +916,13 @@ lemma dmo_getActiveIRQ_reads_respects:
done
lemma dmo_getActiveIRQ_globals_equiv:
"\<lbrace>globals_equiv st\<rbrace> do_machine_op getActiveIRQ \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
"\<lbrace>globals_equiv st\<rbrace> do_machine_op (getActiveIRQ in_kernel) \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (wp dmo_getActiveIRQ_wp)
apply(auto simp: globals_equiv_def idle_equiv_def)
done
lemma dmo_getActiveIRQ_reads_respects_g :
"reads_respects_g aag l (invs and only_timer_irq_inv irq st) (do_machine_op getActiveIRQ)"
"reads_respects_g aag l (invs and only_timer_irq_inv irq st) (do_machine_op (getActiveIRQ in_kernel))"
apply(rule equiv_valid_guard_imp[OF reads_respects_g])
apply(rule dmo_getActiveIRQ_reads_respects)
apply(rule doesnt_touch_globalsI)

4
proof/infoflow/Decode_IF.thy
View File

@ -484,13 +484,13 @@ lemma resolve_vaddr_reads_respects:
done
lemma lookup_pt_slot_no_fail_is_subject:
"\<lbrakk>(\<exists>\<rhd> pd) s; valid_arch_objs s; pspace_aligned s; pas_refined aag s;
"\<lbrakk>(\<exists>\<rhd> pd) s; valid_vspace_objs s; pspace_aligned s; pas_refined aag s;
is_subject aag pd; is_aligned pd pd_bits; vptr < kernel_base;
kheap s pd = Some (ArchObj (PageDirectory pdo));
pdo (ucast (vptr >> 20)) = PageTablePDE p x xa\<rbrakk>
\<Longrightarrow> is_subject aag (lookup_pt_slot_no_fail (ptrFromPAddr p) vptr && ~~ mask pt_bits)"
apply (clarsimp simp: lookup_pt_slot_no_fail_def)
apply (drule valid_arch_objsD)
apply (drule valid_vspace_objsD)
apply (simp add: obj_at_def)
apply assumption
apply (drule kheap_eq_state_vrefs_pas_refinedD)

24
proof/infoflow/Example_Valid_State.thy
View File

@ -1244,7 +1244,7 @@ lemma valid_obj_s0[simp]:
apply (clarsimp simp: Low_pd'_def High_pd'_def Low_pt'_def High_pt'_def
valid_vm_rights_def vm_kernel_only_def)+
apply (clarsimp simp: valid_tcb_def tcb_cap_cases_def is_master_reply_cap_def
valid_ipc_buffer_cap_def valid_tcb_state_def
valid_ipc_buffer_cap_def valid_tcb_state_def valid_arch_tcb_def
| simp add: obj_at_def s0_internal_def kh0_def kh0_obj_def is_ntfn_def)+
apply (simp add: valid_vm_rights_def vm_kernel_only_def)
done
@ -1387,7 +1387,7 @@ lemma valid_pspace_s0[simp]:
apply (rule conjI)
apply (clarsimp simp: if_live_then_nonz_cap_def)
apply (subst(asm) s0_internal_def)
apply (clarsimp simp: obj_at_def kh0_def kh0_obj_def s0_ptr_defs split: if_split_asm)
apply (clarsimp simp: live_def hyp_live_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs split: if_split_asm)
apply (clarsimp simp: ex_nonz_cap_to_def)
apply (rule_tac x="High_cnode_ptr" in exI)
apply (rule_tac x="the_nat_to_bl_10 1" in exI)
@ -1403,7 +1403,12 @@ lemma valid_pspace_s0[simp]:
apply (rule conjI)
apply (simp add: Invariants_AI.cte_wp_at_caps_of_state zombies_final_def)
apply (force dest: s0_caps_of_state simp: is_zombie_def)
apply (clarsimp simp: sym_refs_def state_refs_of_def s0_internal_def)
apply (rule conjI)
apply (clarsimp simp: sym_refs_def state_refs_of_def state_hyp_refs_of_def s0_internal_def)
apply (subst(asm) kh0_def)
apply (clarsimp split: if_split_asm)
apply (simp add: refs_of_def kh0_def s0_ptr_defs kh0_obj_def)+
apply (clarsimp simp: sym_refs_def state_hyp_refs_of_def s0_internal_def)
apply (subst(asm) kh0_def)
apply (clarsimp split: if_split_asm)
by (simp add: refs_of_def kh0_def s0_ptr_defs kh0_obj_def)+
@ -1579,6 +1584,17 @@ lemma valid_arch_objs_s0[simp]:
| erule vs_lookupE, force simp: vs_lookup_def arch_state0_def vs_asid_refs_def)+
done
lemma valid_vspace_objs_s0[simp]:
"valid_vspace_objs s0_internal"
apply (clarsimp simp: valid_vspace_objs_def obj_at_def s0_internal_def)
apply (drule kh0_SomeD)
apply (erule disjE | clarsimp simp: pageBits_def addrFromPPtr_def
physMappingOffset_def kernelBase_addr_def physBase_def is_aligned_def
obj_at_def kh0_def kh0_obj_def a_type_def kernel_mapping_slots_def
High_pt'_def Low_pt'_def High_pd'_def Low_pd'_def ptrFromPAddr_def
| erule vs_lookupE, force simp: vs_lookup_def arch_state0_def vs_asid_refs_def)+
done
lemma valid_arch_caps_s0[simp]:
"valid_arch_caps s0_internal"
apply (clarsimp simp: valid_arch_caps_def)
@ -1598,7 +1614,7 @@ lemma valid_arch_caps_s0[simp]:
lemma valid_global_objs_s0[simp]:
"valid_global_objs s0_internal"
apply (clarsimp simp: valid_global_objs_def s0_internal_def arch_state0_def)
by (force simp: valid_ao_at_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs
by (force simp: valid_vso_at_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs
addrFromPPtr_def physMappingOffset_def kernelBase_addr_def
physBase_def is_aligned_def a_type_def pageBits_def
kernel_mapping_slots_def empty_table_def pde_ref_def

17
proof/infoflow/Finalise_IF.thy
View File

@ -1432,7 +1432,7 @@ lemma arch_finalise_cap_reads_respects:
unmap_page_table_reads_respects
delete_asid_reads_respects
| simp add: invs_psp_aligned invs_arch_objs invs_valid_objs valid_cap_def
| simp add: invs_psp_aligned invs_vspace_objs invs_valid_objs valid_cap_def
split: option.splits bool.splits | intro impI conjI allI |
elim conjE |
(rule aag_cap_auth_subject,assumption,assumption) |
@ -1566,7 +1566,8 @@ lemma rec_del_spec_reads_respects_f:
notes drop_spec_valid[wp_split del] drop_spec_validE[wp_split del]
drop_spec_ev[wp_split del] rec_del.simps[simp del]
shows
"spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and
"spec_reads_respects_f s aag l (silc_inv aag st and only_timer_irq_inv irq st' and
einvs and simple_sched_action and pas_refined aag and
valid_rec_del_call call and
emptyable (slot_rdcall call) and
(\<lambda>s. \<not> exposed_rdcall call \<longrightarrow>
@ -1625,10 +1626,14 @@ next
\<and> emptyable slot s
\<and> simple_sched_action s
\<and> pas_cap_cur_auth aag (fst fin)
\<and> is_subject aag (fst slot) \<and>
(case (fst fin) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst fin)) | _ \<Rightarrow> True) \<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and>
\<and> is_subject aag (fst slot)
\<and> (case (fst fin) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst fin))
| _ \<Rightarrow> True)
\<and> (is_zombie (fst fin) \<or> fst fin = NullCap) \<and>
(is_zombie (fst fin) \<or> fst fin = NullCap)" in hoare_vcg_conj_lift)
apply(wp finalise_cap_invs finalise_cap_replaceable finalise_cap_makes_halted finalise_cap_auth' finalise_cap_ret_is_subject finalise_cap_ret' finalise_cap_silc_inv finalise_cap_ret_is_silc finalise_cap_only_timer_irq_inv)[1]
apply(wp finalise_cap_invs finalise_cap_replaceable Finalise_AC.finalise_cap_makes_halted finalise_cap_auth'
finalise_cap_ret_is_subject finalise_cap_ret' finalise_cap_silc_inv
finalise_cap_ret_is_silc finalise_cap_only_timer_irq_inv)[1]
apply(rule finalise_cap_cases[where slot=slot])
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (erule disjE)
@ -1966,7 +1971,7 @@ lemma pagebitsforsize_ge_2[simp] :
done
lemma arch_finalise_cap_globals_equiv:
"\<lbrace>globals_equiv st and valid_global_objs and valid_arch_state and pspace_aligned and valid_arch_objs and valid_global_refs and valid_vs_lookup\<rbrace>
"\<lbrace>globals_equiv st and valid_global_objs and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_refs and valid_vs_lookup\<rbrace>
arch_finalise_cap cap b
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (induct cap)

4
proof/infoflow/IRQMasks_IF.thy
View File

@ -396,7 +396,7 @@ crunch irq_masks[wp]: handle_vm_fault, handle_hypervisor_fault "\<lambda>s. P (i
lemma dmo_getActiveIRQ_irq_masks[wp]:
"\<lbrace>(\<lambda>s. P (irq_masks_of_state s))\<rbrace>
do_machine_op getActiveIRQ
do_machine_op (getActiveIRQ in_kernel)
\<lbrace>\<lambda>rv s. P (irq_masks_of_state s) \<rbrace>"
apply(rule hoare_pre, rule dmo_wp)
apply(simp add: getActiveIRQ_def | wp | simp add: no_irq_def | clarsimp)+
@ -404,7 +404,7 @@ lemma dmo_getActiveIRQ_irq_masks[wp]:
lemma dmo_getActiveIRQ_return_axiom[wp]:
"\<lbrace>\<top>\<rbrace>
do_machine_op getActiveIRQ
do_machine_op (getActiveIRQ in_kernel)
\<lbrace>(\<lambda>rv s. (\<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ)) \<rbrace>"
apply (simp add: getActiveIRQ_def)
apply(rule hoare_pre, rule dmo_wp)

6
proof/infoflow/Noninterference.thy
View File

@ -388,7 +388,7 @@ lemma kernel_entry_if_integrity:
apply(fastforce intro: integrity_update_reference_state)
apply(wp thread_set_integrity_autarch thread_set_pas_refined
guarded_pas_domain_lift thread_set_invs_trivial thread_set_not_state_valid_sched
| simp add: tcb_cap_cases_def schact_is_rct_def arch_tcb_update_aux2)+
| simp add: tcb_cap_cases_def schact_is_rct_def arch_tcb_update_aux2 tcb_arch_ref_def)+
apply(wp_once prop_of_two_valid[where f="ct_active" and g="cur_thread"])
apply (wp | simp)+
apply(wp thread_set_tcb_context_update_wp)+
@ -2743,7 +2743,7 @@ lemma kernel_entry_if_reads_respects_f_g:
thread_set_invs_trivial
thread_set_not_state_valid_sched
thread_set_pas_refined
| simp add: tcb_cap_cases_def arch_tcb_update_aux2)+
| simp add: tcb_cap_cases_def arch_tcb_update_aux2 tcb_arch_ref_def)+
apply(elim conjE)
apply(frule (1) ct_active_cur_thread_not_idle_thread[OF invs_valid_idle])
apply(clarsimp simp: ct_in_state_def runnable_eq_active)
@ -3304,7 +3304,7 @@ lemma confidentiality_part_not_PSched:
apply(fastforce dest: non_PSched_steps_run_in_lock_step)
done
lemma getActiveIRQ_ret_no_dmo[wp]: "\<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
lemma getActiveIRQ_ret_no_dmo[wp]: "\<lbrace>\<lambda>_. True\<rbrace> getActiveIRQ in_kernel \<lbrace>\<lambda>rv s. \<forall>x. rv = Some x \<longrightarrow> x \<le> maxIRQ\<rbrace>"
apply (simp add: getActiveIRQ_def)
apply(rule hoare_pre)
apply (insert irq_oracle_max_irq)

9
proof/infoflow/Retype_IF.thy
View File

@ -673,7 +673,7 @@ lemma retype_region_globals_equiv:
apply (rule conjI)
apply(clarsimp simp: pspace_no_overlap_def)
apply(drule_tac x="arm_global_pd (arch_state sa)" in spec)
apply(clarsimp simp: invs_def valid_state_def valid_global_objs_def valid_ao_at_def obj_at_def ptr_add_def)
apply(clarsimp simp: invs_def valid_state_def valid_global_objs_def valid_vso_at_def obj_at_def ptr_add_def)
apply(frule_tac p=p in range_cover_subset)
apply(simp add: blah)
apply simp
@ -1117,6 +1117,13 @@ lemma untyped_cap_refs_in_kernel_window_helper:
apply blast
done
crunch valid_global_objs[wp]: create_cap "valid_global_objs"
(simp: crunch_simps)
lemma invs_valid_global_objs_strg:
"invs s \<longrightarrow> valid_global_objs s"
by (clarsimp simp: invs_def valid_state_def)
lemma invoke_untyped_reads_respects_g_wcap:
notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex

4
proof/infoflow/Scheduler_IF.thy
View File

@ -1600,7 +1600,7 @@ lemma schedule_reads_respects_scheduler_cur_domain: "reads_respects_scheduler aa
apply (rule bind_ev)
apply simp
apply (rule next_domain_snippit)
apply (wp_trace when_ev gts_wp get_thread_state_reads_respects_scheduler)+
apply (wp when_ev gts_wp get_thread_state_reads_respects_scheduler)+
apply (clarsimp simp: reads_lrefl)
apply (intro impI conjI allI)
apply (simp add: guarded_pas_domain_def)
@ -2035,7 +2035,7 @@ lemma dmo_return_distr: "do_machine_op (return x) = return x"
(*FIXME: Move to scheduler_if*)
lemma dmo_getActive_IRQ_reads_respect_scheduler: "reads_respects_scheduler aag l (\<lambda>s. irq_masks_of_state st = irq_masks_of_state s)
(do_machine_op getActiveIRQ)"
(do_machine_op (getActiveIRQ in_kernel))"
apply (simp add: getActiveIRQ_def)
apply (simp add: dmo_distr dmo_if_distr dmo_gets_distr dmo_modify_distr dmo_return_distr cong: if_cong)
apply wp

5
proof/infoflow/Syscall_IF.thy
View File

@ -51,6 +51,9 @@ lemma thread_set_globals_equiv':
apply(fastforce simp: valid_ko_at_arm_def obj_at_def get_tcb_def)+
done
crunch valid_global_objs[wp]: cap_move valid_global_objs
(wp: cap_move_ext.valid_global_objs dxo_wp_weak)
lemma invoke_cnode_globals_equiv:
"\<lbrace>globals_equiv st and invs and valid_cnode_inv cinv\<rbrace> invoke_cnode cinv \<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
unfolding invoke_cnode_def without_preemption_def fun_app_def
@ -1029,7 +1032,7 @@ lemma perform_invocation_globals_equiv:
invoke_irq_handler_globals_equiv
arch_perform_invocation_globals_equiv
| wpc | simp)+
apply (auto simp add: invs_imps invs_arch_objs
apply (auto simp add: invs_imps invs_vspace_objs
invs_psp_aligned invs_kernel_mappings
authorised_for_globals_inv_def)
done

6
proof/infoflow/Tcb_IF.thy
View File

@ -128,7 +128,7 @@ crunch globals_equiv[wp]: suspend,prepare_thread_delete "globals_equiv st"
(wp: dxo_wp_weak)
lemma finalise_cap_globals_equiv:
"\<lbrace>globals_equiv st and valid_global_objs and valid_arch_state and pspace_aligned and valid_arch_objs and valid_global_refs and valid_vs_lookup\<rbrace>
"\<lbrace>globals_equiv st and valid_global_objs and valid_arch_state and pspace_aligned and valid_vspace_objs and valid_global_refs and valid_vs_lookup\<rbrace>
finalise_cap cap b
\<lbrace>\<lambda> _. globals_equiv st\<rbrace>"
apply (induct cap)
@ -204,7 +204,7 @@ next
in hoare_vcg_conj_lift)
apply (wp finalise_cap_invs[where slot=slot]
finalise_cap_replaceable[where sl=slot]
finalise_cap_makes_halted[where slot=slot]
Finalise_AC.finalise_cap_makes_halted[where slot=slot]
finalise_cap_P)[1]
apply (rule finalise_cap_cases[where slot=slot])
@ -285,7 +285,7 @@ lemma rec_del_globals_equiv:
"\<lbrace>\<lambda>s. invs s \<and> globals_equiv st s \<and> emptyable (slot_rdcall call) s \<and> valid_rec_del_call call s\<rbrace>
rec_del call
\<lbrace>\<lambda>_. globals_equiv st\<rbrace>"
apply (wp rec_del_preservation2[where Q="valid_ko_at_arm" and R="valid_global_objs and valid_arch_state and pspace_aligned and valid_arch_objs and
apply (wp rec_del_preservation2[where Q="valid_ko_at_arm" and R="valid_global_objs and valid_arch_state and pspace_aligned and valid_vspace_objs and
valid_global_refs and
valid_vs_lookup"] finalise_cap_globals_equiv)
apply simp

32
proof/infoflow/UserOp_IF.thy
View File

@ -515,6 +515,12 @@ lemma valid_pdpt_align_pdD:
apply (clarsimp simp: entries_align_def)
done
lemma valid_vspace_objsD2:
"\<lbrakk>(\<exists>\<rhd> p) s; ko_at (ArchObj ao) p s;
valid_vspace_objs s\<rbrakk>
\<Longrightarrow> valid_vspace_obj ao s"
by (clarsimp simp: valid_vspace_objsD)
lemma ptable_lift_data_consistant:
assumes vs: "valid_state s"
and vpdpt: "valid_pdpt_objs s"
@ -538,7 +544,7 @@ lemma ptable_lift_data_consistant:
apply word_bitwise
apply (simp add: mask_def)
done
have vs': "valid_objs s \<and> valid_arch_objs s \<and> pspace_distinct s \<and> pspace_aligned s"
have vs': "valid_objs s \<and> valid_vspace_objs s \<and> pspace_distinct s \<and> pspace_aligned s"
using vs
by (simp add: valid_state_def valid_pspace_def)
have x_less_kb: "x < kernel_base"
@ -557,14 +563,14 @@ lemma ptable_lift_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr mw pd pt)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add:)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
apply (clarsimp simp: valid_pde_def obj_at_def a_type_def)
apply (case_tac "pt (ucast ((x >> 12) && mask 8))",simp_all)
apply (frule valid_arch_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (frule valid_vspace_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (rule exI)
apply (erule vs_lookup_step)
apply (simp add: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting
@ -586,7 +592,7 @@ lemma ptable_lift_data_consistant:
get_arch_obj_def entries_align_def aligned_stuff mask_AND_NOT_mask
dest!: data_at_aligned is_aligned_ptrFromPAddrD[where a = 16,simplified])
apply (simp add: neg_mask_add_aligned[OF _ and_mask_less'] is_aligned_neg_mask_eq)
apply (frule valid_arch_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (frule valid_vspace_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (rule exI)
apply (erule vs_lookup_step)
apply (simp add: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting
@ -613,7 +619,7 @@ lemma ptable_lift_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr mw pd caprights)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
@ -631,7 +637,7 @@ lemma ptable_lift_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr rights pd)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
@ -669,7 +675,7 @@ lemma ptable_rights_data_consistant:
apply word_bitwise
apply (simp add: mask_def)
done
have vs': "valid_objs s \<and> valid_arch_objs s \<and> pspace_distinct s \<and> pspace_aligned s"
have vs': "valid_objs s \<and> valid_vspace_objs s \<and> pspace_distinct s \<and> pspace_aligned s"
using vs
by (simp add: valid_state_def valid_pspace_def)
have x_less_kb: "x < kernel_base"
@ -688,14 +694,14 @@ lemma ptable_rights_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr mw pd pt)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
apply (rule kernel_mappings_kernel_mapping_slots[OF misc(2)])
apply (clarsimp simp: valid_pde_def obj_at_def a_type_def)
apply (case_tac "pt (ucast ((x >> 12) && mask 8))",simp_all)
apply (frule valid_arch_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (frule valid_vspace_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (rule exI)
apply (erule vs_lookup_step)
apply (simp add: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting
@ -716,7 +722,7 @@ lemma ptable_rights_data_consistant:
apply (clarsimp simp: mask_shift_le get_pt_info_def get_pt_entry_def
get_arch_obj_def entries_align_def aligned_stuff mask_AND_NOT_mask
dest!: data_at_aligned is_aligned_ptrFromPAddrD[where a = 16,simplified])
apply (frule valid_arch_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (frule valid_vspace_objsD2[where p = "ptrFromPAddr p" for p,rotated,unfolded obj_at_def,simplified],simp)
apply (rule exI)
apply (erule vs_lookup_step)
apply (simp add: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting
@ -743,7 +749,7 @@ lemma ptable_rights_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr mw pd caprights)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])
@ -758,7 +764,7 @@ lemma ptable_rights_data_consistant:
split: option.splits arch_kernel_obj.split_asm kernel_object.splits)
apply (rename_tac pd_base vmattr rights pd)
apply (cut_tac get_pd_of_thread_reachable[OF misc(1)])
apply (frule(1) valid_arch_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (frule(1) valid_vspace_objsD2[rotated,unfolded obj_at_def,simplified],simp)
apply (simp add: valid_arch_obj_def)
apply (drule bspec)
apply (rule Compl_iff[THEN iffD2])