From 99e993f2a8ceacf9cf84d601e9767d0aa115a960 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 19 Jul 2022 16:05:24 +1000 Subject: [PATCH] rt riscv ainvs: set handler params when configuring TCBs This updates ainvs after modifying the tcb_decode functions so that it is possible to set the badge and rights of fault and timeout handler caps. Signed-off-by: Corey Lewis --- proof/invariant-abstract/CSpace_AI.thy | 2 +- .../DetSchedSchedule_AI.thy | 36 ++-- .../invariant-abstract/RISCV64/ArchTcb_AI.thy | 59 +++--- proof/invariant-abstract/Tcb_AI.thy | 177 ++++++++++++++++-- 4 files changed, 212 insertions(+), 62 deletions(-) diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index cef79646ca..a3b1ed8d36 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -3837,7 +3837,7 @@ locale CSpace_AI "\rs cap. obj_refs (mask_cap rs cap) = obj_refs cap" assumes mask_cap_zobjrefs[simp]: "\rs cap. zobj_refs (mask_cap rs cap) = zobj_refs cap" - assumes derive_cap_valid_cap: + assumes derive_cap_valid_cap[wp]: "\cap slot. \valid_cap cap :: 'state_ext state \ bool\ derive_cap slot cap \valid_cap\,-" assumes valid_cap_update_rights[simp]: diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 411ca1ad5e..c492760079 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -7722,7 +7722,7 @@ method invoke_tcb_install_tcb_cap_helper uses wp = ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift install_tcb_cap_invs static_imp_wp static_imp_conj_wp wp | strengthen tcb_cap_always_valid_strg - | wp install_tcb_cap_cte_wp_at_ep)+)[1]) + | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1]) crunches restart_thread_if_no_fault for budget_sufficient[wp]: "budget_sufficient tp" @@ -7871,9 +7871,9 @@ lemma tcc_valid_sched: apply (intro conjI impI; clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte dest!: is_valid_vtable_root_is_arch_cap) - apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) + apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) - by auto + by (auto simp: is_cap_simps dest: is_derived_ep_cap) lemma restart_thread_if_no_fault_ct_in_state_neq: "\ct_in_state P and (\s. t \ cur_thread s \ (P Inactive \ P Restart))\ @@ -17205,9 +17205,9 @@ lemma tcc_cur_sc_chargeable: apply (intro conjI impI; clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte dest!: is_valid_vtable_root_is_arch_cap) - apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) - apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) - by auto + apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) + apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) + by (auto simp: is_cap_simps dest: is_derived_ep_cap) crunches maybe_sched_context_unbind_tcb, maybe_sched_context_bind_tcb, set_priority , bind_notification @@ -20616,9 +20616,9 @@ lemma tcc_ct_not_queued: apply (intro conjI impI; clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte dest!: is_valid_vtable_root_is_arch_cap) - apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) + apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) - by auto + by (auto simp: is_cap_simps dest: is_derived_ep_cap) lemma invoke_tcb_ct_not_queuedE_E[wp]: "\ct_not_queued and invs and scheduler_act_sane and ct_not_blocked and tcb_inv_wf iv\ @@ -25471,16 +25471,16 @@ lemma invoke_tcb_ct_ready_if_schedulable[wp]: apply wpsimp apply wpsimp apply invoke_tcb_install_tcb_cap_helper+ - apply simp - apply (strengthen tcb_cap_valid_ep_strgs) - apply (clarsimp cong: conj_cong) - apply (intro conjI impI; - clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats - real_cte_at_cte ct_in_state_def - dest!: is_valid_vtable_root_is_arch_cap) - apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) - apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) - by auto + apply simp + apply (strengthen tcb_cap_valid_ep_strgs) + apply (clarsimp cong: conj_cong) + apply (intro conjI impI; + clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats + real_cte_at_cte ct_in_state_def + dest!: is_valid_vtable_root_is_arch_cap) + apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state valid_fault_handler_def\) + apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) + by (auto simp: is_cap_simps dest: is_derived_ep_cap) subgoal for target slot fault_handler mcp priority sc apply (rule_tac Q="\_ s. released_if_bound_sc_tcb_at (cur_thread s) s" in hoare_strengthen_post[rotated]) apply (clarsimp simp: ct_ready_if_schedulable_def vs_all_heap_simps) diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index 54dbda2f28..bbaca00a15 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -93,7 +93,7 @@ lemma checked_insert_tcb_invs: (* arch specific *) and valid_cap new_cap and tcb_cap_valid new_cap (target, ref) and (\s. valid_fault_handler new_cap - \ cte_wp_at (\c. c = new_cap \ c = NullCap) src_slot s) + \ cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) and (cte_wp_at (\c. obj_refs c = obj_refs new_cap \ table_cap_ref c = table_cap_ref new_cap \ vspace_asid c = vspace_asid new_cap) src_slot)\ @@ -128,7 +128,7 @@ lemma checked_insert_tcb_invs: (* arch specific *) apply (rule conjI) apply (erule disjE) apply (erule(1) checked_insert_is_derived, simp+) - apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def) + apply (auto simp: is_cnode_or_valid_arch_def is_derived_def is_cap_simps valid_fault_handler_def) done lemma checked_insert_tcb_invs': (* arch specific *) @@ -240,26 +240,26 @@ lemma install_tcb_cap_invs: "\invs and tcb_at target and (\s. \new_cap src_slot. slot_opt = Some (new_cap, src_slot) - \ K (is_cnode_or_valid_arch new_cap \ - valid_fault_handler new_cap) s + \ K (is_cnode_or_valid_arch new_cap \ valid_fault_handler new_cap) s \ valid_cap new_cap s \ tcb_cap_valid new_cap (target, tcb_cnode_index n) s \ (valid_fault_handler new_cap - \ cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s - \ cte_wp_at (\c. c = new_cap \ c = NullCap) src_slot s) + \ cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s) + \ (is_ep_cap new_cap \ cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) \ (case tcb_cap_cases (tcb_cnode_index n) of None \ True | Some (getF, setF, restr) \ \st. restr target st new_cap) \ (tcb_cnode_index n = tcb_cnode_index 2 \ (\ptr. valid_ipc_buffer_cap new_cap ptr)) \ real_cte_at src_slot s \ no_cap_to_obj_dr_emp new_cap s)\ install_tcb_cap target slot n slot_opt \\_. invs\" - apply (simp add: install_tcb_cap_def) + unfolding install_tcb_cap_def apply (wpsimp wp: checked_insert_tcb_invs cap_delete_deletes hoare_vcg_imp_lift_R | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wpsimp wp: cap_delete_ep)+ + | wpsimp wp: cap_delete_is_derived_ep)+ by (auto simp: typ_at_eq_kheap_obj cap_table_at_typ tcb_at_typ is_cnode_or_valid_arch_def is_cap_simps real_cte_at_cte - elim!: cte_wp_at_weakenE) + valid_fault_handler_def + elim!: notE[OF _ cte_wp_at_weakenE] is_derived_ep_cap) lemma install_tcb_cap_no_cap_to_obj_dr_emp[wp, Tcb_AI_asms]: "\no_cap_to_obj_dr_emp cap and @@ -296,15 +296,16 @@ lemma install_tcb_frame_cap_invs: \ \non-exception case\ apply wpsimp apply (wpsimp wp: checked_insert_tcb_invs[where ref="tcb_cnode_index 2"]) - apply (wpsimp wp: hoare_vcg_all_lift static_imp_wp - thread_set_tcb_ipc_buffer_cap_cleared_invs - thread_set_cte_wp_at_trivial[where Q="\x. x", OF ball_tcb_cap_casesI] - thread_set_ipc_tcb_cap_valid) + apply ((wpsimp wp: hoare_vcg_all_lift static_imp_wp + thread_set_tcb_ipc_buffer_cap_cleared_invs + thread_set_cte_wp_at_trivial[where Q="\x. x", OF ball_tcb_cap_casesI] + thread_set_ipc_tcb_cap_valid + | wps)+)[1] apply((wpsimp wp: cap_delete_deletes hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift static_imp_wp static_imp_conj_wp | strengthen use_no_cap_to_obj_asid_strg - | wp cap_delete_ep)+)[1] + | wp cap_delete_is_derived_ep)+)[1] by (clarsimp simp: is_cap_simps' valid_fault_handler_def is_cnode_or_valid_arch_def) lemma tcc_invs[Tcb_AI_asms]: @@ -331,21 +332,21 @@ lemma tcc_invs[Tcb_AI_asms]: apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R install_tcb_cap_invs | strengthen tcb_cap_always_valid_strg - | wp install_tcb_cap_cte_wp_at_ep)+)[1] + | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1] \ \install_tcb_cap 4\ apply (simp) apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs) apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R install_tcb_cap_invs | strengthen tcb_cap_always_valid_strg - | wp install_tcb_cap_cte_wp_at_ep)+)[1] + | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1] \ \install_tcb_cap 3\ apply (simp) apply (rule hoare_vcg_E_elim, wp install_tcb_cap_invs) apply ((wpsimp wp: hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R install_tcb_cap_invs | strengthen tcb_cap_always_valid_strg - | wp install_tcb_cap_cte_wp_at_ep)+)[1] + | wp install_tcb_cap_cte_wp_at_ep install_tcb_cap_is_derived_ep)+)[1] \ \cleanup\ apply (simp) apply (strengthen tcb_cap_always_valid_strg) @@ -354,9 +355,10 @@ lemma tcc_invs[Tcb_AI_asms]: apply (intro conjI impI; clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte dest!: is_valid_vtable_root_is_arch_cap) - apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\) + apply (all \clarsimp simp: is_cap_simps cte_wp_at_caps_of_state\) apply (all \clarsimp simp: obj_at_def is_tcb typ_at_eq_kheap_obj cap_table_at_typ\) - by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def) + by (auto simp: valid_ipc_buffer_cap valid_fault_handler_def is_cap_simps + dest: is_derived_ep_cap) crunches empty_slot for sc_tcb_sc_at[wp]: "sc_tcb_sc_at P target" @@ -396,7 +398,6 @@ lemma tcs_invs[Tcb_AI_asms]: apply (intro conjI impI; (clarsimp simp: is_cnode_or_valid_arch_is_cap_simps tcb_ep_slot_cte_wp_ats real_cte_at_cte dest!: is_valid_vtable_root_is_arch_cap)?) - apply (erule cte_wp_at_strengthen, simp) apply (clarsimp simp: obj_at_def is_ep is_tcb) apply (intro conjI; intro allI impI) apply (clarsimp simp: pred_tcb_at_def obj_at_def is_tcb) @@ -466,10 +467,20 @@ lemma no_cap_to_obj_with_diff_ref_update_cap_data[Tcb_AI_asms]: = 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 (clarsimp simp: update_cap_data_closedform + split: cap.split) + apply simp + done + +lemma no_cap_to_obj_with_diff_ref_mask_cap[Tcb_AI_asms]: + "no_cap_to_obj_with_diff_ref c S s \ + no_cap_to_obj_with_diff_ref (mask_cap R c) S s" + apply (case_tac "mask_cap R c = NullCap") + apply (simp add: no_cap_to_obj_with_diff_ref_Null del: mask_cap_Null) + apply (subgoal_tac "vs_cap_ref (mask_cap R c) = vs_cap_ref c") + apply (simp add: no_cap_to_obj_with_diff_ref_def) + apply (clarsimp simp: mask_cap_def cap_rights_update_def acap_rights_update_def + split: cap.split arch_cap.split) apply simp done diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 138887471d..e8b22ae1b0 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -12,7 +12,7 @@ context begin interpretation Arch . requalify_facts arch_derive_is_arch rec_del_invs'' - as_user_valid_tcbs + as_user_valid_tcbs is_derived_arch_non_arch end @@ -558,12 +558,16 @@ where and case_option \ ((real_cte_at And ex_cte_cap_to) \ snd) vroot and case_option \ (valid_cap \ fst) fh and K (case_option True (valid_fault_handler o fst) fh) - and case_option \ (\(cap, slot). cte_wp_at ((=) cap) slot) fh + and (case_option \ (\(cap, slot) s. + cap \ NullCap \ + cte_wp_at (is_derived (cdt s) slot cap) slot s) fh) and case_option \ (no_cap_to_obj_dr_emp \ fst) fh and case_option \ ((real_cte_at And ex_cte_cap_to) \ snd) fh and case_option \ (valid_cap \ fst) th and K (case_option True (valid_fault_handler o fst) th) - and case_option \ (\(cap, slot). cte_wp_at ((=) cap) slot) th + and (case_option \ (\(cap, slot) s. + cap \ NullCap \ + cte_wp_at (is_derived (cdt s) slot cap) slot s) th) and case_option \ (no_cap_to_obj_dr_emp \ fst) th and case_option \ ((real_cte_at And ex_cte_cap_to) \ snd) th and (case_option \ (case_option \ (valid_cap o fst) o snd) buf) @@ -582,7 +586,9 @@ where = (tcb_at t and case_option \ (valid_cap \ fst) fh and K (case_option True (valid_fault_handler o fst) fh) - and case_option \ (\(cap, slot). cte_wp_at ((=) cap) slot) fh + and (case_option \ (\(cap, slot) s. + cap \ NullCap \ + cte_wp_at (is_derived (cdt s) slot cap) slot s) fh) and case_option \ (no_cap_to_obj_dr_emp \ fst) fh and case_option \ ((real_cte_at And ex_cte_cap_to) \ snd) fh and case_option \ @@ -687,6 +693,9 @@ locale Tcb_AI = Tcb_AI_1 state_ext_t is_cnode_or_valid_arch 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" + assumes no_cap_to_obj_with_diff_ref_mask_cap: + "\c S R s. no_cap_to_obj_with_diff_ref c S (s::'state_ext state) \ + no_cap_to_obj_with_diff_ref (mask_cap R c) S s" lemma out_no_cap_to_trivial: @@ -893,6 +902,58 @@ lemma cap_delete_ep: apply (simp add: cte_wp_at_caps_of_state valid_fault_handler_def) done +lemma is_derived_ep_cap: + "is_derived m p (EndpointCap r badge rights) cap \ is_ep_cap cap" + unfolding is_derived_def + by (auto simp: is_cap_simps cap_master_cap_def split: cap.splits if_splits) + +lemma is_derived_ep_cap_rewrite: + "is_ep_cap cap' \ + is_derived m p cap' cap = + (cap_master_cap cap = cap_master_cap cap' \ + (cap_badge cap, cap_badge cap') \ capBadge_ordering False)" + unfolding is_derived_def + by (cases cap; cases cap'; + clarsimp simp: is_zombie_def cap_master_cap_def is_derived_arch_non_arch is_cap_simps) + +crunches cancel_all_ipc + for cdt[wp]: "\s. P (cdt s)" + (wp: crunch_wps) + +lemma finalise_cap_is_derived_ep: + "\(\s. cte_wp_at (is_derived (cdt s) p new_cap) p s) and + K (is_ep_cap cap)\ + finalise_cap cap is_final + \\rv s. cte_wp_at (is_derived (cdt s) p new_cap) p s \ fst rv = NullCap\" + apply (rule hoare_gen_asm, clarsimp simp: is_cap_simps) + by (wpsimp simp: comp_def | wps)+ + +lemma cap_delete_is_derived_ep: + "\(\s. cte_wp_at (is_derived (cdt s) p new_cap) p s) and + cte_wp_at valid_fault_handler slot and + cte_wp_at is_ep_cap p and + K (slot \ p \ is_ep_cap new_cap)\ + cap_delete slot + \\_ s. cte_wp_at (is_derived (cdt s) p new_cap) p s\, -" + apply (rule hoare_gen_asmE; clarsimp) + apply (rule hoare_post_imp_R[rotated]) + apply (rule cte_wp_at_weakenE[rotated]) + apply (subst is_derived_ep_cap_rewrite; clarsimp) + apply simp + apply simp + apply (simp add: cap_delete_def rec_del_CTEDeleteCall) + apply (subst rec_del_FinaliseSlot) + apply (simp cong: if_cong) + apply (wp empty_slot_cte_wp_elsewhere|wpc)+ + apply (rule hoare_FalseE_R) (* `else` case will not be taken *) + apply wpsimp+ + apply (rule hoare_strengthen_post, rule finalise_cap_is_derived_ep[where p=p and new_cap=new_cap]) + apply (clarsimp simp: cte_wp_at_def is_derived_ep_cap_rewrite) + apply (wpsimp wp: get_cap_wp)+ + apply (clarsimp simp: cte_wp_at_caps_of_state valid_fault_handler_def + is_derived_ep_cap_rewrite) + done + lemma cap_delete_deletes_fh: "\\s. p \ ptr \ cte_wp_at valid_fault_handler ptr s \ cte_wp_at (\c. P c \ c = cap.NullCap) p s\ @@ -928,6 +989,24 @@ lemma install_tcb_cap_cte_wp_at_ep: apply (simp add: install_tcb_cap_def) by (wpsimp wp: checked_insert_cte_wp_at_weak cap_delete_ep hoare_vcg_const_imp_lift_R) +lemma install_tcb_cap_is_derived_ep: + "\(\s. cte_wp_at (is_derived (cdt s) p new_cap) p s) and + cte_wp_at valid_fault_handler (target, tcb_cnode_index n) and + cte_wp_at is_ep_cap p and + K ((target, tcb_cnode_index n) \ p \ is_ep_cap new_cap)\ + install_tcb_cap target slot n slot_opt + \\_ s. cte_wp_at (is_derived (cdt s) p new_cap) p s\, -" + apply (rule hoare_gen_asmE; clarsimp) + apply (rule hoare_post_imp_R[rotated]) + apply (rule cte_wp_at_weakenE[rotated]) + apply (subst is_derived_ep_cap_rewrite; clarsimp) + apply simp + apply simp + apply (wpsimp wp: install_tcb_cap_cte_wp_at_ep) + apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_ep_cap_rewrite + is_cap_simps cap_master_cap_def) + done + lemma tcb_ep_slot_cte_wp_at: "\ invs s; tcb_at t s; slot = 3 \ slot = 4 \ \ cte_wp_at valid_fault_handler (t, tcb_cnode_index slot) s" @@ -1206,13 +1285,60 @@ lemma (in Tcb_AI) decode_set_mcpriority_wf[wp]: by (wpsimp simp: decode_set_mcpriority_def wp: check_prio_wp_weak whenE_throwError_wp) lemma check_handler_ep_inv[wp]: - "\P\ check_handler_ep n cap_slot \\_. P\" + "check_handler_ep n cap_slot \P\" unfolding check_handler_ep_def unlessE_def by wpsimp lemma check_handler_ep_wpE[wp]: - "\\s. valid_fault_handler (fst cap_slot) \ P cap_slot s\ check_handler_ep n cap_slot \P\, -" + "\\s. valid_fault_handler (fst cap_slot) \ P cap_slot s\ + check_handler_ep n cap_slot + \P\, -" unfolding check_handler_ep_def unlessE_def by wpsimp +lemma update_and_check_handler_ep_inv[wp]: + "update_and_check_handler_ep args pos excaps \P\" + unfolding update_and_check_handler_ep_def + by (wpsimp wp: hoare_drop_imps) + +lemma update_and_check_handler_ep_snd[wp]: + "\P (snd (excaps ! 0))\ + update_and_check_handler_ep args pos excaps + \\rv. P (snd rv)\,-" + unfolding update_and_check_handler_ep_def + by (wpsimp wp: hoare_drop_imps) + +lemma update_and_check_handler_ep_valid_cap[wp]: + "\\s. (\x \ set fh_caps. s \ fst x) + \ (2 \ length args \ 0 < length fh_caps)\ + update_and_check_handler_ep args pos fh_caps + \\rv. valid_cap (fst rv)\,-" + unfolding update_and_check_handler_ep_def + apply (wpsimp wp: hoare_drop_imps) + by (auto simp: update_handler_ep_def update_cap_data_validI) + +lemma update_and_check_handler_ep_valid_fault_handler[wp]: + "\\\ + update_and_check_handler_ep args pos fh_caps + \\rv s. valid_fault_handler (fst rv)\,-" + unfolding update_and_check_handler_ep_def + by (wpsimp wp: derive_cap_is_derived_foo) + +lemma update_and_check_handler_ep_is_derived[wp]: + "\\s. valid_objs s \ + (\x \ set fh_caps. cte_wp_at ((=) (fst x)) (snd x) s) \ + (2 \ length args \ 0 < length fh_caps)\ + update_and_check_handler_ep args pos fh_caps + \\rv s. fst rv \ NullCap \ + cte_wp_at (is_derived (cdt s) (snd rv) (fst rv)) (snd rv) s\,-" + unfolding update_and_check_handler_ep_def + apply wpsimp + apply (rule hoare_drop_imps) + apply (wpsimp wp: derive_cap_is_derived)+ + apply (drule_tac x="fh_caps ! 0" in bspec, clarsimp) + apply (clarsimp simp: cte_wp_at_caps_of_state update_handler_ep_def + cap_master_update_cap_data cap_asid_update_cap_data + cap_badge_update_cap_data) + done + lemma decode_update_sc_inv[wp]: "\P\ decode_update_sc cap slot sc_cap \\_. P\" unfolding decode_update_sc_def is_blocked_def by (wpsimp wp: hoare_drop_imps) @@ -1220,8 +1346,19 @@ lemma decode_update_sc_inv[wp]: context Tcb_AI begin +lemma update_and_check_handler_ep_no_cap_to_obj_with_diff_ref[wp]: + "\\s::'state_ext state. (\x \ set fh_caps. no_cap_to_obj_with_diff_ref (fst x) S s) + \ (2 \ length args \ 0 < length fh_caps)\ + update_and_check_handler_ep args pos fh_caps + \\rv. no_cap_to_obj_with_diff_ref (fst rv) S\,-" + unfolding update_and_check_handler_ep_def + apply (wpsimp wp: hoare_drop_imps) + by (clarsimp simp: update_handler_ep_def + no_cap_to_obj_with_diff_ref_update_cap_data + no_cap_to_obj_with_diff_ref_mask_cap) + lemma decode_set_sched_params_wf[wp]: - "\invs and tcb_at t and ex_nonz_cap_to t and + "\(invs::'state_ext state\bool) and tcb_at t and ex_nonz_cap_to t and cte_at slot and ex_cte_cap_to slot and (\s. \x \ set excaps. s \ fst x \ real_cte_at (snd x) s \ cte_wp_at ((=) (fst x)) (snd x) s @@ -1231,19 +1368,20 @@ lemma decode_set_sched_params_wf[wp]: decode_set_sched_params args (ThreadCap t) slot excaps \tcb_inv_wf\, -" unfolding decode_set_sched_params_def decode_update_sc_def is_blocked_def - apply (wpsimp simp: get_tcb_obj_ref_def + apply (wpsimp simp: get_tcb_obj_ref_def split_def wp: check_prio_wp_weak whenE_throwError_wp thread_get_wp gts_wp split_del: if_split) apply (clarsimp simp: split_paired_Ball) apply (rule conjI; clarsimp) + apply (fastforce dest: in_set_dropD) apply (clarsimp simp: obj_at_def is_tcb pred_tcb_at_def is_cap_simps sc_tcb_sc_at_def sc_at_ppred_def) - apply (rule conjI, fastforce) + apply (rule conjI, fastforce dest: in_set_dropD) apply (subgoal_tac "excaps ! Suc 0 \ set excaps") prefer 2 apply fastforce apply (cases "excaps ! Suc 0") - apply (clarsimp) + apply (fastforce dest: in_set_dropD) done end @@ -1395,16 +1533,16 @@ lemma decode_set_space_wf[wp]: decode_set_space args (ThreadCap t) slot extras \tcb_inv_wf\,-" unfolding decode_set_space_def - apply (wpsimp wp: hoare_vcg_const_imp_lift_R simp_del: tcb_inv_wf.simps + apply (wpsimp wp: hoare_vcg_const_imp_lift_R + simp: split_def simp_del: tcb_inv_wf.simps | strengthen tcb_inv_set_space_strg - | rule hoare_drop_imps)+ - apply (clarsimp simp: valid_fault_handler_def real_cte_at_cte) + | rule hoare_drop_imps + | simp only: tcb_inv_wf.simps)+ apply (prop_tac "set (take 2 (drop (Suc 0) extras)) \ set extras") apply (meson basic_trans_rules(23) set_drop_subset set_take_subset) - apply (intro conjI) - apply blast - apply fastforce - apply (metis gr0I nth_mem zero_less_numeral crunch_simps(1) gr0I nth_mem rel_simps(51))+ + apply (intro conjI; clarsimp?) + apply (fastforce dest: in_set_takeD)+ + apply (metis gt_or_eq_0 nth_mem zero_less_numeral)+ done end @@ -1558,9 +1696,10 @@ lemma decode_set_timeout_ep_tc_inv[wp]: \ cte_wp_at ((=) (fst x)) (snd x) s \ ex_cte_cap_to (snd x) s \ no_cap_to_obj_dr_emp (fst x) s)\ - decode_set_timeout_ep (ThreadCap t) slot extras \tcb_inv_wf\, -" + decode_set_timeout_ep args (ThreadCap t) slot extras + \tcb_inv_wf\, -" unfolding decode_set_timeout_ep_def - by (wpsimp simp: neq_Nil_conv) + by (wpsimp simp: neq_Nil_conv split_def) lemma decode_tcb_inv_wf: "\invs and tcb_at t and ex_nonz_cap_to t