theory Finalise_IF

lemma finalise_cap_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_f aag l
       (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) cap) slot
                        and K (pas_cap_cur_auth aag cap)
                        and K (final \<longrightarrow> (case cap of EndpointCap r badge rights \<Rightarrow> is_subject aag r
                                                | NotificationCap r badge rights \<Rightarrow> is_subject aag r
                                                | _ \<Rightarrow> True)))
       (finalise_cap cap final)" apply (case_tac cap, simp_all split del: if_split) apply ((wp cancel_all_ipc_reads_respects cancel_all_signals_reads_respects
                        prepare_thread_delete_reads_respects_f
                        suspend_reads_respects_f[where st=st] deleting_irq_handler_reads_respects
                        unbind_notification_is_subj_reads_respects
                        unbind_maybe_notification_reads_respects
                        unbind_notification_invs unbind_maybe_notification_invs
                     | simp add: when_def invs_valid_objs invs_sym_refs aag_cap_auth_def
                                 cap_auth_conferred_def cap_rights_to_auth_def cap_links_irq_def
                                 aag_has_Control_iff_owns cte_wp_at_caps_of_state
                            split del: if_split
                     | rule aag_Control_into_owns_irq
                     | clarsimp split del: if_split
                     | rule conjI
                     | wp (once) reads_respects_f[where st=st]
                     | blast
                     | clarsimp
                     | force dest: caps_of_state_valid simp: valid_cap_def)+)[11] apply (rule equiv_valid_guard_imp) by (wp arch_finalise_cap_reads_respects reads_respects_f[where st=st] arch_finalise_cap_silc_inv
      | simp | elim conjE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) cap) slot and K (pas_cap_cur_auth aag cap) and K (final \<longrightarrow> (case cap of EndpointCap r badge rights \<Rightarrow> is_subject aag r | NotificationCap r badge rights \<Rightarrow> is_subject aag r | _ \<Rightarrow> True))) (finalise_cap cap final) proof (prove)
goal (12 subgoals):
 1. cap = NullCap \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) NullCap) slot) (return (NullCap, NullCap))
 2. \<And>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (UntypedCap x21 x22 x23 x24)) slot and (\<lambda>y. pas_cap_cur_auth aag (UntypedCap x21 x22 x23 x24))) (return (NullCap, NullCap))
 3. \<And>x31 x32 x33. cap = EndpointCap x31 x32 x33 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (EndpointCap x31 x32 x33)) slot and (\<lambda>y. pas_cap_cur_auth aag (EndpointCap x31 x32 x33)) and (\<lambda>y. final \<longrightarrow> is_subject aag x31)) (liftM (\<lambda>y. (NullCap, NullCap)) (when final (cancel_all_ipc x31)))
 4. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (NotificationCap x41 x42 x43)) slot and (\<lambda>y. pas_cap_cur_auth aag (NotificationCap x41 x42 x43)) and (\<lambda>y. final \<longrightarrow> is_subject aag x41)) (liftM (\<lambda>y. (NullCap, NullCap)) (when final (do y <- unbind_maybe_notification x41;
cancel_all_signals x41
od)))
 5. \<And>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (ReplyCap x51 x52 x53)) slot and (\<lambda>y. pas_cap_cur_auth aag (ReplyCap x51 x52 x53))) (return (NullCap, NullCap))
 6. \<And>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (CNodeCap x61 x62 x63)) slot and (\<lambda>y. pas_cap_cur_auth aag (CNodeCap x61 x62 x63))) (return (if final then Zombie x61 (Some x62) (2 ^ x62) else NullCap, NullCap))
 7. \<And>x7. cap = ThreadCap x7 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (ThreadCap x7)) slot and (\<lambda>y. pas_cap_cur_auth aag (ThreadCap x7))) (do y <- when final (unbind_notification x7);
y <- when final (suspend x7);
y <- when final (prepare_thread_delete x7);
return (if final then Zombie x7 None 5 else NullCap, NullCap)
od)
 8. cap = DomainCap \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) DomainCap) slot and (\<lambda>y. pas_cap_cur_auth aag DomainCap)) (return (NullCap, NullCap))
 9. cap = IRQControlCap \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) IRQControlCap) slot and (\<lambda>y. pas_cap_cur_auth aag IRQControlCap)) (return (NullCap, NullCap))
 10. \<And>x10. cap = IRQHandlerCap x10 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (IRQHandlerCap x10)) slot and (\<lambda>y. pas_cap_cur_auth aag (IRQHandlerCap x10))) (if final then do deleting_irq_handler x10;
return (NullCap, IRQHandlerCap x10)
od else return (NullCap, NullCap))
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (ArchObjectCap x12)) slot and (\<lambda>y. pas_cap_cur_auth aag (ArchObjectCap x12))) (arch_finalise_cap x12 final) proof (prove)
goal (2 subgoals):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (?Q423 x12) (arch_finalise_cap x12 final)
 2. \<And>x12 s. \<lbrakk>cap = ArchObjectCap x12; (silc_inv aag st and pas_refined aag and invs and cte_wp_at ((=) (ArchObjectCap x12)) slot and (\<lambda>y. pas_cap_cur_auth aag (ArchObjectCap x12))) s\<rbrakk> \<Longrightarrow> ?Q423 x12 s