theory Interrupt_AC

lemma invoke_irq_control_pas_refined:
  "\<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and irq_control_inv_valid irq_ctl_inv
                    and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace>
   invoke_irq_control irq_ctl_inv
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (cases irq_ctl_inv; simp) apply (wpsimp wp: cap_insert_pas_refined_not_transferable) apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
                         authorised_irq_ctl_inv_def aag_cap_auth_def) apply (wp arch_invoke_irq_control_pas_refined) apply (clarsimp simp: cte_wp_at_caps_of_state clas_no_asid cap_links_irq_def
                        authorised_irq_ctl_inv_def aag_cap_auth_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and irq_control_inv_valid irq_ctl_inv and K (authorised_irq_ctl_inv aag irq_ctl_inv)\<rbrace> invoke_irq_control irq_ctl_inv \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. irq_ctl_inv = IRQControl x11 x12 x13 \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and (cte_wp_at ((=) NullCap) x12 and cte_wp_at ((=) IRQControlCap) x13 and ex_cte_cap_wp_to is_cnode_cap x12 and real_cte_at x12 and (\<lambda>y. x11 \<le> maxIRQ)) and (\<lambda>y. authorised_irq_ctl_inv aag (IRQControl x11 x12 x13))\<rbrace> liftE (do y <- set_irq_state IRQSignal x11;
cap_insert (IRQHandlerCap x11) x13 x12
od) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x2. irq_ctl_inv = ArchIRQControl x2 \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid x2 and (\<lambda>y. authorised_irq_ctl_inv aag (ArchIRQControl x2))\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 a b aa ba s. \<lbrakk>irq_ctl_inv = IRQControl x11 (a, b) (aa, ba); pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; cte_wp_at ((=) NullCap) (a, b) s; cte_wp_at ((=) IRQControlCap) (aa, ba) s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; cap_table_at (length b) a s; x11 \<le> maxIRQ; authorised_irq_ctl_inv aag (IRQControl x11 (a, b) (aa, ba))\<rbrakk> \<Longrightarrow> \<not> cte_wp_at is_transferable_cap (aa, ba) s \<and> is_subject aag a \<and> is_subject aag aa \<and> pas_cap_cur_auth aag (IRQHandlerCap x11)
 2. \<And>x2. irq_ctl_inv = ArchIRQControl x2 \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid x2 and (\<lambda>y. authorised_irq_ctl_inv aag (ArchIRQControl x2))\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. irq_ctl_inv = ArchIRQControl x2 \<Longrightarrow> \<lbrace>pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid x2 and (\<lambda>y. authorised_irq_ctl_inv aag (ArchIRQControl x2))\<rbrace> arch_invoke_irq_control x2 \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>irq_ctl_inv = ArchIRQControl x2; (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid x2 and (\<lambda>y. authorised_irq_ctl_inv aag (ArchIRQControl x2))) s\<rbrakk> \<Longrightarrow> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and arch_irq_control_inv_valid x2 and K (arch_authorised_irq_ctl_inv aag x2)) s proof (prove)
goal:
No subgoals!