theory ArchAcc_AI

lemma pde_at_aligned_vptr:
  "\<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; page_directory_at pd s;
   pspace_aligned s; is_aligned vptr 24 \<rbrakk>
  \<Longrightarrow> pde_at (x + lookup_pd_slot pd vptr) s" apply (clarsimp simp: lookup_pd_slot_def Let_def
                        obj_at_def pde_at_def) apply (drule(1) pspace_alignedD[rotated]) apply (clarsimp simp: a_type_def
                 split: kernel_object.split_asm
                        arch_kernel_obj.split_asm if_split_asm
                 cong: kernel_object.case_cong) apply (prop_tac "is_aligned x 2") subgoal apply (clarsimp simp: upto_enum_step_def word_shift_by_2) by (rule is_aligned_shiftl_self) apply (simp add: aligned_add_aligned word_bits_conv
                   is_aligned_shiftl_self)+ apply (prop_tac "pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits)") subgoal supply bit_simps[simp del] apply (subst mask_lower_twice[symmetric, where n=6]) apply (simp add: pd_bits_def pageBits_def) apply (subst add.commute, subst add_mask_lower_bits) apply (erule aligned_add_aligned) apply (intro is_aligned_shiftl is_aligned_shiftr) apply simp apply (simp add: word_bits_conv) apply simp apply (subst upper_bits_unset_is_l2p_32[unfolded word_bits_conv]) apply simp apply (clarsimp simp: upto_enum_step_def word_shift_by_2) apply (rule shiftl_less_t2n[where m=6, simplified]) apply (rule word_leq_minus_one_le) apply simp+ 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 (rule shiftr_less_t2n') apply (simp add: pd_bits_def pageBits_def) by (simp add: pd_bits_def pageBits_def)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 24\<rbrakk> \<Longrightarrow> pde_at (x + lookup_pd_slot pd vptr) s proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned (x + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (ArchObj (PageDirectory pda)))\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned (x + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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) \<and> is_aligned (x + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14\<rbrakk> \<Longrightarrow> is_aligned x 2
 2. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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) \<and> is_aligned (x + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14\<rbrakk> \<Longrightarrow> is_aligned x 2 proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> is_aligned (xa << 2) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> (\<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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) \<and> is_aligned (x + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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 proof (prove)
goal (2 subgoals):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits
 2. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2; pd = x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> 6 \<le> pd_bits
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask 6) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = (x + (pd + (vptr >> 20 << 2)) && ~~ mask 6) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (pd + (vptr >> 20 << 2)) 6
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < LENGTH(32) \<longrightarrow> \<not> x !! n'
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 20 << 2) 6
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned x 2\<rbrakk> \<Longrightarrow> 6 \<le> 14
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < LENGTH(32) \<longrightarrow> \<not> x !! n'
 4. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (4 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 20)
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned x 2\<rbrakk> \<Longrightarrow> 6 \<le> 14
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < LENGTH(32) \<longrightarrow> \<not> x !! n'
 4. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned x 2\<rbrakk> \<Longrightarrow> 6 \<le> 14
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < LENGTH(32) \<longrightarrow> \<not> x !! n'
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < LENGTH(32) \<longrightarrow> \<not> x !! n'
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>6. n' < 32 \<longrightarrow> \<not> x !! n'
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> 6 < 32
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> x < 2 ^ 6
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> x < 2 ^ 6
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> xa << 2 < 0x40
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (3 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> xa < 2 ^ (6 - 2)
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (4 subgoals):
 1. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 2 ^ (6 - 2) \<noteq> 0
 2. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> xa \<le> 2 ^ (6 - 2) - 1
 3. \<And>xa. \<lbrakk>is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned (xa << 2) 2; x = xa << 2; xa \<le> 0xF\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 4. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd = pd + (vptr >> 20 << 2) && ~~ mask pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> (vptr >> 20 << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> (vptr >> 20 << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < 32 \<longrightarrow> \<not> (vptr >> 20 << 2) !! n' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits < 32
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> vptr >> 20 << 2 < 2 ^ pd_bits proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> vptr >> 20 < 2 ^ (pd_bits - 2)
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> vptr && mask (20 + (pd_bits - 2)) = vptr
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits - 2 < LENGTH(32)
 3. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits - 2 < LENGTH(32)
 2. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda_)); is_aligned pd 14; is_aligned x 2\<rbrakk> \<Longrightarrow> pd_bits < LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>pda. \<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd 14; is_aligned x 2; pd = x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (x + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) = Some ko \<and> (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 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 proof (prove)
goal:
No subgoals!