theory CSpace_R

lemma cteInsert_valid_globals [wp]:
 "\<lbrace>valid_global_refs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<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 is_derived'_def badge_derived'_def) apply (frule capMaster_eq_capBits_eq) apply (drule capMaster_capRange) apply (drule (1) valid_global_refsD_with_objSize) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<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. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)\<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. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs' and (\<lambda>s. cte_wp_at' (is_derived' (ctes_of s) src cap \<circ> cteCap) src s)) 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 cteb. \<lbrakk>valid_global_refs' s; cap \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isIRQControlCap cap; capMasterCap (cteCap cte) = capMasterCap cap; (capBadge (cteCap cte), capBadge cap) \<in> capBadge_ordering False; isUntypedCap (cteCap cte) \<longrightarrow> descendants_of' src (ctes_of s) = {}; isReplyCap (cteCap cte) = isReplyCap cap; isReplyCap cap \<longrightarrow> capReplyMaster (cteCap cte); isReplyCap cap \<longrightarrow> \<not> capReplyMaster cap; vsCapRef (cteCap cte) = vsCapRef cap \<or> isArchCap isPageCap cap; isArchCap isPageTableCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); isArchCap isPageDirectoryCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = 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 cteb. \<lbrakk>valid_global_refs' s; cap \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isIRQControlCap cap; capMasterCap (cteCap cte) = capMasterCap cap; (capBadge (cteCap cte), capBadge cap) \<in> capBadge_ordering False; isUntypedCap (cteCap cte) \<longrightarrow> descendants_of' src (ctes_of s) = {}; isReplyCap (cteCap cte) = isReplyCap cap; isReplyCap cap \<longrightarrow> capReplyMaster (cteCap cte); isReplyCap cap \<longrightarrow> \<not> capReplyMaster cap; vsCapRef (cteCap cte) = vsCapRef cap \<or> isArchCap isPageCap cap; isArchCap isPageTableCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); isArchCap isPageDirectoryCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capBits (cteCap cte) = capBits cap\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_global_refs' s; cap \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isIRQControlCap cap; (capBadge (cteCap cte), capBadge cap) \<in> capBadge_ordering False; isUntypedCap (cteCap cte) \<longrightarrow> descendants_of' src (ctes_of s) = {}; isReplyCap (cteCap cte) = isReplyCap cap; isReplyCap cap \<longrightarrow> capReplyMaster (cteCap cte); isReplyCap cap \<longrightarrow> \<not> capReplyMaster cap; vsCapRef (cteCap cte) = vsCapRef cap \<or> isArchCap isPageCap cap; isArchCap isPageTableCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); isArchCap isPageDirectoryCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); ctes_of s src = Some cte; ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capBits (cteCap cte) = capBits cap; capRange (cteCap cte) = capRange cap\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte cteb. \<lbrakk>valid_global_refs' s; cap \<noteq> capability.NullCap; \<not> isZombie (cteCap cte); \<not> isIRQControlCap cap; (capBadge (cteCap cte), capBadge cap) \<in> capBadge_ordering False; isUntypedCap (cteCap cte) \<longrightarrow> descendants_of' src (ctes_of s) = {}; isReplyCap (cteCap cte) = isReplyCap cap; isReplyCap cap \<longrightarrow> capReplyMaster (cteCap cte); isReplyCap cap \<longrightarrow> \<not> capReplyMaster cap; vsCapRef (cteCap cte) = vsCapRef cap \<or> isArchCap isPageCap cap; isArchCap isPageTableCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); isArchCap isPageDirectoryCap (cteCap cte) \<longrightarrow> capASID (cteCap cte) = capASID cap \<and> (\<exists>y. capASID (cteCap cte) = Some y); ctes_of s dest = Some cteb; cteCap cteb = capability.NullCap; mdbPrev (cteMDBNode cteb) = nullPointer; mdbNext (cteMDBNode cteb) = nullPointer; capBits (cteCap cte) = capBits cap; capRange (cteCap cte) = capRange cap; 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!