theory ArchAcc_R

lemma aligned_distinct_relation_pte_atI'[elim]:
  "\<lbrakk> pte_at p s; pspace_relation (kheap s) (ksPSpace s');
     pspace_aligned' s'; pspace_distinct' s' \<rbrakk>
        \<Longrightarrow> pte_at' p s'" apply (clarsimp simp add: pte_at_def obj_at_def a_type_def) apply (simp split: Structures_A.kernel_object.split_asm
                     if_split_asm arch_kernel_obj.split_asm) apply (drule(1) pspace_relation_absD) apply (clarsimp simp: other_obj_relation_def) apply (drule_tac x="ucast ((p && mask pt_bits) >> 2)"
                in spec) apply (subst(asm) ucast_ucast_len) apply (rule shiftr_less_t2n) apply (rule less_le_trans, rule and_mask_less_size) apply (simp add: word_size pt_bits_def pageBits_def) apply (simp add: pt_bits_def pageBits_def) apply (simp add: shiftr_shiftl1) apply (subst(asm) is_aligned_neg_mask_eq[where n=2]) apply (erule is_aligned_andI1) apply (subst(asm) add.commute,
         subst(asm) word_plus_and_or_coroll2) apply (clarsimp simp: pte_relation_def) apply (drule(2) aligned_distinct_pte_atI') apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def
                        projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pte_at p s; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; kheap s (p && ~~ mask pt_bits) = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; ko = ArchObj (PageTable x2); x5 = PageTable x2; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (PageTable x2)) (p && ~~ mask pt_bits). \<exists>z. ksPSpace s' x' = Some z \<and> P (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<forall>x. \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) x << 2)) = Some z \<and> pte_relation x (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> p && mask pt_bits >> 2 < 2 ^ LENGTH(8)
 2. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits >> 2 << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> p && mask pt_bits < 2 ^ (2 + LENGTH(8))
 2. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits >> 2 << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> pt_bits < size p
 2. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 3. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits >> 2 << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> 2 ^ pt_bits \<le> 2 ^ (2 + LENGTH(8))
 2. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits >> 2 << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits >> 2 << 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + ((p && mask pt_bits) && ~~ mask 2)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask pt_bits) 2
 2. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pt_bits) + (p && mask pt_bits)) = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' p = Some z \<and> pte_relation (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (ArchObj (PageTable x2)) z\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2 pte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; ksPSpace s' p = Some (KOArch (KOPTE pte)); pte_relation_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (x2 (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) pte\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x2 pte. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; pte_relation_aligned (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2)) (x2 (UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2))) pte; ko_at' pte p s'\<rbrakk> \<Longrightarrow> pte_at' p s' proof (prove)
goal:
No subgoals!