From c21127eb0f35e5edb2be5b95ee087d30179a1368 Mon Sep 17 00:00:00 2001 From: Miki Tanaka Date: Thu, 25 May 2017 21:51:59 +1000 Subject: [PATCH] arm InfoFlow: fixes for the backports from arm-hyp --- proof/infoflow/ADT_IF.thy | 79 ++++++++++------- proof/infoflow/Arch_IF.thy | 112 ++++++++++++++++++++----- proof/infoflow/CNode_IF.thy | 18 ++-- proof/infoflow/Decode_IF.thy | 4 +- proof/infoflow/Example_Valid_State.thy | 24 +++++- proof/infoflow/Finalise_IF.thy | 17 ++-- proof/infoflow/IRQMasks_IF.thy | 4 +- proof/infoflow/Noninterference.thy | 6 +- proof/infoflow/Retype_IF.thy | 9 +- proof/infoflow/Scheduler_IF.thy | 4 +- proof/infoflow/Syscall_IF.thy | 5 +- proof/infoflow/Tcb_IF.thy | 6 +- proof/infoflow/UserOp_IF.thy | 32 ++++--- 13 files changed, 223 insertions(+), 97 deletions(-) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 67f989df9..f1f97d21d 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -927,8 +927,9 @@ lemma kernel_entry_if_invs: "\invs and (\s. e \ Interrupt \ ct_active s)\ kernel_entry_if e tc \\_. invs\" - 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) \ idle_thread s \ idle_equiv st s = @@ -1035,10 +1036,11 @@ lemma kernel_entry_silc_inv[wp]: "\silc_inv aag st and einvs and simple_ (\s. ct_active s \ is_subject aag (cur_thread s)) and domain_sep_inv (pasMaySendIrqs aag) st'\ kernel_entry_if ev tc \\_. silc_inv aag st\" - 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]: "\pas_refined aag and guarded_pas_do (\s. ct_active s \ is_subject aag (cur_thread s)) and (\s. ev \ Interrupt \ ct_active s)\ kernel_entry_if ev tc \\rv. pas_refined aag\" - 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: "\domain_sep_inv irqs st and einvs and (\s. e \ Interrupt \ ct_active s)\ kernel_entry_if e tc \\_. domain_sep_inv irqs st\" - 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: (\s. (e \ Interrupt \ ct_active s) \ scheduler_action s = resume_cur_thread)\ kernel_entry_if e tc \\_. valid_sched\" - 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: "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st and invs\ kernel_entry_if e tc \\_ s. P (irq_masks_of_state s)\" - 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 \ (user_context,det_ext) s_monad" where "handle_preemption_if tc \ do - irq \ do_machine_op getActiveIRQ; + irq \ do_machine_op (getActiveIRQ False); when (irq \ None) $ handle_interrupt (the irq); return tc od" @@ -1146,9 +1148,17 @@ crunch idle_thread[wp]: handle_preemption_if "\s. P (idle_thread s)" lemma handle_preemption_if_guarded_pas_domain[wp]: "\guarded_pas_domain aag\ handle_preemption_if tc \\_. guarded_pas_domain aag\" 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]: + "\valid_sched and invs and (\s. irq \ non_kernel_IRQs \ scheduler_act_sane s \ ct_not_queued s)\ + handle_preemption_if irq \\_. valid_sched\" + 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 \ (irq option \ user_context, ('z :: state_ext)) s_monad" where "check_active_irq_if tc \ - do irq \ do_machine_op getActiveIRQ; + do irq \ do_machine_op (getActiveIRQ True); return (irq, tc) od" @@ -2074,9 +2084,9 @@ lemma kernel_entry_if_valid_pdpt_objs[wp]: "\valid_pdpt_objs and invs and (\s. e \ Interrupt \ ct_active s)\kernel_entry_if e tc \\s. valid_pdpt_objs\" 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') \ fst (do_machine_op getActiveIRQ s) \ + "(None,s') \ fst (do_machine_op (getActiveIRQ in_kernel) s) \ 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') \ fst (do_machine_op getActiveIRQ s) \ + "(Some i,s') \ fst (do_machine_op (getActiveIRQ in_kernel) s) \ 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="\"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] | simp add: tcb_cap_cases_def)+ + apply(wpsimp wp: irq_measure_if_inv'[where Q="\"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] + 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="\"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] | simp add: tcb_cap_cases_def)+ + apply(wpsimp wp: irq_measure_if_inv'[where Q="\"] irq_state_inv_triv + thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] + 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="\"] irq_state_inv_triv thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] | simp add: tcb_cap_cases_def)+ + apply(wpsimp wp: irq_measure_if_inv'[where Q="\"] irq_state_inv_triv + thread_set_invs_trivial irq_is_recurring_triv[where Q="\"] + 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) diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy index 108177365..b34554b62 100644 --- a/proof/infoflow/Arch_IF.thy +++ b/proof/infoflow/Arch_IF.thy @@ -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 \ 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 \ 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 \ 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 \ 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 \ 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 \ 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 : "\Q\ f \\ r. P r\pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup + "\pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state\ find_pd_for_asid asid \\rv s. lookup_pd_slot rv vptr && ~~ mask pd_bits \ arm_global_pd (arch_state s)\, -" @@ -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: - "\pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup + "\pspace_aligned and valid_vspace_objs and valid_global_objs and valid_vs_lookup and valid_global_refs and valid_arch_state\ find_pd_for_asid asid \\rv s. @@ -1702,7 +1702,7 @@ done declare dmo_mol_globals_equiv[wp] lemma unmap_page_table_globals_equiv: - "\pspace_aligned and valid_arch_objs and valid_global_objs and valid_vs_lookup + "\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\ unmap_page_table asid vaddr pt \\rv. globals_equiv st\" 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: "\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\ perform_page_table_invocation pti \\_. globals_equiv st\" 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: - "\globals_equiv st and valid_arch_state and pspace_aligned and valid_arch_objs + "\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 \ unmap_page pgsz asid vptr pptr \\_. globals_equiv st\" 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: "\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\ perform_page_invocation pgi \\_. globals_equiv st\" @@ -2253,7 +2253,7 @@ lemma arch_perform_invocation_globals_equiv: done lemma find_pd_for_asid_authority3: - "\\s. \pd. (pspace_aligned s \ valid_arch_objs s \ is_aligned pd pd_bits) + "\\s. \pd. (pspace_aligned s \ valid_vspace_objs s \ is_aligned pd pd_bits) \ (\\ pd) s \ Q pd s\ find_pd_for_asid asid \Q\, -" (is "\?P\ ?f \Q\,-") @@ -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 + \ tab = arm_asid_table (arch_state s) + \ valid_vspace_objs (s\arch_state := arch_state s\arm_asid_table := tab(asid_high_bits_of base := None)\\)" + 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]: + "\valid_vspace_objs\ invalidate_hw_asid_entry asid \\_. valid_vspace_objs\" + 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 \ valid_vspace_objs \" + 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 _ _" "\_ 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]: "\valid_arch_objs\ 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]: + "\valid_vspace_objs\ + delete_asid_pool base pptr + \\_. valid_vspace_objs\" + 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'': "\(valid_arch_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\ set_asid_pool p f \\_. valid_arch_objs\" 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'': + "\(valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p) and K(f = (ap |` S))\ set_asid_pool p f \\_. valid_vspace_objs\" + 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 \ 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]: + "\valid_vspace_objs and pspace_aligned\ delete_asid a b \\_. valid_vspace_objs\" + 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]: + "\valid_vspace_objs and valid_pte pte\ + store_pte p pte + \\_. (valid_vspace_objs)\" + 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) diff --git a/proof/infoflow/CNode_IF.thy b/proof/infoflow/CNode_IF.thy index 6ec22cb21..191bf17bf 100644 --- a/proof/infoflow/CNode_IF.thy +++ b/proof/infoflow/CNode_IF.thy @@ -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 \ 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 \ Interrupted) odE else returnOk() odE" @@ -675,13 +675,13 @@ definition irq_is_recurring :: "irq \ ('z::state_ext) state \\s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) (s\machine_state := (machine_state s\irq_state := irq_state (machine_state s) + 1\)\)\ do_machine_op getActiveIRQ \P\" - apply(simp add: do_machine_op_def getActiveIRQ_def) + "\\s. P (irq_at (irq_state (machine_state s) + 1) (irq_masks (machine_state s))) (s\machine_state := (machine_state s\irq_state := irq_state (machine_state s) + 1\)\)\ do_machine_op (getActiveIRQ in_kernel) \P\" + 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: "\domain_sep_inv False st and valid_irq_states\ - do_machine_op getActiveIRQ + do_machine_op (getActiveIRQ in_kernel) \\rv s. (\x. rv = Some x \ interrupt_states s x = IRQTimer)\" 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: - "\globals_equiv st\ do_machine_op getActiveIRQ \\_. globals_equiv st\" + "\globals_equiv st\ do_machine_op (getActiveIRQ in_kernel) \\_. globals_equiv st\" 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) diff --git a/proof/infoflow/Decode_IF.thy b/proof/infoflow/Decode_IF.thy index e998331a5..7793a4413 100644 --- a/proof/infoflow/Decode_IF.thy +++ b/proof/infoflow/Decode_IF.thy @@ -484,13 +484,13 @@ lemma resolve_vaddr_reads_respects: done lemma lookup_pt_slot_no_fail_is_subject: - "\(\\ pd) s; valid_arch_objs s; pspace_aligned s; pas_refined aag s; + "\(\\ 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\ \ 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) diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy index 4d4bc2356..c7bc8c4fb 100644 --- a/proof/infoflow/Example_Valid_State.thy +++ b/proof/infoflow/Example_Valid_State.thy @@ -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 diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 31507f7d1..27fc65b25 100644 --- a/proof/infoflow/Finalise_IF.thy +++ b/proof/infoflow/Finalise_IF.thy @@ -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 (\s. \ exposed_rdcall call \ @@ -1625,10 +1626,14 @@ next \ emptyable slot s \ simple_sched_action s \ pas_cap_cur_auth aag (fst fin) - \ is_subject aag (fst slot) \ -(case (fst fin) of Zombie ptr bits n \ is_subject aag (obj_ref_of (fst fin)) | _ \ True) \ (is_zombie (fst fin) \ fst fin = NullCap) \ + \ is_subject aag (fst slot) + \ (case (fst fin) of Zombie ptr bits n \ is_subject aag (obj_ref_of (fst fin)) + | _ \ True) + \ (is_zombie (fst fin) \ fst fin = NullCap) \ (is_zombie (fst fin) \ 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: - "\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\ + "\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\ arch_finalise_cap cap b \\_. globals_equiv st\" apply (induct cap) diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index f18c43a3b..31e563a6f 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -396,7 +396,7 @@ crunch irq_masks[wp]: handle_vm_fault, handle_hypervisor_fault "\s. P (i lemma dmo_getActiveIRQ_irq_masks[wp]: "\(\s. P (irq_masks_of_state s))\ - do_machine_op getActiveIRQ + do_machine_op (getActiveIRQ in_kernel) \\rv s. P (irq_masks_of_state s) \" 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]: "\\\ - do_machine_op getActiveIRQ + do_machine_op (getActiveIRQ in_kernel) \(\rv s. (\x. rv = Some x \ x \ maxIRQ)) \" apply (simp add: getActiveIRQ_def) apply(rule hoare_pre, rule dmo_wp) diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 9a8b6a095..15c93d216 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -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]: "\\_. True\ getActiveIRQ \\rv s. \x. rv = Some x \ x \ maxIRQ\" +lemma getActiveIRQ_ret_no_dmo[wp]: "\\_. True\ getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) apply(rule hoare_pre) apply (insert irq_oracle_max_irq) diff --git a/proof/infoflow/Retype_IF.thy b/proof/infoflow/Retype_IF.thy index d9d0d217c..305263d7a 100644 --- a/proof/infoflow/Retype_IF.thy +++ b/proof/infoflow/Retype_IF.thy @@ -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 \ 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 diff --git a/proof/infoflow/Scheduler_IF.thy b/proof/infoflow/Scheduler_IF.thy index d5adf98b7..90762acc7 100644 --- a/proof/infoflow/Scheduler_IF.thy +++ b/proof/infoflow/Scheduler_IF.thy @@ -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 (\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 diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index f0701d8e4..73b865567 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -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: "\globals_equiv st and invs and valid_cnode_inv cinv\ invoke_cnode cinv \\_. globals_equiv st\" 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 diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy index c5b3bc330..5c8a87021 100644 --- a/proof/infoflow/Tcb_IF.thy +++ b/proof/infoflow/Tcb_IF.thy @@ -128,7 +128,7 @@ crunch globals_equiv[wp]: suspend,prepare_thread_delete "globals_equiv st" (wp: dxo_wp_weak) lemma finalise_cap_globals_equiv: - "\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\ + "\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\ finalise_cap cap b \\ _. globals_equiv st\" 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: "\\s. invs s \ globals_equiv st s \ emptyable (slot_rdcall call) s \ valid_rec_del_call call s\ rec_del call \\_. globals_equiv st\" - 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 diff --git a/proof/infoflow/UserOp_IF.thy b/proof/infoflow/UserOp_IF.thy index efdb15128..f63023acb 100644 --- a/proof/infoflow/UserOp_IF.thy +++ b/proof/infoflow/UserOp_IF.thy @@ -515,6 +515,12 @@ lemma valid_pdpt_align_pdD: apply (clarsimp simp: entries_align_def) done +lemma valid_vspace_objsD2: + "\(\\ p) s; ko_at (ArchObj ao) p s; + valid_vspace_objs s\ + \ 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 \ valid_arch_objs s \ pspace_distinct s \ pspace_aligned s" + have vs': "valid_objs s \ valid_vspace_objs s \ pspace_distinct s \ 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 \ valid_arch_objs s \ pspace_distinct s \ pspace_aligned s" + have vs': "valid_objs s \ valid_vspace_objs s \ pspace_distinct s \ 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])