theory ArchCNodeInv_AI

lemma finalise_cap_makes_halted_proof[CNodeInv_AI_assms]:
  "\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s)
         and cte_wp_at ((=) cap) slot\<rbrace>
    finalise_cap cap ex
   \<lbrace>\<lambda>rv s. \<forall>t \<in> obj_refs (fst rv). halted_if_tcb t s\<rbrace>" apply (case_tac cap, simp_all) apply (wp unbind_notification_valid_objs
                 | clarsimp simp: o_def valid_cap_def cap_table_at_typ
                                  is_tcb obj_at_def
                 | clarsimp simp: halted_if_tcb_def
                           split: option.split
                 | intro impI conjI
                 | rule hoare_drop_imp)+ apply (drule_tac final_zombie_not_live; (assumption | simp add: invs_iflive)?) apply (clarsimp simp: pred_tcb_at_def is_tcb obj_at_def live_def, elim disjE) apply (clarsimp; case_tac "tcb_state tcb"; simp)+ apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all add: arch_finalise_cap_def) apply (wp
            | clarsimp simp: valid_cap_def obj_at_def is_tcb_def is_cap_table_def
                       split: option.splits bool.split
            | intro impI conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s) and cte_wp_at ((=) cap) slot\<rbrace> finalise_cap cap ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>invs and valid_cap NullCap and (\<lambda>s. ex = is_final_cap' NullCap s) and cte_wp_at ((=) NullCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs and valid_cap (UntypedCap x21 x22 x23 x24) and (\<lambda>s. ex = is_final_cap' (UntypedCap x21 x22 x23 x24) s) and cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>invs and valid_cap (EndpointCap x31 x32 x33) and (\<lambda>s. ex = is_final_cap' (EndpointCap x31 x32 x33) s) and cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when ex (cancel_all_ipc x31)) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs and valid_cap (NotificationCap x41 x42 x43) and (\<lambda>s. ex = is_final_cap' (NotificationCap x41 x42 x43) s) and cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when ex (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>invs and valid_cap (ReplyCap x51 x52 x53) and (\<lambda>s. ex = is_final_cap' (ReplyCap x51 x52 x53) s) and cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> (ex \<longrightarrow> \<lbrace>invs and valid_cap (CNodeCap x61 x62 x63) and is_final_cap' (CNodeCap x61 x62 x63) and cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>) \<and> (\<not> ex \<longrightarrow> \<lbrace>invs and valid_cap (CNodeCap x61 x62 x63) and (\<lambda>s. \<not> is_final_cap' (CNodeCap x61 x62 x63) s) and cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>)
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (ex \<longrightarrow> \<lbrace>invs and valid_cap (ThreadCap x7) and is_final_cap' (ThreadCap x7) and cte_wp_at ((=) (ThreadCap x7)) slot\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>) \<and> (\<not> ex \<longrightarrow> \<lbrace>invs and valid_cap (ThreadCap x7) and (\<lambda>s. \<not> is_final_cap' (ThreadCap x7) s) and cte_wp_at ((=) (ThreadCap x7)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>)
 8. cap = DomainCap \<Longrightarrow> \<lbrace>invs and valid_cap DomainCap and (\<lambda>s. ex = is_final_cap' DomainCap s) and cte_wp_at ((=) DomainCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>invs and valid_cap IRQControlCap and (\<lambda>s. ex = is_final_cap' IRQControlCap s) and cte_wp_at ((=) IRQControlCap) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (ex \<longrightarrow> \<lbrace>invs and valid_cap (IRQHandlerCap x10) and is_final_cap' (IRQHandlerCap x10) and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>) \<and> (\<not> ex \<longrightarrow> \<lbrace>invs and valid_cap (IRQHandlerCap x10) and (\<lambda>s. \<not> is_final_cap' (IRQHandlerCap x10) s) and cte_wp_at ((=) (IRQHandlerCap x10)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>)
A total of 12 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113 s tcb. \<lbrakk>cap = Zombie x111 x112 x113; invs s; cap_aligned (Zombie x111 x112 x113); case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0; cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; ex; is_final_cap' (Zombie x111 x112 x113) s; kheap s x111 = Some (TCB tcb)\<rbrakk> \<Longrightarrow> st_tcb_at halted x111 s
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap x12) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap x12) s) and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x111 x112 x113 s tcb. \<lbrakk>cap = Zombie x111 x112 x113; invs s; cap_aligned (Zombie x111 x112 x113); case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0; cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; ex; kheap s x111 = Some (TCB tcb); \<not> obj_at live x111 s\<rbrakk> \<Longrightarrow> st_tcb_at halted x111 s
 2. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap x12) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap x12) s) and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x111 x112 x113 s tcb. \<lbrakk>cap = Zombie x111 x112 x113; invs s; cap_aligned (Zombie x111 x112 x113); case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0; cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; ex; kheap s x111 = Some (TCB tcb); tcb_bound_notification tcb = None; \<not> hyp_live (TCB tcb); inactive (tcb_state tcb)\<rbrakk> \<Longrightarrow> halted (tcb_state tcb)
 2. \<And>x111 x112 x113 s tcb. \<lbrakk>cap = Zombie x111 x112 x113; invs s; cap_aligned (Zombie x111 x112 x113); case x112 of None \<Rightarrow> tcb_at x111 s \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 s \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0; cte_wp_at ((=) (Zombie x111 x112 x113)) slot s; ex; kheap s x111 = Some (TCB tcb); tcb_bound_notification tcb = None; \<not> hyp_live (TCB tcb); idle (tcb_state tcb)\<rbrakk> \<Longrightarrow> halted (tcb_state tcb)
 3. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap x12) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap x12) s) and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap x12) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap x12) s) and cte_wp_at ((=) (ArchObjectCap x12)) slot\<rbrace> arch_finalise_cap x12 ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap arch_cap) s) and cte_wp_at ((=) (ArchObjectCap arch_cap)) slot\<rbrace> arch_finalise_cap arch_cap ex \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>cap = ArchObjectCap (ASIDPoolCap x11 x12); arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (ASIDPoolCap x11 x12)) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap (ASIDPoolCap x11 x12)) s) and cte_wp_at ((=) (ArchObjectCap (ASIDPoolCap x11 x12))) slot\<rbrace> case ex of True \<Rightarrow> do delete_asid_pool x12 x11;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 2. \<And>arch_cap. \<lbrakk>cap = ArchObjectCap ASIDControlCap; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap ASIDControlCap) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap ASIDControlCap) s) and cte_wp_at ((=) (ArchObjectCap ASIDControlCap)) slot\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 3. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap (PageCap x31 x32 x33 x34 x35)) s) and cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) slot\<rbrace> case x35 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> do y <- unmap_page x34 a v x32;
return (NullCap, NullCap)
od \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 4. \<And>arch_cap x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); arch_cap = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageTableCap x41 x42)) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap (PageTableCap x41 x42)) s) and cte_wp_at ((=) (ArchObjectCap (PageTableCap x41 x42))) slot\<rbrace> case x42 of None \<Rightarrow> return (NullCap, NullCap) | Some (a, v) \<Rightarrow> case ex of True \<Rightarrow> do unmap_page_table a v x41;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace>
 5. \<And>arch_cap x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); arch_cap = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<lbrace>invs and valid_cap (ArchObjectCap (PageDirectoryCap x51 x52)) and (\<lambda>s. ex = is_final_cap' (ArchObjectCap (PageDirectoryCap x51 x52)) s) and cte_wp_at ((=) (ArchObjectCap (PageDirectoryCap x51 x52))) slot\<rbrace> case x52 of None \<Rightarrow> return (NullCap, NullCap) | Some a \<Rightarrow> case ex of True \<Rightarrow> do delete_asid a x51;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<forall>t\<in>obj_refs (fst rv). halted_if_tcb t s\<rbrace> proof (prove)
goal:
No subgoals!