theory Arch_R

lemma createObject_typ_at':
  "\<lbrace>\<lambda>s.  koTypeOf ty = otype \<and> is_aligned ptr (objBitsKO ty) \<and>
         pspace_aligned' s \<and> pspace_no_overlap' ptr (objBitsKO ty) s\<rbrace>
   createObjects' ptr (Suc 0) ty 0
   \<lbrace>\<lambda>rv s. typ_at' otype ptr s\<rbrace>" apply (clarsimp simp:createObjects'_def alignError_def split_def | wp unless_wp | wpc )+ apply (clarsimp simp:obj_at'_def ko_wp_at'_def typ_at'_def pspace_distinct'_def)+ apply (subgoal_tac "ps_clear ptr (objBitsKO ty)
    (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)") apply (simp add:ps_clear_def)+ apply (rule ccontr) apply (drule int_not_emptyD) apply clarsimp apply (unfold pspace_no_overlap'_def) apply (erule allE)+ apply (erule(1) impE) apply (subgoal_tac "x \<in> {x..x + 2 ^ objBitsKO y - 1}") apply (fastforce simp: p_assoc_help) apply (rule first_in_uptoD) apply (drule(1) pspace_alignedD') apply (clarsimp simp: is_aligned_no_wrap' p_assoc_help) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. koTypeOf ty = otype \<and> is_aligned ptr (objBitsKO ty) \<and> pspace_aligned' s \<and> pspace_no_overlap' ptr (objBitsKO ty) s\<rbrace> createObjects' ptr (Suc 0) ty 0 \<lbrace>\<lambda>rv. typ_at' otype ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> typ_at' (koTypeOf ty) ptr (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> typ_at' (koTypeOf ty) ptr (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0; ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc 0) (objBitsKO ty) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>))
 2. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0\<rbrakk> \<Longrightarrow> ps_clear ptr (objBitsKO ty) (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some ty else ksPSpace s a\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0\<rbrakk> \<Longrightarrow> ({ptr..ptr + 2 ^ objBitsKO ty - 1} - {ptr}) \<inter> dom (\<lambda>a. if a = ptr then Some ty else ksPSpace s a) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0; ({ptr..ptr + 2 ^ objBitsKO ty - 1} - {ptr}) \<inter> dom (\<lambda>a. if a = ptr then Some ty else ksPSpace s a) \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0; \<exists>x. x \<in> {ptr..ptr + 2 ^ objBitsKO ty - 1} - {ptr} \<and> x \<in> dom (\<lambda>a. if a = ptr then Some ty else ksPSpace s a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; pspace_no_overlap' ptr (objBitsKO ty) s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> {x..x + 2 ^ objBitsKO ko - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; ksPSpace s (?x71 s x y) = Some (?ko73 s x y) \<longrightarrow> {?x71 s x y..?x71 s x y + 2 ^ objBitsKO (?ko73 s x y) - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}; x \<in> {x..x + 2 ^ objBitsKO y - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}\<rbrakk> \<Longrightarrow> x \<in> {x..x + 2 ^ objBitsKO y - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}\<rbrakk> \<Longrightarrow> x \<in> {x..x + 2 ^ objBitsKO y - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; ksPSpace s x = Some y; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ objBitsKO y - 1 proof (prove)
goal (1 subgoal):
 1. \<And>s x y. \<lbrakk>otype = koTypeOf ty; is_aligned ptr (objBitsKO ty); pspace_aligned' s; ptr && mask (objBitsKO ty) = 0; ptr \<le> x; x \<le> ptr + 2 ^ objBitsKO ty - 1; x \<noteq> ptr; {x..x + 2 ^ objBitsKO y - 1} \<inter> up_aligned_area ptr (objBitsKO ty) = {}; is_aligned x (objBitsKO y)\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ objBitsKO y - 1 proof (prove)
goal:
No subgoals!