theory ArchAInvsPre

lemma obj_bits_data_at:
  "data_at sz (ptrFromPAddr b) s
  \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz" apply (clarsimp simp add: obj_at_def a_type_def data_at_def
                     split: kernel_object.splits arch_kernel_obj.split_asm if_splits) apply (case_tac ko,simp_all) apply fastforce subgoal for ko archko by (case_tac archko,fastforce+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. data_at sz (ptrFromPAddr b) s \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>\<forall>x5. ((\<forall>x1. x5 \<noteq> ASIDPool x1) \<or> ko \<noteq> ArchObj x5) \<and> ((\<forall>x2. x5 \<noteq> PageTable x2) \<or> ko \<noteq> ArchObj x5) \<and> ((\<forall>x3. x5 \<noteq> PageDirectory x3) \<or> ko \<noteq> ArchObj x5) \<and> (ko = ArchObj x5 \<longrightarrow> (\<forall>x41 x42. (x5 = DataPage x41 x42 \<longrightarrow> x41 \<longrightarrow> kheap s (ptrFromPAddr b) = Some (ArchObj (DataPage True x42)) \<and> x42 = sz) \<and> (x41 \<or> x5 \<noteq> DataPage x41 x42))); \<forall>x11 x12. (well_formed_cnode_n x11 x12 \<longrightarrow> ko \<noteq> CNode x11 x12) \<and> (well_formed_cnode_n x11 x12 \<or> ko \<noteq> CNode x11 x12); \<forall>x2. ko \<noteq> TCB x2; \<forall>x3. ko \<noteq> Endpoint x3; \<forall>x4. ko \<noteq> Notification x4\<rbrakk> \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. \<And>ko x11 x12. \<lbrakk>\<forall>x11a x12a. (well_formed_cnode_n x11a x12a \<longrightarrow> x11 = x11a \<longrightarrow> x12 \<noteq> x12a) \<and> (x11 = x11a \<longrightarrow> well_formed_cnode_n x11a x12a \<or> x12 \<noteq> x12a); ko = CNode x11 x12\<rbrakk> \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz
 2. \<And>ko x5. \<lbrakk>\<forall>x5a. ((\<forall>x1. x5a \<noteq> ASIDPool x1) \<or> x5 \<noteq> x5a) \<and> ((\<forall>x2. x5a \<noteq> PageTable x2) \<or> x5 \<noteq> x5a) \<and> ((\<forall>x3. x5a \<noteq> PageDirectory x3) \<or> x5 \<noteq> x5a) \<and> (x5 = x5a \<longrightarrow> (\<forall>x41 x42. (x5a = DataPage x41 x42 \<longrightarrow> x41 \<longrightarrow> kheap s (ptrFromPAddr b) = Some (ArchObj (DataPage True x42)) \<and> x42 = sz) \<and> (x41 \<or> x5a \<noteq> DataPage x41 x42))); ko = ArchObj x5\<rbrakk> \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<And>ko x5. \<lbrakk>\<forall>x5a. ((\<forall>x1. x5a \<noteq> ASIDPool x1) \<or> x5 \<noteq> x5a) \<and> ((\<forall>x2. x5a \<noteq> PageTable x2) \<or> x5 \<noteq> x5a) \<and> ((\<forall>x3. x5a \<noteq> PageDirectory x3) \<or> x5 \<noteq> x5a) \<and> (x5 = x5a \<longrightarrow> (\<forall>x41 x42. (x5a = DataPage x41 x42 \<longrightarrow> x41 \<longrightarrow> kheap s (ptrFromPAddr b) = Some (ArchObj (DataPage True x42)) \<and> x42 = sz) \<and> (x41 \<or> x5a \<noteq> DataPage x41 x42))); ko = ArchObj x5\<rbrakk> \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x5. ((\<forall>x1. x5 \<noteq> ASIDPool x1) \<or> archko \<noteq> x5) \<and> ((\<forall>x2. x5 \<noteq> PageTable x2) \<or> archko \<noteq> x5) \<and> ((\<forall>x3. x5 \<noteq> PageDirectory x3) \<or> archko \<noteq> x5) \<and> (archko = x5 \<longrightarrow> (\<forall>x41 x42. (x5 = DataPage x41 x42 \<longrightarrow> x41 \<longrightarrow> kheap s (ptrFromPAddr b) = Some (ArchObj (DataPage True x42)) \<and> x42 = sz) \<and> (x41 \<or> x5 \<noteq> DataPage x41 x42))); ko = ArchObj archko\<rbrakk> \<Longrightarrow> obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize sz proof (prove)
goal:
No subgoals!