theory Retype_R

lemma createNewCaps_global_refs':
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0
       \<and> pspace_aligned' s \<and> pspace_distinct' s
       \<and> pspace_no_overlap' ptr sz s \<and> valid_global_refs' s
       \<and> 0 < gsMaxObjectSize s\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: valid_global_refs'_def valid_cap_sizes'_def valid_refs'_def) apply (rule_tac Q="\<lambda>rv s. \<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. (kernel_data_refs \<inter> capRange (cteCap cte) \<noteq> {}
        \<or> 2 ^ capBits (cteCap cte) > gsMaxObjectSize s)) ptr s \<and> global_refs' s \<subseteq> kernel_data_refs"
                 in hoare_post_imp) apply (auto simp: cte_wp_at_ctes_of linorder_not_less elim!: ranE)[1] apply (rule hoare_pre) apply (simp add: global_refs'_def) apply (rule hoare_use_eq [where f=ksArchState, OF createNewCaps_ksArch]) apply (rule hoare_use_eq [where f=ksIdleThread, OF createNewCaps_it]) apply (rule hoare_use_eq [where f=irq_node', OF createNewCaps_ksInterrupt]) apply (rule hoare_use_eq [where f=gsMaxObjectSize], wp) apply (wp hoare_vcg_all_lift createNewCaps_cte_wp_at2[where sz=sz]) apply (clarsimp simp: cte_wp_at_ctes_of global_refs'_def
                        makeObject_cte) apply (auto simp: linorder_not_less ball_ran_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> valid_global_refs' s \<and> 0 < gsMaxObjectSize s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<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>rv s. \<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) \<noteq> {} \<or> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s \<and> global_refs' s \<subseteq> kernel_data_refs \<Longrightarrow> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s)
 2. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) \<noteq> {} \<or> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s \<and> global_refs' s \<subseteq> kernel_data_refs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) \<noteq> {} \<or> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s \<and> global_refs' s \<subseteq> kernel_data_refs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q32\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) \<noteq> {} \<or> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s \<and> global_refs' s \<subseteq> kernel_data_refs\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?Q32 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q32\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s) \<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\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?Q32 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P37 f\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s) \<and> ksIdleThread s \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD f) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs f)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?P37 (ksArchState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa. \<lbrace>?P57 f fa\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s) \<and> fa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD f) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs f)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?P57 (ksArchState s) (ksIdleThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb. \<lbrace>?P77 f fa fb\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) ptr s) \<and> fa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD f) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs f)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. fb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?P77 (ksArchState s) (ksIdleThread s) (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb fc. \<lbrace>?P97 f fa fb fc\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. (\<forall>ptr. \<not> cte_wp_at' (\<lambda>cte. kernel_data_refs \<inter> capRange (cteCap cte) = {} \<longrightarrow> fc < 2 ^ capBits (cteCap cte)) ptr s) \<and> fa \<in> kernel_data_refs \<and> page_directory_refs' (armKSGlobalPD f) \<subseteq> kernel_data_refs \<and> \<Union> (page_table_refs' ` set (armKSGlobalPTs f)) \<subseteq> kernel_data_refs \<and> range (\<lambda>irq. fb + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs\<rbrace>
 2. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> ?P97 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s) \<and> 0 < gsMaxObjectSize s \<Longrightarrow> (\<forall>x. \<not> cte_wp_at' (\<lambda>a. kernel_data_refs \<inter> capRange (cteCap a) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap a)) x s \<and> \<not> (kernel_data_refs \<inter> capRange (cteCap makeObject) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap makeObject)) \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) \<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> \<not> ?P'110 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) makeObject \<and> n \<noteq> 0 \<and> range_cover ptr sz (APIType_capBits ty us) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; ksIdleThread s \<in> kernel_data_refs; page_directory_refs' (armKSGlobalPD (ksArchState s)) \<subseteq> kernel_data_refs; \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<subseteq> kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s; 0 < gsMaxObjectSize s\<rbrakk> \<Longrightarrow> (\<forall>x cte. ctes_of s x = Some cte \<longrightarrow> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> \<not> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) \<and> \<not> ?P'110 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) (CTE capability.NullCap nullMDBNode) proof (prove)
goal:
No subgoals!