theory CSpace_R

lemma cteInsert_valid_globals_simple:
 "\<lbrace>valid_global_refs' and (\<lambda>s. safe_parent_for' (ctes_of s) src cap)\<rbrace>
  cteInsert cap src dest
  \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: cteInsert_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule (1) safe_parent_for_capRange_capBits) apply (drule (1) valid_global_refsD_with_objSize) apply (auto elim: order_trans[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. safe_parent_for' (ctes_of s) src cap)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. safe_parent_for' (ctes_of s) src cap)\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
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. valid_global_refs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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 <- setUntypedCapAsFull (cteCap srcCTE) cap src;
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. valid_global_refs'\<rbrace>
 2. \<And>s. (valid_global_refs' and (\<lambda>s. safe_parent_for' (ctes_of s) src cap)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs' and (\<lambda>s. safe_parent_for' (ctes_of s) src cap)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>ctea. cte_wp_at' ((=) ctea) dest s \<and> (cteCap ctea = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode ctea) = nullPointer \<and> mdbNext (cteMDBNode ctea) = nullPointer \<longrightarrow> (valid_global_refs' s \<and> cte_wp_at' ((=) cte) src s) \<and> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; safe_parent_for' (ctes_of s) src cap; ctes_of s src = Some cte; ctes_of s dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; ctes_of s src = Some cte; ctes_of s dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_global_refs' s; ctes_of s dest = Some ctea; cteCap ctea = capability.NullCap; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte); kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!