theory CNodeInv_AI

lemma cap_swap_zombies[wp]:
  "\<lbrace>zombies_final and cte_wp_at (\<lambda>x. is_zombie x = is_zombie c
                                   \<and> gen_obj_refs x = gen_obj_refs c) a
          and cte_wp_at (\<lambda>x. is_zombie x = is_zombie c' \<and> gen_obj_refs x = gen_obj_refs c') b\<rbrace>
     cap_swap c a c' b
   \<lbrace>\<lambda>rv. zombies_final\<rbrace>" apply (simp only: zombies_final_def final_cap_at_eq
                    cte_wp_at_caps_of_state simp_thms pred_conj_def) apply wp apply (elim conjE) apply (erule allfEI[where f="id ( a := b, b := a )"]) apply (intro impI) apply (drule mp) apply (clarsimp split: if_split_asm) apply (elim exE conjE, simp only: simp_thms option.simps) apply (rule conjI) apply (clarsimp simp: is_cap_simps gen_obj_refs_def) apply (erule allfEI[where f="id ( a := b, b := a )"]) apply (intro impI, elim exE conjE, simp only: simp_thms option.simps gen_obj_refs_eq) apply (clarsimp simp: gen_obj_refs_Int split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and cte_wp_at (\<lambda>x. is_zombie x = is_zombie c \<and> gen_obj_refs x = gen_obj_refs c) a and cte_wp_at (\<lambda>x. is_zombie x = is_zombie c' \<and> gen_obj_refs x = gen_obj_refs c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. ((\<forall>p. (\<exists>cap. caps_of_state x p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state x p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state x p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state x p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (\<exists>cap. caps_of_state x a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c)) \<and> (\<exists>cap. caps_of_state x b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c')\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv s. \<forall>p. (\<exists>cap. caps_of_state s p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state s p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<forall>p. (\<exists>cap. caps_of_state s p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state s p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))) \<and> (\<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c)) \<and> (\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c') \<Longrightarrow> \<forall>p. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<forall>p. (\<exists>cap. caps_of_state s p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state s p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))); \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c\<rbrakk> \<Longrightarrow> \<forall>p. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c; (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})))\<rbrakk> \<Longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c; (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> is_zombie cap) \<longrightarrow> (\<exists>cp. (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))); \<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap\<rbrakk> \<Longrightarrow> \<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c; \<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> is_zombie cap
 2. \<And>s p. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c; \<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap; \<exists>cp. (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))\<rbrakk> \<Longrightarrow> \<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s p. \<lbrakk>\<exists>cap. caps_of_state s b = Some cap \<and> is_zombie cap = is_zombie c' \<and> gen_obj_refs cap = gen_obj_refs c'; \<exists>cap. caps_of_state s a = Some cap \<and> is_zombie cap = is_zombie c \<and> gen_obj_refs cap = gen_obj_refs c; \<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> is_zombie cap; \<exists>cp. (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p) = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))\<rbrakk> \<Longrightarrow> \<exists>cp. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some cap \<and> cap = cp) \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s p cap capa capb cp capc. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; gen_obj_refs cap = gen_obj_refs c'; is_zombie capa = is_zombie c; gen_obj_refs capa = gen_obj_refs c; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp\<rbrakk> \<Longrightarrow> gen_obj_refs capb \<noteq> {} \<and> (\<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs capb \<inter> gen_obj_refs cap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>s p cap capa capb cp capc. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; gen_obj_refs cap = gen_obj_refs c'; is_zombie capa = is_zombie c; gen_obj_refs capa = gen_obj_refs c; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp\<rbrakk> \<Longrightarrow> gen_obj_refs capb \<noteq> {}
 2. \<And>s p cap capa capb cp capc. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; gen_obj_refs cap = gen_obj_refs c'; is_zombie capa = is_zombie c; gen_obj_refs capa = gen_obj_refs c; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs capb \<inter> gen_obj_refs cap = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s p cap capa capb cp capc. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; gen_obj_refs cap = gen_obj_refs c'; is_zombie capa = is_zombie c; gen_obj_refs capa = gen_obj_refs c; gen_obj_refs cp \<noteq> {}; \<forall>p'. (\<exists>cap. caps_of_state s p' = Some cap) \<and> p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s p' = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp\<rbrakk> \<Longrightarrow> \<forall>p'. (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs capb \<inter> gen_obj_refs cap = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s p cap capa capb cp capc p'. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; gen_obj_refs cap = gen_obj_refs c'; is_zombie capa = is_zombie c; gen_obj_refs capa = gen_obj_refs c; gen_obj_refs cp \<noteq> {}; caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp; (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p') = Some cap) \<and> (id(a := b, b := a)) p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p') = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})\<rbrakk> \<Longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap) \<and> p' \<noteq> p \<longrightarrow> (\<exists>cap. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some cap \<and> gen_obj_refs capb \<inter> gen_obj_refs cap = {}) proof (prove)
goal (1 subgoal):
 1. \<And>s p cap capa capb cp capc p' capd. \<lbrakk>caps_of_state s b = Some cap; caps_of_state s a = Some capa; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p = Some capb; is_zombie capb; is_zombie cap = is_zombie c'; obj_refs cap = obj_refs c' \<and> cap_irqs cap = cap_irqs c' \<and> arch_gen_refs cap = arch_gen_refs c'; is_zombie capa = is_zombie c; obj_refs capa = obj_refs c \<and> cap_irqs capa = cap_irqs c \<and> arch_gen_refs capa = arch_gen_refs c; gen_obj_refs cp \<noteq> {}; caps_of_state s ((id(a := b, b := a)) p) = Some cp; capc = cp; (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p') = Some cap) \<and> (id(a := b, b := a)) p' \<noteq> (id(a := b, b := a)) p \<longrightarrow> (\<exists>cap. caps_of_state s ((id(a := b, b := a)) p') = Some cap \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}); p' \<noteq> p; ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) p' = Some capd\<rbrakk> \<Longrightarrow> gen_obj_refs capb \<inter> gen_obj_refs capd = {} proof (prove)
goal:
No subgoals!