theory VSpace_R

lemma flushTable_corres:
  "corres dc
          (pspace_aligned and valid_objs and valid_arch_state and
           cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and
           pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs
           and unique_table_refs o caps_of_state and
           K (is_aligned vptr (pageBitsForSize ARMSection) \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0))
          (pspace_aligned' and pspace_distinct' and no_0_obj' and
           valid_arch_state' and cur_tcb')
          (flush_table pd asid vptr ptr)
          (flushTable pd asid vptr)" apply (simp add: flush_table_def flushTable_def) apply (rule corres_assume_pre) apply (simp add: ptBits_def pt_bits_def pageBits_def is_aligned_mask cong: corres_weak_cong) apply (thin_tac "P" for P)+ apply (rule corres_guard_imp) apply (rule corres_split[OF setVMRootForFlush_corres]) apply (rule corres_split[OF load_hw_asid_corres2[where pd=pd]]) apply (clarsimp cong: corres_weak_cong) apply (rule corres_when, rule refl) apply (rule corres_split[where r' = dc, OF corres_machine_op corres_when]) apply (rule corres_Id[OF refl]) apply simp apply (rule no_fail_invalidateLocalTLB_ASID) apply simp apply (rule corres_split[OF getCurThread_corres]) apply (simp, rule setVMRoot_corres) apply ((wp mapM_wp' hoare_vcg_const_imp_lift get_pte_wp getPTE_wp|
                   wpc|simp|fold cur_tcb_def cur_tcb'_def)+)[4] apply (wp hoare_drop_imps | simp)+ apply (wp load_hw_asid_wp hoare_drop_imps |
                simp add: cur_tcb'_def [symmetric] cur_tcb_def [symmetric] )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and K (is_aligned vptr (pageBitsForSize ARMSection) \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (flush_table pd asid vptr ptr) (flushTable pd asid vptr) proof (prove)
goal (1 subgoal):
 1. corres dc (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do y <- assert (vptr && mask 20 = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do y <- assert (vptr && mask 20 = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s; (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do y <- assert (vptr && mask 20 = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do y <- assert (vptr && mask 20 = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>pspace_aligned s \<and> valid_objs s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid pd s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> unique_table_refs (caps_of_state s) \<and> vptr && mask 20 = 0 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0; pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<and> valid_arch_state' s' \<and> cur_tcb' s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. corres dc (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. corres dc (?Q28 s s') (?Q'28 s s') (do root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (getCurThread >>= setVMRoot)
od)
od)
 2. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> ?Q28 s s' sa
 3. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> ?Q'28 s s' sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> corres dc (?R32 s s' rv) (?R'32 s s' rv') (do maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when rv (gets cur_thread >>= set_vm_root)
od)
od) (do maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asid));
when rv' (getCurThread >>= setVMRoot)
od)
od)
 2. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>?R32 s s'\<rbrace>
 3. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>?R'32 s s'\<rbrace>
 4. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 5. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv rv' maybe_hw_asid maybe_hw_asida. \<lbrakk>rv = rv'; maybe_hw_asid = maybe_hw_asida\<rbrakk> \<Longrightarrow> corres dc (?R37 s s' rv rv' maybe_hw_asid) (?R'37 s s' rv rv' maybe_hw_asida) (when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when rv (gets cur_thread >>= set_vm_root)
od)) (when (\<exists>y. maybe_hw_asida = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida));
when rv' (getCurThread >>= setVMRoot)
od))
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>?R37 s s' rv rv'\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>?R'37 s s' rv rv'\<rbrace>
 4. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 6. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 7. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres dc (?R37 s s' rv' rv' maybe_hw_asida) (?R'37 s s' rv' rv' maybe_hw_asida) (when (\<exists>y. maybe_hw_asida = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida));
when rv' (gets cur_thread >>= set_vm_root)
od)) (when (\<exists>y. maybe_hw_asida = Some y) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida));
when rv' (getCurThread >>= setVMRoot)
od))
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>?R37 s s' rv rv'\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>?R'37 s s' rv rv'\<rbrace>
 4. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 6. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 7. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres dc (?P53 s s' rv' rv' maybe_hw_asida) (?P'52 s s' rv' rv' maybe_hw_asida) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida));
when rv' (gets cur_thread >>= set_vm_root)
od) (do y <- doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida));
when rv' (getCurThread >>= setVMRoot)
od)
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ?P53 s s' rv rv' a b\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ?P'52 s s' rv rv' a b\<rbrace>
 4. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 6. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 7. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (11 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (invalidateLocalTLB_ASID (the maybe_hw_asida)) (invalidateLocalTLB_ASID (the maybe_hw_asida))
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> rv' = rv'
 3. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?P60 s s' rv' maybe_hw_asida rv) (?P'62 s s' rv' maybe_hw_asida rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P60 s s' rv' maybe_hw_asida rv x\<rbrace>
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'62 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 8. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 9. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 10. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rv. dc rv rv
 2. \<And>s s' rv' maybe_hw_asida. True \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_ASID (the maybe_hw_asida))
 3. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> rv' = rv'
 4. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?P60 s s' rv' maybe_hw_asida rv) (?P'62 s s' rv' maybe_hw_asida rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P60 s s' rv' maybe_hw_asida rv x\<rbrace>
 6. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'62 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 8. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 9. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 10. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. True \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_ASID (the maybe_hw_asida))
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> rv' = rv'
 3. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?P60 s s' rv' maybe_hw_asida rv) (?P'62 s s' rv' maybe_hw_asida rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P60 s s' rv' maybe_hw_asida rv x\<rbrace>
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'62 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 8. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 9. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 10. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> rv' = rv'
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?P60 s s' rv' maybe_hw_asida rv) (?P'62 s s' rv' maybe_hw_asida rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P60 s s' rv' maybe_hw_asida rv x\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'62 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 9. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 10. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?P60 s s' rv' maybe_hw_asida rv) (?P'62 s s' rv' maybe_hw_asida rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 2. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P60 s s' rv' maybe_hw_asida rv x\<rbrace>
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'62 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 4. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 6. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 7. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 8. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 9. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (11 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rv rv'a rva rv'b. \<lbrakk>dc rv rv'a; rva = rv'b\<rbrakk> \<Longrightarrow> corres dc (?R82 s s' rv' maybe_hw_asida rv rv'a rva) (?R'82 s s' rv' maybe_hw_asida rv rv'a rv'b) (set_vm_root rva) (setVMRoot rv'b)
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> \<lbrace>?Q83 s s' rv' maybe_hw_asida rv\<rbrace> gets cur_thread \<lbrace>?R82 s s' rv' maybe_hw_asida rv rv'a\<rbrace>
 3. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> \<lbrace>?Q'84 s s' rv' maybe_hw_asida rv'a\<rbrace> getCurThread \<lbrace>?R'82 s s' rv' maybe_hw_asida rv rv'a\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q83 s s' rv' maybe_hw_asida rv) x\<rbrace>
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'84 s s' rv' maybe_hw_asida rv'a) x\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 8. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 9. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 10. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> \<lbrace>?Q83 s s' rv' maybe_hw_asida rv\<rbrace> gets cur_thread \<lbrace>\<lambda>a. tcb_at a 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\<rbrace>
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> \<lbrace>?Q'84 s s' rv' maybe_hw_asida rv'a\<rbrace> getCurThread \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' a and no_0_obj'\<rbrace>
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q71 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q83 s s' rv' maybe_hw_asida rv) x\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'70 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_ASID (the maybe_hw_asida)) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'84 s s' rv' maybe_hw_asida rv'a) x\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q71 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'70 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 9. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 10. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q42 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. rv' \<longrightarrow> True \<and> cur_tcb a \<and> valid_arch_state a \<and> valid_objs a \<and> valid_asid_map a \<and> unique_table_refs (caps_of_state a) \<and> valid_vs_lookup a \<and> valid_global_objs a \<and> pspace_aligned a \<and> pspace_distinct a \<and> valid_vspace_objs a)) b\<rbrace>
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. rv' \<longrightarrow> True \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) b\<rbrace>
 3. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q42 s s' rv\<rbrace>
 4. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 5. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 6. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal (6 subgoals):
 1. \<And>s s' rv. \<lbrace>?P'222 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>rv s. 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\<rbrace>
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'43 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. rv' \<longrightarrow> True \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) b\<rbrace>
 3. \<And>s s'. \<lbrace>?Q32 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and (\<lambda>sa. True \<and> True \<and> cur_tcb sa \<and> valid_arch_state sa \<and> valid_objs sa \<and> ?P'222 s s' rv sa)\<rbrace>
 4. \<And>s s'. \<lbrace>?Q'32 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'43 s s' rv'\<rbrace>
 5. \<And>s s' sa. (pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and (\<lambda>y. is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) sa \<Longrightarrow> (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 and ?Q32 s s') sa
 6. \<And>s s' sa. (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') sa \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'32 s s') sa proof (prove)
goal:
No subgoals!