theory FinalCaps

lemma invoke_irq_control_silc_inv:
  "\<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and
         K (authorised_irq_ctl_inv aag blah)\<rbrace>
      invoke_irq_control blah
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" unfolding authorised_irq_ctl_inv_def apply (case_tac blah) apply (rule hoare_gen_asm) apply (wp cap_insert_silc_inv'' hoare_vcg_ex_lift slots_holding_overlapping_caps_lift
         | simp add: authorised_irq_ctl_inv_def)+ apply (fastforce dest: new_irq_handler_caps_are_intra_label) apply (simp, rule arch_invoke_irq_control_silc_inv[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (authorised_irq_ctl_inv aag blah)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. blah = IRQControl x11 x12 x13 \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x2. blah = ArchIRQControl x2 \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. \<lbrakk>blah = IRQControl x11 x12 x13; case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv\<rbrakk> \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x2. blah = ArchIRQControl x2 \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13 s. \<lbrakk>blah = IRQControl x11 x12 x13; is_subject aag (fst x12) \<and> is_subject aag (fst x13) \<and> (pasSubject aag, Control, pasIRQAbs aag x11) \<in> pasPolicy aag; silc_inv aag st s \<and> pas_refined aag s \<and> cte_wp_at ((=) NullCap) x12 s \<and> cte_wp_at ((=) IRQControlCap) x13 s \<and> ex_cte_cap_wp_to is_cnode_cap x12 s \<and> real_cte_at x12 s \<and> x11 \<le> maxIRQ\<rbrakk> \<Longrightarrow> \<not> cap_points_to_label aag (IRQHandlerCap x11) (pasSubject aag) \<longrightarrow> (\<exists>a. (\<exists>b. (a, b) \<in> slots_holding_overlapping_caps (IRQHandlerCap x11) s) \<and> pasObjectAbs aag a = SilcLabel)
 2. \<And>x2. blah = ArchIRQControl x2 \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x2. blah = ArchIRQControl x2 \<Longrightarrow> \<lbrace>silc_inv aag st and pas_refined aag and irq_control_inv_valid blah and K (case blah of IRQControl irq x1 x2 \<Rightarrow> is_subject aag (fst x1) \<and> is_subject aag (fst x2) \<and> (pasSubject aag, Control, pasIRQAbs aag irq) \<in> pasPolicy aag | ArchIRQControl acinv \<Rightarrow> arch_authorised_irq_ctl_inv aag acinv)\<rbrace> invoke_irq_control blah \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!