theory CSpace_R

lemma setCTE_valid_globals[wp]:
  "\<lbrace>valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (cteCap c) = {})
      and (\<lambda>s. 2 ^ capBits (cteCap c) \<le> gsMaxObjectSize s)\<rbrace>
  setCTE p c
  \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>" apply (simp add: valid_global_refs'_def valid_refs'_def pred_conj_def) apply (rule hoare_lift_Pf2 [where f=global_refs']) apply (rule hoare_lift_Pf2 [where f=gsMaxObjectSize]) apply wp apply (clarsimp simp: ran_def valid_cap_sizes'_def) apply metis apply wp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (cteCap c) = {}) and (\<lambda>s. 2 ^ capBits (cteCap c) \<le> gsMaxObjectSize s)\<rbrace> setCTE p c \<lbrace>\<lambda>_. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<forall>c\<in>ran (ctes_of x). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize x) (ctes_of x) \<and> kernel_data_refs \<inter> capRange (cteCap c) = {} \<and> 2 ^ capBits (cteCap c) \<le> gsMaxObjectSize x\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>xa. (\<forall>c\<in>ran (ctes_of xa). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize xa) (ctes_of xa) \<and> kernel_data_refs \<inter> capRange (cteCap c) = {} \<and> 2 ^ capBits (cteCap c) \<le> gsMaxObjectSize xa\<rbrace> setCTE p c \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize a) (ctes_of a)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (global_refs' x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (global_refs' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>xb. (\<forall>c\<in>ran (ctes_of xb). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' xa (ctes_of xb) \<and> kernel_data_refs \<inter> capRange (cteCap c) = {} \<and> 2 ^ capBits (cteCap c) \<le> xa\<rbrace> setCTE p c \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' xa (ctes_of a)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>x. P (gsMaxObjectSize x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (gsMaxObjectSize x)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>x. P (global_refs' x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (global_refs' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' xa (ctes_of s) \<and> kernel_data_refs \<inter> capRange (cteCap c) = {} \<and> 2 ^ capBits (cteCap c) \<le> xa \<Longrightarrow> (\<forall>c\<in>ran ((ctes_of s)(p \<mapsto> c)). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> x \<subseteq> kernel_data_refs \<and> valid_cap_sizes' xa ((ctes_of s)(p \<mapsto> c))
 2. \<And>x P. \<lbrace>\<lambda>x. P (gsMaxObjectSize x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (gsMaxObjectSize x)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>x. P (global_refs' x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (global_refs' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa s. \<lbrakk>\<forall>c. (\<exists>a. ctes_of s a = Some c) \<longrightarrow> kernel_data_refs \<inter> capRange (cteCap c) = {}; x \<subseteq> kernel_data_refs; \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> 2 ^ capBits (cteCap cte) \<le> xa; kernel_data_refs \<inter> capRange (cteCap c) = {}; 2 ^ capBits (cteCap c) \<le> xa\<rbrakk> \<Longrightarrow> (\<forall>ca. (\<exists>a. (a = p \<longrightarrow> c = ca) \<and> (a \<noteq> p \<longrightarrow> ctes_of s a = Some ca)) \<longrightarrow> kernel_data_refs \<inter> capRange (cteCap ca) = {}) \<and> (\<forall>cte. (\<exists>a. (a = p \<longrightarrow> c = cte) \<and> (a \<noteq> p \<longrightarrow> ctes_of s a = Some cte)) \<longrightarrow> 2 ^ capBits (cteCap cte) \<le> xa)
 2. \<And>x P. \<lbrace>\<lambda>x. P (gsMaxObjectSize x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (gsMaxObjectSize x)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>x. P (global_refs' x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (global_refs' x)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x P. \<lbrace>\<lambda>x. P (gsMaxObjectSize x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (gsMaxObjectSize x)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>x. P (global_refs' x)\<rbrace> setCTE p c \<lbrace>\<lambda>_ x. P (global_refs' x)\<rbrace> proof (prove)
goal:
No subgoals!