theory ArchInvariants_AI

lemma page_table_pte_atI:
  "\<lbrakk> page_table_at p s; x < 2^(pt_bits - 2); pspace_aligned s \<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s" supply bit_simps[simp del] apply (clarsimp simp: obj_at_def pte_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 pt_bits)") subgoal by auto apply (rule sym, rule add_mask_lower_bits) apply (simp add: pt_bits_def pageBits_def) apply simp apply (subst upper_bits_unset_is_l2p_32[unfolded word_bits_conv]) apply (simp add: pt_bits_def pageBits_def) apply (rule shiftl_less_t2n) apply (simp add: pt_bits_def pageBits_def) apply (simp add: pt_bits_def pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) p s; x < 2 ^ (pt_bits - 2); pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) p s; x < 2 ^ (pt_bits - 2); pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (p + (x << 2)) s proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); pspace_aligned s; kheap s p = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (p + (x << 2) && ~~ mask pt_bits) = Some ko \<and> a_type ko = AArch APageTable) \<and> is_aligned (p + (x << 2)) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (p + (x << 2) && ~~ mask pt_bits) = Some ko \<and> a_type ko = AArch APageTable) \<and> is_aligned (p + (x << 2)) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<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 = ArchObj (PageTable x2) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable x2))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko \<noteq> 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>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<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 = ArchObj (PageTable x2) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable x2))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko \<noteq> 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>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10; p = p + (x << 2) && ~~ mask pt_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 = ArchObj (PageTable x2) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable x2))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko \<noteq> 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>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> p = p + (x << 2) && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt_)); is_aligned p 10; p = p + (x << 2) && ~~ mask pt_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 = ArchObj (PageTable x2) \<longrightarrow> kheap s (p + (x << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable x2))) \<and> (\<forall>x3. x5 = PageDirectory x3 \<longrightarrow> ko \<noteq> 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>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> p = p + (x << 2) && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> is_aligned p pt_bits
 2. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < 32 \<longrightarrow> \<not> (x << 2) !! n' proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> pt_bits < 32
 2. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> x << 2 < 2 ^ pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> x < 2 ^ (pt_bits - 2)
 2. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>pt. \<lbrakk>x < 2 ^ (pt_bits - 2); kheap s p = Some (ArchObj (PageTable pt)); is_aligned p 10\<rbrakk> \<Longrightarrow> pt_bits < LENGTH(32) proof (prove)
goal:
No subgoals!