From eb7f7b15641178889fca653408baf36b4449fa38 Mon Sep 17 00:00:00 2001 From: Miki Tanaka Date: Wed, 29 Jun 2016 16:21:23 +1000 Subject: [PATCH] arch-split: Tcb_AI.thy done --- proof/access-control/DomainSepInv.thy | 2 +- proof/access-control/Syscall_AC.thy | 2 +- proof/access-control/Tcb_AC.thy | 18 +- proof/drefine/Tcb_DR.thy | 4 +- proof/infoflow/ADT_IF.thy | 2 +- proof/infoflow/FinalCaps.thy | 2 +- proof/infoflow/IRQMasks_IF.thy | 2 +- proof/infoflow/Tcb_IF.thy | 12 +- proof/invariant-abstract/ARM/ArchTcb_AI.thy | 354 +++++++++++++- proof/invariant-abstract/Syscall_AI.thy | 4 +- proof/invariant-abstract/Tcb_AI.thy | 490 +++++--------------- proof/refine/Tcb_R.thy | 2 +- 12 files changed, 475 insertions(+), 419 deletions(-) diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index 44a504f99..d5c1894e2 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -1212,7 +1212,7 @@ crunch domain_sep_inv[wp]: bind_notification "domain_sep_inv irqs st" lemma invoke_tcb_domain_sep_inv: "\domain_sep_inv irqs st and - tcb_inv_wf tinv\ + Tcb_AI.tcb_inv_wf tinv\ invoke_tcb tinv \\_. domain_sep_inv irqs st\" apply(case_tac tinv) diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index c667c5714..70e3d154b 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -29,7 +29,7 @@ where \ aag_has_auth_to aag SyncSend epptr | Invocations_A.InvokeNotification ep badge \ aag_has_auth_to aag Notify ep | Invocations_A.InvokeReply thread slot \ is_subject aag thread \ is_subject aag (fst slot) - | Invocations_A.InvokeTCB i' \ tcb_inv_wf i' s \ authorised_tcb_inv aag i' + | Invocations_A.InvokeTCB i' \ Tcb_AI.tcb_inv_wf i' s \ authorised_tcb_inv aag i' | Invocations_A.InvokeDomain thread slot \ False | Invocations_A.InvokeCNode i' \ authorised_cnode_inv aag i' s \ is_subject aag (cur_thread s) \ cnode_inv_auth_derivations i' s diff --git a/proof/access-control/Tcb_AC.thy b/proof/access-control/Tcb_AC.thy index f54280a39..a589e4b24 100644 --- a/proof/access-control/Tcb_AC.thy +++ b/proof/access-control/Tcb_AC.thy @@ -222,7 +222,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemma invoke_tcb_tc_respects_aag: "\ integrity aag X st and pas_refined aag - and einvs and simple_sched_action and tcb_inv_wf (tcb_invocation.ThreadControl t sl ep priority croot vroot buf) + and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf (tcb_invocation.ThreadControl t sl ep priority croot vroot buf) and K (authorised_tcb_inv aag (tcb_invocation.ThreadControl t sl ep priority croot vroot buf))\ invoke_tcb (tcb_invocation.ThreadControl t sl ep priority croot vroot buf) \\rv. integrity aag X st and pas_refined aag\" @@ -294,7 +294,7 @@ lemma invoke_tcb_tc_respects_aag: lemma invoke_tcb_unbind_notification_respects: "\integrity aag X st and pas_refined aag - and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t None) + and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t None) and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t None))\ invoke_tcb (tcb_invocation.NotificationControl t None) \\rv. integrity aag X st\" @@ -331,7 +331,7 @@ lemma bind_notification_respects: lemma invoke_tcb_bind_notification_respects: "\integrity aag X st and pas_refined aag - and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t (Some ntfn)) + and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t (Some ntfn)) and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t (Some ntfn)))\ invoke_tcb (tcb_invocation.NotificationControl t (Some ntfn)) \\rv. integrity aag X st\" @@ -343,21 +343,21 @@ lemma invoke_tcb_bind_notification_respects: lemma invoke_tcb_ntfn_control_respects[wp]: "\integrity aag X st and pas_refined aag - and einvs and tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) + and einvs and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\ invoke_tcb (tcb_invocation.NotificationControl t ntfn) \\rv. integrity aag X st\" - apply (case_tac ntfn, simp_all del: invoke_tcb.simps tcb_inv_wf.simps K_def) + apply (case_tac ntfn, simp_all del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) apply (wp invoke_tcb_bind_notification_respects invoke_tcb_unbind_notification_respects) done lemma invoke_tcb_respects: "\integrity aag X st and pas_refined aag - and einvs and simple_sched_action and tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\ + and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti and K (authorised_tcb_inv aag ti)\ invoke_tcb ti \\rv. integrity aag X st\" apply (cases ti, simp_all add: hoare_conjD1 [OF invoke_tcb_tc_respects_aag [simplified simp_thms]] - del: invoke_tcb.simps tcb_inv_wf.simps K_def) + del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps K_def) apply (safe intro!: hoare_gen_asm) apply ((wp itr_wps mapM_x_wp' | simp add: if_apply_def2 split del: split_if | wpc | clarsimp simp: authorised_tcb_inv_def @@ -383,7 +383,7 @@ lemma bind_notification_pas_refined[wp]: done lemma invoke_tcb_ntfn_control_pas_refined[wp]: - "\pas_refined aag and tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) and einvs and simple_sched_action + "\pas_refined aag and Tcb_AI.tcb_inv_wf (tcb_invocation.NotificationControl t ntfn) and einvs and simple_sched_action and K (authorised_tcb_inv aag (tcb_invocation.NotificationControl t ntfn))\ invoke_tcb (tcb_invocation.NotificationControl t ntfn) \\_. pas_refined aag\" @@ -393,7 +393,7 @@ lemma invoke_tcb_ntfn_control_pas_refined[wp]: done lemma invoke_tcb_pas_refined: - "\pas_refined aag and tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\ + "\pas_refined aag and Tcb_AI.tcb_inv_wf ti and einvs and simple_sched_action and K (authorised_tcb_inv aag ti)\ invoke_tcb ti \\rv. pas_refined aag\" apply (cases "\t sl ep priority croot vroot buf. diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy index 1ba1842f5..57ab0c416 100644 --- a/proof/drefine/Tcb_DR.thy +++ b/proof/drefine/Tcb_DR.thy @@ -1501,7 +1501,7 @@ lemma invoke_tcb_corres_thread_control: "\ t' = tcb_invocation.ThreadControl obj_id' a' fault_ep' prio' croot' vroot' ipc_buffer'; t = translate_tcb_invocation t' \ \ dcorres (dc \ dc) \ (\s. invs s \ valid_etcbs s \ not_idle_thread obj_id' s - \ valid_pdpt_objs s \ tcb_inv_wf t' s) + \ valid_pdpt_objs s \ Tcb_AI.tcb_inv_wf t' s) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (rule corres_guard_imp[OF dcorres_thread_control]) apply fastforce @@ -1606,7 +1606,7 @@ lemmas invoke_tcb_rules = ex_nonz_cap_implies_normal_tcb lemma invoke_tcb_corres: "\ t = translate_tcb_invocation t' \ \ - dcorres (dc \ dc) \ (invs and valid_pdpt_objs and tcb_inv_wf t' and valid_etcbs) + dcorres (dc \ dc) \ (invs and valid_pdpt_objs and Tcb_AI.tcb_inv_wf t' and valid_etcbs) (Tcb_D.invoke_tcb t) (Tcb_A.invoke_tcb t')" apply (clarsimp) apply (case_tac t') diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 62bfb9f42..6d8cf02aa 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -2905,7 +2905,7 @@ lemmas bind_notification_irq_state_inv[wp] = lemma invoke_tcb_irq_state_inv: "\(\s. irq_state_inv st s) and domain_sep_inv False sta and - tcb_inv_wf tinv and K (irq_is_recurring irq st)\ + Tcb_AI.tcb_inv_wf tinv and K (irq_is_recurring irq st)\ invoke_tcb tinv \\_ s. irq_state_inv st s\,\\_. irq_state_next st\" apply(case_tac tinv) diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index 870aa3032..b861ef68f 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -3013,7 +3013,7 @@ lemma invoke_tcb_silc_inv: static_imp_conj_wp [wp] shows "\silc_inv aag st and einvs and simple_sched_action and pas_refined aag and - tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\ + Tcb_AI.tcb_inv_wf tinv and K (authorised_tcb_inv aag tinv)\ invoke_tcb tinv \\_. silc_inv aag st\" apply(case_tac tinv) diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index 37c90f11b..324a35226 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -205,7 +205,7 @@ lemma checked_insert_irq_masks[wp]: goals *) lemma invoke_tcb_irq_masks: "\(\s. P (irq_masks_of_state s)) and domain_sep_inv False st and - tcb_inv_wf tinv\ + Tcb_AI.tcb_inv_wf tinv\ invoke_tcb tinv \\_ s. P (irq_masks_of_state s)\" apply(case_tac tinv) diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy index cb08e64fc..2250373b0 100644 --- a/proof/infoflow/Tcb_IF.thy +++ b/proof/infoflow/Tcb_IF.thy @@ -331,7 +331,7 @@ lemma invoke_tcb_thread_preservation: assumes thread_set_P': "\f ptr. \invs and P\ thread_set (tcb_fault_handler_update f) ptr \\_.P\" assumes P_trans[simp]: "\f s. P (trans_state f s) = P s" shows " - \P and invs and tcb_inv_wf (tcb_invocation.ThreadControl t sl ep prio croot vroot buf)\ + \P and invs and Tcb_AI.tcb_inv_wf (tcb_invocation.ThreadControl t sl ep prio croot vroot buf)\ invoke_tcb (tcb_invocation.ThreadControl t sl ep prio croot vroot buf) \\rv. P\" @@ -431,17 +431,17 @@ lemma invoke_tcb_NotificationControl_globals_equiv: done lemma invoke_tcb_globals_equiv: - "\ invs and globals_equiv st and tcb_inv_wf ti\ + "\ invs and globals_equiv st and Tcb_AI.tcb_inv_wf ti\ invoke_tcb ti \\_. globals_equiv st\" apply(case_tac ti) prefer 4 - apply (simp del: invoke_tcb.simps tcb_inv_wf.simps) + apply (simp del: invoke_tcb.simps Tcb_AI.tcb_inv_wf.simps) apply (wp invoke_tcb_thread_preservation cap_delete_globals_equiv cap_insert_globals_equiv'' thread_set_globals_equiv | clarsimp simp add: invs_valid_ko_at_arm split del: split_if)+ - apply (simp_all del: tcb_inv_wf.simps split del: split_if) + apply (simp_all del: Tcb_AI.tcb_inv_wf.simps split del: split_if) apply (wp | clarsimp simp: invs_valid_ko_at_arm no_cap_to_idle_thread | intro conjI impI)+ apply (rename_tac word1 word2 bool1 bool2 bool3 bool4 arm_copy_register_sets) apply (rule_tac Q="\_. valid_ko_at_arm and globals_equiv st and (\s. word1 \ idle_thread s) @@ -650,7 +650,7 @@ lemma invoke_tcb_reads_respects_f: notes validE_valid[wp del] static_imp_wp [wp] shows - "reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and (\s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \ authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)" + "reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and Tcb_AI.tcb_inv_wf ti and (\s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \ authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)" apply(case_tac ti) apply(wp when_ev restart_reads_respects_f as_user_reads_respects_f static_imp_wp | simp)+ apply(auto intro: requiv_cur_thread_eq intro!: det_zipWithM simp: det_setRegister det_getRestartPC det_setNextPC authorised_tcb_inv_def simp: reads_equiv_f_def)[1] @@ -707,7 +707,7 @@ lemma invoke_tcb_reads_respects_f: lemma invoke_tcb_reads_respects_f_g: -"reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and tcb_inv_wf ti and (\s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \ authorised_tcb_inv_extra aag ti)) +"reads_respects_f_g aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and pas_cur_domain aag and einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti and (\s. is_subject aag (cur_thread s)) and K (authorised_tcb_inv aag ti \ authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)" apply (rule equiv_valid_guard_imp) apply (rule reads_respects_f_g) diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index a257ca089..60a74f01b 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -12,23 +12,357 @@ theory ArchTcb_AI imports "../Tcb_AI" begin -context Arch begin +context Arch begin global_naming ARM named_theorems Tcb_AI_asms -definition "Tcb_AI_dummy_const \ (1 :: nat)" -lemma Tcb_AI_trivial_result[Tcb_AI_asms]: - "Tcb_AI_dummy_const > 0" - by (simp add: Tcb_AI_dummy_const_def) +lemma activate_idle_invs[Tcb_AI_asms]: + "\invs and ct_idle\ + arch_activate_idle_thread thread + \\rv. invs and ct_idle\" + by (simp add: arch_activate_idle_thread_def) + + +lemma empty_fail_getRegister [intro!, simp, Tcb_AI_asms]: + "empty_fail (getRegister r)" + by (simp add: getRegister_def) + + +lemma same_object_also_valid: (* arch specific *) + "\ same_object_as cap cap'; s \ cap'; wellformed_cap cap; + cap_asid cap = None \ (\asid. cap_asid cap = Some asid \ 0 < asid \ asid \ 2^asid_bits - 1); + cap_vptr cap = None; cap_asid_base cap = None \ + \ s \ cap" + apply (cases cap, + (clarsimp simp: same_object_as_def is_cap_simps cap_asid_def + wellformed_cap_def wellformed_acap_def + valid_cap_def bits_of_def cap_aligned_def + split: cap.split_asm arch_cap.split_asm option.splits)+) + done + +lemma same_object_obj_refs[Tcb_AI_asms]: + "\ same_object_as cap cap' \ + \ obj_refs cap = obj_refs cap'" + apply (cases cap, simp_all add: same_object_as_def) + apply ((clarsimp simp: is_cap_simps bits_of_def same_aobject_as_def + split: cap.split_asm )+) + by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp) + + +definition + is_cnode_or_valid_arch :: "cap \ bool" +where + "is_cnode_or_valid_arch cap \ + is_cnode_cap cap + \ (is_arch_cap cap + \ (is_pt_cap cap \ cap_asid cap \ None) + \ (is_pd_cap cap \ cap_asid cap \ None))" + + +definition (* arch specific *) + "pt_pd_asid cap \ case cap of + ArchObjectCap (PageTableCap _ (Some (asid, _))) \ Some asid + | ArchObjectCap (PageDirectoryCap _ (Some asid)) \ Some asid + | _ \ None" + +lemmas pt_pd_asid_simps [simp] = (* arch specific *) + pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split] + +lemma checked_insert_is_derived: (* arch specific *) + "\ same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; + obj_refs new_cap = obj_refs old_cap + \ table_cap_ref old_cap = table_cap_ref new_cap + \ pt_pd_asid old_cap = pt_pd_asid new_cap\ + \ is_derived m slot new_cap old_cap" + apply (cases slot) + apply (frule same_object_as_cap_master) + apply (frule master_cap_obj_refs) + apply (frule cap_master_eq_badge_none) + apply (frule same_master_cap_same_types) + apply (simp add: is_derived_def) + apply clarsimp + apply (auto simp: is_cap_simps cap_master_cap_def + is_cnode_or_valid_arch_def vs_cap_ref_def + table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq + split: cap.split_asm arch_cap.split_asm + option.split_asm)[1] + done + +lemma is_cnode_or_valid_arch_cap_asid: (* arch specific *) + "is_cnode_or_valid_arch cap + \ (is_pt_cap cap \ cap_asid cap \ None) + \ (is_pd_cap cap \ cap_asid cap \ None)" + by (auto simp add: is_cnode_or_valid_arch_def + is_cap_simps) + +lemma checked_insert_tcb_invs[wp]: (* arch specific *) + "\invs and cte_wp_at (\c. c = cap.NullCap) (target, ref) + and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap + and tcb_cap_valid new_cap (target, ref) + and K (is_pt_cap new_cap \ is_pd_cap new_cap + \ cap_asid new_cap \ None) + and (cte_wp_at (\c. obj_refs c = obj_refs new_cap + \ table_cap_ref c = table_cap_ref new_cap \ + pt_pd_asid c = pt_pd_asid new_cap) src_slot)\ + check_cap_at new_cap src_slot + (check_cap_at (cap.ThreadCap target) slot + (cap_insert new_cap src_slot (target, ref))) \\rv. invs\" + apply (simp add: check_cap_at_def) + apply (rule hoare_pre) + apply (wp get_cap_wp) + apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce) + apply (frule caps_of_state_valid_cap[where p=slot], fastforce) + apply (rule conjI, simp only: ex_cte_cap_wp_to_def) + apply (rule_tac x=slot in exI) + apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs) + apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps + dest!: cap_master_cap_eqDs) + apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x]) + apply (erule cte_wp_atE[OF caps_of_state_cteD]) + apply (fastforce simp: obj_at_def is_obj_defs) + apply clarsimp + apply (rule conjI) + apply clarsimp + apply (subgoal_tac "\ is_zombie new_cap") + apply (simp add: same_object_zombies same_object_obj_refs) + apply (erule(2) zombies_final_helperE) + apply fastforce + apply (fastforce simp add: cte_wp_at_caps_of_state) + apply assumption + apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps + is_valid_vtable_root_def) + apply (rule conjI) + apply (erule(1) checked_insert_is_derived, simp+) + apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps) + done + + +lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]: + assumes x: "P cap.NullCap" + shows "\\s. \cp \ ran (caps_of_state s). P cp\ + finalise_cap cap fin + \\rv s. \cp \ ran (caps_of_state s). P cp\" + apply (cases cap, simp_all) + apply (wp suspend_caps_of_state hoare_vcg_all_lift + | simp + | rule impI + | rule hoare_drop_imps)+ + apply (clarsimp simp: ball_ran_eq x) + apply (wp delete_one_caps_of_state + | rule impI + | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+ + done + + +lemma table_cap_ref_max_free_index_upd[simp,Tcb_AI_asms]: + "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" + by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) + + +interpretation Tcb_AI_1? : Tcb_AI_1 + where state_ext_t = state_ext_t + and is_cnode_or_valid_arch = is_cnode_or_valid_arch +by (unfold_locales; fact Tcb_AI_asms) + + +lemma use_no_cap_to_obj_asid_strg: (* arch specific *) + "(cte_at p s \ no_cap_to_obj_dr_emp cap s \ valid_cap cap s \ invs s) + \ cte_wp_at (\c. obj_refs c = obj_refs cap + \ table_cap_ref c = table_cap_ref cap \ pt_pd_asid c = pt_pd_asid cap) p s" + apply (clarsimp simp: cte_wp_at_caps_of_state + no_cap_to_obj_with_diff_ref_def + simp del: split_paired_All) + apply (frule caps_of_state_valid_cap, fastforce) + apply (erule allE)+ + apply (erule (1) impE)+ + apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) + apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ + done + +lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: + "\no_cap_to_obj_dr_emp cap\ + cap_delete slot + \\rv. no_cap_to_obj_dr_emp cap\" + apply (simp add: cap_delete_def + no_cap_to_obj_with_diff_ref_ran_caps_form) + apply wp + apply simp + apply (rule use_spec) + apply (rule rec_del_all_caps_in_range) + apply (simp add: table_cap_ref_def[simplified, split_simps cap.split] + | rule obj_ref_none_no_asid)+ + done + + +lemma tc_invs[Tcb_AI_asms]: + "\invs and tcb_at a + and (case_option \ (valid_cap o fst) e) + and (case_option \ (valid_cap o fst) f) + and (case_option \ (case_option \ (valid_cap o fst) o snd) g) + and (case_option \ (cte_at o snd) e) + and (case_option \ (cte_at o snd) f) + and (case_option \ (case_option \ (cte_at o snd) o snd) g) + and (case_option \ (no_cap_to_obj_dr_emp o fst) e) + and (case_option \ (no_cap_to_obj_dr_emp o fst) f) + and (case_option \ (case_option \ (no_cap_to_obj_dr_emp o fst) o snd) g) + and K (case_option True (is_cnode_cap o fst) e) + and K (case_option True (is_valid_vtable_root o fst) f) + and K (case_option True (\v. case_option True + ((swp valid_ipc_buffer_cap (fst v) + and is_arch_cap and is_cnode_or_valid_arch) + o fst) (snd v)) g) + and K (case_option True (\bl. length bl = word_bits) b)\ + invoke_tcb (ThreadControl a sl b pr e f g) + \\rv. invs\" + apply (rule hoare_gen_asm)+ + apply (simp add: split_def cong: option.case_cong) + apply (rule hoare_vcg_precond_imp) + apply wp + apply ((simp only: simp_thms + | rule wp_split_const_if wp_split_const_if_R + hoare_vcg_all_lift_R + hoare_vcg_E_elim hoare_vcg_const_imp_lift_R + hoare_vcg_R_conj + | (wp out_invs_trivial case_option_wpE cap_delete_deletes + cap_delete_valid_cap cap_insert_valid_cap out_cte_at + cap_insert_cte_at cap_delete_cte_at out_valid_cap + hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R + thread_set_tcb_ipc_buffer_cap_cleared_invs + thread_set_invs_trivial[OF ball_tcb_cap_casesI] + hoare_vcg_all_lift thread_set_valid_cap out_emptyable + check_cap_inv [where P="valid_cap c" for c] + check_cap_inv [where P="tcb_cap_valid c p" for c p] + check_cap_inv[where P="cte_at p0" for p0] + check_cap_inv[where P="tcb_at p0" for p0] + thread_set_cte_at + thread_set_cte_wp_at_trivial[where Q="\x. x", OF ball_tcb_cap_casesI] + thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI] + checked_insert_no_cap_to + out_no_cap_to_trivial[OF ball_tcb_cap_casesI] + thread_set_ipc_tcb_cap_valid + static_imp_wp static_imp_conj_wp)[1] + | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] + emptyable_def + del: hoare_True_E_R + | wpc + | strengthen use_no_cap_to_obj_asid_strg + tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] + tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+) + apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] + is_cap_simps is_valid_vtable_root_def + is_cnode_or_valid_arch_def tcb_cap_valid_def + invs_valid_objs cap_asid_def vs_cap_ref_def + split: option.split_asm + | rule conjI)+ + done + + +lemma check_valid_ipc_buffer_inv: (* arch_specific *) + "\P\ check_valid_ipc_buffer vptr cap \\rv. P\" + apply (simp add: check_valid_ipc_buffer_def whenE_def + cong: cap.case_cong arch_cap.case_cong + split del: split_if) + apply (rule hoare_pre) + apply (wp | simp split del: split_if | wpcw)+ + done + +lemma check_valid_ipc_buffer_wp[Tcb_AI_asms]: + "\\(s::'state_ext::state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap + \ valid_ipc_buffer_cap cap vptr + \ is_aligned vptr msg_align_bits + \ P s\ + check_valid_ipc_buffer vptr cap + \\rv. P\,-" + apply (simp add: check_valid_ipc_buffer_def whenE_def + cong: cap.case_cong arch_cap.case_cong + split del: split_if) + apply (rule hoare_pre) + apply (wp | simp split del: split_if | wpc)+ + apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def + valid_ipc_buffer_cap_def) + done + +lemma derive_no_cap_asid[wp,Tcb_AI_asms]: + "\(no_cap_to_obj_with_diff_ref cap S)::'state_ext::state_ext state\bool\ + derive_cap slot cap + \\rv. no_cap_to_obj_with_diff_ref rv S\,-" + apply (simp add: derive_cap_def arch_derive_cap_def + cong: cap.case_cong) + apply (rule hoare_pre) + apply (wp | simp | wpc)+ + apply (auto simp add: no_cap_to_obj_with_diff_ref_Null, + auto simp add: no_cap_to_obj_with_diff_ref_def + table_cap_ref_def) + done + + +lemma decode_set_ipc_inv[wp,Tcb_AI_asms]: + "\P::'state_ext::state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" + apply (simp add: decode_set_ipc_buffer_def whenE_def + split_def + split del: split_if) + apply (rule hoare_pre, wp check_valid_ipc_buffer_inv) + apply simp + done + +lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: + "no_cap_to_obj_with_diff_ref c S s \ + no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" + apply (case_tac "update_cap_data P x c = NullCap") + apply (simp add: no_cap_to_obj_with_diff_ref_Null) + apply (subgoal_tac "vs_cap_ref (update_cap_data P x c) + = vs_cap_ref c") + apply (simp add: no_cap_to_obj_with_diff_ref_def + update_cap_objrefs) + apply (clarsimp simp: update_cap_data_closedform + table_cap_ref_def + arch_update_cap_data_def + split: cap.split) + apply simp + done + + +lemma update_cap_valid[Tcb_AI_asms]: + "valid_cap cap (s::'state_ext::state_ext state) \ + valid_cap (case capdata of + None \ cap_rights_update rs cap + | Some x \ update_cap_data p x + (cap_rights_update rs cap)) s" + apply (case_tac capdata, simp_all)[1] + apply (case_tac cap, + simp_all add: update_cap_data_def cap_rights_update_def + is_cap_defs Let_def split_def valid_cap_def + badge_update_def the_cnode_cap_def cap_aligned_def + arch_update_cap_data_def + split del: split_if) + apply (simp add: badge_update_def cap_rights_update_def) + apply (simp add: badge_update_def) + apply simp + apply (rename_tac arch_cap) + using valid_validate_vm_rights[simplified valid_vm_rights_def] + apply (case_tac arch_cap, simp_all add: acap_rights_update_def + split: option.splits prod.splits) + done + + +crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t" + (wp: crunch_wps simp: crunch_simps) + end -interpretation Tcb_AI?: Tcb_AI - where Tcb_AI_dummy_const = Arch.Tcb_AI_dummy_const - proof goal_cases +context begin interpretation Arch . +requalify_consts is_cnode_or_valid_arch +end + +global_interpretation Tcb_AI?: Tcb_AI + where is_cnode_or_valid_arch = ARM.is_cnode_or_valid_arch + proof goal_cases interpret Arch . - case 1 show ?case by (intro_locales; (unfold_locales, fact Tcb_AI_asms)?) - qed + case 1 show ?case + by (unfold_locales; fact Tcb_AI_asms) +qed end \ No newline at end of file diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index f47cea92f..37bf53331 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -76,7 +76,7 @@ where "valid_invocation (Invocations_A.InvokeUntyped i) = valid_untyped_inv i" | "valid_invocation (Invocations_A.InvokeEndpoint w w2 b) = (ep_at w and ex_nonz_cap_to w)" | "valid_invocation (Invocations_A.InvokeNotification w w2) = (ntfn_at w and ex_nonz_cap_to w)" -| "valid_invocation (Invocations_A.InvokeTCB i) = tcb_inv_wf i" +| "valid_invocation (Invocations_A.InvokeTCB i) = Tcb_AI.tcb_inv_wf i" | "valid_invocation (Invocations_A.InvokeDomain thread domain) = (tcb_at thread and (\s. thread \ idle_thread s))" | "valid_invocation (Invocations_A.InvokeReply thread slot) = (tcb_at thread and cte_wp_at (op = (cap.ReplyCap thread False)) slot)" @@ -521,7 +521,7 @@ lemma decode_inv_wf[wp]: cong: cap.case_cong if_cong split del: split_if) apply (rule hoare_pre) - apply (wp decode_tcb_inv_wf decode_domain_inv_wf[simplified split_def] | wpc | + apply (wp Tcb_AI.decode_tcb_inv_wf decode_domain_inv_wf[simplified split_def] | wpc | simp add: o_def uncurry_def split_def del: is_cnode_cap.simps cte_refs.simps)+ apply (strengthen cnode_diminished_strg) apply (clarsimp simp: valid_cap_def cte_wp_at_eq_simp is_cap_simps diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 5103eb219..f3377d526 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -12,13 +12,23 @@ theory Tcb_AI imports "./$L4V_ARCH/ArchCNodeInv_AI" begin -locale Tcb_AI begin - -extend_locale - fixes Tcb_AI_dummy_const :: nat - assumes Tcb_AI_trivial_asm: "Tcb_AI_dummy_const > 0" - -end +locale Tcb_AI_1 = + fixes state_ext_t :: "('state_ext::state_ext) itself" + fixes is_cnode_or_valid_arch :: "cap \ bool" + assumes activate_idle_invs: + "\thread. \(invs::'state_ext state \ bool) and ct_idle\ + arch_activate_idle_thread thread + \\rv. invs and ct_idle\" + assumes empty_fail_getRegister [intro!, simp]: + "\r. empty_fail (getRegister r)" + assumes same_object_obj_refs: + "\cap cap'. \ same_object_as cap cap' \ + \ obj_refs cap = obj_refs cap'" + assumes finalise_cap_not_cte_wp_at: + "\P cap fin. P cap.NullCap \ \\(s::'state_ext state). \cp \ ran (caps_of_state s). P cp\ + finalise_cap cap fin \\rv s. \cp \ ran (caps_of_state s). P cp\" + assumes table_cap_ref_max_free_index_upd[simp]: (* reodered to resolve dependency in tc_invs *) + "\cap. table_cap_ref (max_free_index_update cap) = table_cap_ref cap" lemma ct_in_state_weaken: "\ ct_in_state Q s; \st. Q st \ P st \ \ ct_in_state P s" @@ -36,16 +46,8 @@ lemma set_thread_state_ct_st: apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def) done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma activate_idle_invs: - "\invs and ct_idle\ - arch_activate_idle_thread thread - \\rv. invs and ct_idle\" - by (simp add: arch_activate_idle_thread_def) -end - -lemma activate_invs: - "\invs\ activate_thread \\rv s. invs s \ (ct_running s \ ct_idle s)\" +lemma (in Tcb_AI_1) activate_invs: + "\(invs::'state_ext::state_ext state \ bool)\ activate_thread \\rv s. invs s \ (ct_running s \ ct_idle s)\" apply (unfold activate_thread_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_seq_ext [OF _ gts_sp]) @@ -87,7 +89,6 @@ lemma setup_reply_master_reply_master[wp]: apply (auto simp: cte_wp_at_caps_of_state is_cap_simps) done - lemma setup_reply_master_has_reply[wp]: "\\s. P (has_reply_cap t s)\ setup_reply_master t' \\rv s. P (has_reply_cap t s)\" apply (simp add: has_reply_cap_def cte_wp_at_caps_of_state @@ -98,7 +99,6 @@ lemma setup_reply_master_has_reply[wp]: apply auto done - lemma setup_reply_master_nonz_cap[wp]: "\ex_nonz_cap_to p\ setup_reply_master t \\rv. ex_nonz_cap_to p\" apply (simp add: setup_reply_master_def ex_nonz_cap_to_def cte_wp_at_caps_of_state) @@ -108,7 +108,6 @@ lemma setup_reply_master_nonz_cap[wp]: apply clarsimp done - lemma restart_invs[wp]: "\invs and tcb_at t and ex_nonz_cap_to t\ restart t \\rv. invs\" apply (simp add: restart_def) @@ -147,12 +146,6 @@ lemma copyAreaToRegs_tcb'[wp]: "\tcb_at t\ copyAreaToRegs regs a b \\rv. tcb_at t\" by (simp add: tcb_at_typ, wp copyAreaToRegs_typ_at) -context begin interpretation Arch . (*FIXME: arch_split*) -lemma empty_fail_getRegister [intro!, simp]: - "empty_fail (getRegister r)" - by (simp add: getRegister_def) -end - lemma copyRegsToArea_typ_at: "\\s. P (typ_at T p s)\ copyRegsToArea regs a b \\rv s. P (typ_at T p s)\" apply (simp add: copyRegsToArea_def) @@ -406,21 +399,6 @@ lemma out_cte_wp_at_trivialT: done -context Arch begin global_naming ARM (*FIXME: arch_split*) -lemma same_object_also_valid: - "\ same_object_as cap cap'; s \ cap'; wellformed_cap cap; - cap_asid cap = None \ (\asid. cap_asid cap = Some asid \ 0 < asid \ asid \ 2^asid_bits - 1); - cap_vptr cap = None; cap_asid_base cap = None \ - \ s \ cap" - apply (cases cap, - (clarsimp simp: same_object_as_def is_cap_simps cap_asid_def - wellformed_cap_def wellformed_acap_def - valid_cap_def bits_of_def cap_aligned_def - split: cap.split_asm arch_cap.split_asm option.splits)+) - done -end - - lemma same_object_as_cte_refs: "\ same_object_as cap cap' \ \ cte_refs cap' = cte_refs cap" @@ -436,17 +414,6 @@ lemma same_object_untyped_range: by (cases cap, (clarsimp simp: same_object_as_def is_cap_simps)+) -context begin interpretation Arch . (*FIXME: arch_split*) -lemma same_object_obj_refs: - "\ same_object_as cap cap' \ - \ obj_refs cap = obj_refs cap'" - apply (cases cap, simp_all add: same_object_as_def) - apply ((clarsimp simp: is_cap_simps bits_of_def - split: cap.split_asm )+) - by (cases "the_arch_cap cap"; cases "the_arch_cap cap'"; simp) -end - - lemma same_object_zombies: "\ same_object_as cap cap' \ \ is_zombie cap = is_zombie cap'" @@ -463,18 +430,6 @@ lemma zombies_final_helperE: apply (fastforce simp: cte_wp_at_caps_of_state) done - -context Arch begin global_naming ARM (*FIXME: arch_split*) -definition - is_cnode_or_valid_arch :: "cap \ bool" -where - "is_cnode_or_valid_arch cap \ - is_cnode_cap cap - \ (is_arch_cap cap - \ (is_pt_cap cap \ cap_asid cap \ None) - \ (is_pd_cap cap \ cap_asid cap \ None))" -end - lemma cap_badge_none_master: "(cap_badge (cap_master_cap cap) = None) = (cap_badge cap = None)" @@ -488,88 +443,6 @@ lemma cap_master_eq_badge_none: apply (simp add: cap_badge_none_master) done -context Arch begin global_naming ARM (*FIXME: arch_split*) - -definition - "pt_pd_asid cap \ case cap of - ArchObjectCap (PageTableCap _ (Some (asid, _))) \ Some asid - | ArchObjectCap (PageDirectoryCap _ (Some asid)) \ Some asid - | _ \ None" - -lemmas pt_pd_asid_simps [simp] = - pt_pd_asid_def [split_simps cap.split arch_cap.split option.split prod.split] - -lemma checked_insert_is_derived: - "\ same_object_as new_cap old_cap; is_cnode_or_valid_arch new_cap; - obj_refs new_cap = obj_refs old_cap - \ table_cap_ref old_cap = table_cap_ref new_cap - \ pt_pd_asid old_cap = pt_pd_asid new_cap\ - \ is_derived m slot new_cap old_cap" - apply (cases slot) - apply (frule same_object_as_cap_master) - apply (frule master_cap_obj_refs) - apply (frule cap_master_eq_badge_none) - apply (frule same_master_cap_same_types) - apply (simp add: is_derived_def) - apply clarsimp - apply (auto simp: is_cap_simps cap_master_cap_def - is_cnode_or_valid_arch_def vs_cap_ref_def - table_cap_ref_def pt_pd_asid_def up_ucast_inj_eq - split: cap.split_asm arch_cap.split_asm - option.split_asm)[1] - done - -lemma is_cnode_or_valid_arch_cap_asid: - "is_cnode_or_valid_arch cap - \ (is_pt_cap cap \ cap_asid cap \ None) - \ (is_pd_cap cap \ cap_asid cap \ None)" - by (auto simp add: is_cnode_or_valid_arch_def - is_cap_simps) - -lemma checked_insert_tcb_invs[wp]: - "\invs and cte_wp_at (\c. c = cap.NullCap) (target, ref) - and K (is_cnode_or_valid_arch new_cap) and valid_cap new_cap - and tcb_cap_valid new_cap (target, ref) - and K (is_pt_cap new_cap \ is_pd_cap new_cap - \ cap_asid new_cap \ None) - and (cte_wp_at (\c. obj_refs c = obj_refs new_cap - \ table_cap_ref c = table_cap_ref new_cap \ - pt_pd_asid c = pt_pd_asid new_cap) src_slot)\ - check_cap_at new_cap src_slot - (check_cap_at (cap.ThreadCap target) slot - (cap_insert new_cap src_slot (target, ref))) \\rv. invs\" - apply (simp add: check_cap_at_def) - apply (rule hoare_pre) - apply (wp get_cap_wp) - apply (clarsimp simp: cte_wp_at_caps_of_state) - apply (frule caps_of_state_valid_cap[where p=src_slot], fastforce) - apply (frule caps_of_state_valid_cap[where p=slot], fastforce) - apply (rule conjI, simp only: ex_cte_cap_wp_to_def) - apply (rule_tac x=slot in exI) - apply (clarsimp simp: cte_wp_at_caps_of_state same_object_as_cte_refs) - apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps - dest!: cap_master_cap_eqDs) - apply (clarsimp simp: valid_cap_def[where c="cap.ThreadCap x" for x]) - apply (erule cte_wp_atE[OF caps_of_state_cteD]) - apply (fastforce simp: obj_at_def is_obj_defs) - apply clarsimp - apply (rule conjI) - apply clarsimp - apply (subgoal_tac "\ is_zombie new_cap") - apply (simp add: same_object_zombies same_object_obj_refs) - apply (erule(2) zombies_final_helperE) - apply fastforce - apply (fastforce simp add: cte_wp_at_caps_of_state) - apply assumption - apply (clarsimp simp: is_cnode_or_valid_arch_def is_cap_simps - is_valid_vtable_root_def) - apply (rule conjI) - apply (erule(1) checked_insert_is_derived, simp+) - apply (auto simp: is_cnode_or_valid_arch_def is_cap_simps) - done - -end - lemma check_cap_inv2: assumes x: "\P\ f \Q\" @@ -599,30 +472,13 @@ lemma thread_set_emptyable[wp]: crunch not_cte_wp_at[wp]: unbind_maybe_notification "\s. \cp\ran (caps_of_state s). P cp" (wp: thread_set_caps_of_state_trivial simp: tcb_cap_cases_def) -context begin interpretation Arch . (*FIXME: arch_split*) -lemma finalise_cap_not_cte_wp_at: - assumes x: "P cap.NullCap" - shows "\\s. \cp \ ran (caps_of_state s). P cp\ - finalise_cap cap fin - \\rv s. \cp \ ran (caps_of_state s). P cp\" - apply (cases cap, simp_all) - apply (wp suspend_caps_of_state hoare_vcg_all_lift - | simp - | rule impI - | rule hoare_drop_imps)+ - apply (clarsimp simp: ball_ran_eq x) - apply (wp delete_one_caps_of_state - | rule impI - | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+ - done -end -lemma rec_del_all_caps_in_range: +lemma (in Tcb_AI_1) rec_del_all_caps_in_range: assumes x: "P cap.NullCap" and y: "\x n zt. P (cap.ThreadCap x) \ P (cap.Zombie x zt n)" and z: "\x y gd n zt. P (cap.CNodeCap x y gd) \ P (cap.Zombie x zt n)" and w: "\x zt zt' n m. P (cap.Zombie x zt n) \ P (cap.Zombie x zt' m)" - shows "s \ \\s. \cp \ ran (caps_of_state s). P cp\ + shows "s \ \\(s::'state_ext state). \cp \ ran (caps_of_state s). P cp\ rec_del args \\rv s. \cp \ ran (caps_of_state s). P cp\, \\e s. \cp \ ran (caps_of_state s). P cp\" @@ -692,22 +548,6 @@ qed abbreviation "no_cap_to_obj_dr_emp cap \ no_cap_to_obj_with_diff_ref cap {}" -context Arch begin global_naming ARM (*FIXME: arch_split*) -lemma use_no_cap_to_obj_asid_strg: - "(cte_at p s \ no_cap_to_obj_dr_emp cap s \ valid_cap cap s \ invs s) - \ cte_wp_at (\c. obj_refs c = obj_refs cap - \ table_cap_ref c = table_cap_ref cap \ pt_pd_asid c = pt_pd_asid cap) p s" - apply (clarsimp simp: cte_wp_at_caps_of_state - no_cap_to_obj_with_diff_ref_def - simp del: split_paired_All) - apply (frule caps_of_state_valid_cap, fastforce) - apply (erule allE)+ - apply (erule (1) impE)+ - apply (simp add: table_cap_ref_def pt_pd_asid_def split: cap.splits arch_cap.splits option.splits prod.splits) - apply (fastforce simp: table_cap_ref_def valid_cap_simps elim!: asid_low_high_bits)+ - done -end - lemma no_cap_to_obj_with_diff_ref_ran_caps_form: "no_cap_to_obj_dr_emp cap = (\s. \cp \ ran (caps_of_state s). @@ -717,21 +557,56 @@ lemma no_cap_to_obj_with_diff_ref_ran_caps_form: apply auto done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma cap_delete_no_cap_to_obj_asid[wp]: - "\no_cap_to_obj_dr_emp cap\ +locale Tcb_AI = Tcb_AI_1 state_ext_t is_cnode_or_valid_arch + for state_ext_t :: "('state_ext::state_ext) itself" + and is_cnode_or_valid_arch :: "cap \ bool" + + assumes cap_delete_no_cap_to_obj_asid[wp]: + "\cap slot. \(no_cap_to_obj_dr_emp cap::'state_ext state \ bool)\ cap_delete slot \\rv. no_cap_to_obj_dr_emp cap\" - apply (simp add: cap_delete_def - no_cap_to_obj_with_diff_ref_ran_caps_form) - apply wp - apply simp - apply (rule use_spec) - apply (rule rec_del_all_caps_in_range) - apply (simp add: table_cap_ref_def[simplified, split_simps cap.split] - | rule obj_ref_none_no_asid)+ - done -end + assumes tc_invs: + "\a e f g b sl pr. \(invs::'state_ext state \ bool) and tcb_at a + and (case_option \ (valid_cap o fst) e) + and (case_option \ (valid_cap o fst) f) + and (case_option \ (case_option \ (valid_cap o fst) o snd) g) + and (case_option \ (cte_at o snd) e) + and (case_option \ (cte_at o snd) f) + and (case_option \ (case_option \ (cte_at o snd) o snd) g) + and (case_option \ (no_cap_to_obj_dr_emp o fst) e) + and (case_option \ (no_cap_to_obj_dr_emp o fst) f) + and (case_option \ (case_option \ (no_cap_to_obj_dr_emp o fst) o snd) g) + and K (case_option True (is_cnode_cap o fst) e) + and K (case_option True (is_valid_vtable_root o fst) f) + and K (case_option True (\v. case_option True + ((swp valid_ipc_buffer_cap (fst v) + and is_arch_cap and is_cnode_or_valid_arch) + o fst) (snd v)) g) + and K (case_option True (\bl. length bl = word_bits) b)\ + invoke_tcb (ThreadControl a sl b pr e f g) + \\rv. invs\" + assumes decode_set_ipc_inv[wp]: + "\P args cap slot excaps. \P::'state_ext state \ bool\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" + assumes update_cap_valid: + "\cap s capdata rs p. valid_cap cap (s::'state_ext state) \ + valid_cap (case capdata of + None \ cap_rights_update rs cap + | Some x \ update_cap_data p x + (cap_rights_update rs cap)) s" + assumes check_valid_ipc_buffer_wp: + "\cap vptr P. \\(s::'state_ext state). is_arch_cap cap \ is_cnode_or_valid_arch cap + \ valid_ipc_buffer_cap cap vptr + \ is_aligned vptr msg_align_bits + \ P s\ + check_valid_ipc_buffer vptr cap + \\rv. P\,-" + assumes derive_no_cap_asid[wp]: + "\cap S slot. \(no_cap_to_obj_with_diff_ref cap S)::'state_ext state \ bool\ + derive_cap slot cap + \\rv. no_cap_to_obj_with_diff_ref rv S\,-" + assumes no_cap_to_obj_with_diff_ref_update_cap_data: + "\c S s P x. no_cap_to_obj_with_diff_ref c S (s::'state_ext state) \ + no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" + lemma out_no_cap_to_trivial: "(\tcb v. \(getF, x)\ran tcb_cap_cases. getF (f v tcb) = getF tcb) @@ -754,13 +629,8 @@ lemma thread_set_no_cap_to_trivial: | simp)+ done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma table_cap_ref_max_free_index_upd[simp]: - "table_cap_ref (max_free_index_update cap) = table_cap_ref cap" - by (simp add:free_index_update_def table_cap_ref_def split:cap.splits) -end -lemma checked_insert_no_cap_to: +lemma (in Tcb_AI_1) checked_insert_no_cap_to: "\no_cap_to_obj_with_diff_ref c' {} and no_cap_to_obj_with_diff_ref a {}\ check_cap_at a b (check_cap_at c d (cap_insert a b e)) @@ -862,70 +732,8 @@ lemma thread_set_ipc_tcb_cap_valid: dest!: get_tcb_SomeD) done -context begin interpretation Arch . (*FIXME: arch_split*) - -lemma tc_invs: - "\invs and tcb_at a - and (case_option \ (valid_cap o fst) e) - and (case_option \ (valid_cap o fst) f) - and (case_option \ (case_option \ (valid_cap o fst) o snd) g) - and (case_option \ (cte_at o snd) e) - and (case_option \ (cte_at o snd) f) - and (case_option \ (case_option \ (cte_at o snd) o snd) g) - and (case_option \ (no_cap_to_obj_dr_emp o fst) e) - and (case_option \ (no_cap_to_obj_dr_emp o fst) f) - and (case_option \ (case_option \ (no_cap_to_obj_dr_emp o fst) o snd) g) - and K (case_option True (is_cnode_cap o fst) e) - and K (case_option True (is_valid_vtable_root o fst) f) - and K (case_option True (\v. case_option True - ((swp valid_ipc_buffer_cap (fst v) - and is_arch_cap and is_cnode_or_valid_arch) - o fst) (snd v)) g) - and K (case_option True (\bl. length bl = word_bits) b)\ - invoke_tcb (ThreadControl a sl b pr e f g) - \\rv. invs\" - apply (rule hoare_gen_asm)+ - apply (simp add: split_def cong: option.case_cong) - apply (rule hoare_vcg_precond_imp) - apply wp - apply ((simp only: simp_thms - | rule wp_split_const_if wp_split_const_if_R - hoare_vcg_all_lift_R - hoare_vcg_E_elim hoare_vcg_const_imp_lift_R - hoare_vcg_R_conj - | (wp out_invs_trivial case_option_wpE cap_delete_deletes - cap_delete_valid_cap cap_insert_valid_cap out_cte_at - cap_insert_cte_at cap_delete_cte_at out_valid_cap - hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R - thread_set_tcb_ipc_buffer_cap_cleared_invs - thread_set_invs_trivial[OF ball_tcb_cap_casesI] - hoare_vcg_all_lift thread_set_valid_cap out_emptyable - check_cap_inv [where P="valid_cap c" for c] - check_cap_inv [where P="tcb_cap_valid c p" for c p] - check_cap_inv[where P="cte_at p0" for p0] - check_cap_inv[where P="tcb_at p0" for p0] - thread_set_cte_at - thread_set_cte_wp_at_trivial[where Q="\x. x", OF ball_tcb_cap_casesI] - thread_set_no_cap_to_trivial[OF ball_tcb_cap_casesI] - checked_insert_no_cap_to - out_no_cap_to_trivial[OF ball_tcb_cap_casesI] - thread_set_ipc_tcb_cap_valid - static_imp_wp static_imp_conj_wp)[1] - | simp add: ran_tcb_cap_cases dom_tcb_cap_cases[simplified] - emptyable_def - del: hoare_True_E_R - | wpc - | strengthen use_no_cap_to_obj_asid_strg - tcb_cap_always_valid_strg[where p="tcb_cnode_index 0"] - tcb_cap_always_valid_strg[where p="tcb_cnode_index (Suc 0)"])+) - apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] - is_cap_simps is_valid_vtable_root_def - is_cnode_or_valid_arch_def tcb_cap_valid_def - invs_valid_objs cap_asid_def vs_cap_ref_def - split: option.split_asm - | rule conjI)+ - done +context Tcb_AI begin (* FIXME-NTFN *) primrec tcb_inv_wf :: "tcb_invocation \ 'z::state_ext state \ bool" @@ -1031,17 +839,17 @@ lemma bind_notification_invs: done -lemma tcbinv_invs: - "\invs and tcb_inv_wf ti\ +lemma (in Tcb_AI) tcbinv_invs: + "\(invs::('state_ext::state_ext) state\bool) and tcb_inv_wf ti\ invoke_tcb ti \\rv. invs\" apply (case_tac ti, simp_all only:) - apply ((wp writereg_invs readreg_invs copyreg_invs tc_invs + apply ((wp_trace writereg_invs readreg_invs copyreg_invs tc_invs | simp | clarsimp simp: invs_def valid_state_def valid_pspace_def dest!: idle_no_ex_cap split: option.split - | rule conjI)+)[6] + | rule conjI)+)[6] apply (rename_tac option) apply (case_tac option, simp_all) apply (rule hoare_pre) @@ -1050,7 +858,6 @@ lemma tcbinv_invs: apply clarsimp done - crunch typ_at[wp]: invoke_tcb "\s. P (typ_at T p s)" (ignore: check_cap_at setNextPC zipWithM wp: hoare_drop_imps mapM_x_wp' check_cap_inv @@ -1094,7 +901,7 @@ lemma decode_copyreg_inv: | wp_once | wpcw)+ done -lemma decode_readreg_wf: +lemma (in Tcb_AI) decode_readreg_wf: "\invs and tcb_at t and ex_nonz_cap_to t\ decode_read_registers args (cap.ThreadCap t) \tcb_inv_wf\,-" @@ -1105,7 +912,7 @@ lemma decode_readreg_wf: apply simp done -lemma decode_writereg_wf: +lemma (in Tcb_AI) decode_writereg_wf: "\invs and tcb_at t and ex_nonz_cap_to t\ decode_write_registers args (cap.ThreadCap t) \tcb_inv_wf\,-" @@ -1116,7 +923,7 @@ lemma decode_writereg_wf: apply simp done -lemma decode_copyreg_wf: +lemma (in Tcb_AI) decode_copyreg_wf: "\invs and tcb_at t and ex_nonz_cap_to t and (\s. \x \ set extras. s \ x \ (\y \ zobj_refs x. ex_nonz_cap_to y s))\ @@ -1137,7 +944,8 @@ lemma OR_choice_E_weak_wp: "\P\ f \ g \Q\invs and tcb_at t and ex_nonz_cap_to t\ decode_set_priority args (cap.ThreadCap t) slot \tcb_inv_wf\,-" apply (simp add: decode_set_priority_def split del: split_if) @@ -1185,34 +993,6 @@ lemma decode_set_priority_inv[wp]: apply simp done -context begin interpretation Arch . (*FIXME: arch_split*) - -lemma check_valid_ipc_buffer_inv: - "\P\ check_valid_ipc_buffer vptr cap \\rv. P\" - apply (simp add: check_valid_ipc_buffer_def whenE_def - cong: cap.case_cong arch_cap.case_cong - split del: split_if) - apply (rule hoare_pre) - apply (wp | simp split del: split_if | wpcw)+ - done - -lemma check_valid_ipc_buffer_wp: - "\\s. is_arch_cap cap \ is_cnode_or_valid_arch cap - \ valid_ipc_buffer_cap cap vptr - \ is_aligned vptr msg_align_bits - \ P s\ - check_valid_ipc_buffer vptr cap - \\rv. P\,-" - apply (simp add: check_valid_ipc_buffer_def whenE_def - cong: cap.case_cong arch_cap.case_cong - split del: split_if) - apply (rule hoare_pre) - apply (wp | simp split del: split_if | wpc)+ - apply (clarsimp simp: is_cap_simps is_cnode_or_valid_arch_def - valid_ipc_buffer_cap_def) - done - -end lemma derive_is_arch[wp]: "\\s. is_arch_cap c\ derive_cap slot c \\rv s. is_arch_cap rv\,-" @@ -1222,23 +1002,9 @@ lemma derive_is_arch[wp]: apply fastforce done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma derive_no_cap_asid[wp]: - "\no_cap_to_obj_with_diff_ref cap S\ - derive_cap slot cap - \\rv. no_cap_to_obj_with_diff_ref rv S\,-" - apply (simp add: derive_cap_def arch_derive_cap_def - cong: cap.case_cong) - apply (rule hoare_pre) - apply (wp | simp | wpc)+ - apply (auto simp add: no_cap_to_obj_with_diff_ref_Null, - auto simp add: no_cap_to_obj_with_diff_ref_def - table_cap_ref_def) - done -end -lemma decode_set_ipc_wf[wp]: - "\invs and tcb_at t and cte_at slot and ex_cte_cap_to slot +lemma (in Tcb_AI) decode_set_ipc_wf[wp]: + "\(invs::('state_ext::state_ext) state\bool) and tcb_at t and cte_at slot and ex_cte_cap_to slot and ex_nonz_cap_to t and (\s. \x \ set excaps. s \ fst x \ cte_at (snd x) s \ ex_cte_cap_to (snd x) s @@ -1254,7 +1020,6 @@ lemma decode_set_ipc_wf[wp]: apply (clarsimp simp: neq_Nil_conv) done - lemma decode_set_ipc_is_tc[wp]: "\\\ decode_set_ipc_buffer args cap slot excaps \\rv s. is_thread_control rv\,-" apply (rule hoare_pre) @@ -1265,16 +1030,6 @@ lemma decode_set_ipc_is_tc[wp]: done -lemma decode_set_ipc_inv[wp]: - "\P\ decode_set_ipc_buffer args cap slot excaps \\rv. P\" - apply (simp add: decode_set_ipc_buffer_def whenE_def - split_def - split del: split_if) - apply (rule hoare_pre, wp check_valid_ipc_buffer_inv) - apply simp - done - - lemma slot_long_running_inv[wp]: "\P\ slot_cap_long_running_delete ptr \\rv. P\" apply (simp add: slot_cap_long_running_delete_def) @@ -1288,26 +1043,10 @@ lemma val_le_length_Cons: apply (cases n, simp_all) done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma no_cap_to_obj_with_diff_ref_update_cap_data: - "no_cap_to_obj_with_diff_ref c S s \ - no_cap_to_obj_with_diff_ref (update_cap_data P x c) S s" - apply (case_tac "update_cap_data P x c = NullCap") - apply (simp add: no_cap_to_obj_with_diff_ref_Null) - apply (subgoal_tac "vs_cap_ref (update_cap_data P x c) - = vs_cap_ref c") - apply (simp add: no_cap_to_obj_with_diff_ref_def - update_cap_objrefs) - apply (clarsimp simp: update_cap_data_closedform - table_cap_ref_def - arch_update_cap_data_def - split: cap.split) - apply simp - done - -lemma decode_set_space_wf[wp]: - "\invs and tcb_at t and cte_at slot and ex_cte_cap_to slot +lemma (in Tcb_AI) decode_set_space_wf[wp]: + "\(invs::('state_ext::state_ext) state\bool) + and tcb_at t and cte_at slot and ex_cte_cap_to slot and ex_nonz_cap_to t and (\s. \x \ set extras. s \ fst x \ cte_at (snd x) s \ ex_cte_cap_to (snd x) s @@ -1319,7 +1058,7 @@ lemma decode_set_space_wf[wp]: split del: split_if) apply (rule hoare_pre) apply (wp derive_cap_valid_cap - | simp add: is_valid_vtable_root_def o_def + | simp add: ARM_A.is_valid_vtable_root_def o_def split del: split_if | rule hoare_drop_imps)+ apply (clarsimp split del: split_if simp: ball_conj_distrib @@ -1329,7 +1068,6 @@ lemma decode_set_space_wf[wp]: del: length_greater_0_conv) done -end lemma decode_set_space_inv[wp]: @@ -1363,8 +1101,9 @@ lemma boring_simp[simp]: "(if x then True else False) = x" by simp -lemma decode_tcb_conf_wf[wp]: - "\invs and tcb_at t and cte_at slot and ex_cte_cap_to slot +lemma (in Tcb_AI) decode_tcb_conf_wf[wp]: + "\(invs::('state_ext::state_ext) state\bool) + and tcb_at t and cte_at slot and ex_cte_cap_to slot and ex_nonz_cap_to t and (\s. \x \ set extras. s \ fst x \ cte_at (snd x) s \ ex_cte_cap_to (snd x) s @@ -1382,20 +1121,20 @@ lemma decode_tcb_conf_wf[wp]: in hoare_post_imp_R) apply wp apply (clarsimp simp: is_thread_control_def2 cong: option.case_cong) - apply (wp | simp add: whenE_def split del: split_if)+ + apply (wp_trace | simp add: whenE_def split del: split_if)+ apply (clarsimp simp: linorder_not_less val_le_length_Cons del: ballI) done - -lemma decode_tcb_conf_inv[wp]: - "\P\ decode_tcb_configure args cap slot extras \\rv. P\" +lemma (in Tcb_AI) decode_tcb_conf_inv[wp]: + "\P::'state_ext state \ bool\ decode_tcb_configure args cap slot extras \\rv. P\" apply (clarsimp simp add: decode_tcb_configure_def Let_def whenE_def split del: split_if) apply (rule hoare_pre, wp) apply simp done + lemmas derived_cap_valid = derive_cap_valid_cap lemma derived_cap_cnode_valid: @@ -1409,29 +1148,6 @@ lemma derived_cap_cnode_valid: apply (clarsimp simp add: liftME_def in_monad) done -context begin interpretation Arch . (*FIXME: arch_split*) -lemma update_cap_valid: - "valid_cap cap s \ - valid_cap (case capdata of - None \ cap_rights_update rs cap - | Some x \ update_cap_data p x - (cap_rights_update rs cap)) s" - apply (case_tac capdata, simp_all)[1] - apply (case_tac cap, - simp_all add: update_cap_data_def cap_rights_update_def - is_cap_defs Let_def split_def valid_cap_def - badge_update_def the_cnode_cap_def cap_aligned_def - arch_update_cap_data_def - split del: split_if) - apply (simp add: badge_update_def cap_rights_update_def) - apply (simp add: badge_update_def) - apply simp - apply (rename_tac arch_cap) - using valid_validate_vm_rights[simplified valid_vm_rights_def] - apply (case_tac arch_cap, simp_all add: acap_rights_update_def - split: option.splits prod.splits) - done -end crunch inv[wp]: decode_unbind_notification P (simp: whenE_def) @@ -1441,8 +1157,9 @@ lemma decode_bind_notification_inv[wp]: unfolding decode_bind_notification_def by (rule hoare_pre) (wp get_ntfn_wp gbn_wp | wpc | clarsimp simp: whenE_def split del: split_if)+ -lemma decode_tcb_inv_inv: - "\P\ decode_tcb_invocation label args (cap.ThreadCap t) slot extras \\rv. P\" + +lemma (in Tcb_AI) decode_tcb_inv_inv: + "\P::'state_ext state \ bool\ decode_tcb_invocation label args (cap.ThreadCap t) slot extras \\rv. P\" apply (simp add: decode_tcb_invocation_def Let_def cong: if_cong split del: split_if) @@ -1453,10 +1170,12 @@ lemma decode_tcb_inv_inv: apply simp done + lemma real_cte_at_not_tcb_at: "real_cte_at (x, y) s \ \ tcb_at x s" by (clarsimp simp: obj_at_def is_tcb is_cap_table) +context Tcb_AI begin lemma decode_bind_notification_wf: "\invs and tcb_at t and ex_nonz_cap_to t and (\s. \x \ set extras. s \ (fst x) \ (\y \ zobj_refs (fst x). ex_nonz_cap_to y s))\ @@ -1485,22 +1204,23 @@ lemma decode_unbind_notification_wf: lemma decode_tcb_inv_wf: "\invs and tcb_at t and ex_nonz_cap_to t and cte_at slot and ex_cte_cap_to slot - and (\s. \x \ set extras. real_cte_at (snd x) s \ s \ fst x + and (\(s::'state_ext::state_ext state). \x \ set extras. real_cte_at (snd x) s \ s \ fst x \ ex_cte_cap_to (snd x) s \ (\y \ zobj_refs (fst x). ex_nonz_cap_to y s) \ no_cap_to_obj_dr_emp (fst x) s)\ decode_tcb_invocation label args (cap.ThreadCap t) slot extras \tcb_inv_wf\,-" - apply (simp add: decode_tcb_invocation_def Let_def + apply (simp add: decode_tcb_invocation_def Let_def del: tcb_inv_wf_def cong: if_cong split del: split_if) apply (rule hoare_vcg_precond_impE_R) apply wpc - apply (wp decode_tcb_conf_wf decode_readreg_wf + apply (wp_trace decode_tcb_conf_wf decode_readreg_wf decode_writereg_wf decode_copyreg_wf decode_bind_notification_wf decode_unbind_notification_wf) apply (clarsimp simp: real_cte_at_cte) apply (fastforce simp: real_cte_at_not_tcb_at) done +end lemma out_pred_tcb_at_preserved: "\ \tcb x. tcb_state (f x tcb) = tcb_state tcb \ \ @@ -1514,10 +1234,12 @@ lemma pred_tcb_at_arch_state[simp]: "pred_tcb_at proj P t (arch_state_update f s) = pred_tcb_at proj P t s" by (simp add: pred_tcb_at_def obj_at_def) +(* context begin interpretation Arch . (*FIXME: arch_split*) -crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t" +crunch pred_tcb_at: arch_switch_to_thread "pred_tcb_at proj P t" (wp: crunch_wps simp: crunch_simps) end +*) lemma invoke_domain_invs: "\invs\ @@ -1551,6 +1273,7 @@ lemma decode_domain_inv_wf: apply (erule ballE[where x="hd excs"]) apply simp+ done + lemma tcb_bound_refs_no_NTFNBound: "(x, NTFNBound) \ tcb_bound_refs a" by (simp add: tcb_bound_refs_def split: option.splits) @@ -1602,5 +1325,4 @@ lemma unbind_notification_sym_refs[wp]: intro!: ntfn_q_refs_no_NTFNBound) done - end diff --git a/proof/refine/Tcb_R.thy b/proof/refine/Tcb_R.thy index 91ff8e387..1c3fc1898 100644 --- a/proof/refine/Tcb_R.thy +++ b/proof/refine/Tcb_R.thy @@ -1485,7 +1485,7 @@ where lemma tcbinv_corres: "tcbinv_relation ti ti' \ corres (intr \ op =) - (einvs and simple_sched_action and tcb_inv_wf ti) + (einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti) (invs' and sch_act_simple and tcb_inv_wf' ti') (invoke_tcb ti) (invokeTCB ti')" apply (case_tac ti, simp_all only: tcbinv_relation.simps valid_tcb_invocation_def)