theory KHeap_R

lemma valid_global_refs_lift':
  assumes ctes: "\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>"
  assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>"
  assumes idle: "\<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
  assumes irqn: "\<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>"
  assumes maxObj: "\<And>P. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace>"
  shows "\<lbrace>valid_global_refs'\<rbrace> f \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>" apply (simp add: valid_global_refs'_def valid_refs'_def global_refs'_def valid_cap_sizes'_def) apply (rule hoare_lift_Pf [where f="ksArchState"]) apply (rule hoare_lift_Pf [where f="ksIdleThread"]) apply (rule hoare_lift_Pf [where f="irq_node'"]) apply (rule hoare_lift_Pf [where f="gsMaxObjectSize"]) apply (wp ctes hoare_vcg_const_Ball_lift arch idle irqn maxObj)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> f \<lbrace>\<lambda>_. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> ksIdleThread s \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> ksIdleThread s \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> ksIdleThread s \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> ksIdleThread a \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' a + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of a). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize a)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' a + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of a). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize a)\<rbrace>
 2. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x xa xb. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. xb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. xb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of a). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize a)\<rbrace>
 2. \<And>x xa P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>
 3. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x xa xb xc. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. xb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> xc)\<rbrace> f \<lbrace>\<lambda>_ a. (\<forall>c\<in>ran (ctes_of a). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> xa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD x) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs x)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. xb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of a). 2 ^ capBits (cteCap cte) \<le> xc)\<rbrace>
 2. \<And>x xa xb P. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> f \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace>
 3. \<And>x xa P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>
 4. \<And>x P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal:
No subgoals!