theory VSpace_R

lemma flushPage_corres:
  "corres dc
          (K (is_aligned vptr pageBits \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0) and
           cur_tcb and valid_arch_state and valid_objs and
           vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and
           valid_vs_lookup and valid_global_objs and
           unique_table_refs o caps_of_state and
           pspace_aligned and pspace_distinct)
          (pspace_aligned' and pspace_distinct' and no_0_obj'
             and valid_arch_state' and cur_tcb')
          (flush_page pageSize pd asid vptr)
          (flushPage pageSize pd asid vptr)" apply (clarsimp simp: flush_page_def flushPage_def) apply (rule corres_assume_pre) apply (simp add: 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[OF corres_machine_op [where r=dc]]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_pre, wp no_fail_invalidateLocalTLB_VAASID) apply simp apply (rule corres_when, rule refl) apply (rule corres_split[OF getCurThread_corres]) apply simp apply (rule setVMRoot_corres) apply wp+ apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric]) apply (wp hoare_drop_imps)[1] apply (assumption | wp hoare_drop_imps load_hw_asid_wp
              | clarsimp simp: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (K (is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (flush_page pageSize pd asid vptr) (flushPage pageSize pd asid vptr) proof (prove)
goal (1 subgoal):
 1. corres dc ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do y <- assert (vptr && mask pageBits = 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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do y <- assert (vptr && mask pageBits = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb') (do y <- assert (vptr && mask pageBits = 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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od) (do y <- assert (vptr && mask pageBits = 0);
root_switched <- setVMRootForFlush pd asid;
maybe_hw_asid <- loadHWASID asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>vptr && mask pageBits = 0 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0 \<and> cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> vspace_at_asid asid pd s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> unique_table_refs (caps_of_state s) \<and> pspace_aligned s \<and> pspace_distinct s; 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 ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. corres dc ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s'. corres dc (?Q16 s s') (?Q'16 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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when root_switched (getCurThread >>= setVMRoot)
od)
od)
 2. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) sa \<Longrightarrow> ?Q16 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'16 s s' sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> corres dc (?R20 s s' rv) (?R'20 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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asid)));
when rv' (getCurThread >>= setVMRoot)
od)
od)
 2. \<And>s s'. \<lbrace>?Q20 s s'\<rbrace> set_vm_root_for_flush pd asid \<lbrace>?R20 s s'\<rbrace>
 3. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>?R'20 s s'\<rbrace>
 4. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 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 (?R25 s s' rv rv' maybe_hw_asid) (?R'25 s s' rv rv' maybe_hw_asida) (when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)));
when rv' (getCurThread >>= setVMRoot)
od))
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>?R25 s s' rv rv'\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>?R'25 s s' rv rv'\<rbrace>
 4. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 6. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres dc (?R25 s s' rv' rv' maybe_hw_asida) (?R'25 s s' rv' rv' maybe_hw_asida) (when (\<exists>y. maybe_hw_asida = Some y) (do y <- do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (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_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)));
when rv' (getCurThread >>= setVMRoot)
od))
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>?R25 s s' rv rv'\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>?R'25 s s' rv rv'\<rbrace>
 4. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 6. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres dc (?P41 s s' rv' rv' maybe_hw_asida) (?P'40 s s' rv' rv' maybe_hw_asida) (do y <- do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)));
when rv' (gets cur_thread >>= set_vm_root)
od) (do y <- doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)));
when rv' (getCurThread >>= setVMRoot)
od)
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ?P41 s s' rv rv' a b\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ?P'40 s s' rv rv' a b\<rbrace>
 4. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 6. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (10 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)))
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?R45 s s' rv' maybe_hw_asida rv) (?R'45 s s' rv' maybe_hw_asida rv'a) (when rv' (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R45 s s' rv' maybe_hw_asida\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R'45 s s' rv' maybe_hw_asida\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 9. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (10 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. True \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida)))
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?R45 s s' rv' maybe_hw_asida rv) (?R'45 s s' rv' maybe_hw_asida rv'a) (when rv' (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R45 s s' rv' maybe_hw_asida\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R'45 s s' rv' maybe_hw_asida\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 9. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (10 subgoals):
 1. \<And>s s' rv' maybe_hw_asida sa. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> True
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> corres dc (?R45 s s' rv' maybe_hw_asida rv) (?R'45 s s' rv' maybe_hw_asida rv'a) (when rv' (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R45 s s' rv' maybe_hw_asida\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R'45 s s' rv' maybe_hw_asida\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 9. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 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 (?R45 s s' rv' maybe_hw_asida rv) (?R'45 s s' rv' maybe_hw_asida rv'a) (when rv' (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 2. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R45 s s' rv' maybe_hw_asida\<rbrace>
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>?R'45 s s' rv' maybe_hw_asida\<rbrace>
 4. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 6. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 7. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 8. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 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 (?P68 s s' rv' maybe_hw_asida rv) (?P'70 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>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ?P68 s s' rv' maybe_hw_asida rv x\<rbrace>
 3. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'70 s s' rv' maybe_hw_asida rv'a x\<rbrace>
 4. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 6. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 7. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 8. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 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 (?R74 s s' rv' maybe_hw_asida rv rv'a rva) (?R'74 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>?Q75 s s' rv' maybe_hw_asida rv\<rbrace> gets cur_thread \<lbrace>?R74 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'76 s s' rv' maybe_hw_asida rv'a\<rbrace> getCurThread \<lbrace>?R'74 s s' rv' maybe_hw_asida rv rv'a\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q75 s s' rv' maybe_hw_asida rv) x\<rbrace>
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'76 s s' rv' maybe_hw_asida rv'a) x\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 8. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 9. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 10. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 s s') sa
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s s' rv' maybe_hw_asida rva. corres dc (?R74 s s' rv' maybe_hw_asida () () rva) (?R'74 s s' rv' maybe_hw_asida () () rva) (set_vm_root rva) (setVMRoot rva)
 2. \<And>s s' rv' maybe_hw_asida rv rv'a. dc rv rv'a \<Longrightarrow> \<lbrace>?Q75 s s' rv' maybe_hw_asida rv\<rbrace> gets cur_thread \<lbrace>?R74 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'76 s s' rv' maybe_hw_asida rv'a\<rbrace> getCurThread \<lbrace>?R'74 s s' rv' maybe_hw_asida rv rv'a\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q75 s s' rv' maybe_hw_asida rv) x\<rbrace>
 5. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'76 s s' rv' maybe_hw_asida rv'a) x\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 7. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 8. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 9. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 10. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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>?Q75 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'76 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>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q75 s s' rv' maybe_hw_asida rv) x\<rbrace>
 4. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'76 s s' rv' maybe_hw_asida rv'a) x\<rbrace>
 5. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 6. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 7. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 8. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 9. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (tcb_at (cur_thread 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) a)) x\<rbrace>
 2. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 4. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 5. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 6. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 7. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 s s') sa
 8. \<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'20 s s') sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q50 s s' rv' rv' maybe_hw_asida\<rbrace> do_machine_op (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv x. rv' \<longrightarrow> cur_tcb x \<and> valid_arch_state x \<and> valid_objs x \<and> valid_asid_map x \<and> unique_table_refs (caps_of_state x) \<and> valid_vs_lookup x \<and> valid_global_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> valid_vspace_objs x\<rbrace>
 2. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q50 s s' rv rv' a) b\<rbrace>
 4. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 5. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 6. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 7. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 s s') sa
 8. \<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'20 s s') sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' rv' maybe_hw_asida. \<lbrace>?Q'49 s s' rv' rv' maybe_hw_asida\<rbrace> doMachineOp (invalidateLocalTLB_VAASID (vptr || UCAST(8 \<rightarrow> 32) (the maybe_hw_asida))) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 2. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q30 s s' rv\<rbrace> load_hw_asid asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. 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>
 3. \<And>s s' rv rv'. rv = rv' \<Longrightarrow> \<lbrace>?Q'31 s s' rv'\<rbrace> loadHWASID asid \<lbrace>\<lambda>a b. (\<exists>y. a = Some y) \<longrightarrow> ((\<lambda>_. True) and ?Q'49 s s' rv rv' a) b\<rbrace>
 4. \<And>s s'. \<lbrace>?Q20 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 ?Q30 s s' rv\<rbrace>
 5. \<And>s s'. \<lbrace>?Q'20 s s'\<rbrace> setVMRootForFlush pd asid \<lbrace>\<lambda>rv'. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'31 s s' rv'\<rbrace>
 6. \<And>s s' sa. ((\<lambda>y. is_aligned vptr pageBits \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and cur_tcb and valid_arch_state and valid_objs and vspace_at_asid asid pd and valid_asid_map and valid_vspace_objs and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and pspace_aligned and pspace_distinct) 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 ?Q20 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'20 s s') sa proof (prove)
goal:
No subgoals!