theory Untyped_R

lemma descendants_range[simp]:
      "descendants_range_in' usable_range cref (ctes_of s)"
      "descendants_range_in' retype_range cref (ctes_of s)" proof - have "descendants_range_in' usable_range cref (ctes_of s)" using misc idx_cases cte_wp_at' cover apply - apply (erule disjE) apply (erule cte_wp_at_caps_descendants_range_inI'
             [OF _ _ _ range_cover.sz(1)[where 'a=32, folded word_bits_def]]) apply simp+ using desc_range apply simp done thus "descendants_range_in' usable_range cref (ctes_of s)" by simp thus "descendants_range_in' retype_range cref (ctes_of s)" by (rule descendants_range_in_subseteq'[OF _ subset_stuff]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) &&& descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s) proof (state)
goal (2 subgoals):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)
 2. descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
using this:
ct_active' s
invs' s
\<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s
range_cover ptr sz (APIType_capBits tp us) (length slots)

goal (1 subgoal):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots)\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)
 2. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ct_active' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap ?d8 (ptr && ~~ mask sz) sz ?idx8) cref s
 2. \<lbrakk>ct_active' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> ?idx8 \<le> unat (ptr && mask sz)
 3. \<lbrakk>ct_active' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); \<not> reset \<and> idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> range_cover ?ptr9 sz ?sbit9 ?n9
 4. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev ptr sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
using this:
reset \<longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s)

goal (1 subgoal):
 1. \<lbrakk>ct_active' s; invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap dev ptr sz idx) cref s; range_cover ptr sz (APIType_capBits tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..ptr + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal:
No subgoals! proof (state)
this:
descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)

goal (2 subgoals):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)
 2. descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s) proof (prove)
using this:
descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)

goal (1 subgoal):
 1. descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (state)
this:
descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)

goal (1 subgoal):
 1. descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s) proof (prove)
using this:
descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s)

goal (1 subgoal):
 1. descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s) proof (state)
this:
descendants_range_in' {ptr..ptr + word_of_nat (length slots) * 2 ^ APIType_capBits tp us - 1} cref (ctes_of s)

goal:
No subgoals!