theory VSpace_R

lemma setVMRoot_corres:
  "corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map
              and unique_table_refs o caps_of_state and valid_vs_lookup
              and valid_global_objs and pspace_aligned and pspace_distinct
              and valid_vspace_objs)
             (pspace_aligned' and pspace_distinct'
                 and valid_arch_state' and tcb_at' t and no_0_obj')
             (set_vm_root t) (setVMRoot t)" proof - have P: "corres dc \<top> \<top>
        (do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
            do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
         od)
        (do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
            doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
         od)" apply (rule corres_guard_imp) apply (rule corres_split_eqr) apply (subst corres_gets) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (rule setCurrentPD_corres) apply (wp | simp)+ done have Q: "\<And>P P'. corres dc P P'
        (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch>
         (\<lambda>_ . do global_pd \<leftarrow> gets (arm_global_pd \<circ> arch_state);
                  do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
               od))
        (throwError Fault_H.lookup_failure.InvalidRoot <catch>
         (\<lambda>_ . do globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
                  doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
               od))" apply (rule corres_guard_imp) apply (rule corres_split_catch [where f=lfr]) apply (subst corres_throwError, simp add: lookup_failure_map_def) apply (simp, rule P) apply (wp | simp)+ done show ?thesis unfolding set_vm_root_def setVMRoot_def locateSlot_conv
                     getThreadVSpaceRoot_def setCurrentPD_to_abs[symmetric] apply (rule corres_guard_imp) apply (rule corres_underlying_split [where r'="(=) \<circ> cte_map"]) apply (simp add: tcbVTableSlot_def cte_map_def objBits_def cte_level_bits_def
                          objBitsKO_def tcb_cnode_index_def to_bl_1) apply (rule_tac R="\<lambda>thread_root. valid_arch_state and valid_asid_map and
                                         valid_vspace_objs and valid_vs_lookup and
                                         unique_table_refs o caps_of_state and
                                         valid_global_objs and valid_objs and
                                         pspace_aligned and pspace_distinct and
                                         cte_wp_at ((=) thread_root) thread_root_slot"
                     and R'="\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'"
                     in corres_split) apply (rule getSlotCap_corres; simp) apply (insert Q) apply (case_tac rv, simp_all add: isCap_simps Q[simplified])[1] apply (rename_tac arch_cap) apply (case_tac arch_cap, simp_all add: isCap_simps Q[simplified])[1] apply (rename_tac word option) apply (case_tac option, simp_all add: Q[simplified])[1] apply (clarsimp simp: cap_asid_def) apply (rule corres_guard_imp) apply (rule corres_split_catch [where f=lfr]) apply (rule corres_split_eqrE) apply (rule find_pd_for_asid_corres; simp) apply (rule whenE_throwError_corres) apply (simp add: lookup_failure_map_def) apply simp apply simp apply (rule armv_contextSwitch_corres) apply (wp hoare_drop_imps)+ apply (simp add: checkPDNotInASIDMap_def
                               checkPDASIDMapMembership_def) apply (rule_tac P'="(Not \<circ> vspace_at_asid aa word) and K (aa \<le> mask asid_bits)
                                    and pd_at_uniq aa word
                                    and valid_asid_map and valid_vs_lookup
                                    and (unique_table_refs o caps_of_state)
                                    and valid_vspace_objs and valid_global_objs
                                    and valid_arch_state"
                          in corres_stateAssert_implied) apply (rule P) apply (clarsimp simp: restrict_map_def state_relation_asid_map
                             elim!: ranE) apply (frule(1) valid_asid_mapD) apply (case_tac "x = aa") apply clarsimp apply (clarsimp simp: pd_at_uniq_def restrict_map_def) apply (erule notE, rule_tac a=x in ranI) apply simp apply (wp find_pd_for_asid_pd_at_asid_again)+ apply clarsimp apply (frule page_directory_cap_pd_at_uniq, simp+) apply (frule(1) cte_wp_at_valid_objs_valid_cap) apply (clarsimp simp: valid_cap_def mask_def
                                 word_neq_0_conv) apply (drule(1) pd_at_asid_unique2, simp) apply simp+ apply (wp get_cap_wp | simp)+ apply (clarsimp simp: tcb_at_cte_at_1 [simplified]) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t) proof (state)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>_. True) (\<lambda>_. True) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P4 ?P'4 (gets (arm_global_pd \<circ> arch_state)) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<And>global_pd. corres dc (?R4 global_pd) (?R'4 global_pd) (do_machine_op (setCurrentPD (addrFromKPPtr global_pd))) (doMachineOp (setCurrentPD (addrFromKPPtr global_pd)))
 3. \<lbrace>?Q4\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. True \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<forall>s s'. ?P4 s \<and> ?P'4 s' \<and> (s, s') \<in> state_relation \<longrightarrow> (arm_global_pd \<circ> arch_state) s = (armKSGlobalPD \<circ> ksArchState) s'
 2. \<And>global_pd. corres dc (?R4 global_pd) (?R'4 global_pd) (do_machine_op (setCurrentPD (addrFromKPPtr global_pd))) (doMachineOp (setCurrentPD (addrFromKPPtr global_pd)))
 3. \<lbrace>?Q4\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?R4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. True \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>global_pd. corres dc (?R4 global_pd) (?R'4 global_pd) (do_machine_op (setCurrentPD (addrFromKPPtr global_pd))) (doMachineOp (setCurrentPD (addrFromKPPtr global_pd)))
 2. \<lbrace>?Q4\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?R'4\<rbrace>
 4. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 5. \<And>s. True \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets (arm_global_pd \<circ> arch_state) \<lbrace>\<lambda>global_pd _. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>global_pd _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> (?P4 and ?Q4) s
 4. \<And>s. True \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (\<lambda>_. True) (\<lambda>_. True) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)

goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)) proof (prove)
goal (3 subgoals):
 1. \<And>P P'. corres dc (?Q P P') (?Q' P P') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))
 2. \<And>P P' s. P s \<Longrightarrow> ?Q P P' s
 3. \<And>P P' s. P' s \<Longrightarrow> ?Q' P P' s proof (prove)
goal (6 subgoals):
 1. \<And>P P'. corres (lfr \<oplus> dc) (?P4 P P') (?P'4 P P') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot) (throwError Fault_H.lookup_failure.InvalidRoot)
 2. \<And>P P' uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E4 P P' uu_) (?E'4 P P' uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
 3. \<And>P P'. \<lbrace>?Q4 P P'\<rbrace> throwError ExceptionTypes_A.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4 P P'\<rbrace>
 4. \<And>P P'. \<lbrace>?Q'4 P P'\<rbrace> throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4 P P'\<rbrace>
 5. \<And>P P' s. P s \<Longrightarrow> (?P4 P P' and ?Q4 P P') s
 6. \<And>P P' s. P' s \<Longrightarrow> (?P'4 P P' and ?Q'4 P P') s proof (prove)
goal (5 subgoals):
 1. \<And>P P' uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E4 P P' uu_) (?E'4 P P' uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
 2. \<And>P P'. \<lbrace>?Q4 P P'\<rbrace> throwError ExceptionTypes_A.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4 P P'\<rbrace>
 3. \<And>P P'. \<lbrace>?Q'4 P P'\<rbrace> throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4 P P'\<rbrace>
 4. \<And>P P' s. P s \<Longrightarrow> (?P10 P P' (?Pa10 P P') (?P'a10 P P') and ?Q4 P P') s
 5. \<And>P P' s. P' s \<Longrightarrow> (?P'10 P P' (?Pa10 P P') (?P'a10 P P') and ?Q'4 P P') s proof (prove)
goal (4 subgoals):
 1. \<And>P P'. \<lbrace>?Q4 P P'\<rbrace> throwError ExceptionTypes_A.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>P P'. \<lbrace>?Q'4 P P'\<rbrace> throwError Fault_H.lookup_failure.InvalidRoot \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>P P' s. P s \<Longrightarrow> (?P10 P P' (?Pa10 P P') (?P'a10 P P') and ?Q4 P P') s
 4. \<And>P P' s. P' s \<Longrightarrow> (?P'10 P P' (?Pa10 P P') (?P'a10 P P') and ?Q'4 P P') s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc ?P ?P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))

goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (do thread_root_slot <- return (t, tcb_cnode_index 1);
thread_root <- get_cap thread_root_slot;
(case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)
od) (do threadRootSlot <- return (t + 2 ^ cte_level_bits * tcbVTableSlot);
threadRoot <- getSlotCap threadRootSlot;
catchFailure (case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do thread_root_slot <- return (t, tcb_cnode_index 1);
thread_root <- get_cap thread_root_slot;
(case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)
od) (do threadRootSlot <- return (t + 2 ^ cte_level_bits * tcbVTableSlot);
threadRoot <- getSlotCap threadRootSlot;
catchFailure (case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
od)
 2. \<And>s. (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres ((=) \<circ> cte_map) ?Q ?Q' (return (t, tcb_cnode_index 1)) (return (t + 2 ^ cte_level_bits * tcbVTableSlot))
 2. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> corres dc (?Q4 thread_root_slot) (?Q'4 threadRootSlot) (do thread_root <- get_cap thread_root_slot;
(case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)
od) (do threadRoot <- getSlotCap threadRootSlot;
catchFailure (case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
od)
 3. \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>?Q4\<rbrace>
 4. \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q'4\<rbrace>
 5. \<And>s. (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s \<Longrightarrow> ?Q s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> corres dc (?Q4 thread_root_slot) (?Q'4 threadRootSlot) (do thread_root <- get_cap thread_root_slot;
(case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)
od) (do threadRoot <- getSlotCap threadRootSlot;
catchFailure (case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case threadRoot of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od)
od)
 2. \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>?Q4\<rbrace>
 3. \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?Q'4\<rbrace>
 4. \<And>s. (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s \<Longrightarrow> ?Q s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> corres (?r'9 thread_root_slot threadRootSlot) (?P11 thread_root_slot) (?P'13 threadRootSlot) (get_cap thread_root_slot) (getSlotCap threadRootSlot)
 2. \<And>thread_root_slot threadRootSlot rv rv'. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; ?r'9 thread_root_slot threadRootSlot rv rv'\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) rv) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (catchFailure (case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))
 3. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. ?P11 thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. ?P'13 threadRootSlot and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s \<Longrightarrow> ?Q s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv'. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; cap_relation rv rv'\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) rv) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (catchFailure (case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))
 2. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. ((=) \<circ> cte_map) thread_root_slot threadRootSlot \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s \<Longrightarrow> ?Q s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv'. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; cap_relation rv rv'; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) rv) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap pd None) \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | cap.ArchObjectCap _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (catchFailure (case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>_. do case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv' x12. \<lbrakk>cte_map thread_root_slot = threadRootSlot; \<exists>a'. acap_relation x12 a' \<and> rv' = capability.ArchObjectCap a'; rv = cap.ArchObjectCap x12\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap x12)) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case x12 of arch_cap.PageDirectoryCap pd None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | arch_cap.PageDirectoryCap pd (Some asid) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) ((case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do y <- case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv' arch_cap. \<lbrakk>cte_map thread_root_slot = threadRootSlot; \<exists>a'. acap_relation arch_cap a' \<and> rv' = capability.ArchObjectCap a'; rv = cap.ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap arch_cap)) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case arch_cap of arch_cap.PageDirectoryCap pd None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | arch_cap.PageDirectoryCap pd (Some asid) \<Rightarrow> doE pd' <- find_pd_for_asid asid;
whenE (pd \<noteq> pd') $ throwError ExceptionTypes_A.lookup_failure.InvalidRoot;
liftE $ arm_context_switch pd asid
odE | _ \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) ((case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some asid)) \<Rightarrow> doE pd' <- findPDForASID asid;
whenE (pd \<noteq> pd') $ throw Fault_H.lookup_failure.InvalidRoot;
withoutFailure $ armv_contextSwitch pd asid
odE | capability.ArchObjectCap _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) <catch> (\<lambda>_. do y <- case rv' of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd None) \<Rightarrow> return () | capability.ArchObjectCap (arch_capability.PageDirectoryCap pd (Some x)) \<Rightarrow> checkPDNotInASIDMap pd | capability.ArchObjectCap _ \<Rightarrow> return () | _ \<Rightarrow> return ();
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv' arch_cap x51 x52. \<lbrakk>cte_map thread_root_slot = threadRootSlot; rv' = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case x52 of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some asid \<Rightarrow> doE pd' <- find_pd_for_asid asid;
y <- whenE (x51 \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch x51 asid)
odE) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) ((case x52 of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some asid \<Rightarrow> doE pd' <- findPDForASID asid;
y <- whenE (x51 \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch x51 asid)
odE) <catch> (\<lambda>_. do y <- case x52 of None \<Rightarrow> return () | Some x \<Rightarrow> checkPDNotInASIDMap x51;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv' arch_cap word option. \<lbrakk>cte_map thread_root_slot = threadRootSlot; rv' = capability.ArchObjectCap (arch_capability.PageDirectoryCap word option); rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap word option); arch_cap = arch_cap.PageDirectoryCap word option\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word option))) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') ((case option of None \<Rightarrow> throwError ExceptionTypes_A.lookup_failure.InvalidRoot | Some asid \<Rightarrow> doE pd' <- find_pd_for_asid asid;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word asid)
odE) <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) ((case option of None \<Rightarrow> throwError Fault_H.lookup_failure.InvalidRoot | Some asid \<Rightarrow> doE pd' <- findPDForASID asid;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word asid)
odE) <catch> (\<lambda>_. do y <- case option of None \<Rightarrow> return () | Some x \<Rightarrow> checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>thread_root_slot threadRootSlot rv rv' arch_cap word option a. \<lbrakk>cte_map thread_root_slot = threadRootSlot; rv' = capability.ArchObjectCap (arch_capability.PageDirectoryCap word (Some a)); rv = cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some a)); arch_cap = arch_cap.PageDirectoryCap word (Some a); option = Some a\<rbrakk> \<Longrightarrow> corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some a)))) thread_root_slot) (pspace_aligned' and pspace_distinct' and no_0_obj') (doE pd' <- find_pd_for_asid a;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word a)
odE <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) (doE pd' <- findPDForASID a;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word a)
odE <catch> (\<lambda>_. do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>a b word aa. corres dc (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) (pspace_aligned' and pspace_distinct' and no_0_obj') (doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) (doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE <catch> (\<lambda>_. do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (9 subgoals):
 1. \<And>a b word aa. corres dc (?Q52 a b word aa) (?Q'52 a b word aa) (doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) (doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE <catch> (\<lambda>_. do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))
 2. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ?Q52 a b word aa s
 3. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'52 a b word aa s
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 5. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 7. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 8. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 9. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (12 subgoals):
 1. \<And>a b word aa. corres (lfr \<oplus> dc) (?P56 a b word aa) (?P'56 a b word aa) (doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE) (doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE)
 2. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 3. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 4. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 5. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> (?P56 a b word aa and ?Q56 a b word aa) s
 6. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'56 a b word aa and ?Q'56 a b word aa) s
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 8. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 10. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>a b word aa. corres (lfr \<oplus> (=)) (?P61 a b word aa) (?P'61 a b word aa) (find_pd_for_asid aa) (findPDForASID aa)
 2. \<And>a b word aa pd'. corres (lfr \<oplus> dc) (?R61 a b word aa pd') (?R'61 a b word aa pd') (doE y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE) (doE y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE)
 3. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>?R61 a b word aa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>?R'61 a b word aa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 6. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 7. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 8. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> (?P61 a b word aa and ?Q61 a b word aa and ?Q56 a b word aa) s
 9. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'61 a b word aa and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 10. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b word aa pd'. corres (lfr \<oplus> dc) (?R61 a b word aa pd') (?R'61 a b word aa pd') (doE y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE) (doE y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE)
 2. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>?R61 a b word aa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>?R'61 a b word aa\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 5. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 6. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 7. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 8. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 9. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 10. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>a b word aa pd'. lfr ExceptionTypes_A.lookup_failure.InvalidRoot Fault_H.lookup_failure.InvalidRoot
 2. \<And>a b word aa pd'. (word \<noteq> pd') = (word \<noteq> pd')
 3. \<And>a b word aa pd'. \<not> word \<noteq> pd' \<Longrightarrow> corres (lfr \<oplus> dc) (?Q72 a b word aa pd') (?Q'72 a b word aa pd') (liftE (arm_context_switch word aa)) (liftE (armv_contextSwitch word aa))
 4. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q'72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 7. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 8. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 9. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 10. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>a b word aa pd'. (word \<noteq> pd') = (word \<noteq> pd')
 2. \<And>a b word aa pd'. \<not> word \<noteq> pd' \<Longrightarrow> corres (lfr \<oplus> dc) (?Q72 a b word aa pd') (?Q'72 a b word aa pd') (liftE (arm_context_switch word aa)) (liftE (armv_contextSwitch word aa))
 3. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q'72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 6. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 7. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 8. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 9. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 10. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b word aa pd'. \<not> word \<noteq> pd' \<Longrightarrow> corres (lfr \<oplus> dc) (?Q72 a b word aa pd') (?Q'72 a b word aa pd') (liftE (arm_context_switch word aa)) (liftE (armv_contextSwitch word aa))
 2. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q'72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 5. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 6. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 7. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 8. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 9. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 10. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>a b word aa. corres dc (?Q72 a b word aa word) (?Q'72 a b word aa word) (arm_context_switch word aa) (armv_contextSwitch word aa)
 2. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> ?Q'72 a b word aa pd' s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 5. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 6. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 7. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 8. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 9. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 10. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>a b word aa. \<lbrace>?Q61 a b word aa\<rbrace> find_pd_for_asid aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> (vspace_at_asid aa pd' and K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>a b word aa. \<lbrace>?Q'61 a b word aa\<rbrace> findPDForASID aa \<lbrace>\<lambda>pd' s. \<not> word \<noteq> pd' \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 4. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 5. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 6. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and ?Q61 a b word aa and ?Q56 a b word aa) s
 7. \<And>a b word aa s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'61 a b word aa and ?Q'56 a b word aa) s
 8. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 9. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 10. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
A total of 13 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b word aa uu_ uua_. lfr uu_ uua_ \<Longrightarrow> corres dc (?E56 a b word aa uu_) (?E'56 a b word aa uua_) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- checkPDNotInASIDMap word;
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b word aa uu_. corres dc (?E56 a b word aa uu_) (?E'56 a b word aa (lookup_failure_map uu_)) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do y <- stateAssert (\<lambda>s. word \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s) |` UNIV)) [];
globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E56 a b word aa\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>a b word aa uu_. corres dc (?P119 a b word aa uu_) (?E'56 a b word aa (lookup_failure_map uu_)) (do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od) (do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od)
 2. \<And>a b word aa uu_ s s'. \<lbrakk>(s, s') \<in> state_relation; ?P119 a b word aa uu_ s; (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state) s; ?E'56 a b word aa (lookup_failure_map uu_) s'\<rbrakk> \<Longrightarrow> word \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s') |` UNIV)
 3. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>uu_. ?P119 a b word aa uu_ and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 4. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'56 a b word aa\<rbrace>
 5. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 6. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 8. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 10. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>a b word aa _ s s'. \<lbrakk>(s, s') \<in> state_relation; True; (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state) s; True\<rbrakk> \<Longrightarrow> word \<notin> ran (map_option snd \<circ> armKSASIDMap (ksArchState s') |` UNIV)
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; pd_at_uniq aa b s; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; pd_at_uniq aa b s; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); vspace_at_asid x b s \<and> x \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; pd_at_uniq aa b s; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); vspace_at_asid x b s \<and> x \<le> mask local.asid_bits; x = aa\<rbrakk> \<Longrightarrow> False
 2. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; pd_at_uniq aa b s; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); vspace_at_asid x b s \<and> x \<le> mask local.asid_bits; x \<noteq> aa\<rbrakk> \<Longrightarrow> False
 3. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 4. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 6. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 8. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 10. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; pd_at_uniq aa b s; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); vspace_at_asid x b s \<and> x \<le> mask local.asid_bits; x \<noteq> aa\<rbrakk> \<Longrightarrow> False
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; b \<notin> ran (map_option snd \<circ> (\<lambda>x. if x \<noteq> aa then arm_asid_map (arch_state s) x else None)); valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); x \<noteq> aa; vspace_at_asid x b s; x \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> False
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>aa s s' x a b. \<lbrakk>(s, s') \<in> state_relation; \<not> vspace_at_asid aa b s; aa \<le> mask local.asid_bits; valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_vspace_objs s; valid_global_objs s; valid_arch_state s; arm_asid_map (arch_state s) x = Some (a, b); x \<noteq> aa; vspace_at_asid x b s; x \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> (map_option snd \<circ> (\<lambda>x. if x \<noteq> aa then arm_asid_map (arch_state s) x else None)) x = Some b
 2. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 3. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 4. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 5. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 7. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 9. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 10. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>a b word aa. \<lbrace>?Q56 a b word aa\<rbrace> doE pd' <- find_pd_for_asid aa;
y <- whenE (word \<noteq> pd') (throwError ExceptionTypes_A.lookup_failure.InvalidRoot);
liftE (arm_context_switch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. (\<lambda>_. True) and (Not \<circ> vspace_at_asid aa word and K (aa \<le> mask local.asid_bits) and pd_at_uniq aa word and valid_asid_map and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_vspace_objs and valid_global_objs and valid_arch_state)\<rbrace>
 2. \<And>a b word aa. \<lbrace>?Q'56 a b word aa\<rbrace> doE pd' <- findPDForASID aa;
y <- whenE (word \<noteq> pd') (throwError Fault_H.lookup_failure.InvalidRoot);
liftE (armv_contextSwitch word aa)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and ?Q56 a b word aa) s
 4. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and ?Q'56 a b word aa) s
 5. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 6. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 7. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 8. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 9. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 10. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>a b word aa s. (valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid aa (?pd67 a b word aa) s) and valid_vspace_objs and pspace_aligned and K (0 < aa \<and> aa \<le> mask asidBits) and (\<lambda>s. True \<and> True \<and> K (aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits) s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_global_objs s \<and> valid_vs_lookup s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_arch_state s) and (\<lambda>s. True \<and> (\<forall>pd. vspace_at_asid aa pd s \<longrightarrow> (if word \<noteq> pd then \<lambda>s. (Not \<circ> vspace_at_asid aa word) s \<and> K (aa \<le> mask local.asid_bits) s \<and> pd_at_uniq aa word s \<and> valid_asid_map s \<and> valid_vs_lookup s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_arch_state s \<and> True else (\<lambda>s. True)) s) \<and> (\<forall>ex. (\<forall>pd. \<not> vspace_at_asid aa pd s) \<longrightarrow> (Not \<circ> vspace_at_asid aa word) s \<and> K (aa \<le> mask local.asid_bits) s \<and> pd_at_uniq aa word s \<and> valid_asid_map s \<and> valid_vs_lookup s \<and> (unique_table_refs \<circ> caps_of_state) s \<and> valid_vspace_objs s \<and> valid_global_objs s \<and> valid_arch_state s) \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> aa \<noteq> 0)) s
 2. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>a b word aa s. \<lbrakk>valid_arch_state s; valid_asid_map s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b) s\<rbrakk> \<Longrightarrow> 0 < aa \<and> aa \<le> mask local.asid_bits \<and> aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits \<and> (\<forall>pd. word \<noteq> pd \<longrightarrow> vspace_at_asid aa pd s \<longrightarrow> \<not> vspace_at_asid aa word s \<and> aa \<le> mask local.asid_bits \<and> pd_at_uniq aa word s) \<and> ((\<forall>pd. \<not> vspace_at_asid aa pd s) \<longrightarrow> aa \<le> mask local.asid_bits \<and> pd_at_uniq aa word s) \<and> aa \<noteq> 0
 2. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>a b word aa s. \<lbrakk>valid_arch_state s; valid_asid_map s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b) s; pd_at_uniq aa word s\<rbrakk> \<Longrightarrow> 0 < aa \<and> aa \<le> mask local.asid_bits \<and> aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits \<and> (\<forall>pd. word \<noteq> pd \<longrightarrow> vspace_at_asid aa pd s \<longrightarrow> \<not> vspace_at_asid aa word s \<and> aa \<le> mask local.asid_bits) \<and> ((\<forall>pd. \<not> vspace_at_asid aa pd s) \<longrightarrow> aa \<le> mask local.asid_bits) \<and> aa \<noteq> 0
 2. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>a b word aa s. \<lbrakk>valid_arch_state s; valid_asid_map s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b) s; pd_at_uniq aa word s; \<exists>cap. cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)) = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> 0 < aa \<and> aa \<le> mask local.asid_bits \<and> aa \<noteq> 0 \<and> aa \<le> mask local.asid_bits \<and> (\<forall>pd. word \<noteq> pd \<longrightarrow> vspace_at_asid aa pd s \<longrightarrow> \<not> vspace_at_asid aa word s \<and> aa \<le> mask local.asid_bits) \<and> ((\<forall>pd. \<not> vspace_at_asid aa pd s) \<longrightarrow> aa \<le> mask local.asid_bits) \<and> aa \<noteq> 0
 2. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (8 subgoals):
 1. \<And>a b word aa s pd. \<lbrakk>valid_arch_state s; valid_asid_map s; valid_vspace_objs s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_objs s; pspace_aligned s; pspace_distinct s; cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa)))) (a, b) s; pd_at_uniq aa word s; cap_aligned (cap.ArchObjectCap (arch_cap.PageDirectoryCap word (Some aa))); typ_at (AArch APageDirectory) word s; 0 < aa; aa < 2 ^ local.asid_bits; word \<noteq> pd; vspace_at_asid aa pd s; vspace_at_asid aa word s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 4. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 6. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 7. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 8. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (7 subgoals):
 1. \<And>a b word aa 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> (pspace_aligned' and pspace_distinct' and no_0_obj') s) and (\<lambda>s. True \<and> True)) s
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 3. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 5. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 6. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 7. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>thread_root_slot. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))) \<Longrightarrow> \<lbrace>?Q12 thread_root_slot\<rbrace> get_cap thread_root_slot \<lbrace>\<lambda>thread_root. valid_arch_state and valid_asid_map and valid_vspace_objs and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_objs and pspace_aligned and pspace_distinct and cte_wp_at ((=) thread_root) thread_root_slot\<rbrace>
 2. \<And>thread_root_slot threadRootSlot. \<lbrakk>((=) \<circ> cte_map) thread_root_slot threadRootSlot; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 threadRootSlot\<rbrace> getSlotCap threadRootSlot \<lbrace>\<lambda>thread_root. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 3. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q\<rbrace> return (t, tcb_cnode_index 1) \<lbrace>\<lambda>thread_root_slot. cte_wp_at (\<lambda>_. True) thread_root_slot and ?Q12 thread_root_slot\<rbrace>
 4. (\<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))) \<Longrightarrow> \<lbrace>?Q'\<rbrace> return (t + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>threadRootSlot. pspace_distinct' and pspace_aligned' and ?Q'14 threadRootSlot\<rbrace>
 5. \<And>s. \<lbrakk>(tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q s
 6. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at t s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op (setCurrentPD (addrFromKPPtr global_pd))
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp (setCurrentPD (addrFromKPPtr globalPD))
od))\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index (Suc 0)) s
 2. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and (pspace_aligned' and pspace_distinct' and no_0_obj')) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') s; \<And>P P'. corres dc P P' (throwError ExceptionTypes_A.lookup_failure.InvalidRoot <catch> (\<lambda>_. do global_pd <- gets (arm_global_pd \<circ> arch_state);
do_machine_op $ setCurrentPD $ addrFromKPPtr global_pd
od)) (throwError Fault_H.lookup_failure.InvalidRoot <catch> (\<lambda>_. do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
doMachineOp $ setCurrentPD $ addrFromKPPtr globalPD
od))\<rbrakk> \<Longrightarrow> (pspace_distinct' and pspace_aligned' and (pspace_aligned' and pspace_distinct' and no_0_obj')) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (tcb_at t and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' t and no_0_obj') (set_vm_root t) (setVMRoot t)

goal:
No subgoals!