theory FinalCaps

lemma finalise_cap_silc_inv:
  "\<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state
                    and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap final
   \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>" apply (case_tac cap) apply (wp cancel_ipc_silc_inv | simp split del: if_split add: suspend_def| clarsimp)+ apply (fastforce simp: aag_cap_auth_Thread) apply (wp | simp split del: if_split | clarsimp split del: if_split)+ apply (rule hoare_pre) apply (wp cap_delete_one_silc_inv
              | simp add: deleting_irq_handler_def
              | strengthen is_subject_not_silc_inv)+ apply (fastforce simp: aag_cap_auth_def cap_links_irq_def elim: aag_Control_into_owns_irq) apply (wp | simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; silc_inv aag st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_mdb s; pas_refined aag s; pas_cap_cur_auth aag (ThreadCap x7); final\<rbrakk> \<Longrightarrow> is_subject aag x7
 2. cap = DomainCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. cap = DomainCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. cap = IRQControlCap \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x10. \<lbrakk>cap = IRQHandlerCap x10; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q116 x10\<rbrace> deleting_irq_handler x10 \<lbrace>\<lambda>y. silc_inv aag st\<rbrace>
 2. \<And>x10. \<lbrakk>cap = IRQHandlerCap x10; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>?R116 x10\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x10 s. \<lbrakk>cap = IRQHandlerCap x10; (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag (IRQHandlerCap x10))) s\<rbrakk> \<Longrightarrow> (final \<longrightarrow> ?Q116 x10 s) \<and> (\<not> final \<longrightarrow> ?R116 x10 s)
 4. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x10. \<lbrakk>cap = IRQHandlerCap x10; final\<rbrakk> \<Longrightarrow> \<lbrace>?Q120 x10\<rbrace> deleting_irq_handler x10 \<lbrace>\<lambda>y. silc_inv aag st\<rbrace>
 2. \<And>x10 s. \<lbrakk>cap = IRQHandlerCap x10; final; ?Q116 x10 s\<rbrakk> \<Longrightarrow> ?Q120 x10 s
 3. \<And>x10. \<lbrakk>cap = IRQHandlerCap x10; \<not> final\<rbrakk> \<Longrightarrow> \<lbrace>?R116 x10\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 4. \<And>x10 s. \<lbrakk>cap = IRQHandlerCap x10; (silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag (IRQHandlerCap x10))) s\<rbrakk> \<Longrightarrow> (final \<longrightarrow> ?Q116 x10 s) \<and> (\<not> final \<longrightarrow> ?R116 x10 s)
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x10 s. \<lbrakk>cap = IRQHandlerCap x10; silc_inv aag st s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_mdb s \<and> pas_refined aag s \<and> pas_cap_cur_auth aag (IRQHandlerCap x10)\<rbrakk> \<Longrightarrow> final \<longrightarrow> (\<exists>st. Ex (silc_inv aag st)) \<and> is_subject_irq aag x10
 2. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 3. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace>
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>silc_inv aag st and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_mdb and pas_refined aag and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_. silc_inv aag st\<rbrace> proof (prove)
goal:
No subgoals!