diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index 1eaf4a71e8..0d67285fa0 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -411,9 +411,9 @@ lemma invoke_tcb_schact_is_rct_imp_cur_sc_active: 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) apply (rename_tac target cnode_index cslot_ptr fault_handler mcp priority sc) apply (rule validE_valid) apply (rule_tac B= "\_ s. (schact_is_rct s \ cur_sc_active s) \ tcb_at target s" @@ -1712,12 +1712,9 @@ lemma invoke_tcb_schact_is_rct_imp_ct_activatable: ct_in_state_def pred_tcb_at_def obj_at_def split: thread_state.splits) apply (case_tac "tcb_state tcb"; clarsimp) - 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\) - apply (metis (no_types, lifting) cap.simps(38) fst_conv is_obj_defs(3) o_apply obj_atI - option.simps(5) real_cte_at_not_tcb_at snd_conv) - apply auto - done + by (auto simp: is_cap_simps is_obj_defs dest: is_derived_ep_cap) apply (rule validE_valid) apply (rule_tac B="\_ . ?Q" in hoare_vcg_seqE[rotated]) apply (wpsimp wp: install_tcb_cap_schact_is_rct_imp_ct_activatable) diff --git a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy index 772c8cba19..19f69d23ae 100644 --- a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy @@ -47,7 +47,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, decode_set_priority, decode_set_mcpriority, decode_set_sched_params, decode_set_timeout_ep, decode_set_tls_base, decode_set_space - (simp: cap.splits arch_cap.splits split_def) + (simp: cap.splits arch_cap.splits split_def Let_def) lemma decode_tcb_invocation_empty_fail[wp]: "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)" diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index dbaffe5d0e..295b6b80d1 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -15,25 +15,28 @@ named_theorems Ipc_AI_assms lemma update_cap_data_closedform: "update_cap_data pres w cap = (case cap of - cap.EndpointCap r badge rights \ - if badge = 0 \ \ pres then (cap.EndpointCap r (w && mask 28) rights) else cap.NullCap - | cap.NotificationCap r badge rights \ - if badge = 0 \ \ pres then (cap.NotificationCap r (w && mask 28) rights) else cap.NullCap - | cap.CNodeCap r bits guard \ - if word_bits < unat ((w >> 3) && mask 5) + bits - then cap.NullCap - else cap.CNodeCap r bits ((\g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18)) - | cap.ThreadCap r \ cap.ThreadCap r - | cap.DomainCap \ cap.DomainCap - | cap.UntypedCap d p n idx \ cap.UntypedCap d p n idx - | cap.NullCap \ cap.NullCap - | cap.ReplyCap t rights \ cap.ReplyCap t rights - | cap.SchedContextCap s n \ cap.SchedContextCap s n - | cap.SchedControlCap \ cap.SchedControlCap - | cap.IRQControlCap \ cap.IRQControlCap - | cap.IRQHandlerCap irq \ cap.IRQHandlerCap irq - | cap.Zombie r b n \ cap.Zombie r b n - | cap.ArchObjectCap cap \ cap.ArchObjectCap cap)" + EndpointCap r badge rights \ + if badge = 0 \ \ pres then (EndpointCap r (w && mask badge_bits) rights) else NullCap + | NotificationCap r badge rights \ + if badge = 0 \ \ pres then (NotificationCap r (w && mask badge_bits) rights) else NullCap + | CNodeCap r bits guard \ + if word_bits < unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits) + bits + then NullCap + else CNodeCap r bits + ((\g''. drop (size g'' - unat ((w >> cnode_padding_bits) && + mask cnode_guard_size_bits)) (to_bl g'')) + ((w >> cnode_padding_bits + cnode_guard_size_bits) && mask 18)) + | ThreadCap r \ ThreadCap r + | DomainCap \ DomainCap + | UntypedCap dev p n idx \ UntypedCap dev p n idx + | NullCap \ NullCap + | ReplyCap t rights \ ReplyCap t rights + | SchedContextCap s n \ SchedContextCap s n + | SchedControlCap \ SchedControlCap + | IRQControlCap \ IRQControlCap + | IRQHandlerCap irq \ IRQHandlerCap irq + | Zombie r b n \ Zombie r b n + | ArchObjectCap cap \ ArchObjectCap cap)" apply (cases cap, simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index e98ddad201..56ccb3cd5f 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -104,7 +104,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 \ pt_pd_asid c = pt_pd_asid new_cap) src_slot)\ @@ -140,7 +140,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 *) @@ -251,26 +251,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 @@ -306,15 +306,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 + 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) + 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) lemma tcc_invs[Tcb_AI_asms]: @@ -341,21 +342,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) @@ -364,9 +365,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" @@ -406,7 +408,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) @@ -476,10 +477,21 @@ 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 table_cap_ref_simps + split: cap.splits) + 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 + table_cap_ref_simps + split: cap.split arch_cap.split) apply simp done 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/ArchEmptyFail_AI.thy b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy index 8e2b60cffb..a41c355d8e 100644 --- a/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy @@ -42,7 +42,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, decode_set_priority, decode_set_mcpriority, decode_set_sched_params, decode_set_timeout_ep, decode_set_tls_base, decode_set_space - (simp: cap.splits arch_cap.splits split_def) + (simp: cap.splits arch_cap.splits split_def Let_def) lemma decode_tcb_invocation_empty_fail[wp]: "empty_fail (decode_tcb_invocation a b (ThreadCap p) d e)" 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..f6f2b3a633 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" @@ -1205,13 +1284,48 @@ lemma (in Tcb_AI) decode_set_mcpriority_wf[wp]: decode_set_mcpriority args (ThreadCap t) slot excs \tcb_inv_wf\, -" 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\" - unfolding check_handler_ep_def unlessE_def by wpsimp +lemma decode_handler_ep_inv[wp]: + "decode_handler_ep args pos excaps \P\" + unfolding decode_handler_ep_def Let_def + by (wpsimp wp: hoare_drop_imps) -lemma check_handler_ep_wpE[wp]: - "\\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 decode_handler_ep_snd[wp]: + "\P (snd (excaps ! 0))\ + decode_handler_ep args pos excaps + \\rv. P (snd rv)\,-" + unfolding decode_handler_ep_def Let_def + by (wpsimp wp: hoare_drop_imps split_del: if_split) + +lemma decode_handler_ep_valid_cap[wp]: + "\\s. (\x \ set fh_caps. s \ fst x) \ 0 < length fh_caps\ + decode_handler_ep args pos fh_caps + \\rv. valid_cap (fst rv)\,-" + unfolding decode_handler_ep_def Let_def + apply (wpsimp wp: hoare_drop_imps split_del: if_split) + by (auto simp: update_cap_data_validI) + +lemma decode_handler_ep_valid_fault_handler[wp]: + "\\\ + decode_handler_ep args pos fh_caps + \\rv s. valid_fault_handler (fst rv)\,-" + unfolding decode_handler_ep_def + by (wpsimp split_del: if_split) + +lemma decode_handler_ep_is_derived[wp]: + "\\s. valid_objs s \ + (\x \ set fh_caps. cte_wp_at ((=) (fst x)) (snd x) s) \ 0 < length fh_caps\ + decode_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 decode_handler_ep_def Let_def + apply (wpsimp split_del: if_split) + 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 + 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\" @@ -1220,8 +1334,19 @@ lemma decode_update_sc_inv[wp]: context Tcb_AI begin +lemma decode_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) + \ 0 < length fh_caps\ + decode_handler_ep args pos fh_caps + \\rv. no_cap_to_obj_with_diff_ref (fst rv) S\,-" + unfolding decode_handler_ep_def Let_def + apply (wpsimp wp: hoare_drop_imps split_del: if_split) + by (auto simp: all_set_conv_all_nth + 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,20 +1356,15 @@ 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 (clarsimp simp: all_set_conv_all_nth) 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 (subgoal_tac "excaps ! Suc 0 \ set excaps") - prefer 2 - apply fastforce - apply (cases "excaps ! Suc 0") - apply (clarsimp) - done + apply (rule conjI, fastforce dest: in_set_dropD) + apply (subgoal_tac "Suc 0 < length excaps") + by fastforce+ end @@ -1395,16 +1515,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 +1678,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 diff --git a/proof/refine/ARM/EmptyFail_H.thy b/proof/refine/ARM/EmptyFail_H.thy index 2ab2f06881..a096228fbc 100644 --- a/proof/refine/ARM/EmptyFail_H.thy +++ b/proof/refine/ARM/EmptyFail_H.thy @@ -287,7 +287,7 @@ lemma tcbEPFindIndex_empty_fail[intro!, wp, simp]: by (induct ci; subst tcbEPFindIndex.simps; simp) crunch (empty_fail) empty_fail: callKernel - (wp: empty_fail_catch) + (wp: empty_fail_catch simp: crunch_simps) theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 8f5b3f11e0..d7303d995e 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -1172,7 +1172,7 @@ lemma checkCapAt_cteInsert_corres: and cte_at slot and K (is_cnode_or_valid_arch new_cap \ is_ep_cap new_cap) and K (is_pt_cap new_cap \ is_pd_cap new_cap \ cap_asid new_cap \ None) and (\s. is_ep_cap new_cap - \ cte_wp_at (\c. c = new_cap \ c = cap.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 \ pt_pd_asid c = pt_pd_asid new_cap) src_slot) @@ -1585,18 +1585,18 @@ lemma installTCBCap_corres_helper: lemma installTCBCap_corres: "\ newroot_rel slot_opt slot_opt'; slot_opt \ None \ slot' = cte_map slot; n \ {0,1,3,4} \ \ corres (dc \ dc) - (\s. einvs s \ valid_machine_time s \ simple_sched_action s + (\s. einvs s \ valid_machine_time s \ simple_sched_action s \ tcb_at target s \ cte_at (target, tcb_cnode_index n) s \ current_time_bounded s \ (\new_cap src_slot. slot_opt = Some (new_cap, src_slot) \ (is_cnode_or_valid_arch new_cap \ valid_fault_handler new_cap) \ (new_cap \ cap.NullCap \ s \ new_cap \ - (is_ep_cap new_cap \ (target,tcb_cnode_index n) \ src_slot \ + (is_ep_cap new_cap \ cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s \ - cte_wp_at ((=) new_cap) src_slot s) \ + cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) \ no_cap_to_obj_dr_emp new_cap s \ - cte_at src_slot s \ cte_at slot s))) + real_cte_at src_slot s \ cte_at slot s))) (\s. invs' s \ sch_act_simple s \ cte_at' (cte_map (target, tcb_cnode_index n)) s \ (\newCap srcSlot. slot_opt' = Some (newCap, srcSlot) \ @@ -1618,10 +1618,12 @@ lemma installTCBCap_corres: apply (rule cteDelete_corres) apply ((wp cap_delete_valid_sched cap_delete_deletes_fh cap_delete_deletes cap_delete_cte_at cap_delete_valid_cap cteDelete_invs' cteDelete_deletes hoare_vcg_const_imp_lift_R + cap_delete_is_derived_ep | strengthen use_no_cap_to_obj_asid_strg)+) - apply (fastforce simp: is_cap_simps valid_fault_handler_def - is_cnode_or_valid_arch_def cte_wp_at_def)+ - done + 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 + valid_fault_handler_def + elim!: cte_wp_at_weakenE[OF _ is_derived_ep_cap]) lemma installTCBCap_invs': "\\s. invs' s \ (\newCap srcSlot. slot_opt = Some (newCap,srcSlot) \ @@ -1629,13 +1631,12 @@ lemma installTCBCap_invs': \ isReplyCap newCap \ \ isIRQControlCap newCap)\ installTCBCap target slot n slot_opt \\rv. invs'\" - apply (simp only: installTCBCap_def tcbCTableSlot_def tcbVTableSlot_def tcbFaultHandlerSlot_def - getThreadCSpaceRoot_def getThreadVSpaceRoot_def getThreadFaultHandlerSlot_def) + unfolding installTCBCap_def tcbCTableSlot_def tcbVTableSlot_def tcbFaultHandlerSlot_def + getThreadCSpaceRoot_def getThreadVSpaceRoot_def getThreadFaultHandlerSlot_def + locateSlotBasic_def locateSlotTCB_def getThreadTimeoutHandlerSlot_def apply (wpsimp split_del: if_split wp: checked_insert_tcb_invs cteDelete_invs' - cteDelete_deletes hoare_vcg_const_imp_lift_R - simp: locateSlotBasic_def maybe_def returnOk_bindE - getThreadTimeoutHandlerSlot_def locateSlotTCB_def)+ + cteDelete_deletes hoare_vcg_const_imp_lift_R) apply (auto simp: objBits_def objBitsKO_def cteSizeBits_def tcbTimeoutHandlerSlot_def) done @@ -1767,7 +1768,8 @@ lemma installThreadBuffer_corres: wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift thread_set_tcb_ipc_buffer_cap_cleared_invs thread_set_not_state_valid_sched thread_set_valid_objs' - thread_set_cte_wp_at_trivial thread_set_ipc_tcb_cap_valid) + thread_set_cte_wp_at_trivial thread_set_ipc_tcb_cap_valid + hoare_pre_cont[where P="\_ s. cte_wp_at (is_derived (cdt s) _ _) _ s"]) apply (clarsimp simp: option.case_eq_if if_fun_split) apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift threadSet_invs_trivial threadSet_cte_wp_at' threadSet_valid_objs' threadSet_valid_release_queue @@ -1794,7 +1796,7 @@ lemma installThreadBuffer_corres: apply (fastforce split: option.splits) apply (fastforce simp: obj_at_def is_tcb intro: cte_wp_at_tcbI) apply (fastforce simp: cte_map_def tcb_cnode_index_def obj_at'_def - projectKOs cte_level_bits_def objBits_simps cte_wp_at_tcbI') + cte_level_bits_def objBits_simps projectKOs cte_wp_at_tcbI') done lemma tcb_at_cte_at'_0: "tcb_at' a s \ cte_at' (cte_map (a, tcb_cnode_index 0)) s" @@ -1855,31 +1857,40 @@ lemma tc_corres_caps: apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) - apply ((clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_cte_at_3 tcb_at_cte_at_4 - tcb_cap_valid_def tcb_at_st_tcb_at[symmetric] is_nondevice_page_cap_def - is_nondevice_page_cap_arch_def is_cnode_or_valid_arch_def is_cap_simps - is_valid_vtable_root_def valid_ipc_buffer_cap tcb_ep_slot_cte_wp_at - cte_wp_at_disj cte_wp_at_eq_simp real_cte_at_cte real_cte_at_not_tcb_at - split: option.split - | intro conjI | fastforce simp: valid_fault_handler_def)+)[1] + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + subgoal by ((clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_cte_at_3 + tcb_at_cte_at_4 cteSizeBits_def + tcb_cap_valid_def tcb_at_st_tcb_at[symmetric] is_nondevice_page_cap_def + is_cnode_or_valid_arch_def is_cap_simps + is_valid_vtable_root_def valid_ipc_buffer_cap tcb_ep_slot_cte_wp_at + cte_wp_at_disj cte_wp_at_eq_simp real_cte_at_cte real_cte_at_not_tcb_at + split: option.split cap.splits + | intro conjI + | fastforce simp: valid_fault_handler_def is_cap_simps + typ_at_eq_kheap_obj cap_table_at_typ tcb_at_typ + split: option.splits cap.splits arch_cap.splits + elim!: cte_wp_at_weakenE[OF _ is_derived_ep_cap])+) apply (clarsimp simp: tcb_at_cte_at'_0 tcb_at_cte_at'_1 tcb_at_cte_at'_3 tcb_at_cte_at'_4 isCap_simps case_option_If2 - isValidFaultHandler_def isValidVTableRoot_def | intro conjI)+ + isValidFaultHandler_def isValidVTableRoot_def + | intro conjI)+ done lemma sched_context_resume_weak_valid_sched_action: @@ -2319,7 +2330,8 @@ lemma tc_corres_sched: apply (clarsimp split: Structures_A.kernel_object.splits) apply (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def sc_at_ppred_def obj_at_def is_ep_def is_tcb_def - elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + elim: cte_wp_at_weakenE is_derived_ep_cap + dest: tcb_ep_slot_cte_wp_ats) apply (clarsimp simp: tcs_cross_asrt1_def) apply (intro conjI impI allI; clarsimp?) apply (clarsimp simp: tcb_at_cte_at'_3) @@ -2865,6 +2877,28 @@ lemma decodeSetMCPriority_inv[wp]: | wpcw)+ done +crunches decodeHandlerEP + for inv[wp]: P + (simp: crunch_simps) + +global_interpretation decodeHandlerEP: typ_at_all_props' "decodeHandlerEP args pos fh_caps" + by typ_at_props' + +lemma decodeHandlerEP_valid_cap[wp]: + "\\s. \x \ set fh_caps. s \' fst x\ + decodeHandlerEP args pos fh_caps + \\rv. valid_cap' (fst rv)\,-" + unfolding decodeHandlerEP_def Let_def + apply (wpsimp wp: hoare_drop_imps split_del: if_split) + by (auto simp: valid_updateCapDataI) + +lemma decodeHandlerEP_isValidFaultHandler[wp]: + "\\\ + decodeHandlerEP args pos fh_caps + \\rv s. isValidFaultHandler (fst rv)\,-" + unfolding decodeHandlerEP_def + by (wpsimp split_del: if_split) + lemma decodeSetSchedParams_wf: "\invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot and (\s. \x \ set extras. real_cte_at' (snd x) s @@ -2911,17 +2945,59 @@ lemma corres_case_cap_null_sc: apply (case_tac cp; clarsimp) done +lemma decodeHandlerEP_corres: + "\ list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; + length extras = 1 \ \ + corres (ser \ (\a b. cap_relation (fst a) (fst b) \ snd b = cte_map (snd a))) + (\s. \x \ set extras. cte_at (snd x) s) + (pspace_aligned' and pspace_distinct' and valid_mdb' and + (\s. \x \ set extras'. cte_at' (snd x) s)) + (decode_handler_ep args pos extras) + (decodeHandlerEP args pos extras')" + unfolding decode_handler_ep_def decodeHandlerEP_def unlessE_whenE Let_def + apply (clarsimp simp: list_length_2 list_length_1 list_all2_Cons1 split del: if_split) + apply (rule corres_guard_imp) + apply (rule whenE_throwError_corres) + apply simp + apply (fastforce simp: cap_relation_case is_cap_simps isCap_simps + split: cap.splits arch_cap.splits) + apply (rule_tac r'=cap_relation in corres_splitEE) + prefer 2 + apply (rule corres_if, simp) + apply (rule corres_if) + apply (fastforce split: cap.splits) + apply (rule whenE_throwError_corres) + apply simp + apply (clarsimp simp: cap_relation_NullCap) + apply (rule corres_returnOkTT, simp add: cap_map_update_data) + apply (rule corres_returnOkTT, simp) + apply (rule corres_returnOkTT, simp) + apply (rule_tac r'=cap_relation in corres_splitEE) + prefer 2 + apply (rule corres_if, simp) + apply (rule corres_returnOkTT, + simp add: cap_relation_mask rightsFromWord_correspondence) + apply (rule corres_returnOkTT, simp) + apply (rule corres_splitEE) + prefer 2 + apply (rule deriveCap_corres; simp) + apply (rule whenE_throwError_corres) + apply simp + apply (clarsimp simp: cap_rel_valid_fh) + apply (rule corres_returnOkTT, simp) + by wpsimp+ + lemma decodeSetSchedParams_corres: "\ cap_relation cap cap'; is_thread_cap cap; slot' = cte_map slot; list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ \ corres (ser \ tcbinv_relation) - (invs and valid_sched and (\s. s \ cap \ (\x \ set extras. s \ (fst x)))) - (invs' and (\s. s \' cap' \ (\x \ set extras'. s \' (fst x)))) + (invs and valid_sched and (\s. s \ cap \ (\(x, y) \ set extras. s \ x \ cte_at y s))) + (invs' and (\s. s \' cap' \ (\(x, y) \ set extras'. s \' x \ cte_at' y s))) (decode_set_sched_params args cap slot extras) (decodeSetSchedParams args cap' slot' extras')" apply (clarsimp simp: is_cap_simps) - apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def decode_update_sc_def - check_handler_ep_def unlessE_whenE) + apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def + decode_update_sc_def unlessE_whenE) apply (cases "length args < 2") apply (clarsimp split: list.split) apply (cases "length extras < 3") @@ -2932,10 +3008,12 @@ lemma decodeSetSchedParams_corres: apply (rule corres_split_norE[OF _ checkPrio_corres]) apply (rule corres_split_norE[OF _ checkPrio_corres]) apply (rule corres_split_eqrE) - apply (clarsimp simp: liftE_bindE_bind bindE_assoc) - apply (rule whenE_throwError_corres; simp add: cap_rel_valid_fh) - apply (rule corres_returnOkTT) - apply (clarsimp simp: newroot_rel_def) + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (rule corres_returnOkTT) + apply (clarsimp simp: newroot_rel_def) + apply clarsimp+ + apply wpsimp + apply wpsimp apply (rule corres_case_cap_null_sc[where Pother=\ and Pother'=\] ; clarsimp ; (wpfix add: capability.sel)?) @@ -2958,7 +3036,9 @@ lemma decodeSetSchedParams_corres: apply (wpsimp simp: is_blocked_def)+ apply (rule threadGet_corres) apply (clarsimp simp: tcb_relation_def) - apply (wpsimp wp: thread_get_wp' threadGet_wp check_prio_inv checkPrio_inv)+ + apply (wpsimp wp: thread_get_wp' threadGet_wp check_prio_inv + checkPrio_inv hoare_drop_imps + simp: is_blocked_def)+ apply (clarsimp split: cap.splits ; intro conjI impI allI ; fastforce intro: corres_returnOkTT) @@ -2966,12 +3046,10 @@ lemma decodeSetSchedParams_corres: apply (fastforce simp: valid_cap_def) apply (clarsimp simp: valid_cap_simps') apply normalise_obj_at' - apply (intro exI impI conjI allI) - apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) - apply (rename_tac obj) - apply (case_tac obj; clarsimp) - apply (erule invs_valid_objs') - apply (clarsimp simp: obj_at'_def) + apply (intro exI impI conjI allI; clarsimp?) + apply (clarsimp simp: valid_cap_simps' obj_at'_def ko_wp_at'_def projectKOs) + apply (rename_tac obj) + apply (case_tac obj; clarsimp) done lemma checkValidIPCBuffer_corres: @@ -3175,37 +3253,38 @@ lemma decode_cv_space_is_ThreadControlCaps[wp]: apply (clarsimp simp: return_def validE_def valid_def) done +crunches decodeSetSpace + for inv[wp]: P + (wp: crunch_wps) + lemma decodeSetSpace_corres: - "\cap_relation cap cap'; - list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; - is_thread_cap cap\ \ - corres (ser \ tcbinv_relation) - (invs and valid_cap cap and (\s. \x \ set extras. cte_at (snd x) s)) - (invs' and valid_cap' cap' and (\s. \x \ set extras'. cte_at' (snd x) s)) + "\cap_relation cap cap'; + list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; + is_thread_cap cap\ \ + corres (ser \ tcbinv_relation) + (invs and valid_cap cap and (\s. \x \ set extras. cte_at (snd x) s)) + (invs' and valid_cap' cap' and (\s. \x \ set extras'. cte_at' (snd x) s)) (decode_set_space args cap slot extras) (decodeSetSpace args cap' (cte_map slot) extras')" - apply (simp add: decode_set_space_def decodeSetSpace_def check_handler_ep_def unlessE_whenE) + apply (simp add: decode_set_space_def decodeSetSpace_def unlessE_whenE) apply (cases "\ (2 \ length args \ 3 \ length extras')") apply (clarsimp dest!: list_all2_lengthD split: list.split) - apply fastforce apply (clarsimp simp: val_le_length_Cons list_all2_Cons2 split del: if_split) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF _ decodeCVSpace_corres]) apply (rename_tac abs_space conc_space) apply (rule_tac F="tcb_invocation.is_ThreadControlCaps abs_space" in corres_gen_asm) - apply clarsimp - apply (intro conjI impI; simp add: cap_rel_valid_fh) - apply (prop_tac "newroot_rel (tc_new_croot abs_space) (tcCapsCRoot conc_space)") - apply (case_tac abs_space; clarsimp) - apply (prop_tac "newroot_rel (tc_new_vroot abs_space) (tcCapsVRoot conc_space)") - apply (case_tac abs_space; clarsimp) - apply (rule corres_returnOkTT) - apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps list_all2_conv_all_nth) - apply blast - apply fastforce+ - apply wp+ - apply fastforce+ + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (prop_tac "newroot_rel (tc_new_croot abs_space) (tcCapsCRoot conc_space)") + apply (case_tac abs_space; clarsimp) + apply (prop_tac "newroot_rel (tc_new_vroot abs_space) (tcCapsVRoot conc_space)") + apply (case_tac abs_space; clarsimp) + apply (rule corres_returnOkTT) + apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps list_all2_conv_all_nth) + apply clarsimp+ + apply wpsimp+ + apply fastforce done lemma decodeCVSpace_wf[wp]: @@ -3239,37 +3318,14 @@ lemma decodeSetSpace_wf[wp]: split del: if_split cong: if_cong list.case_cong) apply (rule hoare_pre) apply (wp - | simp add: o_def split_def - split del: if_split - | wpc - | rule hoare_drop_imps)+ + | simp add: o_def split_def split del: if_split + | wpc + | rule hoare_drop_imps)+ apply (clarsimp simp del: length_greater_0_conv split del: if_split) apply (simp del: length_greater_0_conv add: valid_updateCapDataI) done -lemma decodeCVSpace_inv[wp]: - "decodeCVSpace args cap slot extras \P\" - apply (simp add: decodeCVSpace_def Let_def split_def - unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot - split del: if_split cong: if_cong list.case_cong) - apply (rule hoare_pre) - apply (wp hoare_drop_imps - | simp add: o_def split_def split del: if_split - | wpcw)+ - done - -lemma decodeSetSpace_inv[wp]: - "\P\ decodeSetSpace args cap slot extras \\rv. P\" - apply (simp add: decodeSetSpace_def decodeCVSpace_def Let_def split_def - unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot - split del: if_split cong: if_cong list.case_cong) - apply (rule hoare_pre) - apply (wp hoare_drop_imps - | simp add: o_def split_def split del: if_split - | wpcw)+ - done - lemma decodeCVSpace_is_tc[wp]: "\\\ decodeCVSpace args cap slot extras \\rv s. isThreadControlCaps rv\,-" apply (simp add: decodeCVSpace_def Let_def split_def @@ -3508,14 +3564,22 @@ lemma decodeSetTLSBase_corres: lemma decodeSetTimeoutEndpoint_corres: "list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ - corres (ser \ tcbinv_relation) (tcb_at t) (tcb_at' t) - (decode_set_timeout_ep (cap.ThreadCap t) slot extras) - (decodeSetTimeoutEndpoint (capability.ThreadCap t) (cte_map slot) extras')" + corres (ser \ tcbinv_relation) + (\s. \x \ set extras. cte_at (snd x) s) + (pspace_aligned' and pspace_distinct' and valid_mdb' and + (\s. \x \ set extras'. cte_at' (snd x) s)) + (decode_set_timeout_ep args (cap.ThreadCap t) slot extras) + (decodeSetTimeoutEndpoint args (capability.ThreadCap t) (cte_map slot) extras')" apply (clarsimp simp: decode_set_timeout_ep_def decodeSetTimeoutEndpoint_def) - apply (cases extras; cases extras'; clarsimp) - apply (fastforce simp: check_handler_ep_def unlessE_def returnOk_def bindE_def - newroot_rel_def emptyTCCaps_def throwError_def - dest: cap_rel_valid_fh) + apply (cases "length extras < 1") + apply (clarsimp split: list.split simp: list_all2_Cons2) + apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less) + apply (rule corres_guard_imp) + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (rule corres_returnOkTT) + apply (clarsimp simp: newroot_rel_def emptyTCCaps_def) + apply clarsimp+ + apply wpsimp+ done lemma decodeTCBInvocation_corres: @@ -3599,7 +3663,7 @@ lemma decodeSetTLSBase_wf: lemma decodeSetTimeoutEndpoint_wf[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot and (\s. \x \ set extras. s \' fst x \ cte_at' (snd x) s)\ - decodeSetTimeoutEndpoint (ThreadCap t) slot extras + decodeSetTimeoutEndpoint args (ThreadCap t) slot extras \tcb_inv_wf'\,-" apply (simp add: decodeSetTimeoutEndpoint_def emptyTCCaps_def cong: list.case_cong) diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy index 66842aba51..e1cf4e94c1 100644 --- a/proof/refine/RISCV64/EmptyFail_H.thy +++ b/proof/refine/RISCV64/EmptyFail_H.thy @@ -300,7 +300,7 @@ lemma tcbEPFindIndex_empty_fail[intro!, wp, simp]: by (induct ci; subst tcbEPFindIndex.simps; simp) crunch (empty_fail) empty_fail: callKernel - (wp: empty_fail_catch) + (wp: empty_fail_catch simp: crunch_simps) theorem call_kernel_serial: "\ (einvs and (\s. event \ Interrupt \ ct_running s) and (ct_running or ct_idle) and diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index a45997f0f6..9e9d8f28e3 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -1177,7 +1177,7 @@ lemma checkCapAt_cteInsert_corres: corres dc (einvs and cte_wp_at (\c. c = cap.NullCap) (target, ref) and cte_at slot and K (is_cnode_or_valid_arch new_cap \ is_ep_cap new_cap) and (\s. is_ep_cap new_cap - \ cte_wp_at (\c. c = new_cap \ c = cap.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) @@ -1585,18 +1585,18 @@ lemma installTCBCap_corres_helper: lemma installTCBCap_corres: "\ newroot_rel slot_opt slot_opt'; slot_opt \ None \ slot' = cte_map slot; n \ {0,1,3,4} \ \ corres (dc \ dc) - (\s. einvs s \ valid_machine_time s \ simple_sched_action s + (\s. einvs s \ valid_machine_time s \ simple_sched_action s \ tcb_at target s \ cte_at (target, tcb_cnode_index n) s \ current_time_bounded s \ (\new_cap src_slot. slot_opt = Some (new_cap, src_slot) \ (is_cnode_or_valid_arch new_cap \ valid_fault_handler new_cap) \ (new_cap \ cap.NullCap \ s \ new_cap \ - (is_ep_cap new_cap \ (target,tcb_cnode_index n) \ src_slot \ + (is_ep_cap new_cap \ cte_wp_at valid_fault_handler (target, tcb_cnode_index n) s \ - cte_wp_at ((=) new_cap) src_slot s) \ + cte_wp_at (is_derived (cdt s) src_slot new_cap) src_slot s) \ no_cap_to_obj_dr_emp new_cap s \ - cte_at src_slot s \ cte_at slot s))) + real_cte_at src_slot s \ cte_at slot s))) (\s. invs' s \ sch_act_simple s \ cte_at' (cte_map (target, tcb_cnode_index n)) s \ (\newCap srcSlot. slot_opt' = Some (newCap, srcSlot) \ @@ -1617,11 +1617,13 @@ lemma installTCBCap_corres: apply simp apply (rule cteDelete_corres) apply (wp cap_delete_valid_sched cap_delete_deletes_fh cap_delete_deletes cap_delete_cte_at - cap_delete_valid_cap cteDelete_invs' cteDelete_deletes hoare_vcg_const_imp_lift_R + cap_delete_valid_cap cteDelete_invs' cteDelete_deletes hoare_vcg_const_imp_lift_R + cap_delete_is_derived_ep | strengthen use_no_cap_to_obj_asid_strg)+ - apply (fastforce simp: is_cap_simps valid_fault_handler_def - is_cnode_or_valid_arch_def cte_wp_at_def)+ - done + 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 + valid_fault_handler_def + elim!: cte_wp_at_weakenE[OF _ is_derived_ep_cap]) lemma installTCBCap_invs': "\\s. invs' s \ (\newCap srcSlot. slot_opt = Some (newCap,srcSlot) \ @@ -1629,13 +1631,12 @@ lemma installTCBCap_invs': \ isReplyCap newCap \ \ isIRQControlCap newCap)\ installTCBCap target slot n slot_opt \\rv. invs'\" - apply (simp only: installTCBCap_def tcbCTableSlot_def tcbVTableSlot_def tcbFaultHandlerSlot_def - getThreadCSpaceRoot_def getThreadVSpaceRoot_def getThreadFaultHandlerSlot_def) + unfolding installTCBCap_def tcbCTableSlot_def tcbVTableSlot_def tcbFaultHandlerSlot_def + getThreadCSpaceRoot_def getThreadVSpaceRoot_def getThreadFaultHandlerSlot_def + locateSlotBasic_def locateSlotTCB_def getThreadTimeoutHandlerSlot_def apply (wpsimp split_del: if_split wp: checked_insert_tcb_invs cteDelete_invs' - cteDelete_deletes hoare_vcg_const_imp_lift_R - simp: locateSlotBasic_def maybe_def returnOk_bindE - getThreadTimeoutHandlerSlot_def locateSlotTCB_def)+ + cteDelete_deletes hoare_vcg_const_imp_lift_R) apply (auto simp: objBits_def objBitsKO_def cteSizeBits_def tcbTimeoutHandlerSlot_def) done @@ -1767,7 +1768,8 @@ lemma installThreadBuffer_corres: wp: hoare_vcg_all_lift hoare_vcg_const_imp_lift thread_set_tcb_ipc_buffer_cap_cleared_invs thread_set_not_state_valid_sched thread_set_valid_objs' - thread_set_cte_wp_at_trivial thread_set_ipc_tcb_cap_valid) + thread_set_cte_wp_at_trivial thread_set_ipc_tcb_cap_valid + hoare_pre_cont[where P="\_ s. cte_wp_at (is_derived (cdt s) _ _) _ s"]) apply (clarsimp simp: option.case_eq_if if_fun_split) apply (wpsimp wp: hoare_vcg_const_imp_lift hoare_vcg_all_lift threadSet_invs_trivial threadSet_cte_wp_at' threadSet_valid_objs' threadSet_valid_release_queue @@ -1794,7 +1796,7 @@ lemma installThreadBuffer_corres: apply (fastforce split: option.splits) apply (fastforce simp: obj_at_def is_tcb intro: cte_wp_at_tcbI) apply (fastforce simp: cte_map_def tcb_cnode_index_def obj_at'_def - projectKOs cte_level_bits_def objBits_simps cte_wp_at_tcbI') + cte_level_bits_def objBits_simps cte_wp_at_tcbI') done lemma tcb_at_cte_at'_0: "tcb_at' a s \ cte_at' (cte_map (a, tcb_cnode_index 0)) s" @@ -1855,30 +1857,36 @@ lemma tc_corres_caps: apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) apply (rule installTCBCap_corres; clarsimp) apply ((wp hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R install_tcb_cap_invs install_tcb_cap_cte_at install_tcb_cap_cte_wp_at_ep + install_tcb_cap_is_derived_ep | strengthen tcb_cap_always_valid_strg)+)[1] apply (wp installTCBCap_invs' installTCBCap_sch_act_simple - hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) + hoare_case_option_wpR hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R) subgoal by ((clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_cte_at_3 tcb_at_cte_at_4 cteSizeBits_def tcb_cap_valid_def tcb_at_st_tcb_at[symmetric] is_nondevice_page_cap_def is_cnode_or_valid_arch_def is_cap_simps is_valid_vtable_root_def valid_ipc_buffer_cap tcb_ep_slot_cte_wp_at - cte_wp_at_disj cte_wp_at_eq_simp real_cte_at_cte real_cte_at_not_tcb_at + cte_wp_at_disj cte_wp_at_eq_simp real_cte_at_cte real_cte_at_not_tcb_at split: option.split cap.splits | intro conjI - | fastforce simp: valid_fault_handler_def split: option.splits cap.splits )+)[1] + | fastforce simp: valid_fault_handler_def arch_cap.is_FrameCap_def is_cap_simps + typ_at_eq_kheap_obj cap_table_at_typ tcb_at_typ + split: option.splits cap.splits arch_cap.splits + elim!: cte_wp_at_weakenE[OF _ is_derived_ep_cap])+) by (clarsimp simp: tcb_at_cte_at'_0 tcb_at_cte_at'_1 tcb_at_cte_at'_3 tcb_at_cte_at'_4 isCap_simps case_option_If2 isValidFaultHandler_def isValidVTableRoot_def @@ -2315,7 +2323,8 @@ lemma tc_corres_sched: apply (clarsimp split: Structures_A.kernel_object.splits) apply (fastforce simp: tcb_cap_valid_def pred_tcb_at_def pred_neg_def sc_at_ppred_def obj_at_def is_ep_def is_tcb_def - elim: cte_wp_at_weakenE dest: tcb_ep_slot_cte_wp_ats) + elim: cte_wp_at_weakenE is_derived_ep_cap + dest: tcb_ep_slot_cte_wp_ats) apply (clarsimp simp: tcs_cross_asrt1_def) apply (intro conjI impI allI; clarsimp?) apply (clarsimp simp: tcb_at_cte_at'_3) @@ -2864,6 +2873,28 @@ lemma decodeSetMCPriority_inv[wp]: | wpcw)+ done +crunches decodeHandlerEP + for inv[wp]: P + (simp: crunch_simps) + +global_interpretation decodeHandlerEP: typ_at_all_props' "decodeHandlerEP args pos fh_caps" + by typ_at_props' + +lemma decodeHandlerEP_valid_cap[wp]: + "\\s. \x \ set fh_caps. s \' fst x\ + decodeHandlerEP args pos fh_caps + \\rv. valid_cap' (fst rv)\,-" + unfolding decodeHandlerEP_def Let_def + apply (wpsimp wp: hoare_drop_imps split_del: if_split) + by (auto simp: valid_updateCapDataI) + +lemma decodeHandlerEP_isValidFaultHandler[wp]: + "\\\ + decodeHandlerEP args pos fh_caps + \\rv s. isValidFaultHandler (fst rv)\,-" + unfolding decodeHandlerEP_def + by (wpsimp split_del: if_split) + lemma decodeSetSchedParams_wf: "\invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot and (\s. \x \ set extras. real_cte_at' (snd x) s @@ -2910,17 +2941,59 @@ lemma corres_case_cap_null_sc: apply (case_tac cp; clarsimp) done +lemma decodeHandlerEP_corres: + "\ list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; + length extras = 1 \ \ + corres (ser \ (\a b. cap_relation (fst a) (fst b) \ snd b = cte_map (snd a))) + (\s. \x \ set extras. cte_at (snd x) s) + (pspace_aligned' and pspace_distinct' and valid_mdb' and + (\s. \x \ set extras'. cte_at' (snd x) s)) + (decode_handler_ep args pos extras) + (decodeHandlerEP args pos extras')" + unfolding decode_handler_ep_def decodeHandlerEP_def unlessE_whenE Let_def + apply (clarsimp simp: list_length_2 list_length_1 list_all2_Cons1 split del: if_split) + apply (rule corres_guard_imp) + apply (rule whenE_throwError_corres) + apply simp + apply (fastforce simp: cap_relation_case is_cap_simps isCap_simps + split: cap.splits arch_cap.splits) + apply (rule_tac r'=cap_relation in corres_splitEE) + prefer 2 + apply (rule corres_if, simp) + apply (rule corres_if) + apply (fastforce split: cap.splits) + apply (rule whenE_throwError_corres) + apply simp + apply (clarsimp simp: cap_relation_NullCap) + apply (rule corres_returnOkTT, simp add: cap_map_update_data) + apply (rule corres_returnOkTT, simp) + apply (rule corres_returnOkTT, simp) + apply (rule_tac r'=cap_relation in corres_splitEE) + prefer 2 + apply (rule corres_if, simp) + apply (rule corres_returnOkTT, + simp add: cap_relation_mask rightsFromWord_correspondence) + apply (rule corres_returnOkTT, simp) + apply (rule corres_splitEE) + prefer 2 + apply (rule deriveCap_corres; simp) + apply (rule whenE_throwError_corres) + apply simp + apply (clarsimp simp: cap_rel_valid_fh) + apply (rule corres_returnOkTT, simp) + by wpsimp+ + lemma decodeSetSchedParams_corres: "\ cap_relation cap cap'; is_thread_cap cap; slot' = cte_map slot; list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ \ corres (ser \ tcbinv_relation) - (invs and valid_sched and (\s. s \ cap \ (\x \ set extras. s \ (fst x)))) - (invs' and (\s. s \' cap' \ (\x \ set extras'. s \' (fst x)))) + (invs and valid_sched and (\s. s \ cap \ (\(x, y) \ set extras. s \ x \ cte_at y s))) + (invs' and (\s. s \' cap' \ (\(x, y) \ set extras'. s \' x \ cte_at' y s))) (decode_set_sched_params args cap slot extras) (decodeSetSchedParams args cap' slot' extras')" apply (clarsimp simp: is_cap_simps) - apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def decode_update_sc_def - check_handler_ep_def unlessE_whenE) + apply (simp add: decode_set_sched_params_def decodeSetSchedParams_def + decode_update_sc_def unlessE_whenE) apply (cases "length args < 2") apply (clarsimp split: list.split) apply (cases "length extras < 3") @@ -2931,10 +3004,12 @@ lemma decodeSetSchedParams_corres: apply (rule corres_split_norE[OF _ checkPrio_corres]) apply (rule corres_split_norE[OF _ checkPrio_corres]) apply (rule corres_split_eqrE) - apply (clarsimp simp: liftE_bindE_bind bindE_assoc) - apply (rule whenE_throwError_corres; simp add: cap_rel_valid_fh) - apply (rule corres_returnOkTT) - apply (clarsimp simp: newroot_rel_def) + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (rule corres_returnOkTT) + apply (clarsimp simp: newroot_rel_def) + apply clarsimp+ + apply wpsimp + apply wpsimp apply (rule corres_case_cap_null_sc[where Pother=\ and Pother'=\] ; clarsimp ; (wpfix add: capability.sel)?) @@ -2957,18 +3032,18 @@ lemma decodeSetSchedParams_corres: apply (wpsimp simp: is_blocked_def)+ apply (rule threadGet_corres) apply (clarsimp simp: tcb_relation_def) - apply (wpsimp wp: thread_get_wp' threadGet_wp check_prio_inv checkPrio_inv)+ + apply (wpsimp wp: thread_get_wp' threadGet_wp check_prio_inv + checkPrio_inv hoare_drop_imps + simp: is_blocked_def)+ apply (clarsimp split: cap.splits; intro conjI impI allI; fastforce intro: corres_returnOkTT) apply wpsimp+ apply (fastforce simp: valid_cap_def) apply (clarsimp simp: valid_cap_simps') apply normalise_obj_at' - apply (intro exI impI conjI allI) - apply (clarsimp simp: obj_at'_def ko_wp_at'_def) - apply (rename_tac obj) - apply (case_tac obj; clarsimp) - apply (erule invs_valid_objs') - apply (clarsimp simp: obj_at'_def) + apply (intro exI impI conjI allI; clarsimp?) + apply (clarsimp simp: valid_cap_simps' obj_at'_def ko_wp_at'_def) + apply (rename_tac obj) + apply (case_tac obj; clarsimp) done lemma checkValidIPCBuffer_corres: @@ -3173,37 +3248,38 @@ lemma decode_cv_space_is_ThreadControlCaps[wp]: apply (clarsimp simp: return_def validE_def valid_def) done +crunches decodeSetSpace + for inv[wp]: P + (wp: crunch_wps) + lemma decodeSetSpace_corres: - "\cap_relation cap cap'; - list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; - is_thread_cap cap\ \ - corres (ser \ tcbinv_relation) - (invs and valid_cap cap and (\s. \x \ set extras. cte_at (snd x) s)) - (invs' and valid_cap' cap' and (\s. \x \ set extras'. cte_at' (snd x) s)) + "\cap_relation cap cap'; + list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras'; + is_thread_cap cap\ \ + corres (ser \ tcbinv_relation) + (invs and valid_cap cap and (\s. \x \ set extras. cte_at (snd x) s)) + (invs' and valid_cap' cap' and (\s. \x \ set extras'. cte_at' (snd x) s)) (decode_set_space args cap slot extras) (decodeSetSpace args cap' (cte_map slot) extras')" - apply (simp add: decode_set_space_def decodeSetSpace_def check_handler_ep_def unlessE_whenE) + apply (simp add: decode_set_space_def decodeSetSpace_def unlessE_whenE) apply (cases "\ (2 \ length args \ 3 \ length extras')") apply (clarsimp dest!: list_all2_lengthD split: list.split) - apply fastforce apply (clarsimp simp: val_le_length_Cons list_all2_Cons2 split del: if_split) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF _ decodeCVSpace_corres]) apply (rename_tac abs_space conc_space) apply (rule_tac F="tcb_invocation.is_ThreadControlCaps abs_space" in corres_gen_asm) - apply clarsimp - apply (intro conjI impI; simp add: cap_rel_valid_fh) - apply (prop_tac "newroot_rel (tc_new_croot abs_space) (tcCapsCRoot conc_space)") - apply (case_tac abs_space; clarsimp) - apply (prop_tac "newroot_rel (tc_new_vroot abs_space) (tcCapsVRoot conc_space)") - apply (case_tac abs_space; clarsimp) - apply (rule corres_returnOkTT) - apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps list_all2_conv_all_nth) - apply blast - apply fastforce+ - apply wp+ - apply fastforce+ + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (prop_tac "newroot_rel (tc_new_croot abs_space) (tcCapsCRoot conc_space)") + apply (case_tac abs_space; clarsimp) + apply (prop_tac "newroot_rel (tc_new_vroot abs_space) (tcCapsVRoot conc_space)") + apply (case_tac abs_space; clarsimp) + apply (rule corres_returnOkTT) + apply (clarsimp simp: returnOk_def newroot_rel_def is_cap_simps list_all2_conv_all_nth) + apply clarsimp+ + apply wpsimp+ + apply fastforce done lemma decodeCVSpace_wf[wp]: @@ -3247,28 +3323,6 @@ lemma decodeSetSpace_wf[wp]: apply (simp del: length_greater_0_conv add: valid_updateCapDataI) done -lemma decodeCVSpace_inv[wp]: - "decodeCVSpace args cap slot extras \P\" - apply (simp add: decodeCVSpace_def Let_def split_def - unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot - split del: if_split cong: if_cong list.case_cong) - apply (rule hoare_pre) - apply (wp hoare_drop_imps - | simp add: o_def split_def split del: if_split - | wpcw)+ - done - -lemma decodeSetSpace_inv[wp]: - "decodeSetSpace args cap slot extras \P\" - apply (simp add: decodeSetSpace_def decodeCVSpace_def Let_def split_def - unlessE_def getThreadVSpaceRoot getThreadCSpaceRoot - split del: if_split cong: if_cong list.case_cong) - apply (rule hoare_pre) - apply (wp hoare_drop_imps - | simp add: o_def split_def split del: if_split - | wpcw)+ - done - lemma decodeCVSpace_is_tc[wp]: "\\\ decodeCVSpace args cap slot extras \\rv s. isThreadControlCaps rv\,-" apply (simp add: decodeCVSpace_def Let_def split_def @@ -3507,14 +3561,22 @@ lemma decodeSetTLSBase_corres: lemma decodeSetTimeoutEndpoint_corres: "list_all2 (\(c, sl) (c', sl'). cap_relation c c' \ sl' = cte_map sl) extras extras' \ - corres (ser \ tcbinv_relation) (tcb_at t) (tcb_at' t) - (decode_set_timeout_ep (cap.ThreadCap t) slot extras) - (decodeSetTimeoutEndpoint (capability.ThreadCap t) (cte_map slot) extras')" + corres (ser \ tcbinv_relation) + (\s. \x \ set extras. cte_at (snd x) s) + (pspace_aligned' and pspace_distinct' and valid_mdb' and + (\s. \x \ set extras'. cte_at' (snd x) s)) + (decode_set_timeout_ep args (cap.ThreadCap t) slot extras) + (decodeSetTimeoutEndpoint args (capability.ThreadCap t) (cte_map slot) extras')" apply (clarsimp simp: decode_set_timeout_ep_def decodeSetTimeoutEndpoint_def) - apply (cases extras; cases extras'; clarsimp) - apply (fastforce simp: check_handler_ep_def unlessE_def returnOk_def bindE_def - newroot_rel_def emptyTCCaps_def throwError_def - dest: cap_rel_valid_fh) + apply (cases "length extras < 1") + apply (clarsimp split: list.split simp: list_all2_Cons2) + apply (clarsimp simp: list_all2_Cons1 neq_Nil_conv val_le_length_Cons linorder_not_less) + apply (rule corres_guard_imp) + apply (rule corres_splitEE[OF _ decodeHandlerEP_corres]) + apply (rule corres_returnOkTT) + apply (clarsimp simp: newroot_rel_def emptyTCCaps_def) + apply clarsimp+ + apply wpsimp+ done lemma decodeTCBInvocation_corres: @@ -3599,7 +3661,7 @@ lemma decodeSetTLSBase_wf: lemma decodeSetTimeoutEndpoint_wf[wp]: "\invs' and tcb_at' t and ex_nonz_cap_to' t and cte_at' slot and (\s. \x \ set extras. s \' fst x \ cte_at' (snd x) s)\ - decodeSetTimeoutEndpoint (ThreadCap t) slot extras + decodeSetTimeoutEndpoint args (ThreadCap t) slot extras \tcb_inv_wf'\,-" apply (simp add: decodeSetTimeoutEndpoint_def emptyTCCaps_def cong: list.case_cong) diff --git a/spec/abstract/Decode_A.thy b/spec/abstract/Decode_A.thy index 14bd2708d1..9f2abddaae 100644 --- a/spec/abstract/Decode_A.thy +++ b/spec/abstract/Decode_A.thy @@ -258,12 +258,36 @@ definition has_handler_rights :: "cap \ bool" where definition valid_fault_handler :: "cap \ bool" where "valid_fault_handler \ is_ep_cap and has_handler_rights or (=) NullCap" -definition - check_handler_ep :: "nat \ (cap \ cslot_ptr) \ ((cap \ cslot_ptr),'z::state_ext) se_monad" -where - "check_handler_ep pos h_cap_h_slot \ doE - unlessE (valid_fault_handler $ fst h_cap_h_slot) $ throwError $ InvalidCapability pos; - returnOk h_cap_h_slot +definition decode_handler_ep :: + "data list \ nat \ (cap \ cslot_ptr) list \ ((cap \ cslot_ptr),'z::state_ext) se_monad" + where + "decode_handler_ep args cap_pos excaps \ doE + fh_arg \ returnOk $ excaps ! 0; + fh_cap \ returnOk $ fst fh_arg; + fh_slot \ returnOk $ snd fh_arg; + unlessE (is_ep_cap fh_cap \ fh_cap = NullCap) $ throwError $ InvalidCapability cap_pos; + fh_cap \ + if length args \ 1 + then + let fh_data = args ! 0 + in if fh_cap \ NullCap \ fh_data \ 0 + then doE + fh_cap \ returnOk $ update_cap_data False fh_data fh_cap; + whenE (fh_cap = NullCap) $ throwError IllegalOperation; + returnOk fh_cap + odE + else returnOk fh_cap + else returnOk fh_cap; + fh_cap \ + if length args \ 2 + then doE + fh_rights \ returnOk $ args ! 1; + returnOk $ mask_cap (data_to_rights fh_rights) fh_cap + odE + else returnOk fh_cap; + fh_cap \ derive_cap fh_slot fh_cap; + unlessE (valid_fault_handler fh_cap) $ throwError $ InvalidCapability cap_pos; + returnOk (fh_cap, fh_slot) odE" definition @@ -310,8 +334,7 @@ where "decode_set_space args cap slot excaps \ doE whenE (length args < 2 \ length excaps < 3) $ throwError TruncatedMessage; space \ decode_cv_space (take 2 args) cap slot (take 2 (drop 1 excaps)); - fh_arg \ returnOk $ excaps ! 0; - fault_handler \ check_handler_ep 1 fh_arg; + fault_handler \ decode_handler_ep (drop 2 args) 1 (take 1 excaps); returnOk $ ThreadControlCaps (obj_ref_of cap) slot (Some fault_handler) None (tc_new_croot space) (tc_new_vroot space) None odE" @@ -360,12 +383,11 @@ where definition decode_set_timeout_ep :: - "cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" + "data list \ cap \ cslot_ptr \ (cap \ cslot_ptr) list \ (tcb_invocation,'z::state_ext) se_monad" where - "decode_set_timeout_ep cap slot extra_caps \ doE + "decode_set_timeout_ep args cap slot extra_caps \ doE whenE (length extra_caps < 1) $ throwError TruncatedMessage; - th_arg \ returnOk $ extra_caps ! 0; - handler \ check_handler_ep 1 th_arg; + handler \ decode_handler_ep args 1 (take 1 extra_caps); returnOk $ ThreadControlCaps (obj_ref_of cap) slot None (Some handler) None None None odE" @@ -426,14 +448,13 @@ where new_prio \ returnOk $ ucast $ args ! 1; auth_cap \ returnOk $ fst $ extra_caps ! 0; sc_cap \ returnOk $ fst $ extra_caps ! 1; - fh_arg \ returnOk $ extra_caps ! 2; auth_tcb \ case auth_cap of ThreadCap tcb_ptr \ returnOk tcb_ptr | _ \ throwError (InvalidCapability 1); check_prio (args ! 0) auth_tcb; check_prio (args ! 1) auth_tcb; sc \ decode_update_sc cap slot sc_cap; - fh \ check_handler_ep 3 fh_arg; + fh \ decode_handler_ep (drop 2 args) 3 (take 1 (drop 2 extra_caps)); returnOk $ ThreadControlSched (obj_ref_of cap) slot (Some fh) (Some (new_mcp, auth_tcb)) (Some (new_prio, auth_tcb)) (Some sc) @@ -455,7 +476,7 @@ where | TCBSetPriority \ decode_set_priority args cap slot excs | TCBSetMCPriority \ decode_set_mcpriority args cap slot excs | TCBSetSchedParams \ decode_set_sched_params args cap slot excs - | TCBSetTimeoutEndpoint \ decode_set_timeout_ep cap slot excs + | TCBSetTimeoutEndpoint \ decode_set_timeout_ep args cap slot excs | TCBSetIPCBuffer \ decode_set_ipc_buffer args cap slot excs | TCBSetSpace \ decode_set_space args cap slot excs | TCBBindNotification \ decode_bind_notification cap excs diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy index 062d402c8a..fd42ad2689 100644 --- a/spec/design/skel/Structures_H.thy +++ b/spec/design/skel/Structures_H.thy @@ -41,8 +41,8 @@ requalify_consts end -#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isThreadCap isSchedContextCap scBitsFromRefillLength scBitsFromRefillLength' objBitsKO -#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isThreadCap isSchedContextCap scBitsFromRefillLength' scBitsFromRefillLength objBitsKO +#INCLUDE_HASKELL SEL4/Object/Structures.lhs decls_only NOT isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isEndpointCap isThreadCap isSchedContextCap scBitsFromRefillLength scBitsFromRefillLength' objBitsKO +#INCLUDE_HASKELL SEL4/Object/Structures.lhs bodies_only NOT kernelObjectTypeName isNullCap isUntypedCap isIRQControlCap isReplyCap isDomainCap isNotificationCap isEndpointCap isThreadCap isSchedContextCap scBitsFromRefillLength' scBitsFromRefillLength objBitsKO definition scBitsFromRefillLength' :: "nat => nat" where diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs index 6c47955694..3a3960873f 100644 --- a/spec/haskell/src/SEL4/Object/Structures.lhs +++ b/spec/haskell/src/SEL4/Object/Structures.lhs @@ -119,6 +119,10 @@ This is the type used to represent a capability. > isNotificationCap (NotificationCap {}) = True > isNotificationCap _ = False +> isEndpointCap :: Capability -> Bool +> isEndpointCap (EndpointCap {}) = True +> isEndpointCap _ = False + > isSchedContextCap :: Capability -> Bool > isSchedContextCap (SchedContextCap {}) = True > isSchedContextCap _ = False diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 2f804732de..9956579adf 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -87,7 +87,7 @@ There are eleven types of invocation for a thread control block. All require wri > TCBSetMCPriority -> decodeSetMCPriority args cap extraCaps > TCBSetSchedParams -> decodeSetSchedParams args cap slot extraCaps > TCBSetIPCBuffer -> decodeSetIPCBuffer args cap slot extraCaps -> TCBSetTimeoutEndpoint -> decodeSetTimeoutEndpoint cap slot extraCaps +> TCBSetTimeoutEndpoint -> decodeSetTimeoutEndpoint args cap slot extraCaps > TCBSetSpace -> decodeSetSpace args cap slot extraCaps > TCBBindNotification -> decodeBindNotification cap extraCaps > TCBUnbindNotification -> decodeUnbindNotification cap @@ -256,7 +256,7 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > decodeSetSchedParams :: [Word] -> Capability -> PPtr CTE -> [(Capability, PPtr CTE)] -> > KernelF SyscallError TCBInvocation -> decodeSetSchedParams (newMCP : newPrio : _) cap slot ((authCap, _) : (scCap, _) : (fhCap, fhSlot) : _) = do +> decodeSetSchedParams (newMCP:newPrio:args) cap slot ((authCap, _):(scCap, _):fhArg:_) = do > authTCB <- case authCap of > ThreadCap { capTCBPtr = tcbPtr } -> return tcbPtr > _ -> throw $ InvalidCapability 1 @@ -280,11 +280,11 @@ The "SetSchedParams" call sets both the priority and the MCP in a single call. > when (tcbPtr == curTcbPtr) $ throw IllegalOperation > return Nothing > _ -> throw $ InvalidCapability 2 -> when (not $ isValidFaultHandler fhCap) $ throw $ InvalidCapability 3 +> faultHandler <- decodeHandlerEP args 3 [fhArg] > return $ ThreadControlSched { > tcSchedTarget = tcbPtr, > tcSchedSlot = slot, -> tcSchedFaultHandler = Just (fhCap, fhSlot), +> tcSchedFaultHandler = Just faultHandler, > tcSchedMCPriority = Just (fromIntegral newMCP, authTCB), > tcSchedPriority = Just (fromIntegral newPrio, authTCB), > tcSchedSchedContext = Just scPtr } @@ -352,14 +352,35 @@ This is to ensure that the source capability is not made invalid by the deletion > tcCapsBuffer = Nothing } > decodeCVSpace _ _ _ _ = throw TruncatedMessage +> decodeHandlerEP :: [Word] -> Int -> [(Capability, PPtr CTE)] -> +> KernelF SyscallError (Capability, PPtr CTE) +> decodeHandlerEP args pos ((fhCap, fhSlot):_) = do +> unless (isEndpointCap fhCap || isNullCap fhCap) $ throw $ InvalidCapability pos +> fhCap' <- if length args >= 1 +> then +> let fhData = args !! 0 +> in if not (isNullCap fhCap) && fhData /= 0 +> then do +> let fhDataCap = updateCapData False fhData fhCap +> when (isNullCap fhDataCap) $ throw IllegalOperation +> return fhDataCap +> else return fhCap +> else return fhCap +> fhCap'' <- if length args >= 2 +> then do +> let fhRights = args !! 1 +> return $ maskCapRights (rightsFromWord fhRights) fhCap' +> else return fhCap' +> fhCap''' <- deriveCap fhSlot fhCap'' +> unless (isValidFaultHandler fhCap''') $ throw $ InvalidCapability pos +> return (fhCap''', fhSlot) +> decodeHandlerEP _ _ _ = throw TruncatedMessage + > decodeSetSpace :: [Word] -> Capability -> PPtr CTE -> > [(Capability, PPtr CTE)] -> KernelF SyscallError TCBInvocation -> decodeSetSpace (cRootData:vRootData:_) cap slot (fhArg:cRootArg:vRootArg:_) = do +> decodeSetSpace (cRootData:vRootData:args) cap slot (fhArg:cRootArg:vRootArg:_) = do > space <- decodeCVSpace [cRootData,vRootData] cap slot [cRootArg,vRootArg] -> let (fhCap, fhSlot) = fhArg -> faultHandler <- if isValidFaultHandler fhCap -> then return (fhCap, fhSlot) -> else throw $ InvalidCapability 1 +> faultHandler <- decodeHandlerEP args 1 [fhArg] > return $ ThreadControlCaps { > tcCapsTarget = capTCBPtr cap, > tcCapsSlot = slot, @@ -370,18 +391,14 @@ This is to ensure that the source capability is not made invalid by the deletion > tcCapsBuffer = Nothing } > decodeSetSpace _ _ _ _ = throw TruncatedMessage -> decodeSetTimeoutEndpoint :: Capability -> PPtr CTE -> +> decodeSetTimeoutEndpoint :: [Word] -> Capability -> PPtr CTE -> > [(Capability, PPtr CTE)] -> KernelF SyscallError TCBInvocation -> decodeSetTimeoutEndpoint cap slot (thArg:_) -> = do -> let (thCap, thSlot) = thArg -> timeoutHandler <- if isValidFaultHandler thCap -> then return (thCap, thSlot) -> else throw $ InvalidCapability 1 +> decodeSetTimeoutEndpoint args cap slot (thArg:_) = do +> timeoutHandler <- decodeHandlerEP args 1 [thArg] > return $ (emptyTCCaps $ capTCBPtr cap) { > tcCapsSlot = slot, > tcCapsTimeoutHandler = Just timeoutHandler } -> decodeSetTimeoutEndpoint _ _ _ = throw TruncatedMessage +> decodeSetTimeoutEndpoint _ _ _ _ = throw TruncatedMessage \subsubsection{Decode Bound Notification Invocations}