theory CNodeInv_R

lemma cteMove_urz [wp]:
  "\<lbrace>\<lambda>s. untyped_ranges_zero' s
      \<and> valid_pspace' s
      \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s
      \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap = cteCap c) src s
      \<and> cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest s\<rbrace>
     cteMove cap src dest
   \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (clarsimp simp: cteMove_def) apply (rule hoare_pre) apply (wp untyped_ranges_zero_lift getCTE_wp' | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of
             split del: if_split) apply (erule untyped_ranges_zero_delta[where xs="[src, dest]"],
    (clarsimp simp: modify_map_def)+) apply (clarsimp simp: ran_restrict_map_insert modify_map_def
                        cteCaps_of_def untypedZeroRange_def[where ?x0.0=NullCap]) apply (drule weak_derived_untypedZeroRange[OF weak_derived_sym'], clarsimp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. untyped_ranges_zero' s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap = cteCap c) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> cteMove cap src dest \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. untyped_ranges_zero' s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap = cteCap c) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>
 2. \<And>s. untyped_ranges_zero' s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap = cteCap c) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> cap = cteCap c) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) dest s \<longrightarrow> cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s) \<longrightarrow> untyped_ranges_zero_inv (modify_map (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea ctec. \<lbrakk>untyped_ranges_zero' s; valid_pspace' s; weak_derived' (cteCap ctea) cap; isUntypedCap (cteCap ctea) \<longrightarrow> cap = cteCap ctea; cteCap ctec = capability.NullCap; ctes_of s dest = Some ctec; mdbPrev (cteMDBNode ctec) = nullPointer; mdbNext (cteMDBNode ctec) = nullPointer; ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> untyped_ranges_zero_inv (modify_map (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap)) (gsUntypedZeroRanges s) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea ctec. \<lbrakk>valid_pspace' s; weak_derived' (cteCap ctea) cap; isUntypedCap (cteCap ctea) \<longrightarrow> cap = cteCap ctea; cteCap ctec = capability.NullCap; ctes_of s dest = Some ctec; mdbPrev (cteMDBNode ctec) = nullPointer; mdbNext (cteMDBNode ctec) = nullPointer; ctes_of s src = Some ctea; ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {src, dest}) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> (src = dest \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {dest}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m (cteCaps_of s)(dest := map_option (\<lambda>a. capability.NullCap) (map_option (\<lambda>y. cap) (cteCaps_of s dest)))) |` {dest})) \<and> (src \<noteq> dest \<longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - ran ((untypedZeroRange \<circ>\<^sub>m cteCaps_of s) |` {src, dest}) \<union> ran ((untypedZeroRange \<circ>\<^sub>m (cteCaps_of s)(dest := map_option (\<lambda>y. cap) (cteCaps_of s dest), src := map_option (\<lambda>a. capability.NullCap) (cteCaps_of s src))) |` {src, dest})) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea ctec. \<lbrakk>valid_pspace' s; weak_derived' (cteCap ctea) cap; isUntypedCap (cteCap ctea) \<longrightarrow> cap = cteCap ctea; cteCap ctec = capability.NullCap; ctes_of s dest = Some ctec; mdbPrev (cteMDBNode ctec) = nullPointer; mdbNext (cteMDBNode ctec) = nullPointer; ctes_of s src = Some ctea; set_option (untypedZeroRange (cteCap ctea)) \<subseteq> gsUntypedZeroRanges s; src \<noteq> dest\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option (untypedZeroRange (cteCap ctea)) \<union> set_option (untypedZeroRange cap) proof (prove)
goal (1 subgoal):
 1. \<And>s ctea ctec. \<lbrakk>valid_pspace' s; isUntypedCap (cteCap ctea) \<longrightarrow> cap = cteCap ctea; cteCap ctec = capability.NullCap; ctes_of s dest = Some ctec; mdbPrev (cteMDBNode ctec) = nullPointer; mdbNext (cteMDBNode ctec) = nullPointer; ctes_of s src = Some ctea; set_option (untypedZeroRange (cteCap ctea)) \<subseteq> gsUntypedZeroRanges s; src \<noteq> dest; untypedZeroRange cap = untypedZeroRange (cteCap ctea)\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - set_option (untypedZeroRange (cteCap ctea)) \<union> set_option (untypedZeroRange cap) proof (prove)
goal:
No subgoals!