theory Finalise_AI

lemma (in Finalise_AI_3) finalise_cap_cte_cap_to[wp]:
  "\<lbrace>ex_cte_cap_wp_to P sl :: 'a state \<Rightarrow> bool\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace>" apply (cases cap, simp_all add: ex_cte_cap_wp_to_def split del: if_split) apply (wp hoare_vcg_ex_lift hoare_drop_imps
                 prepare_thread_delete_cte_preserved_irqn
                 deleting_irq_handler_cte_preserved_irqn
                 prepare_thread_delete_cte_preserved_irqn
                 | simp
                 | clarsimp simp: can_fast_finalise_def
                           split: cap.split_asm | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P sl\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P sl\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when fin (cancel_all_ipc x31)) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 2. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> liftM (\<lambda>y. (NullCap, NullCap)) (when fin (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 3. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> do y <- when fin (unbind_notification x7);
y <- when fin (suspend x7);
y <- when fin (prepare_thread_delete x7);
return (if fin then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 4. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> if fin then do y <- deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 5. \<And>x111 x112 x113. cap = Zombie x111 x112 x113 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> do y <- assert fin;
return (Zombie x111 x112 x113, NullCap)
od \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace>
 6. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> arch_finalise_cap x12 fin \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. P c \<and> sl \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrace> proof (prove)
goal:
No subgoals!