theory Retype_C

lemma createObjects'_page_directory_at_global:
  "\<lbrace> \<lambda>s. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n
      \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s
      \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s \<rbrace>
    createObjects' ptr n val gbits
  \<lbrace> \<lambda>rv s. page_directory_at' (armKSGlobalPD (ksArchState s)) s \<rbrace>" apply (simp add: page_directory_at'_def) apply (rule hoare_pre, wp hoare_vcg_all_lift hoare_vcg_const_imp_lift) apply (wps createObjects'_ksArch) apply (wp createObjects'_typ_at[where sz=sz]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> page_directory_at' (armKSGlobalPD (ksArchState s)) s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. page_directory_at' (armKSGlobalPD (ksArchState s)) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s)\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. y < 0x1000 \<Longrightarrow> \<lbrace>?Q10 y\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s\<rbrace>
 2. \<And>s. 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>x<0x1000. ?Q10 x s) proof (prove)
goal (2 subgoals):
 1. \<And>y prev_s. y < 0x1000 \<Longrightarrow> \<lbrace>?P12 y prev_s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. pde_at' (armKSGlobalPD (ksArchState prev_s) + (y << 2))\<rbrace>
 2. \<And>s. 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>x<0x1000. ?P12 x s s) proof (prove)
goal (1 subgoal):
 1. \<And>s. 0 < n \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. pde_at' (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>x<0x1000. n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pde_at' (armKSGlobalPD (ksArchState s) + (x << 2)) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) proof (prove)
goal:
No subgoals!