theory Decode_IF

lemma slot_cap_long_running_delete_reads_respects_f:
  "reads_respects_f aag l (silc_inv aag st and pas_refined aag and valid_objs
                                           and zombies_final and K (is_subject aag (fst slot)))
                    (slot_cap_long_running_delete slot)" unfolding slot_cap_long_running_delete_def apply (rule bind_ev_pre) apply (wpc) apply wp apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign
                               intro: return_ev)+ apply ((wp is_final_cap_reads_respects[where slot=slot and st=st])+)[2] apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+ apply (wp is_final_cap_reads_respects[where st=st])[1] apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+ apply (wp reads_respects_f[OF get_cap_rev, where Q="\<top>" and st=st], blast) apply (wp get_cap_wp | simp)+ apply (fastforce intro!: cte_wp_valid_cap aag_has_auth_to_obj_refs_of_owned_cap simp: is_zombie_def
                     dest: silc_inv_not_subject) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) (slot_cap_long_running_delete slot) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) (do cap <- get_cap slot;
case cap of NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap cap;
return (final \<and> long_running_delete cap)
od
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. reads_respects_f aag l (?Q rv) (case rv of NullCap \<Rightarrow> return False | _ \<Rightarrow> do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. reads_respects_f aag l ?P' (get_cap slot)
 3. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>?Q\<rbrace>
 4. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (15 subgoals):
 1. \<And>rv. rv = NullCap \<Longrightarrow> reads_respects_f aag l (?R54 rv) (return False)
 2. \<And>rv x21 x22 x23 x24. rv = UntypedCap x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (?R55 rv x21 x22 x23 x24) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 3. \<And>rv x31 x32 x33. rv = EndpointCap x31 x32 x33 \<Longrightarrow> reads_respects_f aag l (?R56 rv x31 x32 x33) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 4. \<And>rv x41 x42 x43. rv = NotificationCap x41 x42 x43 \<Longrightarrow> reads_respects_f aag l (?R57 rv x41 x42 x43) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 5. \<And>rv x51 x52 x53. rv = ReplyCap x51 x52 x53 \<Longrightarrow> reads_respects_f aag l (?R58 rv x51 x52 x53) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 6. \<And>rv x61 x62 x63. rv = CNodeCap x61 x62 x63 \<Longrightarrow> reads_respects_f aag l (?R59 rv x61 x62 x63) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 7. \<And>rv x7. rv = ThreadCap x7 \<Longrightarrow> reads_respects_f aag l (?R60 rv x7) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 8. \<And>rv. rv = DomainCap \<Longrightarrow> reads_respects_f aag l (?R61 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 9. \<And>rv. rv = IRQControlCap \<Longrightarrow> reads_respects_f aag l (?R62 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 10. \<And>rv x10. rv = IRQHandlerCap x10 \<Longrightarrow> reads_respects_f aag l (?R63 rv x10) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv x21 x22 x23 x24. rv = UntypedCap x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (?R55 rv x21 x22 x23 x24) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. \<And>rv x31 x32 x33. rv = EndpointCap x31 x32 x33 \<Longrightarrow> reads_respects_f aag l (?R56 rv x31 x32 x33) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 3. \<And>rv x41 x42 x43. rv = NotificationCap x41 x42 x43 \<Longrightarrow> reads_respects_f aag l (?R57 rv x41 x42 x43) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 4. \<And>rv x51 x52 x53. rv = ReplyCap x51 x52 x53 \<Longrightarrow> reads_respects_f aag l (?R58 rv x51 x52 x53) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 5. \<And>rv x61 x62 x63. rv = CNodeCap x61 x62 x63 \<Longrightarrow> reads_respects_f aag l (?R59 rv x61 x62 x63) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 6. \<And>rv x7. rv = ThreadCap x7 \<Longrightarrow> reads_respects_f aag l (?R60 rv x7) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 7. \<And>rv. rv = DomainCap \<Longrightarrow> reads_respects_f aag l (?R61 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 8. \<And>rv. rv = IRQControlCap \<Longrightarrow> reads_respects_f aag l (?R62 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 9. \<And>rv x10. rv = IRQHandlerCap x10 \<Longrightarrow> reads_respects_f aag l (?R63 rv x10) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 10. \<And>rv x111 x112 x113. rv = Zombie x111 x112 x113 \<Longrightarrow> reads_respects_f aag l (?R64 rv x111 x112 x113) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
A total of 14 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv x61 x62 x63. rv = CNodeCap x61 x62 x63 \<Longrightarrow> reads_respects_f aag l (?R59 rv x61 x62 x63) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. \<And>rv x7. rv = ThreadCap x7 \<Longrightarrow> reads_respects_f aag l (?R60 rv x7) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 3. \<And>rv. rv = DomainCap \<Longrightarrow> reads_respects_f aag l (?R61 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 4. \<And>rv. rv = IRQControlCap \<Longrightarrow> reads_respects_f aag l (?R62 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 5. \<And>rv x10. rv = IRQHandlerCap x10 \<Longrightarrow> reads_respects_f aag l (?R63 rv x10) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 6. \<And>rv x111 x112 x113. rv = Zombie x111 x112 x113 \<Longrightarrow> reads_respects_f aag l (?R64 rv x111 x112 x113) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 7. \<And>rv x12. rv = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (?R65 rv x12) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 8. reads_respects_f aag l ?P' (get_cap slot)
 9. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> ?R59 rv x xa xb s) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> ?R60 rv x s) \<and> (rv = DomainCap \<longrightarrow> ?R61 rv s) \<and> (rv = IRQControlCap \<longrightarrow> ?R62 rv s) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> ?R63 rv x s) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> ?R64 rv x xa xb s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ?R65 rv x s)\<rbrace>
 10. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (8 subgoals):
 1. \<And>rv. rv = DomainCap \<Longrightarrow> reads_respects_f aag l (?R61 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. \<And>rv. rv = IRQControlCap \<Longrightarrow> reads_respects_f aag l (?R62 rv) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 3. \<And>rv x10. rv = IRQHandlerCap x10 \<Longrightarrow> reads_respects_f aag l (?R63 rv x10) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 4. \<And>rv x111 x112 x113. rv = Zombie x111 x112 x113 \<Longrightarrow> reads_respects_f aag l (?R64 rv x111 x112 x113) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 5. \<And>rv x12. rv = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (?R65 rv x12) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 6. reads_respects_f aag l ?P' (get_cap slot)
 7. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (rv = DomainCap \<longrightarrow> ?R61 rv s) \<and> (rv = IRQControlCap \<longrightarrow> ?R62 rv s) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> ?R63 rv x s) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> ?R64 rv x xa xb s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ?R65 rv x s)\<rbrace>
 8. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (5 subgoals):
 1. \<And>rv x111 x112 x113. rv = Zombie x111 x112 x113 \<Longrightarrow> reads_respects_f aag l (?R64 rv x111 x112 x113) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. \<And>rv x12. rv = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (?R65 rv x12) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 3. reads_respects_f aag l ?P' (get_cap slot)
 4. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (rv = DomainCap \<longrightarrow> True) \<and> (rv = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> ?R64 rv x xa xb s) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ?R65 rv x s)\<rbrace>
 5. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>rv x12. rv = ArchObjectCap x12 \<Longrightarrow> reads_respects_f aag l (?R65 rv x12) (do final <- is_final_cap rv;
return (final \<and> long_running_delete rv)
od)
 2. reads_respects_f aag l ?P' (get_cap slot)
 3. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (rv = DomainCap \<longrightarrow> True) \<and> (rv = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) (?slot123 rv x xa xb) s \<and> aag_can_read aag (fst (?slot123 rv x xa xb)) \<and> pasObjectAbs aag (fst (?slot123 rv x xa xb)) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> ?R65 rv x s)\<rbrace>
 4. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P' (get_cap slot)
 2. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (rv = DomainCap \<longrightarrow> True) \<and> (rv = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) (?slot123 rv x xa xb) s \<and> aag_can_read aag (fst (?slot123 rv x xa xb)) \<and> pasObjectAbs aag (fst (?slot123 rv x xa xb)) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> True)\<rbrace>
 3. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> get_cap slot \<lbrace>\<lambda>rv s. (rv = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rv = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = CNodeCap x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ThreadCap x \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) slot s \<and> aag_can_read aag (fst slot) \<and> pasObjectAbs aag (fst slot) \<noteq> SilcLabel)) s \<and> True) \<and> (rv = DomainCap \<longrightarrow> True) \<and> (rv = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. rv = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rv = Zombie x xa xb \<longrightarrow> (silc_inv aag st and (\<lambda>s. cte_wp_at ((=) rv) (?slot123 rv x xa xb) s \<and> aag_can_read aag (fst (?slot123 rv x xa xb)) \<and> pasObjectAbs aag (fst (?slot123 rv x xa xb)) \<noteq> SilcLabel)) s \<and> True) \<and> (\<forall>x. rv = ArchObjectCap x \<longrightarrow> True)\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and valid_objs and zombies_final and K (is_subject aag (fst slot))) s \<Longrightarrow> (silc_inv aag st and K (aag_can_read aag (fst slot)) and (\<lambda>_. True)) s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> pas_refined aag s \<and> valid_objs s \<and> zombies_final s \<and> is_subject aag (fst slot) \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>x xa xb. cap = CNodeCap x xa xb \<longrightarrow> cte_wp_at ((=) (CNodeCap x xa xb)) slot s \<and> pasSubject aag \<noteq> SilcLabel) \<and> (\<forall>x. cap = ThreadCap x \<longrightarrow> cte_wp_at ((=) (ThreadCap x)) slot s \<and> pasSubject aag \<noteq> SilcLabel) \<and> (\<forall>x xa xb. cap = Zombie x xa xb \<longrightarrow> cte_wp_at ((=) (Zombie x xa xb)) (?slot123 (Zombie x xa xb) x xa xb) s \<and> aag_can_read aag (fst (?slot123 (Zombie x xa xb) x xa xb)) \<and> pasObjectAbs aag (fst (?slot123 (Zombie x xa xb) x xa xb)) \<noteq> SilcLabel) proof (prove)
goal:
No subgoals!