theory Finalise_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 v a && ~~ mask pd_bits) and pspace_aligned
       and valid_idle and K(is_aligned v pd_bits)
       and K (ucast (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots))
    (cdl_lookup_pt_slot v a)
    (lookup_pt_slot v a)" apply (simp add:cdl_lookup_pt_slot_def lookup_pt_slot_def) apply (rule corres_guard_imp) apply (rule_tac F =" is_aligned v 14" in corres_gen_asm2) apply (clarsimp simp:dcorres_lookup_pd_slot) apply (rule corres_splitEE[OF corres_liftE_rel_sum[THEN iffD2,OF dcorres_get_pde] ]) apply (case_tac rv') prefer 2 apply (simp add:transform_pde_def) apply (rule corres_returnOk) apply (erule valid_pde_pt_at) apply (simp add:transform_pde_def)+ apply (rule hoare_TrueI) apply (wp|simp)+ apply (simp add:pd_bits_def pageBits_def) 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 v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and K (is_aligned v pd_bits) and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (cdl_lookup_pt_slot v a) (lookup_pt_slot v a) 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 v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) (liftE (cdl_get_pde (cdl_lookup_pd_slot v a)) >>=E 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 ((a >> 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)) (liftE (get_pde (lookup_pd_slot v a)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((a >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20))) proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) ?Q ?Q' (liftE (cdl_get_pde (cdl_lookup_pd_slot v a)) >>=E 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 ((a >> 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)) (liftE (get_pde (lookup_pd_slot v a)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((a >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. is_aligned v 14 \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) ?Q ?P'4 (liftE (cdl_get_pde (cdl_lookup_pd_slot v a)) >>=E 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 ((a >> 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)) (liftE (get_pde (lookup_pd_slot v a)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((a >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (?P'4 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (3 subgoals):
 1. is_aligned v 14 \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) ?Q ?P'4 (liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) >>=E 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 ((a >> 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)) (liftE (get_pde (lookup_pd_slot v a)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((a >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)))
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (?P'4 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 5. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>rv rv' x31 x32 x33 x34. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>rv rv' x41 x42 x43. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>rv rv' x31 x32 x33 x34. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>rv rv' x41 x42 x43. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned v 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 (cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None)) (?R'7 (PageTablePDE x21 x22 x23)) (returnOk (ptrFromPAddr x21, unat ((a >> 12) && 0xFF))) (returnOk (ptrFromPAddr x21 + ((a >> 12) && 0xFF << 2)))
 2. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>rv rv' x31 x32 x33 x34. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>rv rv' x41 x42 x43. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned v 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; ?R7 (cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None) s; ?R'7 (PageTablePDE x21 x22 x23) s'\<rbrakk> \<Longrightarrow> (ptrFromPAddr x21, unat ((a >> 12) && 0xFF)) = transform_pt_slot_ref (ptrFromPAddr x21 + ((a >> 12) && 0xFF << 2))
 2. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>rv rv' x31 x32 x33 x34. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. \<And>rv rv' x41 x42 x43. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (?R'7 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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 5. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>?R'7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 8. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (\<lambda>a. valid_pde rv' (?s21 rv' a) \<and> pspace_aligned (?s20 rv' a)) (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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 2. \<And>rv rv' x31 x32 x33 x34. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (\<lambda>a. valid_pde rv' (?s21 rv' a) \<and> pspace_aligned (?s20 rv' a)) (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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 3. \<And>rv rv' x41 x42 x43. \<lbrakk>is_aligned v 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) (?R7 rv) (\<lambda>a. valid_pde rv' (?s21 rv' a) \<and> pspace_aligned (?s20 rv' a)) (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 ((a >> 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 + ((a >> 12) && 0xFF << 2)) | _ \<Rightarrow> throwError (MissingCapability 20))
 4. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> liftE (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a))) \<lbrace>?R7\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>\<lambda>a b. valid_pde a (?s21 a b) \<and> pspace_aligned (?s20 a b)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 7. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s
flex-flex pairs:
\<lambda>x21 x22 x23. ?s21 (PageTablePDE x21 x22 x23) \<equiv>\<^sup>? \<lambda>x21 x22 x23. ?s20 (PageTablePDE x21 x22 x23) proof (prove)
goal (4 subgoals):
 1. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q7\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot v a)) \<lbrace>?R7\<rbrace>
 2. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>\<lambda>a b. valid_pde a (?s21 a b) \<and> pspace_aligned (?s20 a b)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 4. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s
flex-flex pairs:
\<lambda>x21 x22 x23. ?s21 (PageTablePDE x21 x22 x23) \<equiv>\<^sup>? \<lambda>x21 x22 x23. ?s20 (PageTablePDE x21 x22 x23) proof (prove)
goal (3 subgoals):
 1. is_aligned v 14 \<Longrightarrow> \<lbrace>?Q'7\<rbrace> liftE (get_pde (lookup_pd_slot v a)) \<lbrace>\<lambda>a b. valid_pde a (?s21 a b) \<and> pspace_aligned (?s20 a b)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q7) s
 3. \<And>s. (valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) and pspace_aligned and valid_idle and (\<lambda>y. is_aligned v pd_bits) and (\<lambda>y. UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) s \<Longrightarrow> (valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'7 and (\<lambda>s. is_aligned v 14)) s
flex-flex pairs:
\<lambda>x21 x22 x23. ?s21 (PageTablePDE x21 x22 x23) \<equiv>\<^sup>? \<lambda>x21 x22 x23. ?s20 (PageTablePDE x21 x22 x23) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_vspace_objs s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot v a && ~~ mask pd_bits)) s) \<and> pspace_aligned s \<and> valid_idle s \<and> is_aligned v pd_bits \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> is_aligned v 14 proof (prove)
goal:
No subgoals!