theory Arch_DR

lemma dcorres_lookup_pt_slot:
  "dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) \<top>
  ( 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> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
  (cdl_lookup_pt_slot pd vptr) (lookup_pt_slot pd vptr)" apply (rule dcorres_expand_pfx) apply (clarsimp simp:cdl_lookup_pt_slot_def
    lookup_pt_slot_def liftE_bindE dcorres_lookup_pd_slot) apply (rule corres_guard_imp) apply (rule corres_split[OF dcorres_get_pde]) apply (rule_tac F = "case rv' of ARM_A.pde.PageTablePDE ptab x xa \<Rightarrow>
        is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True"
        in corres_gen_asm2) apply (case_tac rv') prefer 2 apply (clarsimp simp:transform_pde_def) apply (rename_tac pt rights w) apply (rule dcorres_returnOk) apply (clarsimp simp:transform_pt_slot_ref_def
         vaddr_segment_nonsense3 vaddr_segment_nonsense4) apply (subst shiftl_shiftr_id) apply simp apply (rule le_less_trans) apply (rule word_and_le1) apply simp apply simp apply (simp add: transform_pde_def)+ apply (rule hoare_strengthen_post[where Q = "\<lambda>r. valid_pde r and pspace_aligned"] ) apply (wp get_pde_valid) apply (clarsimp simp:valid_pde_def dest!:pt_aligned
      split:ARM_A.pde.splits) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>_. True) (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> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (cdl_lookup_pt_slot pd vptr) (lookup_pt_slot pd vptr) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (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> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) ((=) s) ((=) s') (cdl_lookup_pt_slot pd vptr) (lookup_pt_slot pd vptr) proof (prove)
goal (1 subgoal):
 1. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) ((=) (transform s')) ((=) s') (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> throw | Fake \<Rightarrow> case option of None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Some a \<Rightarrow> throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (get_pde (lookup_pd_slot pd vptr) >>= 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))) proof (prove)
goal (3 subgoals):
 1. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?Q13 s' ref) (?Q'13 s' ref) (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> throw | Fake \<Rightarrow> case option of None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | Some a \<Rightarrow> throw) (\<lambda>word cdl_frame_cap_type option. throw) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (get_pde (lookup_pd_slot pd vptr) >>= 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)))
 2. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ?Q13 s' ref s
 3. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> ?Q'13 s' ref s proof (prove)
goal (5 subgoals):
 1. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?R'17 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 3. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>?R'17 s' ref\<rbrace>
 4. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 5. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (5 subgoals):
 1. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 3. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. ?P'23 s' ref rv' and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 4. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 5. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>s' ref rv rv' x21 x22 x23. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. ?P'23 s' ref rv' and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref rv rv' x21 x22 x23. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. ?P'23 s' ref rv' and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref x21 x22 x23. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr x21) 10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref (cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None)) (?P'23 s' ref (PageTablePDE x21 x22 x23)) (returnOk (ptrFromPAddr x21, unat ((vptr >> 12) && 0xFF))) (returnOk (ptrFromPAddr x21 + ((vptr >> 12) && 0xFF << 2)))
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. ?P'23 s' ref rv' and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref pt rights w. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref (cdl_cap.PageTableCap (ptrFromPAddr pt) Fake None)) (?P'23 s' ref (PageTablePDE pt rights w)) (returnOk (ptrFromPAddr pt, unat ((vptr >> 12) && 0xFF))) (returnOk (ptrFromPAddr pt + ((vptr >> 12) && 0xFF << 2)))
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R17 s' ref rv) (?P'23 s' ref rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>?R17 s' ref\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. ?P'23 s' ref rv' and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref pt rights w. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (ptrFromPAddr pt, unat ((vptr >> 12) && 0xFF)) = transform_pt_slot_ref (ptrFromPAddr pt + ((vptr >> 12) && 0xFF << 2))
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF << 2 >> 2
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (10 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (LENGTH(32) - 2)
 3. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF
 4. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 6. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 7. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 8. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 9. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 10. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (9 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 2 ^ (LENGTH(32) - 2)
 2. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF
 3. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 9. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (10 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF \<le> ?y37 s' ref pt
 2. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> ?y37 s' ref pt < 2 ^ (LENGTH(32) - 2)
 3. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF
 4. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 6. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 7. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 8. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 9. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 10. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (9 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> 0xFF < 2 ^ (LENGTH(32) - 2)
 2. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF
 3. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 9. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (8 subgoals):
 1. \<And>s' ref pt. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned (ptrFromPAddr pt) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF = (vptr >> 12) && 0xFF
 2. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 8. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (7 subgoals):
 1. \<And>s' ref rv rv'. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>s' ref rv rv' x31 x32 x33 x34. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>s' ref rv rv' x41 x42 x43. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; rv = transform_pde rv'; case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> throw | cdl_cap.PageTableCap ref Fake None \<Rightarrow> doE pt <- returnOk ref;
pt_index <- returnOk ((vptr >> 12) && 0xFF);
returnOk (pt, unat pt_index)
odE | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> throw | _ \<Rightarrow> throw) (case rv' of PageTablePDE ptab x xa \<Rightarrow> returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q17 s' ref\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pd vptr)) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv'. (\<lambda>a. True) and (\<lambda>s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True)\<rbrace>
 6. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 7. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (3 subgoals):
 1. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>rv' s. case rv' of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True\<rbrace>
 2. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 3. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (4 subgoals):
 1. \<And>s' ref. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<lbrace>?Q'17 s' ref\<rbrace> get_pde (lookup_pd_slot pd vptr) \<lbrace>\<lambda>r. valid_pde r and pspace_aligned\<rbrace>
 2. \<And>s' ref rv s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; 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> case rv of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True
 3. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 4. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'17 s' ref) s proof (prove)
goal (3 subgoals):
 1. \<And>s' ref rv s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; 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> case rv of PageTablePDE ptab x xa \<Rightarrow> is_aligned (ptrFromPAddr ptab) 10 | _ \<Rightarrow> True
 2. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 3. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. (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)) s proof (prove)
goal (2 subgoals):
 1. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q17 s' ref) s
 2. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. (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)) s proof (prove)
goal (1 subgoal):
 1. \<And>s' ref s. \<lbrakk>valid_vspace_objs s'; (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s'; valid_idle s'; pspace_aligned s'; is_aligned pd 14; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. (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)) s proof (prove)
goal:
No subgoals!