theory ArchAcc_R

lemma aligned_distinct_relation_pde_atI'[elim]:
  "\<lbrakk> pde_at p s; pspace_relation (kheap s) (ksPSpace s');
     pspace_aligned' s'; pspace_distinct' s' \<rbrakk>
        \<Longrightarrow> pde_at' p s'" apply (clarsimp simp add: pde_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 pd_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 pd_bits_def pageBits_def) apply (simp add: pd_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: pde_relation_def) apply (drule(2) aligned_distinct_pde_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>pde_at p s; pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'\<rbrakk> \<Longrightarrow> pde_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 pd_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 APageDirectory\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3)); ko = ArchObj (PageDirectory x3); x5 = PageDirectory x3\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>ko x5 x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; ko = ArchObj (PageDirectory x3); x5 = PageDirectory x3; \<forall>(x', P)\<in>obj_relation_cuts (ArchObj (PageDirectory x3)) (p && ~~ mask pd_bits). \<exists>z. ksPSpace s' x' = Some z \<and> P (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<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 pd_bits) + (UCAST(12 \<rightarrow> 32) x << 2)) = Some z \<and> pde_relation x (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> p && mask pd_bits >> 2 < 2 ^ LENGTH(12)
 2. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits >> 2 << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> p && mask pd_bits < 2 ^ (2 + LENGTH(12))
 2. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits >> 2 << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (3 subgoals):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> pd_bits < size p
 2. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 3. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits >> 2 << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> 2 ^ pd_bits \<le> 2 ^ (2 + LENGTH(12))
 2. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits >> 2 << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits >> 2 << 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + ((p && mask pd_bits) && ~~ mask 2)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (2 subgoals):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2\<rbrakk> \<Longrightarrow> is_aligned (p && mask pd_bits) 2
 2. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; \<exists>z. ksPSpace s' ((p && ~~ mask pd_bits) + (p && mask pd_bits)) = Some z \<and> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<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> pde_relation (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (ArchObj (PageDirectory x3)) z\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 pde. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; ksPSpace s' p = Some (KOArch (KOPDE pde)); pde_relation_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (x3 (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) pde\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal (1 subgoal):
 1. \<And>x3 pde. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); pspace_aligned' s'; pspace_distinct' s'; is_aligned p 2; pde_relation_aligned (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2)) (x3 (UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2))) pde; ko_at' pde p s'\<rbrakk> \<Longrightarrow> pde_at' p s' proof (prove)
goal:
No subgoals!