theory CNodeInv_AI

lemma reduce_zombie_cap_to:
  "\<And>cap slot exp.
    \<lbrace>invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and
          emptyable slot and
          (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and
          K (\<not> cap_removeable cap slot) and
          (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)\<rbrace>
      rec_del (ReduceZombieCall cap slot exp)
    \<lbrace>\<lambda>rv (s::'state_ext state). \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s\<rbrace>, -" apply (rule validE_validE_R) apply (rule hoare_post_impErr) apply (rule hoare_pre) apply (rule use_spec) apply (rule rec_del_invs') apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap slot exp. \<lbrace>invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>\<lambda>rv s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>cap slot exp. \<lbrace>invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>\<lambda>rv s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>cap slot exp. \<lbrace>invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>?Q2 cap slot exp\<rbrace>, \<lbrace>?E2 cap slot exp\<rbrace>
 2. \<And>cap slot exp rv s. ?Q2 cap slot exp rv s \<Longrightarrow> \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s
 3. \<And>cap slot exp e s. ?E2 cap slot exp e s \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>cap slot exp. \<lbrace>?Q6 cap slot exp\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>?Q2 cap slot exp\<rbrace>, \<lbrace>?E2 cap slot exp\<rbrace>
 2. \<And>cap slot exp s. (invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)) s \<Longrightarrow> ?Q6 cap slot exp s
 3. \<And>cap slot exp rv s. ?Q2 cap slot exp rv s \<Longrightarrow> \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s
 4. \<And>cap slot exp e s. ?E2 cap slot exp e s \<Longrightarrow> True proof (prove)
goal (4 subgoals):
 1. \<And>cap slot exp s. s \<turnstile> \<lbrace>?Q6 cap slot exp\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>?Q2 cap slot exp\<rbrace>, \<lbrace>?E2 cap slot exp\<rbrace>
 2. \<And>cap slot exp s. (invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)) s \<Longrightarrow> ?Q6 cap slot exp s
 3. \<And>cap slot exp rv s. ?Q2 cap slot exp rv s \<Longrightarrow> \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s
 4. \<And>cap slot exp e s. ?E2 cap slot exp e s \<Longrightarrow> True proof (prove)
goal (3 subgoals):
 1. \<And>cap slot exp s. (invs and valid_rec_del_call (ReduceZombieCall cap slot exp) and emptyable slot and (\<lambda>s. \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and K (\<not> cap_removeable cap slot) and (\<lambda>s. \<forall>t\<in>obj_refs cap. halted_if_tcb t s)) s \<Longrightarrow> invs s \<and> valid_rec_del_call (ReduceZombieCall cap slot exp) s \<and> (\<not> exposed_rdcall (ReduceZombieCall cap slot exp) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (ReduceZombieCall cap slot exp)) s) \<and> emptyable (slot_rdcall (ReduceZombieCall cap slot exp)) s \<and> (case ReduceZombieCall cap slot exp of ReduceZombieCall cap sl ex \<Rightarrow> \<not> cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)
 2. \<And>cap slot exp rv s. invs s \<and> (case ReduceZombieCall cap slot exp of CTEDeleteCall x bool \<Rightarrow> True | FinaliseSlotCall sl x \<Rightarrow> (fst rv \<or> x \<longrightarrow> cte_wp_at (replaceable s sl NullCap) sl s) \<and> (snd rv \<noteq> NullCap \<longrightarrow> post_cap_delete_pre (snd rv) ((caps_of_state s)(sl \<mapsto> NullCap))) | ReduceZombieCall cap sl x \<Rightarrow> \<not> x \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) sl s) \<and> emptyable (slot_rdcall (ReduceZombieCall cap slot exp)) s \<Longrightarrow> \<not> exp \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s
 3. \<And>cap slot exp e s. invs s \<Longrightarrow> True proof (prove)
goal:
No subgoals!