theory Finalise_DR

lemma dcorres_page_table_mapped:
   "b < kernel_base
    \<Longrightarrow> dcorres (\<lambda>r r'. r = option_map (\<lambda>x. cdl_lookup_pd_slot x b) r')
    \<top> (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap w (Some (a, b)))))
        (cdl_page_table_mapped (transform_asid a, b) w)
        (page_table_mapped a b w)" apply (simp add:cdl_page_table_mapped_def page_table_mapped_def) apply (rule corres_guard_imp[OF corres_split_catch
      [where f = dc and E = dc and E' =dc]]) apply (rule corres_splitEE[OF dcorres_find_pd_for_asid]) apply (rule_tac F =" is_aligned pda 14" in corres_gen_asm2) apply (clarsimp simp:liftE_bindE dcorres_lookup_pd_slot) apply (rule corres_split[OF dcorres_get_pde]) apply (case_tac  rv') apply (simp add:transform_pde_def) apply (rule dcorres_returnOk,simp) apply (simp add:transform_pde_def PPtrPAddr) apply (intro conjI impI) apply (rule dcorres_returnOk,simp) apply (rule dcorres_returnOk,simp) apply (simp add:transform_pde_def) apply (rule dcorres_returnOk,simp) apply (simp add:transform_pde_def) apply (rule dcorres_returnOk,simp) apply wp+ apply (rule hoare_post_imp_R[OF find_pd_for_asid_aligned_pd]) apply simp apply (erule less_kernel_base_mapping_slots) apply (simp add:pd_bits_def pageBits_def) apply simp apply wp apply ((simp add:dc_def,rule hoareE_TrueI[where P = \<top>])|wp)+ apply simp+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b < kernel_base \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (\<lambda>_. True) (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) (cdl_page_table_mapped (transform_asid a, b) w) (page_table_mapped a b w) proof (prove)
goal (1 subgoal):
 1. b < kernel_base \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (\<lambda>_. True) (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) (doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE <catch> (\<lambda>y. return None)) (doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None)) proof (prove)
goal (6 subgoals):
 1. b < kernel_base \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) ?P1 ?P'1 (doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE) (doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE)
 2. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> (?P1 and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (?P'1 and ?Q'1) s proof (prove)
goal (8 subgoals):
 1. \<And>pd pda. \<lbrakk>b < kernel_base; pd = pda\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R8 pd) (?R'8 pda) (liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)) (liftE (get_pde (lookup_pd_slot pda b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pda else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None))
 2. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 7. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 8. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (8 subgoals):
 1. \<And>pd pda. \<lbrakk>b < kernel_base; pd = pda; is_aligned pda 14\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R8 pd) (?P'14 pda) (liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)) (liftE (get_pde (lookup_pd_slot pda b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pda else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None))
 2. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. ?P'14 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 7. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 8. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (8 subgoals):
 1. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R8 pda) (?P'14 pda) (cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) >>= case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)) (get_pde (lookup_pd_slot pda b) >>= case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pda else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None))
 2. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. ?P'14 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 7. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 8. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (10 subgoals):
 1. \<And>pda rv rv'. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 2. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>?R18 pda\<rbrace>
 3. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>?R'18 pda\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 10. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (13 subgoals):
 1. \<And>pda rv rv'. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 2. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>?R18 pda\<rbrace>
 6. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>?R'18 pda\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pda rv rv'. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = cdl_cap.NullCap; rv' = InvalidPDE\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda cdl_cap.NullCap) (?R'18 pda InvalidPDE) (returnOk None) (returnOk None)
 2. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (?R18 pda rv) (?R'18 pda rv') (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>?R18 pda\<rbrace>
 6. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>?R'18 pda\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 2. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 9. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> (ptrFromPAddr x21 = w \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk (Some (cdl_lookup_pd_slot pda b))) (returnOk (Some pda))) \<and> (ptrFromPAddr x21 \<noteq> w \<longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk None) (returnOk None))
 2. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 9. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23; ptrFromPAddr x21 = w\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk (Some (cdl_lookup_pd_slot pda b))) (returnOk (Some pda))
 2. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23; ptrFromPAddr x21 \<noteq> w\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk None) (returnOk None)
 3. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 6. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 9. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>pda rv rv' x21 x22 x23. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = cdl_cap.PageTableCap (ptrFromPAddr x21) Fake None; rv' = PageTablePDE x21 x22 x23; ptrFromPAddr x21 \<noteq> w\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk None) (returnOk None)
 2. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 4. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 8. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 9. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 2. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pda rv rv' x31 x32 x33 x34. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = FrameCap False (ptrFromPAddr x31) x34 20 Fake None; rv' = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk None) (returnOk None)
 2. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 3. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 10. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = transform_pde rv'; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (case rv of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pda b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None) (case rv' of PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr w = addr then Some pda else None) | _ \<Rightarrow> returnOk None)
 2. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 10. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (10 subgoals):
 1. \<And>pda rv rv' x41 x42 x43. \<lbrakk>b < kernel_base; is_aligned pda 14; rv = FrameCap False (ptrFromPAddr x41) x43 24 Fake None; rv' = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r')) (\<lambda>a. True) (\<lambda>a. True) (returnOk None) (returnOk None)
 2. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 9. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 10. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (9 subgoals):
 1. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q18 pda\<rbrace> cdl_get_pde (transform_pd_slot_ref (lookup_pd_slot pda b)) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>pda. \<lbrakk>b < kernel_base; is_aligned pda 14\<rbrakk> \<Longrightarrow> \<lbrace>?Q'18 pda\<rbrace> get_pde (lookup_pd_slot pda b) \<lbrace>\<lambda>a b. True\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q8\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>\<lambda>pda. (\<lambda>_. True) and ?Q18 pda\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'8\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>pda. valid_idle and K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pda b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and ?Q'18 pda and (\<lambda>s. is_aligned pda 14)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 6. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 7. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 8. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q8 and ?Q1) s
 9. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and ?Q'8 and ?Q'1) s proof (prove)
goal (6 subgoals):
 1. b < kernel_base \<Longrightarrow> \<lbrace>?P'62\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>rv s. K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) s \<and> True \<and> is_aligned rv 14\<rbrace>, -
 2. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> ?P'62 s) and ?Q'1) s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. \<lbrakk>b < kernel_base; is_aligned rv 14\<rbrakk> \<Longrightarrow> K (UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv b && mask pd_bits >> 2) \<notin> kernel_mapping_slots) s \<and> True \<and> is_aligned rv 14
 2. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<lbrakk>b < kernel_base; is_aligned rv 14\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv b && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (6 subgoals):
 1. \<And>rv. is_aligned rv 14 \<Longrightarrow> is_aligned rv pd_bits
 2. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. \<lbrakk>b < kernel_base; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = map_option (\<lambda>x. cdl_lookup_pd_slot x b) r') (dc y) (dc ya) (return None) (return None)
 2. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 4. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 5. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (4 subgoals):
 1. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> doE pd <- cdl_find_pd_for_asid (transform_asid a, b);
liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) >>=E case_cdl_cap (returnOk None) (\<lambda>bool set1 set2. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word1 word2 set. returnOk None) (\<lambda>word set. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word1 word2 nat1 nat2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. returnOk None) (\<lambda>word bool1 bool2. returnOk None) (\<lambda>word. returnOk None) (returnOk None) (returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>bool word set nat cdl_frame_cap_type option. returnOk None) (\<lambda>ref cdl_frame_cap_type option. case cdl_frame_cap_type of Real \<Rightarrow> returnOk None | Fake \<Rightarrow> case option of None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | Some a \<Rightarrow> returnOk None) (\<lambda>word cdl_frame_cap_type option. returnOk None) (returnOk None) (\<lambda>word nat. returnOk None) (\<lambda>word set. returnOk None) (returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None) (\<lambda>word. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 2. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 3. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 4. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (6 subgoals):
 1. \<And>pd x. b < kernel_base \<Longrightarrow> \<lbrace>?B72 pd x\<rbrace> case x of cdl_cap.PageTableCap ref Real option \<Rightarrow> returnOk None | cdl_cap.PageTableCap ref Fake None \<Rightarrow> returnOk $ if ref = w then Some (cdl_lookup_pd_slot pd b) else None | cdl_cap.PageTableCap ref Fake (Some a) \<Rightarrow> returnOk None | _ \<Rightarrow> returnOk None \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 2. \<And>pd. b < kernel_base \<Longrightarrow> \<lbrace>?B71 pd\<rbrace> liftE (cdl_get_pde (cdl_lookup_pd_slot pd b)) \<lbrace>?B72 pd\<rbrace>, \<lbrace>dc\<rbrace>
 3. b < kernel_base \<Longrightarrow> \<lbrace>?Q1\<rbrace> cdl_find_pd_for_asid (transform_asid a, b) \<lbrace>?B71\<rbrace>, \<lbrace>dc\<rbrace>
 4. b < kernel_base \<Longrightarrow> \<lbrace>?Q'1\<rbrace> doE pd <- find_pd_for_asid a;
liftE (get_pde (lookup_pd_slot pd b)) >>=E case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr w = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>dc\<rbrace>
 5. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and ?Q1) s
 6. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and ?Q'1) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>b < kernel_base; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True \<and> True) and (\<lambda>_. True)) s
 2. \<And>s. \<lbrakk>b < kernel_base; (invs and valid_cap (ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) s\<rbrakk> \<Longrightarrow> (valid_idle and (\<lambda>s. True \<and> valid_idle s \<and> (pspace_aligned and valid_vspace_objs) s) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>b < kernel_base; invs s \<and> s \<turnstile> ArchObjectCap (arch_cap.PageTableCap w (Some (a, b)))\<rbrakk> \<Longrightarrow> valid_idle s \<and> pspace_aligned s \<and> valid_vspace_objs s proof (prove)
goal:
No subgoals!