theory CNodeInv_R

lemma capSwap_not_recursive:
  "\<lbrace>\<lambda>s. card (not_recursive_ctes s) \<le> n
     \<and> cte_wp_at' (\<lambda>cte. \<not> (isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1)) p1 s
     \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1) p2 s
     \<and> p1 \<noteq> p2\<rbrace>
     capSwapForDelete p1 p2
   \<lbrace>\<lambda>rv s. card (not_recursive_ctes s) < n\<rbrace>" apply (simp add: not_recursive_ctes_def cteSwap_def capSwapForDelete_def) apply (wp | simp add: o_def | rule getCTE_cteCap_wp)+ apply (simp add: cte_wp_at_ctes_of modify_map_def cteCaps_of_def
             cong: option.case_cong) apply (elim conjE exE) apply (simp cong: conj_cong) apply (erule order_less_le_trans[rotated]) apply (rule psubset_card_mono) apply simp apply (rule psubsetI) apply clarsimp apply (rule_tac f="\<lambda>S. p1 \<in> S" in distinct_lemma) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card (not_recursive_ctes s) \<le> n \<and> cte_wp_at' (\<lambda>cte. \<not> (isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1)) p1 s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1) p2 s \<and> p1 \<noteq> p2\<rbrace> capSwapForDelete p1 p2 \<lbrace>\<lambda>rv s. card (not_recursive_ctes s) < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1) p1 s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1) p2 s \<and> p1 \<noteq> p2\<rbrace> when (p1 \<noteq> p2) (do cap1 <- liftM cteCap (getCTE p1);
cap2 <- liftM cteCap (getCTE p2);
cte1 <- getCTE p1;
y <- updateCap p1 cap2;
y <- updateCap p2 cap1;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. p2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. p2));
cte2 <- getCTE p2;
y <- updateMDB p1 (const (cteMDBNode cte2));
y <- updateMDB p2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. p1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. p1))
od) \<lbrace>\<lambda>rv s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} < n\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. card {ptr. \<exists>cap. cteCaps_of s ptr = Some cap \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1) p1 s \<and> cte_wp_at' (\<lambda>cte. isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1) p2 s \<and> p1 \<noteq> p2 \<Longrightarrow> case cteCaps_of s p1 of None \<Rightarrow> True | Some cap \<Rightarrow> case cteCaps_of s p2 of None \<Rightarrow> True | Some capa \<Rightarrow> card {ptr. \<exists>capb. modify_map (modify_map (cteCaps_of s) p1 (\<lambda>y. capa)) p2 (\<lambda>a. cap) ptr = Some capb \<and> (isZombie capb \<longrightarrow> capZombiePtr capb \<noteq> ptr)} < n proof (prove)
goal (1 subgoal):
 1. \<And>s. card {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n \<and> (\<exists>cte. ctes_of s p1 = Some cte \<and> (isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1)) \<and> (\<exists>cte. ctes_of s p2 = Some cte \<and> isZombie (cteCap cte) \<and> capZombiePtr (cteCap cte) = p1) \<and> p1 \<noteq> p2 \<Longrightarrow> case ctes_of s p1 of None \<Rightarrow> True | Some x2 \<Rightarrow> case ctes_of s p2 of None \<Rightarrow> True | Some x2a \<Rightarrow> card {ptr. (ptr = p1 \<longrightarrow> isZombie (cteCap x2a) \<longrightarrow> capZombiePtr (cteCap x2a) \<noteq> p1) \<and> (ptr \<noteq> p1 \<longrightarrow> (ptr = p2 \<longrightarrow> isZombie (cteCap x2) \<longrightarrow> capZombiePtr (cteCap x2) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr))))} < n proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>card {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n; p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> case ctes_of s p1 of None \<Rightarrow> True | Some x2 \<Rightarrow> case ctes_of s p2 of None \<Rightarrow> True | Some x2a \<Rightarrow> card {ptr. (ptr = p1 \<longrightarrow> isZombie (cteCap x2a) \<longrightarrow> capZombiePtr (cteCap x2a) \<noteq> p1) \<and> (ptr \<noteq> p1 \<longrightarrow> (ptr = p2 \<longrightarrow> isZombie (cteCap x2) \<longrightarrow> capZombiePtr (cteCap x2) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr))))} < n proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>card {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} \<le> n; p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> card {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} < n proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> card {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} < card {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> finite {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}
 2. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} \<subset> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} \<subset> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (2 subgoals):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} \<subseteq> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}
 2. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} \<noteq> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))} \<noteq> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)} proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>p1 \<noteq> p2; ctes_of s p1 = Some cte; isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p1; ctes_of s p2 = Some ctea; isZombie (cteCap ctea); capZombiePtr (cteCap ctea) = p1\<rbrakk> \<Longrightarrow> (p1 \<in> {ptr. ptr \<noteq> p1 \<and> (ptr = p2 \<longrightarrow> isZombie (cteCap cte) \<longrightarrow> capZombiePtr (cteCap cte) \<noteq> p2) \<and> (ptr \<noteq> p2 \<longrightarrow> (\<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)))}) \<noteq> (p1 \<in> {ptr. \<exists>cap. (\<exists>z. ctes_of s ptr = Some z \<and> cteCap z = cap) \<and> (isZombie cap \<longrightarrow> capZombiePtr cap \<noteq> ptr)}) proof (prove)
goal:
No subgoals!