theory ArchRetype_AI

lemma get_master_pde_valid[wp]:
  "\<lbrace>valid_vspace_objs
    and \<exists>\<rhd> (x && ~~mask pd_bits)
    and K (ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace>
   get_master_pde x
   \<lbrace>valid_pde\<rbrace>" apply (simp add: get_master_pde_def get_pde_def) apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift | wpc)+ defer apply (clarsimp simp: mask_lower_twice pd_bits_def pageBits_def)+ apply (drule sym) apply (drule (1) ko_at_obj_congD, clarsimp) apply (drule (2) valid_vspace_objsD) apply simp apply (erule notE, erule bspec) apply (clarsimp simp: kernel_mapping_slots_def not_le) apply (erule le_less_trans[rotated]) apply (rule ucast_mono_le) apply (rule le_shiftr) apply (clarsimp simp: word_bw_comms) apply (clarsimp simp: and.assoc[symmetric]) apply (subst word_bw_comms, rule word_and_le2) apply (rule shiftr_less_t2n) apply (clarsimp simp: pd_bits_def pageBits_def and_mask_less'[where n=14, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> get_master_pde x \<lbrace>valid_pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> do pd <- get_pd ((x && ~~ mask 6) && ~~ mask pd_bits);
case pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) of SuperSectionPDE xa xaa xb \<Rightarrow> return (pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2))) | _ \<Rightarrow> get_pde x
od \<lbrace>valid_pde\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> ((\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> InvalidPDE) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> PageTablePDE xa xb xc) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc xd. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> SectionPDE xa xb xc xd) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> SuperSectionPDE xa xb xc) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> valid_pde (pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> ((\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> InvalidPDE) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> PageTablePDE xa xb xc) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc xd. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> SectionPDE xa xb xc xd) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s) and K (UCAST(32 \<rightarrow> 12) (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s)) \<and> (\<forall>xa xb xc. (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2)) \<noteq> SuperSectionPDE xa xb xc) \<or> (\<forall>pd. ako_at (PageDirectory pd) ((x && ~~ mask 6) && ~~ mask pd_bits) s \<longrightarrow> valid_pde (pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask pd_bits >> 2))) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pd xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; (ref \<rhd> (x && ~~ mask 14)) s; ako_at (PageDirectory pd) (x && ~~ mask 14) s; \<not> valid_pde (pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))) s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2)) = SuperSectionPDE xa xaa xb\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref pd xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; (ref \<rhd> (x && ~~ mask 14)) s; ako_at (PageDirectory pd) (x && ~~ mask 14) s; \<not> valid_pde (pd (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))) s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; (ref \<rhd> (x && ~~ mask 14)) s; \<not> valid_pde (pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))) s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; \<not> valid_pde (pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))) s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2)); valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; \<not> valid_pde (pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))) s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2)); \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) \<notin> kernel_mapping_slots; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2) \<in> - kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2) < UCAST(32 \<rightarrow> 12) (kernel_base >> 20) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2) \<le> UCAST(32 \<rightarrow> 12) (x && mask 14 >> 2) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> (x && ~~ mask 6) && mask 14 >> 2 \<le> x && mask 14 >> 2
 2. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> (x && ~~ mask 6) && mask 14 \<le> x && mask 14
 2. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) (mask 14 && x && ~~ mask 6 >> 2))\<rbrakk> \<Longrightarrow> mask 14 && x && ~~ mask 6 \<le> x && mask 14
 2. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (2 subgoals):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((mask 14 && x) && ~~ mask 6 >> 2))\<rbrakk> \<Longrightarrow> (mask 14 && x) && ~~ mask 6 \<le> x && mask 14
 2. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 >> 2 < 2 ^ LENGTH(12) proof (prove)
goal (1 subgoal):
 1. \<And>s xa xaa xb pda. \<lbrakk>valid_vspace_objs s; ako_at (PageDirectory pda) (x && ~~ mask 14) s; SuperSectionPDE xa xaa xb = pda (UCAST(32 \<rightarrow> 12) ((x && ~~ mask 6) && mask 14 >> 2))\<rbrakk> \<Longrightarrow> x && mask 14 < 2 ^ (2 + LENGTH(12)) proof (prove)
goal:
No subgoals!