theory ArchInvariants_AI

lemma page_directory_pde_atI:
  "\<lbrakk> page_directory_at p s; x < 2 ^ pageBits;
         pspace_aligned s \<rbrakk> \<Longrightarrow> pde_at (p + (x << 2)) s" supply bit_simps[simp del] apply (clarsimp simp: obj_at_def pde_at_def) apply (drule (1) pspace_alignedD[rotated]) apply (clarsimp simp: a_type_def
                 split: kernel_object.splits arch_kernel_obj.splits if_split_asm) apply (simp add: aligned_add_aligned is_aligned_shiftl_self word_bits_conv) apply (subgoal_tac "p = (p + (x << 2) && ~~ mask pd_bits)") subgoal by auto apply (rule sym, rule add_mask_lower_bits) apply (simp add: pd_bits_def pageBits_def) apply simp apply (subst upper_bits_unset_is_l2p_32[unfolded word_bits_conv]) apply (simp add: pd_bits_def pageBits_def) apply (rule shiftl_less_t2n) apply (simp add: pd_bits_def pageBits_def) apply (simp add: pd_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) p s; x < 2 ^ pageBits; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (p + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageDirectory) p s; x < 2 ^ pageBits; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (p + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; pspace_aligned s; kheap s p = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (p + (x << 2) && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned (p + (x << 2)) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p (obj_bits (ArchObj (PageDirectory pd)))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (p + (x << 2) && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned (p + (x << 2)) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> (\<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko \<noteq> ArchObj (ASIDPool x1)) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3))) \<and> (\<forall>x41 x42. (x41 \<longrightarrow> x5 = DataPage True x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage True x42)) \<and> (\<not> x41 \<longrightarrow> x5 = DataPage False x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage False x42))))) \<and> is_aligned (p + (x << 2)) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> \<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko \<noteq> ArchObj (ASIDPool x1)) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3))) \<and> (\<forall>x41 x42. (x41 \<longrightarrow> x5 = DataPage True x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage True x42)) \<and> (\<not> x41 \<longrightarrow> x5 = DataPage False x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage False x42)))) proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14; p = p + (x << 2) && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko \<noteq> ArchObj (ASIDPool x1)) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3))) \<and> (\<forall>x41 x42. (x41 \<longrightarrow> x5 = DataPage True x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage True x42)) \<and> (\<not> x41 \<longrightarrow> x5 = DataPage False x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage False x42))))
 2. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> p = p + (x << 2) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd_)); is_aligned p 14; p = p + (x << 2) && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<exists>ko. (\<forall>x11 x12. ko \<noteq> CNode x11 x12) \<and> (\<forall>x2. ko \<noteq> TCB x2) \<and> (\<forall>x3. ko \<noteq> Endpoint x3) \<and> (\<forall>x4. ko \<noteq> Notification x4) \<and> (\<forall>x5. (\<forall>x1. x5 = ASIDPool x1 \<longrightarrow> ko \<noteq> ArchObj (ASIDPool x1)) \<and> (\<forall>x2. x5 = PageTable x2 \<longrightarrow> ko \<noteq> ArchObj (PageTable x2)) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko = ArchObj (PageDirectory x3) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3))) \<and> (\<forall>x41 x42. (x41 \<longrightarrow> x5 = DataPage True x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage True x42)) \<and> (\<not> x41 \<longrightarrow> x5 = DataPage False x42 \<longrightarrow> ko \<noteq> ArchObj (DataPage False x42)))) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> p = p + (x << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> is_aligned p pd_bits
 2. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < 32 \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> pd_bits < 32
 2. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> x < 2 ^ (pd_bits - 2)
 2. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>pd. \<lbrakk>x < 2 ^ pageBits; kheap s p = Some (ArchObj (PageDirectory pd)); is_aligned p 14\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal:
No subgoals!