theory Detype_R

lemma placeNewObject_pd_at':
  "\<lbrace>K (is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and
    pspace_aligned' and pspace_distinct'\<rbrace>
   placeNewObject ptr (makeObject::ARM_H.pde)
                      (pdBits - objBits (makeObject::ARM_H.pde))
   \<lbrace>\<lambda>rv s. page_directory_at' ptr s\<rbrace>" apply (simp add:page_directory_at'_def typ_at'_def) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift placeNewObject_ko_wp_at') apply (clarsimp simp:objBits_simps archObjSize_def pteBits_def pdeBits_def pdBits_def) apply (intro conjI) apply (clarsimp simp:pdBits_def pageBits_def word_bits_def)+ apply (clarsimp simp:pdBits_def pageBits_def new_cap_addrs_def objBits_simps archObjSize_def image_def) apply (drule_tac x = "unat x" in bspec) apply clarsimp apply (rule unat_less_helper) apply simp apply (simp add: pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and pspace_aligned' and pspace_distinct'\<rbrace> placeNewObject ptr makeObject (pdBits - objBits makeObject) \<lbrace>\<lambda>rv. page_directory_at' ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and pspace_aligned' and pspace_distinct'\<rbrace> placeNewObject ptr makeObject (pdBits - objBits makeObject) \<lbrace>\<lambda>rv s. is_aligned ptr pdBits \<and> (\<forall>y<0x1000. ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (y << 2)) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> placeNewObject ptr makeObject (pdBits - objBits makeObject) \<lbrace>\<lambda>rv s. is_aligned ptr pdBits \<and> (\<forall>y<0x1000. ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (y << 2)) s)\<rbrace>
 2. \<And>s. ((\<lambda>y. is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and pspace_aligned' and pspace_distinct') s \<Longrightarrow> ?Q3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. is_aligned ptr pdBits) and pspace_no_overlap' ptr pdBits and pspace_aligned' and pspace_distinct') s \<Longrightarrow> is_aligned ptr pdBits \<and> (\<forall>x. \<not> x < 0x1000 \<or> (if ptr + (x << 2) \<in> set (new_cap_addrs (2 ^ (pdBits - objBits makeObject)) ptr (injectKOS makeObject)) then koTypeOf (injectKOS makeObject) = ArchT PDET else ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s) \<and> objBitsKO (injectKOS makeObject) + (pdBits - objBits makeObject) < word_bits \<and> is_aligned ptr (objBitsKO (injectKOS makeObject) + (pdBits - objBits makeObject)) \<and> pspace_no_overlap' ptr (objBitsKO (injectKOS makeObject) + (pdBits - objBits makeObject)) s \<and> pspace_aligned' s \<and> pspace_distinct' s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> (ptr + (x << 2) \<in> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) \<longrightarrow> x < 0x1000 \<longrightarrow> 14 < word_bits) \<and> (ptr + (x << 2) \<notin> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) \<longrightarrow> x < 0x1000 \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s \<and> 14 < word_bits) proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ptr + (x << 2) \<in> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) \<longrightarrow> x < 0x1000 \<longrightarrow> 14 < word_bits
 2. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s\<rbrakk> \<Longrightarrow> ptr + (x << 2) \<notin> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))) \<longrightarrow> x < 0x1000 \<longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s \<and> 14 < word_bits proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; ptr + (x << 2) \<notin> set (new_cap_addrs 4096 ptr (KOArch (KOPDE makeObject))); x < 0x1000\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; \<forall>xa\<in>{0..<4096}. x << 2 \<noteq> word_of_nat xa << pdeBits; x < 0x1000\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000\<rbrakk> \<Longrightarrow> unat x \<in> {0..<4096}
 2. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000; x << 2 \<noteq> word_of_nat (unat x) << pdeBits\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000\<rbrakk> \<Longrightarrow> unat x < 4096
 2. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000; x << 2 \<noteq> word_of_nat (unat x) << pdeBits\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000\<rbrakk> \<Longrightarrow> x < word_of_nat 4096
 2. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000; x << 2 \<noteq> word_of_nat (unat x) << pdeBits\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned ptr 14; pspace_no_overlap' ptr 14 s; pspace_aligned' s; pspace_distinct' s; x < 0x1000; x << 2 \<noteq> word_of_nat (unat x) << pdeBits\<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>ko. koTypeOf ko = ArchT PDET) (ptr + (x << 2)) s proof (prove)
goal:
No subgoals!