theory ArchFinalise_AI

lemma (* finalise_cap_invs *)[Finalise_AI_asms]:
  shows "\<lbrace>invs and cte_wp_at ((=) cap) slot\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv. invs\<rbrace>" apply (cases cap, simp_all split del: if_split) apply (wp cancel_all_ipc_invs cancel_all_signals_invs unbind_notification_invs
                   unbind_maybe_notification_invs
                  | simp add: o_def split del: if_split cong: if_cong
                  | wpc )+ apply clarsimp  (* thread *)
       apply (frule cte_wp_at_valid_objs_valid_cap, clarsimp) apply (clarsimp simp: valid_cap_def) apply (frule(1) valid_global_refsD[OF invs_valid_global_refs]) apply (simp add: global_refs_def, rule disjI1, rule refl) apply (simp add: cap_range_def) apply (wp deleting_irq_handler_invs  | simp | intro conjI impI)+ apply (auto dest: cte_wp_at_valid_objs_valid_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and cte_wp_at ((=) cap) slot\<rbrace> finalise_cap cap x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) NullCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when x (cancel_all_ipc x31)) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when x (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot\<rbrace> return (if x then Zombie x61 (Some x62) (2 ^ x62) else NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ThreadCap x7)) slot\<rbrace> do y <- when x (unbind_notification x7);
y <- when x (suspend x7);
y <- when x (prepare_thread_delete x7);
return (if x then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; invs s \<and> cte_wp_at ((=) (ThreadCap x7)) slot s\<rbrakk> \<Longrightarrow> (if x then \<lambda>s. invs s \<and> tcb_at x7 s \<and> x7 \<noteq> idle_thread s else invs) s
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; invs s; cte_wp_at ((=) (ThreadCap x7)) slot s; x\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> x7 \<noteq> idle_thread s
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; invs s; cte_wp_at ((=) (ThreadCap x7)) slot s; x\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> x7 \<noteq> idle_thread s
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x7 s. \<lbrakk>cap = ThreadCap x7; invs s; cte_wp_at ((=) (ThreadCap x7)) slot s; x; \<exists>cap. ThreadCap x7 = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> tcb_at x7 s \<and> x7 \<noteq> idle_thread s
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>cap = ThreadCap (idle_thread s); invs s; cte_wp_at ((=) (ThreadCap (idle_thread s))) slot s; x; cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s\<rbrakk> \<Longrightarrow> False
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>cap = ThreadCap (idle_thread s); invs s; cte_wp_at ((=) (ThreadCap (idle_thread s))) slot s; x; cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s\<rbrakk> \<Longrightarrow> ?r91 s \<in> global_refs s
 2. \<And>s. \<lbrakk>cap = ThreadCap (idle_thread s); invs s; cte_wp_at ((=) (ThreadCap (idle_thread s))) slot s; x; cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s; ?r91 s \<notin> cap_range (ThreadCap (idle_thread s))\<rbrakk> \<Longrightarrow> False
 3. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s. \<lbrakk>cap = ThreadCap (idle_thread s); invs s; cte_wp_at ((=) (ThreadCap (idle_thread s))) slot s; x; cap_aligned (ThreadCap (idle_thread s)); tcb_at (idle_thread s) s; idle_thread s \<notin> cap_range (ThreadCap (idle_thread s))\<rbrakk> \<Longrightarrow> False
 2. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. cap = DomainCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 2. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> if x then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv. invs\<rbrace>
 4. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (Zombie x111 x112 x113)) slot\<rbrace> do y <- assert x;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 x \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12 s. \<lbrakk>cap = ArchObjectCap x12; invs s \<and> cte_wp_at ((=) (ArchObjectCap x12)) slot s\<rbrakk> \<Longrightarrow> s \<turnstile> ArchObjectCap x12 proof (prove)
goal:
No subgoals!