theory VSpace_R

lemma flushSpace_corres:
  "corres dc
          (K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
           and valid_asid_map and valid_vspace_objs
           and pspace_aligned and pspace_distinct
           and unique_table_refs o caps_of_state
           and valid_global_objs and valid_vs_lookup
           and valid_arch_state and vspace_at_asid asid pd)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (flush_space asid) (flushSpace asid)" apply (simp add: flushSpace_def flush_space_def) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule loadHWASID_corres[where pd=pd]) apply (rule corres_split) apply (rule corres_machine_op [where r=dc]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_cleanCaches_PoU) apply (corres_cases; clarsimp) apply (rule corres_machine_op) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_invalidateLocalTLB_ASID) apply wpsimp+ apply (simp add: pd_at_asid_uniq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) (pspace_aligned' and pspace_distinct' and no_0_obj') (flush_space asid) (flushSpace asid) proof (prove)
goal (1 subgoal):
 1. corres dc ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) (pspace_aligned' and pspace_distinct' and no_0_obj') (do maybe_hw_asid <- load_hw_asid asid;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)
od) (do maybe_hw_asid <- loadHWASID asid;
y <- doMachineOp cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q4 ?Q'4 (do maybe_hw_asid <- load_hw_asid asid;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)
od) (do maybe_hw_asid <- loadHWASID asid;
y <- doMachineOp cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid)
od)
 2. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'4 s proof (prove)
goal (6 subgoals):
 1. corres ?r'8 ?P8 ?P'8 (load_hw_asid asid) (loadHWASID asid)
 2. \<And>maybe_hw_asid maybe_hw_asida. ?r'8 maybe_hw_asid maybe_hw_asida \<Longrightarrow> corres dc (?R8 maybe_hw_asid) (?R'8 maybe_hw_asida) (do y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)
od) (do y <- doMachineOp cleanCaches_PoU;
case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid)
od)
 3. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>?R8\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>?R'8\<rbrace>
 5. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (?P8 and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> corres dc (?R8 maybe_hw_asid) (?R'8 maybe_hw_asida) (do y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)
od) (do y <- doMachineOp cleanCaches_PoU;
case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid)
od)
 2. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>?R'8\<rbrace>
 4. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) 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'8) s proof (prove)
goal (8 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> corres (?r'14 maybe_hw_asid maybe_hw_asida) (?P15 maybe_hw_asid) (?P'17 maybe_hw_asida) (do_machine_op cleanCaches_PoU) (doMachineOp cleanCaches_PoU)
 2. \<And>maybe_hw_asid maybe_hw_asida y ya. \<lbrakk>maybe_hw_asid = maybe_hw_asida; ?r'14 maybe_hw_asid maybe_hw_asida y ya\<rbrakk> \<Longrightarrow> corres dc (?R14 maybe_hw_asid maybe_hw_asida y) (?R'14 maybe_hw_asid maybe_hw_asida ya) (case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)) (case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid))
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>?R14 maybe_hw_asid maybe_hw_asida\<rbrace>
 4. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?R'14 maybe_hw_asid maybe_hw_asida\<rbrace>
 5. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. ?P15 maybe_hw_asid and ?Q16 maybe_hw_asid\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. ?P'17 maybe_hw_asida and ?Q'18 maybe_hw_asida\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) cleanCaches_PoU cleanCaches_PoU
 2. \<And>maybe_hw_asid maybe_hw_asida y ya. \<lbrakk>maybe_hw_asid = maybe_hw_asida; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R14 maybe_hw_asid maybe_hw_asida y) (?R'14 maybe_hw_asid maybe_hw_asida ya) (case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)) (case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid))
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>?R14 maybe_hw_asid maybe_hw_asida\<rbrace>
 4. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?R'14 maybe_hw_asid maybe_hw_asida\<rbrace>
 5. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida. \<lbrakk>maybe_hw_asid = maybe_hw_asida; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) cleanCaches_PoU
 2. \<And>maybe_hw_asid maybe_hw_asida y ya. \<lbrakk>maybe_hw_asid = maybe_hw_asida; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R14 maybe_hw_asid maybe_hw_asida y) (?R'14 maybe_hw_asid maybe_hw_asida ya) (case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)) (case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid))
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>?R14 maybe_hw_asid maybe_hw_asida\<rbrace>
 4. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?R'14 maybe_hw_asid maybe_hw_asida\<rbrace>
 5. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 7. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida y ya. \<lbrakk>maybe_hw_asid = maybe_hw_asida; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R14 maybe_hw_asid maybe_hw_asida y) (?R'14 maybe_hw_asid maybe_hw_asida ya) (case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op (invalidateLocalTLB_ASID hw_asid)) (case maybe_hw_asida of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> doMachineOp (invalidateLocalTLB_ASID hw_asid))
 2. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>?R14 maybe_hw_asid maybe_hw_asida\<rbrace>
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>?R'14 maybe_hw_asid maybe_hw_asida\<rbrace>
 4. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>x2. corres dc (?Q69 (Some x2) (Some x2) () x2) (?Q'71 (Some x2) (Some x2) () x2) (do_machine_op (invalidateLocalTLB_ASID x2)) (doMachineOp (invalidateLocalTLB_ASID x2))
 2. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> ?Q68 maybe_hw_asid maybe_hw_asida y s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q69 maybe_hw_asid maybe_hw_asida y x s)\<rbrace>
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>ya s. (maybe_hw_asid = None \<longrightarrow> ?Q'70 maybe_hw_asid maybe_hw_asida ya s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q'71 maybe_hw_asid maybe_hw_asida ya x s)\<rbrace>
 4. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>x2. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (invalidateLocalTLB_ASID x2) (invalidateLocalTLB_ASID x2)
 2. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> ?Q68 maybe_hw_asid maybe_hw_asida y s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>ya s. (maybe_hw_asid = None \<longrightarrow> ?Q'70 maybe_hw_asid maybe_hw_asida ya s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 4. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>x2. True \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_ASID x2)
 2. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> ?Q68 maybe_hw_asid maybe_hw_asida y s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 3. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>ya s. (maybe_hw_asid = None \<longrightarrow> ?Q'70 maybe_hw_asid maybe_hw_asida ya s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 4. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 6. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 7. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q16 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y s. (maybe_hw_asid = None \<longrightarrow> ?Q68 maybe_hw_asid maybe_hw_asida y s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 2. \<And>maybe_hw_asid maybe_hw_asida. maybe_hw_asid = maybe_hw_asida \<Longrightarrow> \<lbrace>?Q'18 maybe_hw_asida\<rbrace> doMachineOp cleanCaches_PoU \<lbrace>\<lambda>ya s. (maybe_hw_asid = None \<longrightarrow> ?Q'70 maybe_hw_asid maybe_hw_asida ya s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 3. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>_. True) and ?Q16 maybe_hw_asid\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida. (\<lambda>_. True) and ?Q'18 maybe_hw_asida\<rbrace>
 5. \<And>s. ((\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_arch_state and vspace_at_asid asid pd) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid asid pd and (\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda. \<lbrakk>asid \<le> mask local.asid_bits; asid \<noteq> 0; valid_asid_map s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_vs_lookup s; valid_arch_state s; vspace_at_asid asid pd s; vspace_at_asid asid pda s\<rbrakk> \<Longrightarrow> pd_at_uniq asid pda s
 2. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ((\<lambda>_. True) and ?Q'146)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ((\<lambda>_. True) and ?Q'146)) s proof (prove)
goal:
No subgoals!