theory ArchFinalise_AC

lemma finalise_cap_fst_ret[Finalise_AC_assms]:
  "\<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace>
   finalise_cap cap is_final
   \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>" including no_pre apply (cases cap, simp_all add: arch_finalise_cap_def split del: if_split) apply (wp | simp add: comp_def split del: if_split | fastforce)+ apply (rule hoare_pre) apply (wp | simp | (rule hoare_pre, wpc))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when is_final (cancel_all_ipc x31)) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when is_final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (if is_final then Zombie x61 (Some x62) (2 ^ x62) else NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> do y <- when is_final (unbind_notification x7);
y <- when is_final (suspend x7);
y <- when is_final (prepare_thread_delete x7);
return (if is_final then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> if is_final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> if is_final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 2. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> do y <- assert is_final;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 3. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case is_final of True \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | ASIDControlCap \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s None \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | PageTableCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageTableCap ptr (Some (a, v)) \<Rightarrow> case is_final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr (Some a) \<Rightarrow> case is_final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>?Q72 x10\<rbrace> if is_final then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 2. \<And>x10 s. \<lbrakk>cap = IRQHandlerCap x10; P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrakk> \<Longrightarrow> ?Q72 x10 s
 3. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> do y <- assert is_final;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace>
 4. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>_. P NullCap \<and> (\<forall>a b c. P (Zombie a b c))\<rbrace> case x12 of ASIDPoolCap ptr b \<Rightarrow> case is_final of True \<Rightarrow> do delete_asid_pool b ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | ASIDControlCap \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s None \<Rightarrow> return (NullCap, NullCap) | PageCap x ptr xa s (Some (a, v)) \<Rightarrow> do unmap_page s a v ptr;
return (NullCap, NullCap)
od | PageTableCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageTableCap ptr (Some (a, v)) \<Rightarrow> case is_final of True \<Rightarrow> do unmap_page_table a v ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr None \<Rightarrow> return (NullCap, NullCap) | PageDirectoryCap ptr (Some a) \<Rightarrow> case is_final of True \<Rightarrow> do delete_asid a ptr;
return (NullCap, NullCap)
od | False \<Rightarrow> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. P (fst rv)\<rbrace> proof (prove)
goal:
No subgoals!