theory CNodeInv_AI

lemma reduce_zombie_cap_somewhere:
  "\<And>exp cap slot.
    \<lbrace>\<lambda>s::'state_ext state. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace>
      rec_del (ReduceZombieCall cap slot exp)
     \<lbrace>\<lambda>rv s. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace>" subgoal for exp cap slot apply (cases exp, simp_all, wp) apply (cases cap, simp_all add: rec_del_fails) apply (rename_tac word option nat) apply (case_tac nat, simp_all add: rec_del_simps_ext) apply (simp add: cte_wp_at_caps_of_state) apply wp apply safe apply (rule_tac x="fst ((id ((word, replicate (zombie_cte_bits option) False) := slot,
                            slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref))"
             in exI) apply (rule_tac x="snd ((id ((word, replicate (zombie_cte_bits option) False) := slot,
                            slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref))"
             in exI) apply fastforce done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>exp cap slot. \<lbrace>\<lambda>s. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>\<lambda>rv s. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace> rec_del (ReduceZombieCall cap slot exp) \<lbrace>\<lambda>rv s. \<not> exp \<longrightarrow> (\<exists>oref cref. cte_wp_at P (oref, cref) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> exp \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> rec_del (ReduceZombieCall cap slot False) \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x111 x112 x113. \<lbrakk>\<not> exp; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> rec_del (ReduceZombieCall (Zombie x111 x112 x113) slot False) \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word option nat. \<lbrakk>\<not> exp; cap = Zombie word option nat\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> rec_del (ReduceZombieCall (Zombie word option nat) slot False) \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); nat = Suc nata\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> doE y <- assertE ((word, replicate (zombie_cte_bits option) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (word, replicate (zombie_cte_bits option) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at P (oref, cref) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); nat = Suc nata\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P cap\<rbrace> doE y <- assertE ((word, replicate (zombie_cte_bits option) False) \<noteq> slot);
y <- liftE (cap_swap_for_delete (word, replicate (zombie_cte_bits option) False) slot);
returnOk undefined
odE \<lbrace>\<lambda>rv s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata s. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); nat = Suc nata; \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P cap\<rbrakk> \<Longrightarrow> (word, replicate (zombie_cte_bits option) False) \<noteq> slot \<longrightarrow> (\<exists>oref cref cap. (caps_of_state s \<circ> id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref) = Some cap \<and> P cap) proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata s oref cref capa. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); caps_of_state s (oref, cref) = Some capa; P capa; (word, replicate (zombie_cte_bits option) False) \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>oref cref cap. (caps_of_state s \<circ> id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata s oref cref capa. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); caps_of_state s (oref, cref) = Some capa; P capa; (word, replicate (zombie_cte_bits option) False) \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>crefa cap. (caps_of_state s \<circ> id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (fst ((id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref)), crefa) = Some cap \<and> P cap proof (prove)
goal (1 subgoal):
 1. \<And>word option nat nata s oref cref capa. \<lbrakk>\<not> exp; cap = Zombie word option (Suc nata); caps_of_state s (oref, cref) = Some capa; P capa; (word, replicate (zombie_cte_bits option) False) \<noteq> slot\<rbrakk> \<Longrightarrow> \<exists>cap. (caps_of_state s \<circ> id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (fst ((id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref)), snd ((id((word, replicate (zombie_cte_bits option) False) := slot, slot := (word, replicate (zombie_cte_bits option) False))) (oref, cref))) = Some cap \<and> P cap proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!