theory ArchTcb_AI

lemma finalise_cap_not_cte_wp_at[Tcb_AI_asms]:
  assumes x: "P cap.NullCap"
  shows      "\<lbrace>\<lambda>s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>
                finalise_cap cap fin
              \<lbrace>\<lambda>rv s. \<forall>cp \<in> ran (caps_of_state s). P cp\<rbrace>" apply (cases cap, simp_all) apply (wp suspend_caps_of_state hoare_vcg_all_lift
            | simp
            | rule impI
            | rule hoare_drop_imps)+ apply (clarsimp simp: ball_ran_eq x) apply (wp delete_one_caps_of_state
         | rule impI
         | simp add: deleting_irq_handler_def get_irq_slot_def x ball_ran_eq)+ done

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