theory CSpace_R

lemma cteInsert_untyped_ranges_zero[wp]:
 "\<lbrace>untyped_ranges_zero' and (\<lambda>s. src \<noteq> dest) and valid_mdb'
    and valid_objs'
    and cte_wp_at' (untyped_derived_eq cap o cteCap) src\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" apply (rule hoare_pre) apply (rule untyped_ranges_zero_lift, wp) apply (simp add: cteInsert_def setUntypedCapAsFull_def) apply (wp getCTE_wp' | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def cteCaps_of_def
                        fun_upd_def[symmetric]) apply (intro impI conjI allI; erule
    untyped_ranges_zero_delta[where xs="[src, dest]", unfolded cteCaps_of_def],
    simp_all add: ran_restrict_map_insert) apply (clarsimp simp: isCap_simps untypedZeroRange_def
                         untyped_derived_eq_def badge_derived'_def
                  split: if_split_asm) apply blast apply (case_tac "isUntypedCap cap", simp_all add: untyped_derived_eq_def) apply (clarsimp simp: isCap_simps untypedZeroRange_def
                        untyped_derived_eq_def badge_derived'_def
                 split: if_split_asm) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero' and (\<lambda>s. src \<noteq> dest) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and (\<lambda>s. src \<noteq> dest) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv s. untyped_ranges_zero_inv (cteCaps_of s) f\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and (\<lambda>s. src \<noteq> dest) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src) s \<Longrightarrow> ?P3 (gsUntypedZeroRanges s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) else return ();
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. untyped_ranges_zero_inv (cteCaps_of s) f\<rbrace>
 2. \<And>s. (untyped_ranges_zero' and (\<lambda>s. src \<noteq> dest) and valid_mdb' and valid_objs' and cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src) s \<Longrightarrow> ?P3 (gsUntypedZeroRanges s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. untyped_ranges_zero' s \<and> src \<noteq> dest \<and> valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' (untyped_derived_eq cap \<circ> cteCap) src s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) src s \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) dest s \<longrightarrow> cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> untyped_ranges_zero_inv (modify_map (modify_map (cteCaps_of s) src (\<lambda>y. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) dest (\<lambda>a. cap)) (gsUntypedZeroRanges s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> untyped_ranges_zero_inv (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) (gsUntypedZeroRanges s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s); src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; untyped_derived_eq cap (cteCap cte); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer\<rbrakk> \<Longrightarrow> (isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap \<longrightarrow> untyped_ranges_zero_inv ((\<lambda>a. map_option cteCap (ctes_of s a))(src \<mapsto> capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte), dest \<mapsto> cap)) (gsUntypedZeroRanges s)) \<and> ((capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap) \<longrightarrow> untyped_ranges_zero_inv ((\<lambda>a. map_option cteCap (ctes_of s a))(dest \<mapsto> cap)) (gsUntypedZeroRanges s)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; untyped_derived_eq cap (cteCap cte); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; isUntypedCap (cteCap cte) \<and> isUntypedCap cap \<and> capPtr (cteCap cte) = capPtr cap \<and> capBlockSize (cteCap cte) = capBlockSize cap; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s \<and> set_option (untypedZeroRange capability.NullCap) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange capability.NullCap)) \<union> (set_option (untypedZeroRange (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap cte))) \<union> set_option (untypedZeroRange cap))
 2. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; untyped_derived_eq cap (cteCap cte); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s \<and> set_option (untypedZeroRange capability.NullCap) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange capability.NullCap)) \<union> (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s cte cteb d v0 v1 f. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; cap = capability.UntypedCap False v0 v1 f; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; cteCap cte = capability.UntypedCap False v0 v1 f; (getFreeRef v0 f, v0 + 2 ^ v1 - 1) \<in> gsUntypedZeroRanges s; f \<noteq> max_free_index v1; \<not> d\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = insert (getFreeRef v0 f, v0 + 2 ^ v1 - 1) (gsUntypedZeroRanges s)
 2. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; untyped_derived_eq cap (cteCap cte); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s \<and> set_option (untypedZeroRange capability.NullCap) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange capability.NullCap)) \<union> (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; untyped_derived_eq cap (cteCap cte); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capPtr (cteCap cte) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap cte) \<longrightarrow> capBlockSize (cteCap cte) \<noteq> capBlockSize cap; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s \<and> set_option (untypedZeroRange capability.NullCap) \<subseteq> gsUntypedZeroRanges s\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange capability.NullCap)) \<union> (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; set_option (untypedZeroRange (cteCap cte)) \<subseteq> gsUntypedZeroRanges s \<and> set_option (untypedZeroRange capability.NullCap) \<subseteq> gsUntypedZeroRanges s; \<not> isUntypedCap cap\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s - (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange capability.NullCap)) \<union> (set_option (untypedZeroRange (cteCap cte)) \<union> set_option (untypedZeroRange cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>src \<noteq> dest; valid_mdb' s; valid_objs' s; ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; set_option (let cap = cteCap cte in if \<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f then if capFreeIndex cap = max_free_index (capBlockSize cap) \<or> capIsDevice cap then None else Some (getFreeRef (capPtr cap) (capFreeIndex cap), capPtr cap + 2 ^ capBlockSize cap - 1) else None) \<subseteq> gsUntypedZeroRanges s; \<forall>d v0 v1 f. cap \<noteq> capability.UntypedCap d v0 v1 f\<rbrakk> \<Longrightarrow> gsUntypedZeroRanges s = gsUntypedZeroRanges s \<union> set_option (let cap = cteCap cte in if \<exists>d v0 v1 f. cap = capability.UntypedCap d v0 v1 f then if capFreeIndex cap = max_free_index (capBlockSize cap) \<or> capIsDevice cap then None else Some (getFreeRef (capPtr cap) (capFreeIndex cap), capPtr cap + 2 ^ capBlockSize cap - 1) else None) proof (prove)
goal:
No subgoals!