theory Untyped_AI

lemma caps_no_overlap[simp]: "caps_no_overlap ptr sz s" using cte_wp_at misc cover idx_cases apply - apply (erule disjE) apply (erule cte_wp_at_caps_no_overlapI[OF  _ _ _ range_cover.sz(1)
       [where 'a=machine_word_len, folded word_bits_def]]) apply (simp add:cte_wp_at_caps_of_state)+ apply (erule descendants_range_caps_no_overlapI) apply (simp add:cte_wp_at_caps_of_state desc_range)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_no_overlap ptr sz s proof (prove)
using this:
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s
ct_active s
invs s
range_cover ptr sz (obj_bits_api tp us) (length slots)
idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz

goal (1 subgoal):
 1. caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active s; invs s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr - (ptr && ~~ mask sz)) \<or> reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active s; invs s; range_cover ptr sz (obj_bits_api tp us) (length slots); idx \<le> unat (ptr - (ptr && ~~ mask sz))\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active s; invs s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active 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) ?cref8 s
 2. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active 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>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active 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>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; ct_active s; invs s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); ct_active s; invs s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> caps_no_overlap ptr sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); ct_active s; range_cover ptr sz (obj_bits_api tp us) (length slots); reset \<and> ptr = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (UntypedCap ?dev16 (ptr && ~~ mask sz) sz ?idx16)) ?cref16 s
 2. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); ct_active 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} ?cref16 s proof (prove)
goal:
No subgoals!