theory VSpace_R

lemma findPDForASIDAssert_corres:
  "corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd)
           (K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
                 and pspace_aligned and pspace_distinct
                 and valid_vspace_objs and valid_asid_map
                 and vspace_at_asid asid pd and pd_at_uniq asid pd)
           (pspace_aligned' and pspace_distinct' and no_0_obj')
       (find_pd_for_asid_assert asid)
       (findPDForASIDAssert asid)" apply (simp add: find_pd_for_asid_assert_def const_def
                   findPDForASIDAssert_def liftM_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (rule corres_split_catch[OF find_pd_for_asid_corres'[where pd=pd]]) apply (rule_tac P="\<bottom>" and P'="\<top>" in corres_inst) apply (simp add: corres_fail) apply (wp find_pd_for_asid_valids[where pd=pd])+ apply (rule_tac F="is_aligned pda pdBits
                              \<and> pda = pd" in corres_gen_asm) apply (clarsimp simp add: is_aligned_mask[symmetric]) apply (rule_tac P="pde_at pd and pd_at_uniq asid pd
                            and pspace_aligned and pspace_distinct
                            and vspace_at_asid asid pd and valid_asid_map"
                 and P'="pspace_aligned' and pspace_distinct'"
                 in stronger_corres_guard_imp) apply (rule corres_symb_exec_l[where P="pde_at pd and pd_at_uniq asid pd
                                                and valid_asid_map and vspace_at_asid asid pd"]) apply (rule corres_symb_exec_r[where P'="page_directory_at' pd"]) apply (simp add: checkPDUniqueToASID_def ran_option_map
                               checkPDASIDMapMembership_def) apply (rule_tac P'="pd_at_uniq asid pd" in corres_stateAssert_implied) apply (simp add: gets_def bind_assoc[symmetric]
                                stateAssert_def[symmetric, where L="[]"]) apply (rule_tac P'="valid_asid_map and vspace_at_asid asid pd"
                                in corres_stateAssert_implied) apply (rule corres_trivial, simp) apply (clarsimp simp: state_relation_def arch_state_relation_def
                                     valid_asid_map_def
                              split: option.split) apply (drule bspec, erule graph_ofI) apply clarsimp apply (drule(1) pd_at_asid_unique2) apply simp apply (clarsimp simp: state_relation_def arch_state_relation_def
                                    pd_at_uniq_def ran_option_map) apply wp+ apply (simp add: checkPDAt_def stateAssert_def) apply (rule no_fail_pre, wp) apply simp apply (clarsimp simp: pde_at_def obj_at_def a_type_def) apply (clarsimp split: Structures_A.kernel_object.splits
                                 arch_kernel_obj.splits if_split_asm) apply (simp add: get_pde_def exs_valid_def bind_def return_def
                           get_pd_def get_object_def simpler_gets_def) apply wp apply simp apply (simp add: get_pde_def get_pd_def) apply (rule no_fail_pre) apply (wp get_object_wp | wpc)+ apply (clarsimp simp: pde_at_def obj_at_def a_type_def) apply (clarsimp split: Structures_A.kernel_object.splits
                               arch_kernel_obj.splits if_split_asm) apply simp apply (clarsimp simp: state_relation_def) apply (erule(3) pspace_relation_pd) apply (simp add: pde_at_def pd_bits_def pdBits_def
                       is_aligned_neg_mask_eq pdeBits_def pageBits_def) apply (wp find_pd_for_asid_valids[where pd=pd])+ apply (clarsimp simp: word_neq_0_conv valid_vspace_objs_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) (pspace_aligned' and pspace_distinct' and no_0_obj') (find_pd_for_asid_assert asid) (findPDForASIDAssert asid) proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) (pspace_aligned' and pspace_distinct' and no_0_obj') (do pd <- find_pd_for_asid asid <catch> (\<lambda>y. fail);
y <- get_pde pd;
return pd
od) (do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- assert (pd && mask pdBits = 0);
y <- checkPDAt pd;
y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od) proof (prove)
goal (3 subgoals):
 1. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) ?Q10 ?Q'10 (do pd <- find_pd_for_asid asid <catch> (\<lambda>y. fail);
y <- get_pde pd;
return pd
od) (do pd <- findPDForASID asid <catch> (\<lambda>y. fail);
y <- assert (pd && mask pdBits = 0);
y <- checkPDAt pd;
y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od)
 2. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> ?Q10 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'10 s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P14 ?P'14 (find_pd_for_asid asid <catch> (\<lambda>y. fail)) (findPDForASID asid <catch> (\<lambda>y. fail))
 2. \<And>pda. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?R14 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 3. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>?R14\<rbrace>
 4. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 5. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (?P14 and ?Q14) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'14 and ?Q'14) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. lfr y ya \<Longrightarrow> corres (=) (?E19 y) (?E'19 ya) fail fail
 2. \<lbrace>?Q19\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E19\<rbrace>
 3. \<lbrace>?Q'19\<rbrace> findPDForASID asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'19\<rbrace>
 4. \<And>pda. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?R14 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 5. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>?R14\<rbrace>
 6. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q19 and ?Q14) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'19 and ?Q'14) s proof (prove)
goal (8 subgoals):
 1. \<And>y ya. lfr y ya \<Longrightarrow> corres (=) (\<lambda>_. False) (\<lambda>_. True) fail fail
 2. \<lbrace>?Q19\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>y _. False\<rbrace>
 3. \<lbrace>?Q'19\<rbrace> findPDForASID asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<And>pda. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?R14 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 5. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>?R14\<rbrace>
 6. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q19 and ?Q14) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'19 and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. \<lbrace>?Q19\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>y _. False\<rbrace>
 2. \<lbrace>?Q'19\<rbrace> findPDForASID asid \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>pda. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?R14 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>?R14\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q19 and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'19 and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. \<And>pda. corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?R14 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>?R14\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. \<And>pda. is_aligned pda pdBits \<and> pda = pd \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?P37 pda) (?R'14 pda) (do y <- get_pde pda;
return pda
od) (do y <- assert (pda && mask pdBits = 0);
y <- checkPDAt pda;
y <- checkPDUniqueToASID pda asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pda = xa);
return pda
od)
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. ?P37 pda and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?P37 pd) (?R'14 pd) (do y <- get_pde pd;
return pd
od) (do y <- checkPDAt pd;
y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od)
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. ?P37 pda and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>?R'14\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) ?Q53 ?Q'53 (do y <- get_pde pd;
return pd
od) (do y <- checkPDAt pd;
y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od)
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q53 s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'53 s'
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (10 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?Q55 rv) ?Q'53 (return pd) (do y <- checkPDAt pd;
y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od)
 2. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>?Q55\<rbrace>
 4. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'53 s'
 7. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 8. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (13 subgoals):
 1. \<And>rv rva. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?Q55 rv) (?Q'61 rv rva) (return pd) (do y <- checkPDUniqueToASID pd asid;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, xa) \<Rightarrow> pd = xa);
return pd
od)
 2. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>?Q'61 rv\<rbrace>
 3. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 5. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>?Q55\<rbrace>
 7. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 8. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 10. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?Q55 rv) (?Q'61 rv ()) (return pd) (do y <- stateAssert (\<lambda>s. pd \<notin> snd ` ran (armKSASIDMap (ksArchState s) |` (- {asid}))) [];
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb);
return pd
od)
 2. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>?Q'61 rv\<rbrace>
 3. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 5. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>?Q55\<rbrace>
 7. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 8. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 10. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?P66 rv) (?Q'61 rv ()) (return pd) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- assert (case asidMap asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> pd = b);
return pd
od)
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ?P66 rv s; pd_at_uniq asid pd s; ?Q'61 rv () s'\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>?Q'61 rv\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. ?P66 rv and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?P66 rv) (?Q'61 rv ()) (return pd) (do y <- stateAssert (\<lambda>s. case armKSASIDMap (ksArchState s) asid of None \<Rightarrow> True | Some (xa, xb) \<Rightarrow> pd = xb) [];
return pd
od)
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ?P66 rv s; pd_at_uniq asid pd s; ?Q'61 rv () s'\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>?Q'61 rv\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. ?P66 rv and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> corres (\<lambda>rv rv'. rv = pd \<and> rv' = pd) (?P71 rv) (?Q'61 rv ()) (return pd) (return pd)
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ?P71 rv s; (valid_asid_map and vspace_at_asid asid pd) s; ?Q'61 rv () s'\<rbrakk> \<Longrightarrow> case armKSASIDMap (ksArchState s') asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> pd = b
 3. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; (?P71 rv and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; ?Q'61 rv () s'\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 4. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>?Q'61 rv\<rbrace>
 5. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 7. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. ?P71 rv and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 9. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; True; (valid_asid_map and vspace_at_asid asid pd) s; True\<rbrakk> \<Longrightarrow> case armKSASIDMap (ksArchState s') asid of None \<Rightarrow> True | Some (x, b) \<Rightarrow> pd = b
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s s' a b. \<lbrakk>is_aligned pd pdBits; pspace_relation (kheap s) (ksPSpace s'); dom (armKSASIDMap (ksArchState s')) \<subseteq> {0..mask local.asid_bits}; ekheap_relation (ekheap s) (ksPSpace s'); \<forall>x\<in>graph_of (armKSASIDMap (ksArchState s')). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid asid pd s; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; armKSASIDMap (ksArchState s') asid = Some (a, b)\<rbrakk> \<Longrightarrow> pd = b
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s s' a b. \<lbrakk>is_aligned pd pdBits; pspace_relation (kheap s) (ksPSpace s'); dom (armKSASIDMap (ksArchState s')) \<subseteq> {0..mask local.asid_bits}; ekheap_relation (ekheap s) (ksPSpace s'); vspace_at_asid asid pd s; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; armKSASIDMap (ksArchState s') asid = Some (a, b); case (asid, a, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> pd = b
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s s' a b. \<lbrakk>is_aligned pd pdBits; pspace_relation (kheap s) (ksPSpace s'); dom (armKSASIDMap (ksArchState s')) \<subseteq> {0..mask local.asid_bits}; ekheap_relation (ekheap s) (ksPSpace s'); vspace_at_asid asid pd s; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; armKSASIDMap (ksArchState s') asid = Some (a, b); vspace_at_asid asid b s; asid \<noteq> 0\<rbrakk> \<Longrightarrow> pd = b
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s s' a b. \<lbrakk>is_aligned pd pdBits; pspace_relation (kheap s) (ksPSpace s'); dom (armKSASIDMap (ksArchState s')) \<subseteq> {0..mask local.asid_bits}; ekheap_relation (ekheap s) (ksPSpace s'); sched_act_relation (scheduler_action s) (ksSchedulerAction s'); ready_queues_relation (ready_queues s) (ksReadyQueues s'); ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); asid_table s = armKSASIDTable (ksArchState s') \<circ> UCAST(7 \<rightarrow> 32); arm_global_pd (arch_state s) = armKSGlobalPD (ksArchState s'); arm_hwasid_table (arch_state s) = armKSHWASIDTable (ksArchState s'); arm_global_pts (arch_state s) = armKSGlobalPTs (ksArchState s'); arm_next_asid (arch_state s) = armKSNextASID (ksArchState s'); arm_asid_map (arch_state s) = armKSASIDMap (ksArchState s'); arm_kernel_vspace (arch_state s) = armKSKernelVSpace (ksArchState s'); interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'; armKSASIDMap (ksArchState s') asid = Some (a, b); vspace_at_asid asid b s; asid \<noteq> 0; pd = b\<rbrakk> \<Longrightarrow> pd = b
 2. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 3. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 6. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 8. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv s s'. \<lbrakk>is_aligned pd pdBits; (s, s') \<in> state_relation; ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd)) s; pd_at_uniq asid pd s; True\<rbrakk> \<Longrightarrow> pd \<notin> snd ` ran (armKSASIDMap (ksArchState s') |` (- {asid}))
 2. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 5. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 7. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 8. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 9. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 10. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv. is_aligned pd pdBits \<Longrightarrow> \<lbrace>page_directory_at' pd\<rbrace> checkPDAt pd \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>rv s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> checkPDAt pd \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 4. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 6. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 7. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 8. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 9. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 10. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>rv. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (page_directory_at' pd) (checkPDAt pd)
 2. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 4. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 7. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 8. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (10 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> no_fail (page_directory_at' pd) (do s <- get;
assert (page_directory_at' pd s)
od)
 2. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 4. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 7. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 8. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>is_aligned pd pdBits; page_directory_at' pd s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and page_directory_at' pd) s
 2. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 4. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 7. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 8. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 9. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 3. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 6. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 7. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (9 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned pd pdBits; is_aligned pd 2; kheap s (pd && ~~ mask pd_bits) = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory; pd_at_uniq asid pd s; valid_asid_map s; vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 3. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 6. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 7. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (9 subgoals):
 1. \<And>s x3. \<lbrakk>pd_at_uniq asid pd s; valid_asid_map s; vspace_at_asid asid pd s; is_aligned pd pdBits; is_aligned pd 2; kheap s (pd && ~~ mask pd_bits) = Some (ArchObj (PageDirectory x3))\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_pde pd \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 3. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 6. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 7. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 8. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (8 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> \<lbrace>pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd\<rbrace> get_pde pd \<lbrace>\<lambda>rv. (\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd\<rbrace>
 2. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 5. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 6. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (8 subgoals):
 1. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (valid_asid_map and vspace_at_asid asid pd) and pd_at_uniq asid pd) s
 2. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 5. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 6. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. \<lbrakk>is_aligned pd pdBits; True\<rbrakk> \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (get_pde pd)
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> no_fail (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) (do pda <- get_object (pd && ~~ mask pd_bits) >>= Structures_A.kernel_object.case_kernel_object (\<lambda>nat fun. fail) (\<lambda>tcb_ext. fail) (\<lambda>endpoint. fail) (\<lambda>notification_ext. fail) (case_arch_kernel_obj (\<lambda>fun. fail) (\<lambda>fun. fail) return (\<lambda>bool vmpage_size. fail));
return (pda (UCAST(32 \<rightarrow> 12) (pd && mask pd_bits >> 2)))
od)
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (8 subgoals):
 1. is_aligned pd pdBits \<Longrightarrow> no_fail ?P223 (do pda <- get_object (pd && ~~ mask pd_bits) >>= Structures_A.kernel_object.case_kernel_object (\<lambda>nat fun. fail) (\<lambda>tcb_ext. fail) (\<lambda>endpoint. fail) (\<lambda>notification_ext. fail) (case_arch_kernel_obj (\<lambda>fun. fail) (\<lambda>fun. fail) return (\<lambda>bool vmpage_size. fail));
return (pda (UCAST(32 \<rightarrow> 12) (pd && mask pd_bits >> 2)))
od)
 2. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> ?P223 s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 4. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 5. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 6. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s\<rbrakk> \<Longrightarrow> (obj_at (\<lambda>_. True) (pd && ~~ mask pd_bits) and (\<lambda>s. \<forall>ko. ko_at ko (pd && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x xa. ko = CNode x xa \<longrightarrow> False) \<and> (\<forall>x. ko = TCB x \<longrightarrow> False) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> False) \<and> (\<forall>x. ko = Notification x \<longrightarrow> False) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> (\<forall>xa. x = arch_kernel_obj.ASIDPool xa \<longrightarrow> False) \<and> (\<forall>xa. x = PageTable xa \<longrightarrow> False) \<and> (\<forall>xa. x = PageDirectory xa \<longrightarrow> True) \<and> (\<forall>xa xb. x = DataPage xa xb \<longrightarrow> False))) and (\<lambda>s. \<forall>ko. ko_at ko (pd && ~~ mask pd_bits) s \<longrightarrow> True)) s
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (7 subgoals):
 1. \<And>s ko. \<lbrakk>is_aligned pd pdBits; is_aligned pd 2; kheap s (pd && ~~ mask pd_bits) = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of arch_kernel_obj.ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageDirectory; pd_at_uniq asid pd s; valid_asid_map s; vspace_at_asid asid pd s\<rbrakk> \<Longrightarrow> (\<forall>x xa. ko \<noteq> CNode x xa) \<and> (\<forall>x. ko \<noteq> TCB x) \<and> (\<forall>x. ko \<noteq> Endpoint x) \<and> (\<forall>x. ko \<noteq> Notification x) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> (\<forall>xa. x \<noteq> arch_kernel_obj.ASIDPool xa) \<and> (\<forall>xa. x \<noteq> PageTable xa) \<and> (\<forall>xa xb. x \<noteq> DataPage xa xb))
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 3. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 4. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 5. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (6 subgoals):
 1. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at pd and pd_at_uniq asid pd and valid_asid_map and vspace_at_asid asid pd) s
 2. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 3. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 4. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 5. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>is_aligned pd pdBits; (pde_at pd and pd_at_uniq asid pd and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and valid_asid_map) s; (pspace_aligned' and pspace_distinct') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>is_aligned pd pdBits; pde_at pd s; pspace_aligned' s'; pspace_distinct' s'; pspace_relation (kheap s) (ksPSpace s'); pd_at_uniq asid pd s; ekheap_relation (ekheap s) (ksPSpace s'); pspace_aligned s; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); pspace_distinct s; ready_queues_relation (ready_queues s) (ksReadyQueues s'); vspace_at_asid asid pd s; valid_asid_map s; ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> page_directory_at' pd s'
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (5 subgoals):
 1. \<And>s s'. \<lbrakk>is_aligned pd pdBits; pde_at pd s; pspace_aligned' s'; pspace_distinct' s'; pd_at_uniq asid pd s; ekheap_relation (ekheap s) (ksPSpace s'); pspace_aligned s; sched_act_relation (scheduler_action s) (ksSchedulerAction s'); pspace_distinct s; ready_queues_relation (ready_queues s) (ksReadyQueues s'); vspace_at_asid asid pd s; valid_asid_map s; ghost_relation (kheap s) (gsUserPages s') (gsCNodes s'); cdt_relation (swp (cte_wp_at (\<lambda>_. True)) s) (cdt s) (ctes_of s'); cdt_list_relation (cdt_list s) (cdt s) (ctes_of s'); revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s'); (arch_state s, ksArchState s') \<in> arch_state_relation; interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s'); cur_thread s = ksCurThread s'; idle_thread s = ksIdleThread s'; machine_state s = ksMachineState s'; work_units_completed s = ksWorkUnitsCompleted s'; domain_index s = ksDomScheduleIdx s'; domain_list s = ksDomSchedule s'; cur_domain s = ksCurDomain s'; domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s
 2. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 3. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q14\<rbrace> find_pd_for_asid asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>pda. pde_at pda and pd_at_uniq asid pda and pspace_aligned and pspace_distinct and vspace_at_asid asid pda and valid_asid_map and (\<lambda>s. is_aligned pda pdBits \<and> pda = pd)\<rbrace>
 2. \<lbrace>?Q'14\<rbrace> findPDForASID asid <catch> (\<lambda>y. fail) \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct'\<rbrace>
 3. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and ?Q14) s
 4. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and ?Q'14) s proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd) s \<Longrightarrow> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and (\<lambda>s. (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> True)) s) and (\<lambda>s. True \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0)) s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and pd_at_uniq asid pd) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> True \<and> valid_asid_map s \<and> (vspace_at_asid asid pd and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0) and K (is_aligned pd pdBits \<longrightarrow> is_aligned pd pdBits \<and> pd = pd)) s)) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. True \<and> True) and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s)) s proof (prove)
goal:
No subgoals!