theory Untyped_AI

lemma descendants_range[simp]:
  "descendants_range_in usable_range cref s"
  "descendants_range_in retype_range cref s" proof - have "descendants_range_in usable_range cref 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=machine_word_len, folded word_bits_def]]) apply (simp add:cte_wp_at_caps_of_state desc_range)+ done thus "descendants_range_in usable_range cref s" by simp thus "descendants_range_in retype_range cref 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 s &&& descendants_range_in {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} cref s proof (state)
goal (2 subgoals):
 1. descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s
 2. descendants_range_in {ptr..ptr + word_of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} cref s proof (prove)
goal (1 subgoal):
 1. descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s proof (prove)
using this:
ct_active s
invs s
idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s
range_cover ptr sz (obj_bits_api tp us) (length slots)

goal (1 subgoal):
 1. descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ct_active s; invs s; idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots)\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s
 2. \<lbrakk>ct_active s; invs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = UntypedCap ?dev8 (ptr && ~~ mask sz) sz ?idx8) cref s
 2. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> ?idx8 \<le> unat (ptr && mask sz)
 3. \<lbrakk>ct_active s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); 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 ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s proof (prove)
goal:
No subgoals! proof (state)
this:
descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref s

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

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

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

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

goal:
No subgoals!