theory VSpace_R

lemma setVMRootForFlush_corres:
  "corres (=)
          (cur_tcb and vspace_at_asid asid pd
           and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
           and valid_asid_map and valid_vs_lookup
           and valid_vspace_objs and valid_global_objs
           and unique_table_refs o caps_of_state
           and valid_arch_state
           and pspace_aligned and pspace_distinct)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (set_vm_root_for_flush pd asid)
          (setVMRootForFlush pd asid)" proof - have X: "corres (=) (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits)
                          and valid_asid_map and valid_vs_lookup
                          and valid_vspace_objs and valid_global_objs
                          and unique_table_refs o caps_of_state
                          and valid_arch_state
                          and pspace_aligned and pspace_distinct)
                       (pspace_aligned' and pspace_distinct' and no_0_obj')
           (do _ \<leftarrow> arm_context_switch pd asid;
               return True
            od)
           (do _ \<leftarrow> armv_contextSwitch pd asid;
               return True
            od)" apply (rule corres_guard_imp) apply (rule corres_split[OF armv_contextSwitch_corres]) apply (rule corres_trivial) apply (wp | simp)+ done show ?thesis apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv) apply (rule corres_guard_imp) apply (rule corres_split[OF getCurThread_corres]) apply (rule corres_split) apply (rule getSlotCap_corres) apply (simp add: cte_map_def tcb_cnode_index_def tcbVTableSlot_def to_bl_1) apply (corres_cases; (simp add: isCap_simps, rule X)?)+ apply (clarsimp simp: isCap_simps, rule X) apply (wpsimp wp: hoare_drop_imp hoare_vcg_all_lift)+ apply (clarsimp simp: cur_tcb_def) apply (erule tcb_at_cte_at) apply (simp add: tcb_cap_cases_def) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (cur_tcb and vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (set_vm_root_for_flush pd asid) (setVMRootForFlush pd asid) proof (state)
goal (1 subgoal):
 1. corres (=) (cur_tcb and vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (set_vm_root_for_flush pd asid) (setVMRootForFlush pd asid) proof (prove)
goal (1 subgoal):
 1. corres (=) (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (do _ <- arm_context_switch pd asid;
return True
od) (do _ <- armv_contextSwitch pd asid;
return True
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do _ <- arm_context_switch pd asid;
return True
od) (do _ <- armv_contextSwitch pd asid;
return True
od)
 2. \<And>s. (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_. dc uu_ uua_ \<Longrightarrow> corres (=) (?R4 uu_) (?R'4 uua_) (return True) (return True)
 2. \<lbrace>?Q4\<rbrace> arm_context_switch pd asid \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> armv_contextSwitch pd asid \<lbrace>?R'4\<rbrace>
 4. \<And>s. (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<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 and ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_ uua_. dc uu_ uua_ \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return True) (return True)
 2. \<lbrace>?Q4\<rbrace> arm_context_switch pd asid \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<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 and ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (=) (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (do _ <- arm_context_switch pd asid;
return True
od) (do _ <- armv_contextSwitch pd asid;
return True
od)

goal (1 subgoal):
 1. corres (=) (cur_tcb and vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (set_vm_root_for_flush pd asid) (setVMRootForFlush pd asid) proof (prove)
goal (1 subgoal):
 1. corres (=) (cur_tcb and vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (set_vm_root_for_flush pd asid) (setVMRootForFlush pd asid) proof (prove)
goal (1 subgoal):
 1. corres (=) (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (do tcb <- gets cur_thread;
thread_root <- get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (do tcb <- getCurThread;
threadRoot <- getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot);
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q2 ?Q'2 (do tcb <- gets cur_thread;
thread_root <- get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (do tcb <- getCurThread;
threadRoot <- getSlotCap (tcb + 2 ^ cte_level_bits * tcbVTableSlot);
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od)
 2. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ?Q2 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'2 s proof (prove)
goal (5 subgoals):
 1. \<And>tcb tcba. tcb = tcba \<Longrightarrow> corres (=) (?R6 tcb) (?R'6 tcba) (do thread_root <- get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (do threadRoot <- getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot);
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od
od)
 2. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>?R'6\<rbrace>
 4. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcba. tcb = tcba \<Longrightarrow> corres (?r'10 tcb tcba) (?P11 tcb) (?P'13 tcba) (get_cap (tcb, tcb_cnode_index (Suc 0))) (getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot))
 2. \<And>tcb tcba rv rv'. \<lbrakk>tcb = tcba; ?r'10 tcb tcba rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?R10 tcb tcba rv) (?R'10 tcb tcba rv') (do not_is_pd <- case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (if isArchObjectCap rv' \<and> isPageDirectoryCap (capCap rv') \<and> (\<exists>y. capPDMappedASID (capCap rv') = Some y) \<and> capPDBasePtr (capCap rv') = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od)
 3. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q12 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?R10 tcb tcba\<rbrace>
 4. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q'14 tcba\<rbrace> getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?R'10 tcb tcba\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. ?P11 tcb and ?Q12 tcb\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>tcba. ?P'13 tcba and ?Q'14 tcba\<rbrace>
 7. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>tcb tcba. tcb = tcba \<Longrightarrow> tcba + 2 ^ cte_level_bits * tcbVTableSlot = cte_map (tcb, tcb_cnode_index (Suc 0))
 2. \<And>tcb tcba rv rv'. \<lbrakk>tcb = tcba; cap_relation rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?R10 tcb tcba rv) (?R'10 tcb tcba rv') (do not_is_pd <- case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (if isArchObjectCap rv' \<and> isPageDirectoryCap (capCap rv') \<and> (\<exists>y. capPDMappedASID (capCap rv') = Some y) \<and> capPDBasePtr (capCap rv') = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od)
 3. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q12 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?R10 tcb tcba\<rbrace>
 4. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q'14 tcba\<rbrace> getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?R'10 tcb tcba\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index (Suc 0)) and ?Q12 tcb\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>tcba. pspace_distinct' and pspace_aligned' and ?Q'14 tcba\<rbrace>
 7. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb tcba rv rv'. \<lbrakk>tcb = tcba; cap_relation rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?R10 tcb tcba rv) (?R'10 tcb tcba rv') (do not_is_pd <- case rv of cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd None) \<Rightarrow> return True | cap.ArchObjectCap (arch_cap.PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | cap.ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (if isArchObjectCap rv' \<and> isPageDirectoryCap (capCap rv') \<and> (\<exists>y. capPDMappedASID (capCap rv') = Some y) \<and> capPDBasePtr (capCap rv') = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od)
 2. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q12 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>?R10 tcb tcba\<rbrace>
 3. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q'14 tcba\<rbrace> getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>?R'10 tcb tcba\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index (Suc 0)) and ?Q12 tcb\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>tcba. pspace_distinct' and pspace_aligned' and ?Q'14 tcba\<rbrace>
 6. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>tcb tcba rv rv' x12 x51 x52 x2. \<lbrakk>tcb = tcba; cap_relation rv rv'; rv = cap.ArchObjectCap x12; x12 = arch_cap.PageDirectoryCap x51 x52; x52 = Some x2\<rbrakk> \<Longrightarrow> corres (=) (?Q667 tcb tcba rv x12 x51 x52 x2) (?B'669 tcb tcba rv') (do not_is_pd <- return (x51 \<noteq> pd);
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od) (if isArchObjectCap rv' \<and> isPageDirectoryCap (capCap rv') \<and> (\<exists>y. capPDMappedASID (capCap rv') = Some y) \<and> capPDBasePtr (capCap rv') = pd then let cur_pd = pd in return False else do armv_contextSwitch pd asid;
return True
od)
 2. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q12 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>rv s. (rv = cap.NullCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.ThreadCap x \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (rv = cap.DomainCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (rv = cap.IRQControlCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.IRQHandlerCap x \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.Zombie x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = arch_cap.ASIDPoolCap xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (x = arch_cap.ASIDControlCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb xc xd xe. x = arch_cap.PageCap xa xb xc xd xe \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb. x = arch_cap.PageTableCap xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb. x = arch_cap.PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xc. xb = Some xc \<longrightarrow> ?Q667 tcb tcba rv x xa xb xc s)))\<rbrace>
 3. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q'14 tcba\<rbrace> getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>rv' s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> ?B'669 tcb tcba rv' s\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index (Suc 0)) and ?Q12 tcb\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>tcba. pspace_distinct' and pspace_aligned' and ?Q'14 tcba\<rbrace>
 6. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q12 tcb\<rbrace> get_cap (tcb, tcb_cnode_index (Suc 0)) \<lbrace>\<lambda>rv s. (rv = cap.NullCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb xc. rv = cap.UntypedCap x xa xb xc \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.EndpointCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.NotificationCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.ReplyCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.CNodeCap x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.ThreadCap x \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (rv = cap.DomainCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (rv = cap.IRQControlCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.IRQHandlerCap x \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x xa xb. rv = cap.Zombie x xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. rv = cap.ArchObjectCap x \<longrightarrow> (\<forall>xa xb. x = arch_cap.ASIDPoolCap xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (x = arch_cap.ASIDControlCap \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb xc xd xe. x = arch_cap.PageCap xa xb xc xd xe \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb. x = arch_cap.PageTableCap xa xb \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>xa xb. x = arch_cap.PageDirectoryCap xa xb \<longrightarrow> (xb = None \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s) \<and> (\<forall>x. xb = Some x \<longrightarrow> (vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s)))\<rbrace>
 2. \<And>tcb tcba. tcb = tcba \<Longrightarrow> \<lbrace>?Q'14 tcba\<rbrace> getSlotCap (tcba + 2 ^ cte_level_bits * tcbVTableSlot) \<lbrace>\<lambda>rv' s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrace>
 3. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb. cte_wp_at (\<lambda>_. True) (tcb, tcb_cnode_index (Suc 0)) and ?Q12 tcb\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> getCurThread \<lbrace>\<lambda>tcba. pspace_distinct' and pspace_aligned' and ?Q'14 tcba\<rbrace>
 5. \<And>s. (cur_tcb and vspace_at_asid asid pd and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cur_tcb s; vspace_at_asid asid pd s; asid \<noteq> 0; asid \<le> mask local.asid_bits; valid_asid_map s; valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; unique_table_refs (caps_of_state s); valid_arch_state s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (cur_thread s, tcb_cnode_index (Suc 0)) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (pspace_distinct' and pspace_aligned' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>tcb_at (cur_thread s) s; vspace_at_asid asid pd s; asid \<noteq> 0; asid \<le> mask local.asid_bits; valid_asid_map s; valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; unique_table_refs (caps_of_state s); valid_arch_state s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (cur_thread s, tcb_cnode_index (Suc 0)) s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (pspace_distinct' and pspace_aligned' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vspace_at_asid asid pd s; asid \<noteq> 0; asid \<le> mask local.asid_bits; valid_asid_map s; valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; unique_table_refs (caps_of_state s); valid_arch_state s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> tcb_cnode_index (Suc 0) \<in> dom tcb_cap_cases
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (pspace_distinct' and pspace_aligned' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ((\<lambda>_. True) and (pspace_distinct' and pspace_aligned' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s \<and> (pspace_aligned' and pspace_distinct' and no_0_obj') s))) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres (=) (cur_tcb and vspace_at_asid asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (set_vm_root_for_flush pd asid) (setVMRootForFlush pd asid)

goal:
No subgoals!