theory Detype_R

lemma createObjects'_page_directory_at':
  "\<lbrace>K (range_cover ptr sz 14 (Suc n)) and
    pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace>
   createObjects' ptr (Suc n) (KOArch (KOPDE makeObject)) 12
   \<lbrace>\<lambda>rv s. (\<forall>x\<le>of_nat n. page_directory_at' (ptr + (x << 14)) s)\<rbrace>" apply (rule createObjects'_wp_subst) apply simp apply (clarsimp simp:valid_def) apply (frule use_valid[OF _  createObjects_ko_at_strg[where 'a = pde]]) apply (simp add:objBits_simps archObjSize_def pdeBits_def) apply simp apply (simp add:projectKO_def projectKO_opt_pde return_def) apply simp apply (clarsimp simp:page_directory_at'_def pdBits_def pageBits_def pdeBits_def) apply (intro conjI) apply (rule aligned_add_aligned[OF range_cover.aligned],simp) apply (rule is_aligned_shiftl_self) apply (simp add:range_cover_def) apply (drule_tac x = "ptr + (x << 14)" in bspec) apply (simp add:createObjects_def bind_def return_def) apply (clarsimp simp:objBits_simps archObjSize_def pdeBits_def) apply (clarsimp simp:typ_at'_def) apply (drule_tac x = y in spec) apply (simp add:obj_at'_real_def objBits_simps archObjSize_def pdeBits_def) apply (erule ko_wp_at'_weakenE) apply (simp add: projectKO_opt_pde) apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz 14 (Suc n)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> createObjects' ptr (Suc n) (KOArch (KOPDE makeObject)) 12 \<lbrace>\<lambda>rv s. \<forall>x\<le>word_of_nat n. page_directory_at' (ptr + (x << 14)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (range_cover ptr sz 14 (Suc n)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 \<lbrace>\<lambda>rv s. \<forall>x\<le>word_of_nat n. page_directory_at' (ptr + (x << 14)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. range_cover ptr sz 14 (Suc n)) and pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 \<lbrace>\<lambda>rv s. \<forall>x\<le>word_of_nat n. page_directory_at' (ptr + (x << 14)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (5 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> range_cover ptr (?sz14 s a b x) (objBitsKO (KOArch (KOPDE makeObject)) + 12) (Suc n)
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> Suc n \<noteq> 0
 3. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> projectKO_opt (KOArch (KOPDE makeObject)) = Some (?val14 s a b x)
 4. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz14 s a b x) s \<and> pspace_aligned' s \<and> pspace_distinct' s
 5. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>xa\<in>set a. \<forall>offs<2 ^ 12. ko_at' (?val14 s a b x) (xa + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (4 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> Suc n \<noteq> 0
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> projectKO_opt (KOArch (KOPDE makeObject)) = Some (?val14 s a b x)
 3. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s
 4. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>xa\<in>set a. \<forall>offs<2 ^ 12. ko_at' (?val14 s a b x) (xa + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> projectKO_opt (KOArch (KOPDE makeObject)) = Some (?val14 s a b x)
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s
 3. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>xa\<in>set a. \<forall>offs<2 ^ 12. ko_at' (?val14 s a b x) (xa + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<2 ^ 12. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<2 ^ 12. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> page_directory_at' (ptr + (x << 14)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> is_aligned (ptr + (x << 14)) 14 \<and> (\<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> is_aligned (ptr + (x << 14)) 14
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (3 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> is_aligned (x << 14) 14
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> 14 \<le> 14
 3. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> 14 \<le> 14
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>x\<in>set a. \<forall>offs<0x1000. ko_at' makeObject (x + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> ptr + (x << 14) \<in> set a
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>offs<0x1000. ko_at' makeObject (ptr + (x << 14) + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b x. \<lbrakk>\<exists>x\<in>fst (createObjects' ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s). (a, b) \<in> fst (case x of (y, s) \<Rightarrow> ({(map (\<lambda>n. ptr + (n << objBitsKO (KOArch (KOPDE makeObject)) + 12)) [0 .e. word_of_nat n], s)}, False)); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n\<rbrakk> \<Longrightarrow> ptr + (x << 14) \<in> set a
 2. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>offs<0x1000. ko_at' makeObject (ptr + (x << 14) + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>offs<0x1000. ko_at' makeObject (ptr + (x << 14) + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. pde_at' (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; \<forall>offs<0x1000. ko_at' makeObject (ptr + (x << 14) + (offs << objBitsKO (KOArch (KOPDE makeObject)))) b; y < 0x1000\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; y < 0x1000 \<longrightarrow> ko_at' makeObject (ptr + (x << 14) + (y << objBitsKO (KOArch (KOPDE makeObject)))) b\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; ko_wp_at' (\<lambda>ko. projectKO_opt ko = Some makeObject) (ptr + (x << 14) + (y << 2)) b\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 14) + (y << 2)) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y ko. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; projectKO_opt ko = Some makeObject\<rbrakk> \<Longrightarrow> koTypeOf ko = ArchT PDET proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y ko. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; (case ko of KOArch (KOPDE e) \<Rightarrow> Some e | KOArch _ \<Rightarrow> None | _ \<Rightarrow> None) = Some makeObject\<rbrakk> \<Longrightarrow> koTypeOf ko = ArchT PDET proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y ko x8. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; (case x8 of KOPDE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some makeObject; ko = KOArch x8\<rbrakk> \<Longrightarrow> archTypeOf x8 = PDET proof (prove)
goal (1 subgoal):
 1. \<And>s a b x y ko arch_kernel_object. \<lbrakk>(a, b) \<in> fst (createObjects ptr (Suc n) (KOArch (KOPDE makeObject)) 12 s); range_cover ptr sz 14 (Suc n); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; x \<le> word_of_nat n; y < 0x1000; (case arch_kernel_object of KOPDE x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some makeObject; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> archTypeOf arch_kernel_object = PDET proof (prove)
goal:
No subgoals!