theory VSpace_R

lemma invalidateTLBByASID_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')
          (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)" apply (simp add: invalidate_tlb_by_asid_def invalidateTLBByASID_def) apply (rule corres_guard_imp) apply (rule corres_split) apply (rule loadHWASID_corres[where pd=pd]) 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') (invalidate_tlb_by_asid asid) (invalidateTLBByASID 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;
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;
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;
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;
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) (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. \<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) (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. \<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 (5 subgoals):
 1. \<And>x2. corres dc (?Q53 (Some x2) x2) (?B'55 (Some x2)) (do_machine_op (invalidateLocalTLB_ASID x2)) (doMachineOp (invalidateLocalTLB_ASID x2))
 2. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q52 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q53 maybe_hw_asid x s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida s. ?A'54 maybe_hw_asida s \<and> ?B'55 maybe_hw_asida s\<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 (5 subgoals):
 1. \<And>x2. corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (invalidateLocalTLB_ASID x2) (invalidateLocalTLB_ASID x2)
 2. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q52 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida s. ?A'54 maybe_hw_asida s \<and> True\<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 (5 subgoals):
 1. \<And>x2. True \<Longrightarrow> no_fail (\<lambda>_. True) (invalidateLocalTLB_ASID x2)
 2. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q52 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida s. ?A'54 maybe_hw_asida s \<and> True\<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 (4 subgoals):
 1. \<lbrace>?Q8\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q52 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> True)\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybe_hw_asida s. ?A'54 maybe_hw_asida s \<and> True\<rbrace>
 3. \<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
 4. \<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>s. True \<and> True)) 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>s. True \<and> True)) s proof (prove)
goal:
No subgoals!