theory Untyped_R

lemma insertNewCap_valid_global_refs':
  "\<lbrace>valid_global_refs' and
        cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte)
            \<and> capBits cap \<le> capBits (cteCap cte)) parent\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: valid_global_refs'_def valid_refs'_cteCaps valid_cap_sizes_cteCaps) apply (rule hoare_pre) apply (rule hoare_use_eq [where f=global_refs', OF insertNewCap_global_refs']) apply (rule hoare_use_eq [where f=gsMaxObjectSize]) apply wp+ apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def ball_ran_eq) apply (frule power_increasing[where a=2], simp) apply (blast intro: order_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)) and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)\<rbrace>
 2. \<And>s. ((\<lambda>s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)) and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> f \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)\<rbrace>
 2. \<And>s. ((\<lambda>s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)) and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent) s \<Longrightarrow> ?P3 (global_refs' s) s proof (prove)
goal (3 subgoals):
 1. \<And>f P. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. P (gsMaxObjectSize s)\<rbrace>
 2. \<And>f fa. \<lbrace>?P16 f fa\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> f \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> fa)\<rbrace>
 3. \<And>s. ((\<lambda>s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)) and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent) s \<Longrightarrow> ?P16 (global_refs' s) (gsMaxObjectSize s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. (\<forall>c\<in>ran (cteCaps_of s). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> gsMaxObjectSize s)) and cte_wp_at' (\<lambda>cte. capRange cap \<subseteq> capRange (cteCap cte) \<and> capBits cap \<le> capBits (cteCap cte)) parent) s \<Longrightarrow> (\<forall>c\<in>ran ((cteCaps_of s)(slot \<mapsto> cap)). kernel_data_refs \<inter> capRange c = {}) \<and> global_refs' s \<subseteq> kernel_data_refs \<and> (\<forall>c\<in>ran ((cteCaps_of s)(slot \<mapsto> cap)). 2 ^ capBits c \<le> gsMaxObjectSize s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>\<forall>x c. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = c) \<longrightarrow> kernel_data_refs \<inter> capRange c = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>x c. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = c) \<longrightarrow> 2 ^ capBits c \<le> gsMaxObjectSize s; ctes_of s parent = Some cte; capRange cap \<subseteq> capRange (cteCap cte); capBits cap \<le> capBits (cteCap cte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>\<forall>x c. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = c) \<longrightarrow> kernel_data_refs \<inter> capRange c = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>x c. (\<exists>z. ctes_of s x = Some z \<and> cteCap z = c) \<longrightarrow> 2 ^ capBits c \<le> gsMaxObjectSize s; ctes_of s parent = Some cte; capRange cap \<subseteq> capRange (cteCap cte); capBits cap \<le> capBits (cteCap cte); (2::?'a50) ^ capBits cap \<le> (2::?'a50) ^ capBits (cteCap cte)\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange cap = {} \<and> 2 ^ capBits cap \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!