theory Untyped_AI

lemma caps_of_state_pspace_no_overlapD:
  "\<lbrakk> caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s;
    idx < 2 ^ sz \<rbrakk>
   \<Longrightarrow> pspace_no_overlap_range_cover (ptr + of_nat idx) sz s" apply (frule(1) caps_of_state_valid) apply (clarsimp simp: valid_cap_simps cap_aligned_def) apply (cut_tac neg_mask_add_aligned[where p=ptr and q="of_nat idx" and n=sz]) apply (rule cte_wp_at_pspace_no_overlapI[where idx=idx and cref=cref], simp_all) apply (simp add: cte_wp_at_caps_of_state) apply (simp add: mask_out_sub_mask) apply (subst unat_of_nat_word_bits, erule order_less_le_trans, simp_all) apply (rule word_of_nat_less) apply (erule order_less_le_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (ptr + word_of_nat idx) sz) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; s \<turnstile> UntypedCap dev ptr sz idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (ptr + word_of_nat idx) sz) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (ptr + word_of_nat idx) sz) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0; ptr + word_of_nat idx && ~~ mask sz = ptr && ~~ mask sz\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (ptr + word_of_nat idx) sz) s
 2. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned ptr sz
 3. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0; ptr + word_of_nat idx && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = UntypedCap ?dev15 ptr sz idx) cref s
 2. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0; ptr + word_of_nat idx && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> idx \<le> unat (ptr + word_of_nat idx && mask sz)
 3. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0; ptr + word_of_nat idx && ~~ mask sz = ptr\<rbrakk> \<Longrightarrow> idx \<le> unat (ptr + word_of_nat idx && mask sz)
 2. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0; word_of_nat idx = ptr + word_of_nat idx && mask sz\<rbrakk> \<Longrightarrow> idx \<le> unat (word_of_nat idx)
 2. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat idx < 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; idx < 2 ^ sz; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> idx < unat (2 ^ sz) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev ptr sz idx); invs s; is_aligned ptr sz; sz < word_bits; valid_untyped (UntypedCap dev ptr sz idx) s; untyped_min_bits \<le> sz; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> 2 ^ sz \<le> unat (2 ^ sz) proof (prove)
goal:
No subgoals!