theory Retype_R

lemma createObjects_no_cte_valid_global:
  assumes no_cte: "\<And>c. projectKO_opt val \<noteq> Some (c::cte)"
  assumes no_tcb: "\<And>t. projectKO_opt val \<noteq> Some (t::tcb)"
  shows "\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
        pspace_no_overlap' ptr sz s \<and>
        range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and>
        valid_global_refs' s\<rbrace>
      createObjects ptr n val gbits
   \<lbrace>\<lambda>rv s. valid_global_refs' s\<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 createObjects_ksArch]) apply (rule hoare_use_eq [where f=ksIdleThread, OF createObjects_it]) apply (rule hoare_use_eq [where f=irq_node', OF createObjects_ksInterrupt]) apply (rule hoare_use_eq [where f=gsMaxObjectSize], wp) apply (simp add: createObjects_def) apply (wp hoare_vcg_all_lift createObjects_orig_cte_wp_at2') apply (simp add: no_cte no_tcb split_def cte_wp_at_ctes_of split: option.splits) apply (clarsimp simp: global_refs'_def) apply (auto simp: ball_ran_eq linorder_not_less[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> valid_global_refs' s\<rbrace> createObjects ptr n val gbits \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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)\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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)\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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)\<rbrace> createObjects ptr n val gbits \<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> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?Q32 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q32\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?Q32 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P37 f\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?P37 (ksArchState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa. \<lbrace>?P54 f fa\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?P54 (ksArchState s) (ksIdleThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb. \<lbrace>?P71 f fa fb\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?P71 (ksArchState s) (ksIdleThread s) (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb fc. \<lbrace>?P88 f fa fb fc\<rbrace> createObjects ptr n val gbits \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?P88 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb fc. \<lbrace>?P88 f fa fb fc\<rbrace> do y <- createObjects' ptr n val gbits;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gbits)) [0 .e. word_of_nat n - 1])
od \<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. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> ?P88 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<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> n \<noteq> 0 \<and> range_cover ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> kernel_data_refs \<inter> capRange (cteCap a) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap a)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> ((\<lambda>a. kernel_data_refs \<inter> capRange (cteCap a) = {} \<longrightarrow> gsMaxObjectSize s < 2 ^ capBits (cteCap a)) \<circ> getF) x)) \<and> pspace_no_overlap' ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) 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> n \<noteq> 0 \<and> range_cover ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> ?P'105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x \<Rightarrow> (?P'105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) \<circ> getF) x)) \<and> pspace_no_overlap' ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> 0 < n \<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) \<Longrightarrow> projectKO_opt val = None \<longrightarrow> (\<forall>x. (\<forall>cte. ctes_of s x = Some cte \<longrightarrow> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> \<not> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) \<and> range_cover ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) 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> range_cover ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val + gbits) n; 0 < n; \<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; projectKO_opt val = None\<rbrakk> \<Longrightarrow> (\<forall>x. (\<forall>cte. ctes_of s x = Some cte \<longrightarrow> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> \<not> gsMaxObjectSize s < 2 ^ capBits (cteCap cte)) \<and> range_cover ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz102 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s) x) s) \<and> range_cover ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) (objBitsKO val + gbits) n \<and> pspace_no_overlap' ptr (?sz105 (ksArchState s) (ksIdleThread s) (irq_node' s) (gsMaxObjectSize s)) s proof (prove)
goal:
No subgoals!