theory FinalCaps

lemma finalise_cap_ret_is_subject:
  "\<lbrace>K ((is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap) \<longrightarrow> is_subject aag (obj_ref_of cap))\<rbrace>
   finalise_cap cap is_final
   \<lbrace>\<lambda>rv _ :: det_state. case (fst rv) of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv))
                                                       | _ \<Rightarrow> True\<rbrace>" including no_pre apply (case_tac cap, simp_all add: is_zombie_def) apply (wp | simp add: comp_def | rule impI | rule conjI)+ apply (fastforce simp: valid_def dest: arch_finalise_cap_ret) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap))\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_cnode_cap cap \<or> is_thread_cap cap \<or> is_zombie cap \<longrightarrow> is_subject aag (obj_ref_of cap))\<rbrace> finalise_cap cap is_final \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when is_final (cancel_all_ipc x31)) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when is_final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> (is_final \<longrightarrow> \<lbrace>\<lambda>y. is_subject aag x61\<rbrace> return (Zombie x61 (Some x62) (2 ^ x62), NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>) \<and> (\<not> is_final \<longrightarrow> \<lbrace>\<lambda>y. is_subject aag x61\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>)
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> (is_final \<longrightarrow> \<lbrace>\<lambda>y. is_subject aag x7\<rbrace> do y <- unbind_notification x7;
y <- suspend x7;
y <- prepare_thread_delete x7;
return (Zombie x7 None 5, NullCap)
od \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>) \<and> (\<not> is_final \<longrightarrow> \<lbrace>\<lambda>y. is_subject aag x7\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>)
 8. cap = DomainCap \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 9. cap = IRQControlCap \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> (is_final \<longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>) \<and> (\<not> is_final \<longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace>)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>y. True\<rbrace> arch_finalise_cap x12 is_final \<lbrace>\<lambda>rv _. case fst rv of Zombie ptr bits n \<Rightarrow> is_subject aag (obj_ref_of (fst rv)) | _ \<Rightarrow> True\<rbrace> proof (prove)
goal:
No subgoals!