theory ArchAcc_AI

lemma lookup_pt_slot_reachable [wp]:
  "\<lbrace>\<exists>\<rhd> pd and K (is_aligned pd 14 \<and> vptr < kernel_base)
   and valid_arch_state and valid_vspace_objs and equal_kernel_mappings
   and pspace_aligned and valid_global_objs\<rbrace>
  lookup_pt_slot pd vptr
  \<lbrace>\<lambda>pt_slot. \<exists>\<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, -" apply (simp add: pred_conj_def ex_simps [symmetric] del: ex_simps) apply (rule hoare_vcg_ex_lift_R1) apply (rule hoare_pre) apply (rule hoare_post_imp_R) apply (rule lookup_pt_slot_looks_up) prefer 2 apply clarsimp apply assumption apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd 14 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>pt_slot s. \<exists>ref. (ref \<rhd> (pt_slot && ~~ mask pt_bits)) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. \<exists>ref. (ref \<rhd> pd) x \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state x \<and> valid_vspace_objs x \<and> equal_kernel_mappings x \<and> pspace_aligned x \<and> valid_global_objs x\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>pt_slot s. \<exists>ref. (ref \<rhd> (pt_slot && ~~ mask pt_bits)) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>ref. \<lbrace>\<lambda>s. (ref \<rhd> pd) s \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>pt_slot s. \<exists>ref. (ref \<rhd> (pt_slot && ~~ mask pt_bits)) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>ref. \<lbrace>?P'2 ref\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>pt_slot s. \<exists>ref. (ref \<rhd> (pt_slot && ~~ mask pt_bits)) s\<rbrace>, -
 2. \<And>ref s. (ref \<rhd> pd) s \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<Longrightarrow> ?P'2 ref s proof (prove)
goal (3 subgoals):
 1. \<And>ref. \<lbrace>?P'2 ref\<rbrace> lookup_pt_slot pd vptr \<lbrace>?Q'5 ref\<rbrace>, -
 2. \<And>ref rv s. ?Q'5 ref rv s \<Longrightarrow> \<exists>ref. (ref \<rhd> (rv && ~~ mask pt_bits)) s
 3. \<And>ref s. (ref \<rhd> pd) s \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<Longrightarrow> ?P'2 ref s proof (prove)
goal (2 subgoals):
 1. \<And>ref rv s. ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ?ref8 ref) \<rhd> (rv && ~~ mask pt_bits)) s \<Longrightarrow> \<exists>ref. (ref \<rhd> (rv && ~~ mask pt_bits)) s
 2. \<And>ref s. (ref \<rhd> pd) s \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<Longrightarrow> (?ref8 ref \<rhd> pd and K (is_aligned pd 14 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs) s proof (prove)
goal (2 subgoals):
 1. \<And>ref s. (ref \<rhd> pd) s \<and> is_aligned pd 14 \<and> vptr < kernel_base \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<Longrightarrow> (?ref8 ref \<rhd> pd and K (is_aligned pd 14 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs) s
 2. \<And>ref rv s. ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ?ref8 ref) \<rhd> (rv && ~~ mask pt_bits)) s \<Longrightarrow> \<exists>ref. (ref \<rhd> (rv && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>ref s. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s\<rbrakk> \<Longrightarrow> (?ref8 ref \<rhd> pd) s
 2. \<And>ref rv s. ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ?ref8 ref) \<rhd> (rv && ~~ mask pt_bits)) s \<Longrightarrow> \<exists>ref. (ref \<rhd> (rv && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>ref rv s. ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (rv && ~~ mask pt_bits)) s \<Longrightarrow> \<exists>ref. (ref \<rhd> (rv && ~~ mask pt_bits)) s proof (prove)
goal:
No subgoals!