theory CNodeInv_R

lemma cteSwap_refs[wp]:
  "\<lbrace>valid_global_refs' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1
           and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace>
     cteSwap c c1 c' c2
   \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: cteSwap_def) apply wp apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) valid_global_refsD_with_objSize)+ apply (drule weak_derived_capRange_capBits)+ apply (clarsimp simp: global_refs'_def Int_Un_distrib2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2) s \<Longrightarrow> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange c' = {}) and (\<lambda>s. 2 ^ capBits c' \<le> gsMaxObjectSize s)) s \<and> kernel_data_refs \<inter> capRange c = {} \<and> 2 ^ capBits c \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; ctes_of s c1 = Some cte; weak_derived' c (cteCap cte); ctes_of s c2 = Some ctea; weak_derived' c' (cteCap ctea)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange c' = {} \<and> 2 ^ capBits c' \<le> gsMaxObjectSize s \<and> kernel_data_refs \<inter> capRange c = {} \<and> 2 ^ capBits c \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; weak_derived' c (cteCap cte); weak_derived' c' (cteCap ctea); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s; kernel_data_refs \<inter> capRange (cteCap ctea) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap ctea) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange c' = {} \<and> 2 ^ capBits c' \<le> gsMaxObjectSize s \<and> kernel_data_refs \<inter> capRange c = {} \<and> 2 ^ capBits c \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s; kernel_data_refs \<inter> capRange (cteCap ctea) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap ctea) \<le> gsMaxObjectSize s; capRange (cteCap cte) = capRange c \<and> capBits (cteCap cte) = capBits c; capRange (cteCap ctea) = capRange c' \<and> capBits (cteCap ctea) = capBits c'\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange c' = {} \<and> 2 ^ capBits c' \<le> gsMaxObjectSize s \<and> kernel_data_refs \<inter> capRange c = {} \<and> 2 ^ capBits c \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!