theory Interrupt_AC

lemma invoke_irq_handler_pas_refined:
  "\<lbrace>pas_refined (aag :: 'a PAS) and invs and irq_handler_inv_valid irq_inv
                                and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace>
   invoke_irq_handler irq_inv
   \<lbrace>\<lambda>_ s. pas_refined aag s\<rbrace>" apply (rule hoare_gen_asm) apply (cases irq_inv, simp_all add: authorised_irq_hdl_inv_def) apply (wp arch_invoke_irq_handler_pas_refined) apply (wp cap_insert_pas_refined_not_transferable delete_one_caps_of_state
          | strengthen invs_mdb | simp add: cte_wp_at_caps_of_state)+ apply (rename_tac irq cap slot) apply (rule_tac Q =
            "\<lambda> irq_slot. K(irq_slot \<noteq> slot) and invs and emptyable irq_slot
                     and cte_wp_at can_fast_finalise irq_slot
                     and not cte_wp_at is_transferable_cap slot
                     and K(is_subject aag (fst irq_slot))" in hoare_post_imp) apply (force simp: cte_wp_at_caps_of_state) apply simp apply (wp get_irq_slot_different) apply (clarsimp simp: emptyable_irq_node cte_wp_at_caps_of_state) apply (fastforce simp: interrupt_derived_def is_cap_simps cap_master_cap_def split: cap.splits) apply (wp delete_one_caps_of_state | simp add: get_irq_slot_def)+ apply (fastforce dest: pas_refined_is_subject_irqD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and irq_handler_inv_valid irq_inv and K (authorised_irq_hdl_inv aag irq_inv)\<rbrace> invoke_irq_handler irq_inv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_irq_hdl_inv aag irq_inv \<Longrightarrow> \<lbrace>pas_refined aag and invs and irq_handler_inv_valid irq_inv\<rbrace> invoke_irq_handler irq_inv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x1. irq_inv = ACKIrq x1 \<Longrightarrow> \<lbrace>pas_refined aag and invs and (\<lambda>s. interrupt_states s x1 \<noteq> IRQInactive)\<rbrace> arch_invoke_irq_handler (ACKIrq x1) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x21 x22 x23. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)\<rbrace> do irq_slot <- get_irq_slot x21;
y <- cap_delete_one irq_slot;
cap_insert x22 x23 irq_slot
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22 x23. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 x21 x22 x23\<rbrace> get_irq_slot x21 \<lbrace>\<lambda>rv s. (x23 = rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> (\<forall>cap. caps_of_state s rv = Some cap \<longrightarrow> \<not> can_fast_finalise cap)) \<and> (x23 \<noteq> rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> ((\<exists>cap. caps_of_state s rv = Some cap \<and> can_fast_finalise cap) \<longrightarrow> (\<forall>cap. caps_of_state s x23 = Some cap \<longrightarrow> \<not> is_transferable_cap cap) \<and> is_subject aag (fst rv)))\<rbrace>
 2. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> ?P'46 x21 x22 x23 s
 3. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap slot. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag irq; irq_inv = SetIRQHandler irq cap slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 irq cap slot\<rbrace> get_irq_slot irq \<lbrace>\<lambda>rv s. (slot = rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> (\<forall>cap. caps_of_state s rv = Some cap \<longrightarrow> \<not> can_fast_finalise cap)) \<and> (slot \<noteq> rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> ((\<exists>cap. caps_of_state s rv = Some cap \<and> can_fast_finalise cap) \<longrightarrow> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> \<not> is_transferable_cap cap) \<and> is_subject aag (fst rv)))\<rbrace>
 2. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> ?P'46 x21 x22 x23 s
 3. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>irq cap slot rv s. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag irq; irq_inv = SetIRQHandler irq cap slot; (K (rv \<noteq> slot) and invs and emptyable rv and cte_wp_at can_fast_finalise rv and not cte_wp_at is_transferable_cap slot and K (is_subject aag (fst rv))) s\<rbrakk> \<Longrightarrow> (slot = rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> (\<forall>cap. caps_of_state s rv = Some cap \<longrightarrow> \<not> can_fast_finalise cap)) \<and> (slot \<noteq> rv \<longrightarrow> is_subject aag (fst rv) \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> emptyable rv s \<and> ((\<exists>cap. caps_of_state s rv = Some cap \<and> can_fast_finalise cap) \<longrightarrow> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> \<not> is_transferable_cap cap) \<and> is_subject aag (fst rv)))
 2. \<And>irq cap slot. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag irq; irq_inv = SetIRQHandler irq cap slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 irq cap slot\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot. K (irq_slot \<noteq> slot) and invs and emptyable irq_slot and cte_wp_at can_fast_finalise irq_slot and not cte_wp_at is_transferable_cap slot and K (is_subject aag (fst irq_slot))\<rbrace>
 3. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> ?P'46 x21 x22 x23 s
 4. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap slot. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag irq; irq_inv = SetIRQHandler irq cap slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 irq cap slot\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot. K (irq_slot \<noteq> slot) and invs and emptyable irq_slot and cte_wp_at can_fast_finalise irq_slot and not cte_wp_at is_transferable_cap slot and K (is_subject aag (fst irq_slot))\<rbrace>
 2. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> ?P'46 x21 x22 x23 s
 3. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>irq cap slot. \<lbrakk>is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap \<and> is_subject_irq aag irq; irq_inv = SetIRQHandler irq cap slot\<rbrakk> \<Longrightarrow> \<lbrace>?P'46 irq cap slot\<rbrace> get_irq_slot irq \<lbrace>\<lambda>irq_slot. (\<lambda>y. irq_slot \<noteq> slot) and invs and emptyable irq_slot and cte_wp_at can_fast_finalise irq_slot and not cte_wp_at is_transferable_cap slot and (\<lambda>y. is_subject aag (fst irq_slot))\<rbrace>
 2. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> ?P'46 x21 x22 x23 s
 3. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 x23 s. \<lbrakk>is_subject aag (fst x23) \<and> pas_cap_cur_auth aag x22 \<and> is_subject_irq aag x21; irq_inv = SetIRQHandler x21 x22 x23; (pas_refined aag and invs and (\<lambda>s. ex_cte_cap_wp_to is_cnode_cap x23 s \<and> (\<exists>a b. cte_wp_at ((=) (IRQHandlerCap x21)) (a, b) s) \<and> cte_wp_at (interrupt_derived x22) x23 s \<and> s \<turnstile> x22 \<and> is_ntfn_cap x22)) s\<rbrakk> \<Longrightarrow> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> valid_mdb s \<and> (valid_global_refs s \<and> ex_cte_cap_wp_to is_cnode_cap x23 s) \<and> invs s \<and> invs s \<and> invs s \<and> (not cte_wp_at is_transferable_cap x23) s \<and> (pas_refined aag and K (is_subject_irq aag x21)) s
 2. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x21 x22 a b s aa ba cap. \<lbrakk>irq_inv = SetIRQHandler x21 x22 (a, b); is_subject aag a; pas_refined aag s; pas_cap_cur_auth aag x22; is_subject_irq aag x21; invs s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; caps_of_state s (aa, ba) = Some (IRQHandlerCap x21); s \<turnstile> x22; is_ntfn_cap x22; caps_of_state s (a, b) = Some cap; interrupt_derived x22 cap\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> valid_global_refs s \<and> \<not> is_transferable_cap cap
 2. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs\<rbrace> get_irq_slot x3 >>= cap_delete_one \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>is_subject_irq aag x3; irq_inv = ClearIRQHandler x3; pas_refined aag s \<and> invs s\<rbrakk> \<Longrightarrow> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> is_subject aag (interrupt_irq_node s x3) proof (prove)
goal:
No subgoals!