theory Finalise_AC

lemma finalise_cap_pas_refined[wp]:
  "\<lbrace>pas_refined aag and invs and valid_cap cap and K (pas_cap_cur_auth aag cap)\<rbrace>
   finalise_cap cap fin
   \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" apply (rule hoare_gen_asm) apply (cases cap; simp only: finalise_cap.simps) apply (wpsimp wp: unbind_notification_invs
             simp: aag_cap_auth_def cap_auth_conferred_def valid_cap_simps
                   cap_links_irq_def pas_refined_Control[symmetric]
         | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and invs and valid_cap cap and K (pas_cap_cur_auth aag cap)\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. pas_cap_cur_auth aag cap \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap cap\<rbrace> finalise_cap cap fin \<lbrace>\<lambda>_. pas_refined aag\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<lbrakk>pas_cap_cur_auth aag NullCap; cap = NullCap\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap NullCap\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 2. \<And>x21 x22 x23 x24. \<lbrakk>pas_cap_cur_auth aag (UntypedCap x21 x22 x23 x24); cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (UntypedCap x21 x22 x23 x24)\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 3. \<And>x31 x32 x33. \<lbrakk>pas_cap_cur_auth aag (EndpointCap x31 x32 x33); cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (EndpointCap x31 x32 x33)\<rbrace> liftM (K (NullCap, NullCap)) $ when fin $ cancel_all_ipc x31 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 4. \<And>x41 x42 x43. \<lbrakk>pas_cap_cur_auth aag (NotificationCap x41 x42 x43); cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (NotificationCap x41 x42 x43)\<rbrace> liftM (K (NullCap, NullCap)) $ when fin $ do unbind_maybe_notification x41;
cancel_all_signals x41
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 5. \<And>x51 x52 x53. \<lbrakk>pas_cap_cur_auth aag (ReplyCap x51 x52 x53); cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (ReplyCap x51 x52 x53)\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 6. \<And>x61 x62 x63. \<lbrakk>pas_cap_cur_auth aag (CNodeCap x61 x62 x63); cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (CNodeCap x61 x62 x63)\<rbrace> return (if fin then Zombie x61 (Some x62) (2 ^ x62) else NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 7. \<And>x7. \<lbrakk>pas_cap_cur_auth aag (ThreadCap x7); cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (ThreadCap x7)\<rbrace> do when fin $ unbind_notification x7;
when fin $ suspend x7;
when fin $ prepare_thread_delete x7;
return (if fin then Zombie x7 None 5 else NullCap, NullCap)
od \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 8. \<lbrakk>pas_cap_cur_auth aag DomainCap; cap = DomainCap\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap DomainCap\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 9. \<lbrakk>pas_cap_cur_auth aag IRQControlCap; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap IRQControlCap\<rbrace> return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
 10. \<And>x10. \<lbrakk>pas_cap_cur_auth aag (IRQHandlerCap x10); cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and invs and valid_cap (IRQHandlerCap x10)\<rbrace> if fin then do deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap) \<lbrace>\<lambda>_. pas_refined aag\<rbrace>
A total of 12 subgoals... proof (prove)
goal:
No subgoals!