From 39666e43c01ce9bed36b034dd4ef6963f526b569 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 2 Mar 2024 11:44:35 +0100 Subject: [PATCH] capDL-api: restyle IRQ_DP Fix + modernise style and proofs. Signed-off-by: Gerwin Klein --- proof/capDL-api/IRQ_DP.thy | 568 +++++++++++++++++-------------------- 1 file changed, 255 insertions(+), 313 deletions(-) diff --git a/proof/capDL-api/IRQ_DP.thy b/proof/capDL-api/IRQ_DP.thy index 6f4a1ec470..82ae7f64f0 100644 --- a/proof/capDL-api/IRQ_DP.thy +++ b/proof/capDL-api/IRQ_DP.thy @@ -9,145 +9,120 @@ imports TCB_DP begin lemma delete_cap_simple_format: - "\c cap \* R> and K (\ ep_related_cap cap)\ (\s. delete_cap_simple ptr s) \\_. c NullCap \* R>\" - apply (clarsimp simp: pred_conj_def) - apply (rule delete_cap_simple_wp) -done - -lemma sep_map_i_cdl_irq: "irq irq_obj \* R> s \ cdl_irq_node s irq = irq_obj" - apply (clarsimp simp: sep_map_c_def sep_map_irq_def sep_conj_def sep_state_projection_def plus_sep_state_def sep_state_add_def) - apply (clarsimp simp: map_add_def) + "\c cap \* R> and K (\ ep_related_cap cap)\ + delete_cap_simple ptr + \\_. c NullCap \* R>\" + by (clarsimp simp: pred_conj_def delete_cap_simple_wp) + +lemma sep_map_i_cdl_irq: + "irq irq_obj \* R> s \ cdl_irq_node s irq = irq_obj" + apply (clarsimp simp: sep_map_c_def sep_map_irq_def sep_conj_def sep_state_projection_def + plus_sep_state_def sep_state_add_def map_add_def) apply (drule fun_cong[where x=irq]) - apply (clarsimp split: option.splits) - apply (clarsimp simp: sep_disj_sep_state_def sep_state_disj_def) + apply (clarsimp simp: sep_disj_sep_state_def sep_state_disj_def split: option.splits) by (metis (lifting) fun_upd_same map_disj_None_left' option.distinct(1)) lemma sep_map_i_map_c: "irq irq_obj \* (irq_obj, 0) \c cap \* R> s \ irq irq_obj \* (get_irq_slot irq s \c cap) \* R> s" - by (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) - + by (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) lemma invoke_irq_handler_clear_handler_wp: "\< irq \irq obj \* (obj, 0) \c cap \* R> and K (\ ep_related_cap cap)\ - invoke_irq_handler (ClearIrqHandler irq) + invoke_irq_handler (ClearIrqHandler irq) \\_. < irq \irq obj \* (obj, 0) \c NullCap \* R> \" - apply (clarsimp simp: invoke_irq_handler_def, wp) - apply (sep_wp delete_cap_simple_format[where cap=cap])+ - apply (safe) - apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) - apply (sep_solve) - apply (clarsimp) + unfolding invoke_irq_handler_def + apply clarsimp + apply (wp sep_wp: delete_cap_simple_format[where cap=cap]) + apply clarsimp + apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) + apply sep_solve done lemma invoke_irq_handler_set_handler_wp: - "\< irq \irq obj \* (obj, 0) \c cap' \* R> and - K (\ ep_related_cap cap' \ \ is_untyped_cap cap)\ - invoke_irq_handler (SetIrqHandler irq cap slot) - \\_. < irq \irq obj \* (obj, 0) \c cap \* R> \" - apply (clarsimp simp: invoke_irq_handler_def, wp) - apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp)+ - apply (sep_wp delete_cap_simple_format[where cap=cap'])+ - apply (safe) - apply (clarsimp) - apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) - apply (sep_solve) - apply (clarsimp) + "\irq obj \* (obj, 0) \c cap' \* R> and K (\ ep_related_cap cap' \ \ is_untyped_cap cap)\ + invoke_irq_handler (SetIrqHandler irq cap slot) + \\_. irq obj \* (obj, 0) \c cap \* R> \" + unfolding invoke_irq_handler_def + apply clarsimp + apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp + delete_cap_simple_format[where cap=cap']) + apply clarsimp + apply (frule sep_map_i_cdl_irq, clarsimp simp: get_irq_slot_def) + apply sep_solve done lemma invoke_irq_control_issue_handler_wp: - "\ <(dest_slot) \c cap \* R> \ - invoke_irq_control (IssueIrqHandler irq control_slot dest_slot) - \\_. < (dest_slot) \c (IrqHandlerCap irq) \* R> \" - apply (clarsimp simp: invoke_irq_control_def, wp sep_wp: insert_cap_child_wp) - apply (clarsimp) - apply (sep_safe,sep_solve) -done - + "\ c cap \* R> \ + invoke_irq_control (IssueIrqHandler irq control_slot dest_slot) + \\_. c IrqHandlerCap irq \* R> \" + by (clarsimp simp: invoke_irq_control_def | wp sep_wp: insert_cap_child_wp | sep_solve)+ lemma decode_invocation_irq_ack_rv': -"\\s. P (AckIrq (the $ cdl_cap_irq cap)) s \ -decode_irq_handler_invocation cap cap_ref caps (IrqHandlerAckIntent) -\P\, -" - apply (clarsimp simp: decode_irq_handler_invocation_def) - apply wp - apply (clarsimp) -done + "\\s. P (AckIrq (the $ cdl_cap_irq cap)) s \ + decode_irq_handler_invocation cap cap_ref caps IrqHandlerAckIntent + \P\, -" + by (wpsimp simp: decode_irq_handler_invocation_def) lemma decode_invocation_irq_clear_rv': -"\\s. P (ClearIrqHandler (the $ cdl_cap_irq cap)) s \ -decode_irq_handler_invocation cap cap_ref caps (IrqHandlerClearIntent) -\P\, -" - apply (clarsimp simp: decode_irq_handler_invocation_def) - apply wp - apply (clarsimp) -done - -lemma irq_inner_lemma: "\\s. P i s \ a = (NotificationCap x y z) \ case a of NotificationCap x xa xb \ returnOk () | _ \ throw \P\, -" - apply (unfold validE_R_def) - apply (rule hoare_name_pre_stateE) - apply (clarsimp) - apply (wp, clarsimp) -done - + "\\s. P (ClearIrqHandler (the $ cdl_cap_irq cap)) s \ + decode_irq_handler_invocation cap cap_ref caps IrqHandlerClearIntent + \P\, -" + by (wpsimp simp: decode_irq_handler_invocation_def) (* Move next to hoare_gen_asm_conj *) lemma validE_R_gen_asm_conj: "(P \ \P'\ f \Q\, -) \ \\s. P' s \ P\ f \Q\, -" by (fastforce simp: validE_R_def validE_def valid_def) - lemma decode_invocation_irq_endpoint_rv': -"\\s. P (SetIrqHandler (the $ cdl_cap_irq cap) endpoint_cap endpoint_ptr) s \ caps = [(endpoint_cap, endpoint_ptr)]@xs \ - is_ntfn_cap endpoint_cap \ -decode_irq_handler_invocation cap cap_ref caps (IrqHandlerSetEndpointIntent) -\P\, -" + "\\s. P (SetIrqHandler (the $ cdl_cap_irq cap) endpoint_cap endpoint_ptr) s \ + caps = [(endpoint_cap, endpoint_ptr)] @ xs \ is_ntfn_cap endpoint_cap\ + decode_irq_handler_invocation cap cap_ref caps IrqHandlerSetEndpointIntent + \P\, -" apply (rule validE_R_gen_asm_conj) - apply (clarsimp simp: decode_irq_handler_invocation_def) - apply (wp | wpc)+ - apply (clarsimp split: cdl_cap.splits, safe) - apply ((wp throw_on_none_rv)+, clarsimp simp: get_index_def) - apply simp + apply (wpsimp simp: decode_irq_handler_invocation_def get_index_def wp: throw_on_none_rv) done lemma decode_irq_control_issue_irq_rv: -"\\s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \ - caps = (root_cap, root_ptr)#xs \ (unat depth) \ word_bits \ 0 < (unat depth) \ + "\\s. P (IssueIrqHandler irq target_ref (cap_object root_cap, offset index r)) s \ + caps = (root_cap, root_ptr) # xs \ unat depth \ word_bits \ 0 < unat depth \ <\ (r, (unat depth)) : root_cap index \u cap \* R> s\ - decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \P\, -" + decode_irq_control_invocation target target_ref caps + (IrqControlIssueIrqHandlerIntent irq index depth) + \P\, -" apply (clarsimp simp: decode_irq_control_invocation_def) apply (wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv) apply (clarsimp simp: get_index_def) - apply (sep_solve) -done - -schematic_goal lookup_extra_caps_once_wp: "\?P\ lookup_extra_caps root_tcb_id [endpoint_cptr] \Q\, \Q'\" -apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp) - apply (rule lookup_cap_and_slot_rvu) -done - -lemma reset_cap_cdl_cap_irq: "reset_cap_asid c = IrqHandlerCap irq \ the (cdl_cap_irq c) = irq" - apply (clarsimp simp: reset_cap_asid_def cdl_cap_irq_def the_def split: cdl_cap.splits) -done + apply sep_solve + done -lemma not_memory_reset: "\ is_memory_cap (reset_cap_asid cap) \ reset_cap_asid cap = cap " - apply (clarsimp simp: is_memory_cap_def reset_cap_asid_def split:cdl_cap.splits) -done +schematic_goal lookup_extra_caps_once_wp: + "\?P\ lookup_extra_caps root_tcb_id [endpoint_cptr] \Q\, \Q'\" + apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp) + apply (rule lookup_cap_and_slot_rvu) + done -lemma not_ep_related_reset_cap_asid: "reset_cap_asid c = IrqControlCap \ \ep_related_cap c" - apply (clarsimp simp: reset_cap_asid_def ep_related_cap_def split: cdl_cap.splits) -done +lemma reset_cap_cdl_cap_irq: + "reset_cap_asid c = IrqHandlerCap irq \ the (cdl_cap_irq c) = irq" + by (clarsimp simp: reset_cap_asid_def cdl_cap_irq_def the_def split: cdl_cap.splits) -lemma reset_cap_asid_control: "reset_cap_asid c = reset_cap_asid cap \ is_irqcontrol_cap cap \ is_irqcontrol_cap c" - apply (clarsimp simp: reset_cap_asid_def is_irqcontrol_cap_def split: cdl_cap.splits) -done +lemma not_memory_reset: + "\ is_memory_cap (reset_cap_asid cap) \ reset_cap_asid cap = cap " + by (clarsimp simp: is_memory_cap_def reset_cap_asid_def split:cdl_cap.splits) +lemma not_ep_related_reset_cap_asid: + "reset_cap_asid c = IrqControlCap \ \ep_related_cap c" + by (clarsimp simp: reset_cap_asid_def ep_related_cap_def split: cdl_cap.splits) +lemma reset_cap_asid_control: + "reset_cap_asid c = reset_cap_asid cap \ is_irqcontrol_cap cap \ is_irqcontrol_cap c" + by (clarsimp simp: reset_cap_asid_def is_irqcontrol_cap_def split: cdl_cap.splits) -(* Note: the cap from the TCB and the cap in the CNode, both pointing to the root CNode, should be different, - but this breaks the proof.*) +(* Note: the cap from the TCB and the cap in the CNode, both pointing to the root CNode, should be + different, but this breaks the proof.*) lemma seL4_IRQHandler_IRQControl_Get_helper: - assumes unify : "irq_cap = IrqHandlerCap irq \ + assumes unify: "irq_cap = IrqHandlerCap irq \ target_index = offset node_index root_size \ root_index = offset croot root_size \ control_index = offset control_cap root_size \ @@ -155,96 +130,84 @@ lemma seL4_IRQHandler_IRQControl_Get_helper: control_ptr = (cap_object root_cap, control_index) \ root_ptr = (cap_object root_cap, root_index) \ root_tcb = Tcb t" -shows "\\root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* irq \irq obj \* - cap_object root_cap \f CNode (empty_cnode root_size) \* - (root_tcb_id, tcb_cspace_slot) \c root_cap \* - control_ptr \c c_cap \* target_ptr \c target_cap \* root_ptr \c root_cap \* R \ - and K ( \ ep_related_cap c_cap \ one_lvl_lookup root_cap word_bits root_size \ - one_lvl_lookup root_cap (unat node_depth) root_size \ - guard_equal root_cap node_index (unat node_depth) \ - guard_equal root_cap croot word_bits \ - guard_equal root_cap control_cap word_bits \ - guard_equal root_cap node_index word_bits \ - unat node_depth \ word_bits \ 0 < unat node_depth \ - is_irqcontrol_cap c_cap \ is_cnode_cap root_cap \ is_cnode_cap root_cap)\ - seL4_IRQControl_Get control_cap irq croot node_index node_depth - \\fail s. \ root_tcb_id \f root_tcb \* - (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* - \ \Root CNode.\ - cap_object root_cap \f CNode (empty_cnode root_size) \* - \ \Cap to the root CNode.\ - (root_tcb_id, tcb_cspace_slot) \c root_cap \* - irq \irq obj \* control_ptr \c c_cap \* target_ptr \c irq_cap \* root_ptr \c root_cap \* R\ s\" + shows + "\\root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + irq \irq obj \* cap_object root_cap \f CNode (empty_cnode root_size) \* + (root_tcb_id, tcb_cspace_slot) \c root_cap \* control_ptr \c c_cap \* + target_ptr \c target_cap \* root_ptr \c root_cap \* R\ and + K (\ ep_related_cap c_cap \ one_lvl_lookup root_cap word_bits root_size \ + one_lvl_lookup root_cap (unat node_depth) root_size \ + guard_equal root_cap node_index (unat node_depth) \ + guard_equal root_cap croot word_bits \ + guard_equal root_cap control_cap word_bits \ + guard_equal root_cap node_index word_bits \ + unat node_depth \ word_bits \ 0 < unat node_depth \ + is_irqcontrol_cap c_cap \ is_cnode_cap root_cap \ is_cnode_cap root_cap)\ + seL4_IRQControl_Get control_cap irq croot node_index node_depth + \\fail. \root_tcb_id \f root_tcb \* + (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + \ \Root CNode\ + cap_object root_cap \f CNode (empty_cnode root_size) \* + \ \Cap to the root CNode\ + (root_tcb_id, tcb_cspace_slot) \c root_cap \* + irq \irq obj \* control_ptr \c c_cap \* target_ptr \c irq_cap \* + root_ptr \c root_cap \* R\\" apply (simp add: seL4_IRQControl_Get_def sep_state_projection2_def) - apply (rule hoare_pre) - apply (wp do_kernel_op_pull_back) - apply (rule call_kernel_with_intent_allow_error_helper - [where check = True and Perror = \ and intent_op = "(IrqControlIntent (IrqControlIssueIrqHandlerIntent irq node_index node_depth))" and tcb = t and intent_cptr = control_cap and intent_extra = "[croot]" ,simplified]) - apply (clarsimp) - apply (rule set_cap_wp[sep_wand_wp]) - apply (rule mark_tcb_intent_error_sep_inv) - apply (wp (once)) - apply (rule corrupt_ipc_buffer_sep_inv) - apply (wp (once)) - apply (rule_tac P = "(iv = (InvokeIrqControl $ (IssueIrqHandler irq control_ptr (cap_object root_cap, offset node_index root_size))))" in hoare_gen_asmEx) - apply (clarsimp simp: unify) - apply (wp invoke_irq_control_issue_handler_wp[sep_wand_wp]) - apply (wp set_cap_wp[sep_wand_wp]) - apply (rule_tac P = "c=IrqControlCap" in hoare_gen_asmEx, simp) - apply (simp add: decode_invocation_def, wp) - apply (rule_tac P = "irq_control_intent=IrqControlIssueIrqHandlerIntent irq node_index node_depth" in hoare_gen_asmE, simp) - apply (wp decode_irq_control_issue_irq_rv[where root_cap=root_cap and root_ptr=root_ptr and xs ="[]" and r = root_size, simplified ]) - apply (simp) - apply (unfold throw_opt_def get_irq_control_intent_def, simp) - apply (rule returnOk_wp) - apply (rule lookup_extra_caps_once_wp[where cap'=root_cap and r=root_size, simplified user_pointer_at_def]) - apply (rule lookup_cap_and_slot_rvu[where cap'=c_cap and r=root_size, simplified user_pointer_at_def]) - apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift - update_thread_intent_update) - apply (clarsimp) - apply (rule conjI) - apply (erule allE impE)+ - apply fastforce - apply (erule conjE allE impE)+ - apply (fastforce) - apply (clarsimp) - apply (rule conjI) - apply (erule allE impE)+ - apply fastforce - apply (erule conjE allE impE)+ - apply (fastforce) - apply (clarsimp) - apply (sep_solve) - apply (intro impI conjI allI) - apply (clarsimp) - apply (clarsimp) - apply (intro impI conjI allI) - apply (sep_solve) - apply (clarsimp simp: unify) - apply (sep_cancel)+ - apply (intro impI conjI allI) + apply (wp do_kernel_op_pull_back) + apply (rule call_kernel_with_intent_allow_error_helper[where + check = True and + Perror = \ and + intent_op = "IrqControlIntent + (IrqControlIssueIrqHandlerIntent irq node_index node_depth)" and + tcb = t and + intent_cptr = control_cap and + intent_extra = "[croot]", simplified]) + apply clarsimp + apply (rule set_cap_wp[sep_wand_wp]) + apply (rule mark_tcb_intent_error_sep_inv) + apply (wp corrupt_ipc_buffer_sep_inv)+ + apply (rule_tac P = "iv = InvokeIrqControl + (IssueIrqHandler irq control_ptr (cap_object root_cap, + offset node_index root_size))" + in hoare_gen_asmEx) + apply (clarsimp simp: unify) + apply (wp invoke_irq_control_issue_handler_wp[sep_wand_wp]) + apply (wp set_cap_wp[sep_wand_wp]) + apply (rule_tac P = "c=IrqControlCap" in hoare_gen_asmEx, simp) + apply (simp add: decode_invocation_def, wp) + apply (rule_tac P = "irq_control_intent=IrqControlIssueIrqHandlerIntent irq node_index node_depth" + in hoare_gen_asmE, simp) + apply (wp decode_irq_control_issue_irq_rv[where root_cap = root_cap and + root_ptr = root_ptr and + xs = "[]" and r = root_size, simplified]) + apply (simp add: throw_opt_def get_irq_control_intent_def) + apply wp + apply (rule lookup_extra_caps_once_wp[where cap'=root_cap and r=root_size, simplified user_pointer_at_def]) + apply (rule lookup_cap_and_slot_rvu[where cap'=c_cap and r=root_size, simplified user_pointer_at_def]) + apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift update_thread_intent_update) + apply clarsimp + apply (rule conjI, fastforce)+ + apply sep_solve + apply (intro impI conjI allI; clarsimp) + apply (intro impI conjI allI; clarsimp simp: unify) apply sep_solve - apply (clarsimp simp: unify) - apply sep_solve - apply (clarsimp simp: unify) + apply sep_cancel+ + apply (intro impI conjI allI; sep_solve) apply fastforce - apply (clarsimp simp: unify) apply (metis is_cnode_cap_not_memory_cap not_memory_cap_reset_asid') - apply (clarsimp simp: unify) apply fastforce - apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) + apply (clarsimp simp: user_pointer_at_def Let_def) apply sep_solve - apply (drule reset_cap_asid_control, assumption, clarsimp simp: is_irqcontrol_cap_def) - apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) + apply (drule (1) reset_cap_asid_control, clarsimp simp: is_irqcontrol_cap_def) + apply (clarsimp simp: user_pointer_at_def Let_def) apply sep_solve - apply (clarsimp simp: unify) apply (drule reset_cap_asid_ep_related_cap) apply clarsimp - apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) + apply (clarsimp simp: user_pointer_at_def Let_def unify) apply sep_solve apply (clarsimp simp: unify) apply sep_solve -done + done lemma obj_tcb_simp [simp]: "is_tcb tcb \ Tcb (obj_tcb tcb) = tcb" @@ -273,170 +236,149 @@ lemma seL4_IRQHandler_IRQControl_Get: guard_equal cnode_cap control_cap word_bits \ guard_equal cnode_cap node_index word_bits \ unat node_depth \ word_bits \ 0 < unat node_depth)\ - seL4_IRQControl_Get control_cap irq croot node_index node_depth + seL4_IRQControl_Get control_cap irq croot node_index node_depth \\fail. \root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* - \ \Cap to the root CNode.\ + \ \Cap to the root CNode\ (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* irq \irq irq_id \* - \ \Root CNode.\ + \ \Root CNode\ cnode_id \f CNode (empty_cnode root_size) \* (cnode_id, control_index) \c IrqControlCap \* (cnode_id, root_index) \c cnode_cap \* (cnode_id, target_index) \c IrqHandlerCap irq \* R\\" apply (rule hoare_gen_asm, elim conjE) apply (sep_wp seL4_IRQHandler_IRQControl_Get_helper [where t="obj_tcb root_tcb"]) - apply (rule conjI, simp)+ - apply simp - apply simp - apply (rule conjI) - apply sep_solve - apply (clarsimp simp: is_irqcontrol_cap_def ep_related_cap_def split: cdl_cap.splits) + apply fastforce + apply clarsimp + apply (rule conjI, sep_solve) + apply (clarsimp simp: is_irqcontrol_cap_def ep_related_cap_def) done - - - - lemma seL4_IRQHandler_SetEndpoint_wp_helper: - assumes unify : "irq_cap = IrqHandlerCap irq \ - offset endpoint_cptr root_size = irq_handler_slot \ endpoint_ptr = (cnode_id, irq_handler_slot) \ + assumes unify: "irq_cap = IrqHandlerCap irq \ + offset endpoint_cptr root_size = irq_handler_slot \ + endpoint_ptr = (cnode_id, irq_handler_slot) \ irq_ptr = (cnode_id, offset irq_handler_cap root_size) \ root_tcb = Tcb t \ cnode_id = cap_object cnode_cap" - -shows "\\root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* irq \irq obj \* (obj, 0) \c cap' \* - cnode_id \f CNode (empty_cnode root_size) \* (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* (endpoint_ptr) \c endpoint_cap \* irq_ptr \c irq_cap \* R \ - and K (\ ep_related_cap cap' \ \ ep_related_cap irq_cap \ \is_untyped_cap endpoint_cap \ \is_memory_cap endpoint_cap \ one_lvl_lookup cnode_cap word_bits root_size \ - guard_equal cnode_cap endpoint_cptr word_bits \ is_ntfn_cap endpoint_cap \ - guard_equal cnode_cap irq_handler_cap word_bits \ - is_cnode_cap cnode_cap \ is_irqhandler_cap irq_cap )\ - seL4_IRQHandler_SetEndpoint irq_handler_cap endpoint_cptr - \\fail s. \ root_tcb_id \f root_tcb \* - (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* - - \ \Root CNode.\ - cnode_id \f CNode (empty_cnode root_size) \* - \ \Cap to the root CNode.\ - (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* - (endpoint_ptr) \c endpoint_cap \* - irq \irq obj \* (obj, 0) \c endpoint_cap \* irq_ptr \c irq_cap \* R\ s\" + shows + "\\root_tcb_id \f root_tcb \* (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + irq \irq obj \* (obj, 0) \c cap' \* cnode_id \f CNode (empty_cnode root_size) \* + (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* endpoint_ptr \c endpoint_cap \* + irq_ptr \c irq_cap \* R\ and + K (\ep_related_cap cap' \ \ep_related_cap irq_cap \ \is_untyped_cap endpoint_cap \ + \is_memory_cap endpoint_cap \ one_lvl_lookup cnode_cap word_bits root_size \ + guard_equal cnode_cap endpoint_cptr word_bits \ is_ntfn_cap endpoint_cap \ + guard_equal cnode_cap irq_handler_cap word_bits \ + is_cnode_cap cnode_cap \ is_irqhandler_cap irq_cap)\ + seL4_IRQHandler_SetEndpoint irq_handler_cap endpoint_cptr + \\fail. \root_tcb_id \f root_tcb \* + (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + \ \Root CNode\ + cnode_id \f CNode (empty_cnode root_size) \* + \ \Cap to the root CNode\ + (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* + endpoint_ptr \c endpoint_cap \* + irq \irq obj \* (obj, 0) \c endpoint_cap \* irq_ptr \c irq_cap \* R\\" apply (simp add: seL4_IRQHandler_SetEndpoint_def sep_state_projection2_def) - apply (rule hoare_pre) - apply (wp do_kernel_op_pull_back) - apply (rule call_kernel_with_intent_allow_error_helper - [where check = True and Perror = \ and intent_op = "(IrqHandlerIntent IrqHandlerSetEndpointIntent)" and tcb = t and intent_cptr = irq_handler_cap and intent_extra = "[endpoint_cptr]" ,simplified]) - apply (clarsimp) - apply (rule set_cap_wp[sep_wand_wp]) - apply (rule mark_tcb_intent_error_sep_inv) - apply (wp (once)) - apply (rule corrupt_ipc_buffer_sep_inv) - apply (wp (once)) - apply (rule_tac P = "(iv = (InvokeIrqHandler $ SetIrqHandler (the $ cdl_cap_irq irq_cap) endpoint_cap endpoint_ptr))" in hoare_gen_asmEx) - apply (clarsimp) - apply (wp) - apply (wp sep_wp: invoke_irq_handler_set_handler_wp) - apply (wp sep_wp: set_cap_wp) - apply (rule_tac P = "c=irq_cap" in hoare_gen_asmEx, simp) - apply (simp add: unify decode_invocation_def) - apply (wp) - apply (rule_tac P = "x = (IrqHandlerSetEndpointIntent)" in hoare_gen_asmE, simp) - apply (wp decode_invocation_irq_endpoint_rv'[where endpoint_cap=endpoint_cap and endpoint_ptr = endpoint_ptr and xs = "[]"]) - apply (unfold throw_opt_def get_irq_handler_intent_def, simp) - apply (rule returnOk_wp) - apply (rule lookup_extra_caps_once_wp[where cap'=endpoint_cap and r=root_size]) - apply (rule lookup_cap_and_slot_rvu[where cap'=irq_cap and r=root_size]) - apply (wp hoare_vcg_ball_lift hoare_vcg_imp_lift hoare_vcg_ex_lift hoare_vcg_all_lift update_thread_intent_update) - apply (clarsimp) - apply (rule conjI) - apply (erule allE impE)+ - apply fastforce - apply (erule conjE allE impE)+ - apply (fastforce) - apply (clarsimp) - apply (rule conjI) - apply (erule allE impE)+ - apply fastforce - apply (erule conjE allE impE)+ - apply (fastforce) - apply (clarsimp) - apply (sep_solve) - apply (clarsimp) - apply (intro impI conjI) - apply (clarsimp simp: unify) - apply (intro impI conjI allI) - apply (sep_solve) - apply (sep_cancel)+ - apply (intro impI conjI allI) - apply (sep_cancel)+ - apply (frule reset_cap_cdl_cap_irq ) - apply (clarsimp simp: unify ) - apply (sep_cancel)+ - apply (safe) - apply (sep_solve) - apply (sep_cancel)+ - apply (erule sep_map_c_asid_reset'' ) - apply (clarsimp simp: unify the_def ) - apply (clarsimp simp: unify) - apply (clarsimp simp: not_memory_reset) - apply (fastforce) - defer - apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) - apply (sep_cancel)+ - apply (metis ep_related_cap_reset_simp) - apply (sep_cancel)+ - apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) - apply sep_solve - apply (clarsimp simp: unify) + apply (wp do_kernel_op_pull_back) + apply (rule call_kernel_with_intent_allow_error_helper[where + check = True and + Perror = \ and + intent_op = "IrqHandlerIntent IrqHandlerSetEndpointIntent" and + tcb = t and + intent_cptr = irq_handler_cap and + intent_extra = "[endpoint_cptr]", simplified]) + apply clarsimp + apply (wp set_cap_wp[sep_wand_wp] mark_tcb_intent_error_sep_inv)+ + apply (rule_tac P = "iv = InvokeIrqHandler (SetIrqHandler (the $ cdl_cap_irq irq_cap) + endpoint_cap endpoint_ptr)" + in hoare_gen_asmEx) + apply clarsimp + apply (wp sep_wp: invoke_irq_handler_set_handler_wp set_cap_wp)+ + apply (rule_tac P = "c=irq_cap" in hoare_gen_asmEx) + apply (simp add: unify decode_invocation_def) + apply wp + apply (rule_tac P = "x = IrqHandlerSetEndpointIntent" in hoare_gen_asmE, simp) + apply (wp decode_invocation_irq_endpoint_rv'[where endpoint_cap=endpoint_cap and + endpoint_ptr = endpoint_ptr and + xs = "[]"]) + apply (wpsimp simp: throw_opt_def get_irq_handler_intent_def) + apply (rule lookup_extra_caps_once_wp[where cap'=endpoint_cap and r=root_size]) + apply (rule lookup_cap_and_slot_rvu[where cap'=irq_cap and r=root_size]) + apply (wp hoare_vcg_ball_lift hoare_vcg_imp_lift hoare_vcg_ex_lift hoare_vcg_all_lift + update_thread_intent_update) + apply clarsimp + apply (rule conjI, fastforce)+ + apply sep_solve + apply (clarsimp simp: unify) + apply (intro impI conjI) + apply clarsimp + apply (intro impI conjI allI) + apply sep_solve + apply sep_cancel+ + apply (intro impI conjI allI) + apply sep_cancel+ + apply (frule reset_cap_cdl_cap_irq) + apply clarsimp + apply sep_cancel+ + apply safe + apply sep_solve + apply sep_cancel+ + apply (erule sep_map_c_asid_reset'') + apply fastforce + apply clarsimp + apply (fastforce simp: not_memory_reset) + apply (clarsimp dest!: reset_cap_asid_simps2) + apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) apply sep_solve - apply (clarsimp dest!: reset_cap_asid_simps2) -done + apply (metis ep_related_cap_reset_simp) + apply (clarsimp simp: user_pointer_at_def Let_unfold sep_conj_assoc unify) + apply sep_solve + apply sep_solve + done lemma seL4_IRQHandler_SetEndpoint_wp: "\\root_tcb_id \f root_tcb \* - (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* - \ \Root CNode.\ - cnode_id \f CNode (empty_cnode root_size) \* - \ \Cap to the root CNode.\ - (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* - (cnode_id, endpoint_slot) \c endpoint_cap \* - irq \irq irq_id \* - (irq_id, 0) \c old_cap \* - (cnode_id, irq_handler_slot) \c IrqHandlerCap irq \* R \ - and K ( - is_tcb root_tcb \ - cnode_id = cap_object cnode_cap \ - - is_ntfn_cap endpoint_cap \ - is_cnode_cap cnode_cap \ - - \ ep_related_cap old_cap \ - - one_lvl_lookup cnode_cap word_bits root_size \ - guard_equal cnode_cap endpoint_cptr word_bits \ - guard_equal cnode_cap irq_handler_cptr word_bits \ - offset endpoint_cptr root_size = endpoint_slot \ - offset irq_handler_cptr root_size = irq_handler_slot)\ - seL4_IRQHandler_SetEndpoint irq_handler_cptr endpoint_cptr - \\fail. \root_tcb_id \f root_tcb \* - (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* - \ \Root CNode.\ + (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + \ \Root CNode\ cnode_id \f CNode (empty_cnode root_size) \* - \ \Cap to the root CNode.\ - (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* - (cnode_id, endpoint_slot) \c endpoint_cap \* + \ \Cap to the root CNode\ + (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* + (cnode_id, endpoint_slot) \c endpoint_cap \* irq \irq irq_id \* - (irq_id, 0) \c endpoint_cap \* - (cnode_id, irq_handler_slot) \c IrqHandlerCap irq \* R\\" + (irq_id, 0) \c old_cap \* + (cnode_id, irq_handler_slot) \c IrqHandlerCap irq \* R\ and + K (is_tcb root_tcb \ + cnode_id = cap_object cnode_cap \ + is_ntfn_cap endpoint_cap \ + is_cnode_cap cnode_cap \ + \ ep_related_cap old_cap \ + one_lvl_lookup cnode_cap word_bits root_size \ + guard_equal cnode_cap endpoint_cptr word_bits \ + guard_equal cnode_cap irq_handler_cptr word_bits \ + offset endpoint_cptr root_size = endpoint_slot \ + offset irq_handler_cptr root_size = irq_handler_slot)\ + seL4_IRQHandler_SetEndpoint irq_handler_cptr endpoint_cptr + \\fail. \root_tcb_id \f root_tcb \* + (root_tcb_id, tcb_pending_op_slot) \c RunningCap \* + \ \Root CNode\ + cnode_id \f CNode (empty_cnode root_size) \* + \ \Cap to the root CNode\ + (root_tcb_id, tcb_cspace_slot) \c cnode_cap \* + (cnode_id, endpoint_slot) \c endpoint_cap \* + irq \irq irq_id \* + (irq_id, 0) \c endpoint_cap \* + (cnode_id, irq_handler_slot) \c IrqHandlerCap irq \* R\\" apply (rule hoare_gen_asm) - apply (wp seL4_IRQHandler_SetEndpoint_wp_helper [where irq_handler_slot=endpoint_slot - and cap'=old_cap and t="obj_tcb root_tcb"], simp) - apply (rule pred_conjI) - apply sep_solve + apply (wp seL4_IRQHandler_SetEndpoint_wp_helper[where irq_handler_slot=endpoint_slot and + cap'=old_cap and t="obj_tcb root_tcb"]) apply clarsimp - apply (case_tac endpoint_cap, simp_all add: is_memory_cap_def cap_type_def) - apply (case_tac old_cap, simp_all add: ep_related_cap_def cap_type_def) + apply (rule pred_conjI, sep_solve) + apply (case_tac endpoint_cap; simp add: is_memory_cap_def cap_type_def) + apply (case_tac old_cap; simp add: ep_related_cap_def cap_type_def) done end