theory CNodeInv_AI

lemma cap_swap_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a
          and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b\<rbrace>
     cap_swap c a c' b
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: cap_swap_def) apply (wp | simp split del: if_split)+ apply (rule hoare_post_imp) apply (simp only: if_live_then_nonz_cap_def ex_nonz_cap_to_def
                        cte_wp_at_caps_of_state imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_ex_lift
               get_cap_wp)+ apply (clarsimp simp add: cte_wp_at_caps_of_state) apply (frule(1) if_live_then_nonz_capD) apply assumption apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state) apply (subst split_paired_Ex[symmetric]) apply (rule_tac x="if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)"
                    in exI) apply (clarsimp | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>\<lambda>ya. if_live_then_nonz_cap\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. (if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. ?Q37 rv s \<Longrightarrow> if_live_then_nonz_cap s
 2. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>?Q37\<rbrace>
 3. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 4. \<And>s. (if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> set_cap c b \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> obj_at live ptr s \<or> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> ptr \<in> zobj_refs cap)\<rbrace>
 2. \<lbrace>?Q\<rbrace> set_cap c' a \<lbrace>?B1\<rbrace>
 3. \<And>s. (if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs c') b) s \<Longrightarrow> \<forall>x. \<not> obj_at live x s \<or> (\<exists>xa xb. ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c)) xa = Some xb \<and> x \<in> zobj_refs xb) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap capa. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((aa, ba) = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> ((aa, ba) \<noteq> a \<longrightarrow> ((aa, ba) = b \<longrightarrow> x \<in> zobj_refs c) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (\<exists>xa. caps_of_state s (aa, ba) = Some xa \<and> x \<in> zobj_refs xa))) proof (prove)
goal (2 subgoals):
 1. \<And>s x cap capa obj. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; live obj; kheap s x = Some obj\<rbrakk> \<Longrightarrow> live obj
 2. \<And>s x cap capa. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; ex_nonz_cap_to x s\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((aa, ba) = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> ((aa, ba) \<noteq> a \<longrightarrow> ((aa, ba) = b \<longrightarrow> x \<in> zobj_refs c) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (\<exists>xa. caps_of_state s (aa, ba) = Some xa \<and> x \<in> zobj_refs xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap capa. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; ex_nonz_cap_to x s\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((aa, ba) = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> ((aa, ba) \<noteq> a \<longrightarrow> ((aa, ba) = b \<longrightarrow> x \<in> zobj_refs c) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (\<exists>xa. caps_of_state s (aa, ba) = Some xa \<and> x \<in> zobj_refs xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap capa aa ba capb. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; caps_of_state s (aa, ba) = Some capb; x \<in> zobj_refs capb\<rbrakk> \<Longrightarrow> \<exists>aa ba. ((aa, ba) = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> ((aa, ba) \<noteq> a \<longrightarrow> ((aa, ba) = b \<longrightarrow> x \<in> zobj_refs c) \<and> ((aa, ba) \<noteq> b \<longrightarrow> (\<exists>xa. caps_of_state s (aa, ba) = Some xa \<and> x \<in> zobj_refs xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap capa aa ba capb. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; caps_of_state s (aa, ba) = Some capb; x \<in> zobj_refs capb\<rbrakk> \<Longrightarrow> \<exists>xa. (xa = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> (xa \<noteq> a \<longrightarrow> (xa = b \<longrightarrow> x \<in> zobj_refs c) \<and> (xa \<noteq> b \<longrightarrow> (\<exists>xb. caps_of_state s xa = Some xb \<and> x \<in> zobj_refs xb))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cap capa aa ba capb. \<lbrakk>if_live_then_nonz_cap s; caps_of_state s a = Some cap; zobj_refs cap = zobj_refs c; caps_of_state s b = Some capa; zobj_refs capa = zobj_refs c'; obj_at live x s; caps_of_state s (aa, ba) = Some capb; x \<in> zobj_refs capb\<rbrakk> \<Longrightarrow> ((if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)) = a \<longrightarrow> (a = b \<longrightarrow> x \<in> zobj_refs c) \<and> (a \<noteq> b \<longrightarrow> x \<in> zobj_refs c')) \<and> ((if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)) \<noteq> a \<longrightarrow> ((if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)) = b \<longrightarrow> x \<in> zobj_refs c) \<and> ((if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)) \<noteq> b \<longrightarrow> (\<exists>xa. caps_of_state s (if (aa, ba) = a then b else if (aa, ba) = b then a else (aa, ba)) = Some xa \<and> x \<in> zobj_refs xa))) proof (prove)
goal:
No subgoals!