theory VSpace_R

lemma invalidateASIDEntry_corres:
  "corres dc (valid_vspace_objs and valid_asid_map
                and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0)
                and vspace_at_asid asid pd and valid_vs_lookup
                and unique_table_refs o caps_of_state
                and valid_global_objs and valid_arch_state
                and pspace_aligned and pspace_distinct)
             (pspace_aligned' and pspace_distinct' and no_0_obj')
             (invalidate_asid_entry asid) (invalidateASIDEntry asid)" apply (simp add: invalidate_asid_entry_def invalidateASIDEntry_def) apply (rule corres_guard_imp) apply (rule corres_split[OF loadHWASID_corres[where pd=pd]]) apply (rule corres_split[OF corres_when]) apply simp apply simp apply (rule invalidateHWASIDEntry_corres) apply (rule invalidateASID_corres[where pd=pd]) apply (wp load_hw_asid_wp
                | clarsimp cong: if_cong)+ apply (simp add: pd_at_asid_uniq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_vspace_objs and valid_asid_map and K (asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_asid_entry asid) (invalidateASIDEntry asid) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') (do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid));
invalidate_asid asid
od) (do maybeHWASID <- loadHWASID asid;
y <- when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID));
invalidateASID asid
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid));
invalidate_asid asid
od) (do maybeHWASID <- loadHWASID asid;
y <- when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID));
invalidateASID asid
od)
 2. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> corres dc (?R4 maybe_hw_asid) (?R'4 maybeHWASID) (do y <- when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid));
invalidate_asid asid
od) (do y <- when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID));
invalidateASID asid
od)
 2. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>?R'4\<rbrace>
 4. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) s
 5. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> (\<exists>y. maybe_hw_asid = Some y) = (\<exists>y. maybeHWASID = Some y)
 2. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> corres dc (?P12 maybe_hw_asid) (?P'15 maybeHWASID) (invalidate_hw_asid_entry (the maybe_hw_asid)) (invalidateHWASIDEntry (the maybeHWASID))
 3. \<And>maybe_hw_asid maybeHWASID y ya. \<lbrakk>maybe_hw_asid = maybeHWASID; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R9 maybe_hw_asid maybeHWASID y) (?R'9 maybe_hw_asid maybeHWASID ya) (invalidate_asid asid) (invalidateASID asid)
 4. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?R9 maybe_hw_asid maybeHWASID\<rbrace>
 5. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q'16 maybeHWASID\<rbrace> when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID)) \<lbrace>?R'9 maybe_hw_asid maybeHWASID\<rbrace>
 6. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>x. (\<exists>y. maybe_hw_asid = Some y) \<longrightarrow> ?P12 maybe_hw_asid x) and ?Q13 maybe_hw_asid\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybeHWASID. (\<lambda>x. (\<exists>y. maybeHWASID = Some y) \<longrightarrow> ?P'15 maybeHWASID x) and ?Q'16 maybeHWASID\<rbrace>
 8. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> corres dc (?P12 maybe_hw_asid) (?P'15 maybeHWASID) (invalidate_hw_asid_entry (the maybe_hw_asid)) (invalidateHWASIDEntry (the maybeHWASID))
 2. \<And>maybe_hw_asid maybeHWASID y ya. \<lbrakk>maybe_hw_asid = maybeHWASID; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R9 maybe_hw_asid maybeHWASID y) (?R'9 maybe_hw_asid maybeHWASID ya) (invalidate_asid asid) (invalidateASID asid)
 3. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?R9 maybe_hw_asid maybeHWASID\<rbrace>
 4. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q'16 maybeHWASID\<rbrace> when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID)) \<lbrace>?R'9 maybe_hw_asid maybeHWASID\<rbrace>
 5. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>x. (\<exists>y. maybe_hw_asid = Some y) \<longrightarrow> ?P12 maybe_hw_asid x) and ?Q13 maybe_hw_asid\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybeHWASID. (\<lambda>x. (\<exists>y. maybeHWASID = Some y) \<longrightarrow> ?P'15 maybeHWASID x) and ?Q'16 maybeHWASID\<rbrace>
 7. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) 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'4) s proof (prove)
goal (8 subgoals):
 1. \<And>maybe_hw_asid. corres dc (?P12 maybe_hw_asid) (?P'15 maybe_hw_asid) (invalidate_hw_asid_entry (the maybe_hw_asid)) (invalidateHWASIDEntry (the maybe_hw_asid))
 2. \<And>maybe_hw_asid maybeHWASID y ya. \<lbrakk>maybe_hw_asid = maybeHWASID; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R9 maybe_hw_asid maybeHWASID y) (?R'9 maybe_hw_asid maybeHWASID ya) (invalidate_asid asid) (invalidateASID asid)
 3. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?R9 maybe_hw_asid maybeHWASID\<rbrace>
 4. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q'16 maybeHWASID\<rbrace> when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID)) \<lbrace>?R'9 maybe_hw_asid maybeHWASID\<rbrace>
 5. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>x. (\<exists>y. maybe_hw_asid = Some y) \<longrightarrow> ?P12 maybe_hw_asid x) and ?Q13 maybe_hw_asid\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybeHWASID. (\<lambda>x. (\<exists>y. maybeHWASID = Some y) \<longrightarrow> ?P'15 maybeHWASID x) and ?Q'16 maybeHWASID\<rbrace>
 7. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) 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'4) s proof (prove)
goal (7 subgoals):
 1. \<And>maybe_hw_asid maybeHWASID y ya. \<lbrakk>maybe_hw_asid = maybeHWASID; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R9 maybe_hw_asid maybeHWASID y) (?R'9 maybe_hw_asid maybeHWASID ya) (invalidate_asid asid) (invalidateASID asid)
 2. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>?R9 maybe_hw_asid maybeHWASID\<rbrace>
 3. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q'16 maybeHWASID\<rbrace> when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID)) \<lbrace>?R'9 maybe_hw_asid maybeHWASID\<rbrace>
 4. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>x. (\<exists>y. maybe_hw_asid = Some y) \<longrightarrow> True) and ?Q13 maybe_hw_asid\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybeHWASID. (\<lambda>x. (\<exists>y. maybeHWASID = Some y) \<longrightarrow> True) and ?Q'16 maybeHWASID\<rbrace>
 6. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) 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'4) s proof (prove)
goal (6 subgoals):
 1. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q13 maybe_hw_asid\<rbrace> when (\<exists>y. maybe_hw_asid = Some y) (invalidate_hw_asid_entry (the maybe_hw_asid)) \<lbrace>\<lambda>y. valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid asid pd and pd_at_uniq asid pd and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)\<rbrace>
 2. \<And>maybe_hw_asid maybeHWASID. maybe_hw_asid = maybeHWASID \<Longrightarrow> \<lbrace>?Q'16 maybeHWASID\<rbrace> when (\<exists>y. maybeHWASID = Some y) (invalidateHWASIDEntry (the maybeHWASID)) \<lbrace>\<lambda>ya. pspace_aligned' and pspace_distinct' and no_0_obj'\<rbrace>
 3. \<lbrace>?Q4\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid. (\<lambda>x. (\<exists>y. maybe_hw_asid = Some y) \<longrightarrow> True) and ?Q13 maybe_hw_asid\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> loadHWASID asid \<lbrace>\<lambda>maybeHWASID. (\<lambda>x. (\<exists>y. maybeHWASID = Some y) \<longrightarrow> True) and ?Q'16 maybeHWASID\<rbrace>
 5. \<And>s. (valid_vspace_objs and valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits \<and> asid \<noteq> 0) and vspace_at_asid asid pd and valid_vs_lookup and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_arch_state and pspace_aligned and pspace_distinct) 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 ?Q4) 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'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_vspace_objs s; valid_asid_map s; asid \<le> mask local.asid_bits; asid \<noteq> 0; vspace_at_asid asid pd s; valid_vs_lookup s; unique_table_refs (caps_of_state s); valid_global_objs s; valid_arch_state s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> (\<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s) \<and> pd_at_uniq asid pd 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. ((\<lambda>x. (\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True) and (if \<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y then \<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a else (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s))) s)) 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. ((\<lambda>x. (\<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y) \<longrightarrow> True) and (if \<exists>y. map_option fst (armKSASIDMap (ksArchState s) asid) = Some y then \<lambda>a. pspace_aligned' a \<and> pspace_distinct' a \<and> no_0_obj' a else (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s))) s)) s proof (prove)
goal:
No subgoals!