theory CNodeInv_R

lemma cteSwap_urz[wp]:
  "\<lbrace>untyped_ranges_zero' and valid_pspace'
    and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> (cteCap cc) = c) c1
    and cte_wp_at' (weak_derived' c' o cteCap) c2
    and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> (cteCap cc) = c') c2
    and cte_wp_at' (weak_derived' c \<circ> cteCap) c1
    and K (c1 \<noteq> c2)\<rbrace>
  cteSwap c c1 c' c2
  \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (simp add: cteSwap_def) apply (rule hoare_pre) apply (rule untyped_ranges_zero_lift) apply wp+ apply clarsimp apply (erule untyped_ranges_zero_delta[where xs="[c1, c2]"]) apply (simp add: modify_map_def) apply clarsimp apply clarsimp apply (clarsimp simp: ran_restrict_map_insert cte_wp_at_ctes_of
                        cteCaps_of_def modify_map_def) apply (drule(1) weak_derived_untypedZeroRange)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and K (c1 \<noteq> c2)\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and valid_pspace' and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and (\<lambda>y. c1 \<noteq> 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. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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. untyped_ranges_zero'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and valid_pspace' and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and (\<lambda>y. c1 \<noteq> c2)) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (gsUntypedZeroRanges s)\<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 s. P (gsUntypedZeroRanges s)\<rbrace>
 2. \<And>f. \<lbrace>?P3 f\<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 s. untyped_ranges_zero_inv (cteCaps_of s) f\<rbrace>
 3. \<And>s. (untyped_ranges_zero' and valid_pspace' and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and (\<lambda>y. c1 \<noteq> c2)) s \<Longrightarrow> ?P3 (gsUntypedZeroRanges s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (untyped_ranges_zero' and valid_pspace' and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 and cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and (\<lambda>y. c1 \<noteq> c2)) s \<Longrightarrow> untyped_ranges_zero_inv (modify_map (modify_map (cteCaps_of s) c1 (K c')) c2 (K c)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>untyped_ranges_zero' s; valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv (modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c)) (gsUntypedZeroRanges s) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> \<forall>p. p \<notin> set [c1, c2] \<longrightarrow> modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) p = cteCaps_of s p
 2. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> valid_mdb' s
 3. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2; ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c)) |` set [c1, c2]) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> valid_mdb' s
 2. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> valid_objs' s
 3. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2; ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c)) |` set [c1, c2]) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2; ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c)) |` set [c1, c2]) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c) c1 s; cte_wp_at' (weak_derived' c' \<circ> cteCap) c2 s; cte_wp_at' (\<lambda>cc. isUntypedCap (cteCap cc) \<longrightarrow> cteCap cc = c') c2 s; cte_wp_at' (weak_derived' c \<circ> cteCap) c1 s; c1 \<noteq> c2; ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` set [c1, c2]) \<union> ran ((untypedZeroRange \<circ>\<^sub>m modify_map (modify_map (cteCaps_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c)) |` set [c1, c2]) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_pspace' s; c1 \<noteq> c2; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s; set_option (untypedZeroRange (cteCap ctea)) \<subseteq> gsUntypedZeroRanges s; isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; weak_derived' c' (cteCap ctea); ctes_of s c2 = Some ctea; isUntypedCap (cteCap ctea) \<longrightarrow> cteCap ctea = c'; ctes_of s c1 = Some cte; weak_derived' c (cteCap cte)\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange (cteCap ctea))) \<union> (set_option (untypedZeroRange c') \<union> set_option (untypedZeroRange c)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_pspace' s; c1 \<noteq> c2; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s; set_option (untypedZeroRange (cteCap ctea)) \<subseteq> gsUntypedZeroRanges s; isUntypedCap (cteCap cte) \<longrightarrow> cteCap cte = c; ctes_of s c2 = Some ctea; isUntypedCap (cteCap ctea) \<longrightarrow> cteCap ctea = c'; ctes_of s c1 = Some cte; untypedZeroRange c' = untypedZeroRange (cteCap ctea); untypedZeroRange c = untypedZeroRange (cteCap cte)\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange (cteCap ctea))) \<union> (set_option (untypedZeroRange c') \<union> set_option (untypedZeroRange c)) proof (prove)
goal:
No subgoals!