theory ArchVSpace_AI

lemma lookup_pt_slot_cap_to_multiple1:
  "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits)
                  and K (vptr < kernel_base)
                  and K (is_aligned vptr 16)\<rbrace>
     lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s. is_aligned rv 6 \<and>
             (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None
                                  \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s)\<rbrace>, -" apply (rule hoare_gen_asmE) apply (rule hoare_post_imp_R) apply (rule lookup_pt_slot_cap_to) apply (rule conjI, clarsimp) apply (elim exEI) apply (clarsimp simp: cte_wp_at_caps_of_state is_pt_cap_def
                        valid_cap_def cap_aligned_def
                   del: subsetI) apply (simp add: subset_eq p_0x3C_shift) apply (clarsimp simp: set_upto_enum_step_4) apply (fold mask_def[where n=4, simplified]) apply (subst(asm) le_mask_iff) apply (subst word_plus_and_or_coroll) apply (rule shiftr_eqD[where n=6]) apply (simp add: shiftr_over_and_dist shiftl_shiftr2) apply (simp add: is_aligned_andI2) apply simp apply (simp add: word_ao_dist) apply (simp add: and_not_mask pt_bits_def pageBits_def) apply (drule arg_cong[where f="\<lambda>x. x >> 4"]) apply (simp add: shiftl_shiftr2 shiftr_shiftr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_aligned vptr 16 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. is_aligned vptr 16 \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>?Q'2\<rbrace>, -
 2. \<And>rv s. \<lbrakk>is_aligned vptr 16; ?Q'2 rv s\<rbrakk> \<Longrightarrow> is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>is_aligned vptr 16; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>is_aligned vptr 16; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa. \<lbrakk>is_aligned vptr 16; \<exists>cap. caps_of_state s (x, xa) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (x, xa) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> {rv && ~~ mask pt_bits} proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + rv && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb \<le> 0xF\<rbrakk> \<Longrightarrow> (xb << 2) + rv && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb \<le> mask 4\<rbrakk> \<Longrightarrow> (xb << 2) + rv && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> (xb << 2) + rv && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> (xb << 2) && rv = 0
 2. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> ((xb << 2) || rv) && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (4 subgoals):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> (xb << 2) && rv >> 6 = 0 >> 6
 2. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> is_aligned ((xb << 2) && rv) 6
 3. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> is_aligned 0 6
 4. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> ((xb << 2) || rv) && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (3 subgoals):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> is_aligned ((xb << 2) && rv) 6
 2. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> is_aligned 0 6
 3. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> ((xb << 2) || rv) && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (2 subgoals):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> is_aligned 0 6
 2. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> ((xb << 2) || rv) && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> ((xb << 2) || rv) && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)); is_aligned (rv && ~~ mask pt_bits) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv && ~~ mask pt_bits) asid)) = Some y; typ_at (AArch APageTable) (rv && ~~ mask pt_bits) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> (xb << 2) && ~~ mask pt_bits || rv && ~~ mask pt_bits = rv && ~~ mask pt_bits proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv >> 10 << 10) asid)); is_aligned (rv >> 10 << 10) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv >> 10 << 10) asid)) = Some y; typ_at (AArch APageTable) (rv >> 10 << 10) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 = 0\<rbrakk> \<Longrightarrow> (xb << 2 >> 10 << 10) || (rv >> 10 << 10) = rv >> 10 << 10 proof (prove)
goal (1 subgoal):
 1. \<And>rv s x xa asid y xb. \<lbrakk>is_aligned vptr 16; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap (rv >> 10 << 10) asid)); is_aligned (rv >> 10 << 10) 10; 10 < word_bits; is_aligned rv 6; cap_asid (ArchObjectCap (PageTableCap (rv >> 10 << 10) asid)) = Some y; typ_at (AArch APageTable) (rv >> 10 << 10) s; case asid of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection); xb >> 4 >> 4 = 0 >> 4\<rbrakk> \<Longrightarrow> (xb << 2 >> 10 << 10) || (rv >> 10 << 10) = rv >> 10 << 10 proof (prove)
goal:
No subgoals!