theory Retype_C

lemma range_cover_gsMaxObjectSize:
  "cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap dev (ptr &&~~ mask sz) sz idx) srcSlot s
    \<Longrightarrow> range_cover ptr sz (APIType_capBits newType userSize) (length destSlots)
    \<Longrightarrow> valid_global_refs' s
    \<Longrightarrow> unat num = length destSlots
    \<Longrightarrow> unat (num << (APIType_capBits newType userSize) :: word32) \<le> gsMaxObjectSize s
        \<and> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s" apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule (1) valid_global_refsD_with_objSize) apply clarsimp apply (rule conjI) apply (frule range_cover.range_cover_compare_bound) apply (drule range_cover.unat_of_nat_n_shift, rule order_refl) apply (drule_tac s="unat num" in sym) apply simp apply (clarsimp simp: range_cover_def) apply (erule order_trans[rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) srcSlot s; range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s \<and> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; ctes_of s srcSlot = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s \<and> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s \<and> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s \<and> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s
 2. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s; length destSlots * 2 ^ APIType_capBits newType userSize + unat (ptr && mask sz) \<le> 2 ^ sz\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s
 2. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s; length destSlots * 2 ^ APIType_capBits newType userSize + unat (ptr && mask sz) \<le> 2 ^ sz; unat (word_of_nat (length destSlots) << APIType_capBits newType userSize) = length destSlots * 2 ^ APIType_capBits newType userSize\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s
 2. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (2 subgoals):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s; length destSlots * 2 ^ APIType_capBits newType userSize + unat (ptr && mask sz) \<le> 2 ^ sz; unat (word_of_nat (length destSlots) << APIType_capBits newType userSize) = length destSlots * 2 ^ APIType_capBits newType userSize; length destSlots = unat num\<rbrakk> \<Longrightarrow> unat (num << APIType_capBits newType userSize) \<le> gsMaxObjectSize s
 2. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) (length destSlots); valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; 2 ^ sz \<le> gsMaxObjectSize s; is_aligned ptr (APIType_capBits newType userSize); sz < 32; APIType_capBits newType userSize \<le> sz; length destSlots + unat (ptr && mask sz >> APIType_capBits newType userSize) \<le> 2 ^ (sz - APIType_capBits newType userSize)\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> gsMaxObjectSize s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>valid_global_refs' s; unat num = length destSlots; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; kernel_data_refs \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; global_refs' s \<subseteq> kernel_data_refs; is_aligned ptr (APIType_capBits newType userSize); sz < 32; APIType_capBits newType userSize \<le> sz; length destSlots + unat (ptr && mask sz >> APIType_capBits newType userSize) \<le> 2 ^ (sz - APIType_capBits newType userSize)\<rbrakk> \<Longrightarrow> 2 ^ APIType_capBits newType userSize \<le> 2 ^ sz proof (prove)
goal:
No subgoals!