theory CNodeInv_R

lemma cteSwap_cte_wp_cteCap:
  "\<lbrace>\<lambda>s. p \<noteq> sl \<and>
       (p = p' \<longrightarrow> cte_at' p' s \<and> P cap') \<and>
       (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace>
  cteSwap cap p' cap' sl
  \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>" apply (simp add: cteSwap_def) apply (rule hoare_pre) apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases getCTE_wp'
             hoare_vcg_all_lift) apply simp apply (wp hoare_drop_imps)[1] apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases
                 getCTE_wp' hoare_vcg_all_lift hoare_weak_lift_imp)+ apply simp apply (clarsimp simp: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace> cteSwap cap p' cap' sl \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s)\<rbrace> do cte1 <- getCTE p';
y <- updateCap p' cap';
y <- updateCap sl cap;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. sl));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. sl));
cte2 <- getCTE sl;
y <- updateMDB p' (const (cteMDBNode cte2));
y <- updateMDB sl (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. p'));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. p'))
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte1 <- getCTE p';
y <- updateCap p' cap';
y <- updateCap sl cap;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. sl));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. sl));
cte2 <- getCTE sl;
y <- updateMDB p' (const (cteMDBNode cte2));
y <- updateMDB sl (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. p'));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. p'))
od \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte1 y ya yb cte. \<lbrace>?P18 cte1 y ya yb cte\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. sl)) \<lbrace>\<lambda>rv s. cte_wp_at' ((=) cte) sl s \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
 2. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. sl)) \<lbrace>\<lambda>yb s. \<forall>x. ?P18 cte1 y ya yb x s\<rbrace>
 3. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap sl cap \<lbrace>?B6 cte1 y\<rbrace>
 4. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap p' cap' \<lbrace>?B5 cte1\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE p' \<lbrace>?B4\<rbrace>
 6. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte1 cte. \<lbrace>?P18 cte1 () () () cte\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. sl)) \<lbrace>\<lambda>rv s. cte_wp_at' ((=) cte) sl s \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>
 2. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. sl)) \<lbrace>\<lambda>yb s. \<forall>x. ?P18 cte1 y ya yb x s\<rbrace>
 3. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap sl cap \<lbrace>?B6 cte1 y\<rbrace>
 4. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap p' cap' \<lbrace>?B5 cte1\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE p' \<lbrace>?B4\<rbrace>
 6. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>cte1 cte. \<lbrace>?P18 cte1 () () () cte\<rbrace> updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. sl)) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. P (cteCap c)) p\<rbrace>
 2. \<And>cte1 y ya. \<lbrace>?B6 cte1 y ya\<rbrace> updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. sl)) \<lbrace>\<lambda>yb s. \<forall>x. ?P18 cte1 y ya yb x s\<rbrace>
 3. \<And>cte1 y. \<lbrace>?B5 cte1 y\<rbrace> updateCap sl cap \<lbrace>?B6 cte1 y\<rbrace>
 4. \<And>cte1. \<lbrace>?B4 cte1\<rbrace> updateCap p' cap' \<lbrace>?B5 cte1\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCTE p' \<lbrace>?B4\<rbrace>
 6. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) p' s \<longrightarrow> (\<forall>x. (sl = p \<longrightarrow> (p' = p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (K cap) \<circ> cteCap_update (K cap')) p s) \<and> (p' \<noteq> p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (K cap)) p s)) \<and> (sl \<noteq> p \<longrightarrow> (p' = p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (K cap')) p s) \<and> (p' \<noteq> p \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> sl \<and> (p = p' \<longrightarrow> cte_wp_at' (\<lambda>_. True) p' s \<and> P cap') \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c)) p s) \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p' s) \<longrightarrow> (sl = p \<longrightarrow> (p' = p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (\<lambda>y. cap) \<circ> cteCap_update (\<lambda>y. cap')) p s) \<and> (p' \<noteq> p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (\<lambda>y. cap)) p s)) \<and> (sl \<noteq> p \<longrightarrow> p' = p \<longrightarrow> cte_wp_at' ((\<lambda>c. P (cteCap c)) \<circ> cteCap_update (\<lambda>y. cap')) p s) proof (prove)
goal:
No subgoals!