theory Arch_DR

lemma lookup_pt_slot_aligned_6':
  "\<lbrace> valid_vspace_objs
  and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))
  and valid_idle and pspace_aligned
  and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace>
  lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6\<rbrace>, -" apply (rule hoare_gen_asmE) apply (simp add:lookup_pt_slot_def) apply (wp|wpc)+ apply clarsimp apply (rule hoare_strengthen_post[where Q = "\<lambda>r. valid_pde r and pspace_aligned"] ) apply wp apply simp+ apply (clarsimp simp:valid_pde_def dest!:pt_aligned split:ARM_A.pde.splits) apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv 6\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>rv s. is_aligned rv 6\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> \<lbrace>?P'48\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>x s. (x = InvalidPDE \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = PageTablePDE xa xb xc \<longrightarrow> is_aligned (ptrFromPAddr xa + ((vptr >> 12) && 0xFF << 2)) 6) \<and> (\<forall>xa xb xc xd. x = SectionPDE xa xb xc xd \<longrightarrow> True) \<and> (\<forall>xa xb xc. x = SuperSectionPDE xa xb xc \<longrightarrow> True)\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> ?P'48 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?P'48\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>x s. \<forall>xa. (\<exists>xb xc. x = PageTablePDE xa xb xc) \<longrightarrow> is_aligned (ptrFromPAddr xa + ((vptr >> 12) && 0xFF << 2)) 6\<rbrace>
 2. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> ?P'48 s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?P'48\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>r. valid_pde r and pspace_aligned\<rbrace>
 2. \<And>rv s. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_pde rv and pspace_aligned) s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa xb. rv = PageTablePDE x xa xb) \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 3. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> ?P'48 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_pde rv and pspace_aligned) s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa xb. rv = PageTablePDE x xa xb) \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_pde rv s \<and> pspace_aligned s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa xb. rv = PageTablePDE x xa xb) \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (6 - 2)
 2. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) (6 - 2)
 2. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 12)
 2. \<And>s x. \<lbrakk>is_aligned pd 14; is_aligned vptr 16; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; pspace_aligned s\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s. \<lbrakk>is_aligned pd 14 \<and> is_aligned vptr 16 \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and valid_idle and pspace_aligned) s\<rbrakk> \<Longrightarrow> True \<and> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<and> pspace_aligned s proof (prove)
goal:
No subgoals!