theory CNodeInv_R

lemma cteSwap_iflive'[wp]:
  "\<lbrace>if_live_then_nonz_cap'
        and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1
        and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') c2\<rbrace>
     cteSwap c c1 c' c2
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: cteSwap_def) apply (wp | simp)+ apply (rule hoare_post_imp,
          simp only: if_live_then_nonz_cap'_def imp_conv_disj
                     ex_nonz_cap_to'_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             hoare_vcg_ex_lift updateCap_cte_wp_at_cases hoare_weak_lift_imp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule(1) if_live_then_nonz_capE') apply (clarsimp simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of) apply (rule_tac x="(id (c1 := c2, c2 := c1)) cref" in exI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap' and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1 and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') c2\<rbrace> cteSwap c c1 c' c2 \<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>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1 and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') 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. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cte1. \<lbrace>?B2 cte1 ()\<rbrace> updateCap c2 c \<lbrace>\<lambda>ya. if_live_then_nonz_cap'\<rbrace>
 2. \<And>cte1. \<lbrace>?B1 cte1\<rbrace> updateCap c1 c' \<lbrace>?B2 cte1\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE c1 \<lbrace>?B1\<rbrace>
 4. \<And>s. (if_live_then_nonz_cap' and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1 and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') c2) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>cte1. \<lbrace>?B2 cte1 ()\<rbrace> updateCap c2 c \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> ko_wp_at' live' ptr s \<or> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)\<rbrace>
 2. \<And>cte1. \<lbrace>?B1 cte1\<rbrace> updateCap c1 c' \<lbrace>?B2 cte1\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCTE c1 \<lbrace>?B1\<rbrace>
 4. \<And>s. (if_live_then_nonz_cap' and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1 and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') c2) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_live_then_nonz_cap' and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c) c1 and cte_wp_at' (\<lambda>cte. zobj_refs' (cteCap cte) = zobj_refs' c') c2) s \<Longrightarrow> \<forall>x. \<not> ko_wp_at' live' x s \<or> (\<exists>xa. (c2 = xa \<longrightarrow> (c1 = xa \<longrightarrow> cte_wp_at' ((\<lambda>a. x \<in> zobj_refs' (cteCap a)) \<circ> cteCap_update (K c) \<circ> cteCap_update (K c')) xa s) \<and> (c1 \<noteq> xa \<longrightarrow> cte_wp_at' ((\<lambda>a. x \<in> zobj_refs' (cteCap a)) \<circ> cteCap_update (K c)) xa s)) \<and> (c2 \<noteq> xa \<longrightarrow> (c1 = xa \<longrightarrow> cte_wp_at' ((\<lambda>a. x \<in> zobj_refs' (cteCap a)) \<circ> cteCap_update (K c')) xa s) \<and> (c1 \<noteq> xa \<longrightarrow> cte_wp_at' (\<lambda>a. x \<in> zobj_refs' (cteCap a)) xa s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cte ctea. \<lbrakk>if_live_then_nonz_cap' s; ctes_of s c1 = Some cte; zobj_refs' (cteCap cte) = zobj_refs' c; ctes_of s c2 = Some ctea; zobj_refs' (cteCap ctea) = zobj_refs' c'; ko_wp_at' live' x s\<rbrakk> \<Longrightarrow> \<exists>xa. (c2 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c) \<and> (c2 \<noteq> xa \<longrightarrow> (c1 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c') \<and> (c1 \<noteq> xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte \<and> x \<in> zobj_refs' (cteCap cte)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cte ctea. \<lbrakk>ctes_of s c1 = Some cte; zobj_refs' (cteCap cte) = zobj_refs' c; ctes_of s c2 = Some ctea; zobj_refs' (cteCap ctea) = zobj_refs' c'; ko_wp_at' live' x s; ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> \<exists>xa. (c2 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c) \<and> (c2 \<noteq> xa \<longrightarrow> (c1 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c') \<and> (c1 \<noteq> xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte \<and> x \<in> zobj_refs' (cteCap cte)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cte ctea cref cteb. \<lbrakk>ctes_of s c1 = Some cte; zobj_refs' (cteCap cte) = zobj_refs' c; ctes_of s c2 = Some ctea; zobj_refs' (cteCap ctea) = zobj_refs' c'; ko_wp_at' live' x s; ctes_of s cref = Some cteb; x \<in> zobj_refs' (cteCap cteb)\<rbrakk> \<Longrightarrow> \<exists>xa. (c2 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c) \<and> (c2 \<noteq> xa \<longrightarrow> (c1 = xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte) \<and> x \<in> zobj_refs' c') \<and> (c1 \<noteq> xa \<longrightarrow> (\<exists>cte. ctes_of s xa = Some cte \<and> x \<in> zobj_refs' (cteCap cte)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x cte ctea cref cteb. \<lbrakk>ctes_of s c1 = Some cte; zobj_refs' (cteCap cte) = zobj_refs' c; ctes_of s c2 = Some ctea; zobj_refs' (cteCap ctea) = zobj_refs' c'; ko_wp_at' live' x s; ctes_of s cref = Some cteb; x \<in> zobj_refs' (cteCap cteb)\<rbrakk> \<Longrightarrow> (c2 = (id(c1 := c2, c2 := c1)) cref \<longrightarrow> (\<exists>cte. ctes_of s ((id(c1 := c2, c2 := c1)) cref) = Some cte) \<and> x \<in> zobj_refs' c) \<and> (c2 \<noteq> (id(c1 := c2, c2 := c1)) cref \<longrightarrow> (c1 = (id(c1 := c2, c2 := c1)) cref \<longrightarrow> (\<exists>cte. ctes_of s ((id(c1 := c2, c2 := c1)) cref) = Some cte) \<and> x \<in> zobj_refs' c') \<and> (c1 \<noteq> (id(c1 := c2, c2 := c1)) cref \<longrightarrow> (\<exists>cte. ctes_of s ((id(c1 := c2, c2 := c1)) cref) = Some cte \<and> x \<in> zobj_refs' (cteCap cte)))) proof (prove)
goal:
No subgoals!