theory VSpace_R

lemma getHWASID_corres:
  "corres (=)
          (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask asid_bits)
           and unique_table_refs o caps_of_state
           and valid_global_objs and valid_vs_lookup
           and valid_asid_map and valid_vspace_objs
           and pspace_aligned and pspace_distinct
           and valid_arch_state)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (get_hw_asid a) (getHWASID a)" apply (simp add: get_hw_asid_def getHWASID_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF loadHWASID_corres[where pd=pd]]) apply (corres_cases; simp) apply (rule corres_split_eqr[OF findFreeHWASID_corres]) apply (rule corres_split[OF storeHWASID_corres[where pd=pd]]) apply (rule corres_trivial, simp) apply (wpsimp wp: load_hw_asid_wp hoare_drop_imp simp: pd_at_asid_uniq)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (vspace_at_asid a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) (pspace_aligned' and pspace_distinct' and no_0_obj') (get_hw_asid a) (getHWASID a) proof (prove)
goal (1 subgoal):
 1. corres (=) (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) (pspace_aligned' and pspace_distinct' and no_0_obj') (do maybe_hw_asid <- load_hw_asid a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
y <- store_hw_asid a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od) (do maybe_hw_asid <- loadHWASID a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q4 ?Q'4 (do maybe_hw_asid <- load_hw_asid a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
y <- store_hw_asid a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od) (do maybe_hw_asid <- loadHWASID a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od)
 2. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>maybe_hw_asid. corres (=) (?R8 maybe_hw_asid) (?R'8 maybe_hw_asid) (case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
y <- store_hw_asid a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid) (case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid)
 2. \<lbrace>?Q8\<rbrace> load_hw_asid a \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID a \<lbrace>?R'8\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and K (a \<noteq> 0 \<and> a \<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. corres (=) (?Q51 None) (?Q'53 None) (do new_hw_asid <- find_free_hw_asid;
y <- store_hw_asid a new_hw_asid;
return new_hw_asid
od) (do new_hw_asid <- findFreeHWASID;
y <- storeHWASID a new_hw_asid;
return new_hw_asid
od)
 2. \<lbrace>?Q8\<rbrace> load_hw_asid a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q51 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q52 maybe_hw_asid x s)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> loadHWASID a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> ?Q'53 maybe_hw_asid s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q'54 maybe_hw_asid x s)\<rbrace>
 4. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and K (a \<noteq> 0 \<and> a \<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 (7 subgoals):
 1. \<And>new_hw_asid. corres (=) (?R66 new_hw_asid) (?R'66 new_hw_asid) (do y <- store_hw_asid a new_hw_asid;
return new_hw_asid
od) (do y <- storeHWASID a new_hw_asid;
return new_hw_asid
od)
 2. \<lbrace>?Q71 None\<rbrace> find_free_hw_asid \<lbrace>?R66\<rbrace>
 3. \<lbrace>?Q'70 None\<rbrace> findFreeHWASID \<lbrace>?R'66\<rbrace>
 4. \<lbrace>?Q8\<rbrace> load_hw_asid a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs and ?Q71 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q52 maybe_hw_asid x s)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> loadHWASID a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'70 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q'54 maybe_hw_asid x s)\<rbrace>
 6. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and K (a \<noteq> 0 \<and> a \<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 (9 subgoals):
 1. \<And>new_hw_asid rv rv'. dc rv rv' \<Longrightarrow> corres (=) (?R75 new_hw_asid rv) (?R'75 new_hw_asid rv') (return new_hw_asid) (return new_hw_asid)
 2. \<And>new_hw_asid. \<lbrace>?Q75 new_hw_asid\<rbrace> store_hw_asid a new_hw_asid \<lbrace>?R75 new_hw_asid\<rbrace>
 3. \<And>new_hw_asid. \<lbrace>?Q'75 new_hw_asid\<rbrace> storeHWASID a new_hw_asid \<lbrace>?R'75 new_hw_asid\<rbrace>
 4. \<lbrace>?Q71 None\<rbrace> find_free_hw_asid \<lbrace>\<lambda>new_hw_asid. vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map and ?Q75 new_hw_asid\<rbrace>
 5. \<lbrace>?Q'70 None\<rbrace> findFreeHWASID \<lbrace>\<lambda>new_hw_asid. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'75 new_hw_asid\<rbrace>
 6. \<lbrace>?Q8\<rbrace> load_hw_asid a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs and ?Q71 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q52 maybe_hw_asid x s)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> loadHWASID a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'70 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q'54 maybe_hw_asid x s)\<rbrace>
 8. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and ?Q8) 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'8) s proof (prove)
goal (8 subgoals):
 1. \<And>new_hw_asid. \<lbrace>?Q75 new_hw_asid\<rbrace> store_hw_asid a new_hw_asid \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>new_hw_asid. \<lbrace>?Q'75 new_hw_asid\<rbrace> storeHWASID a new_hw_asid \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<lbrace>?Q71 None\<rbrace> find_free_hw_asid \<lbrace>\<lambda>new_hw_asid. vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and pspace_distinct and pspace_aligned and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and valid_asid_map and ?Q75 new_hw_asid\<rbrace>
 4. \<lbrace>?Q'70 None\<rbrace> findFreeHWASID \<lbrace>\<lambda>new_hw_asid. pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'75 new_hw_asid\<rbrace>
 5. \<lbrace>?Q8\<rbrace> load_hw_asid a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_arch_state and valid_global_objs and ?Q71 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q52 maybe_hw_asid x s)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> loadHWASID a \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'70 maybe_hw_asid) s) \<and> (\<forall>x. maybe_hw_asid = Some x \<longrightarrow> ?Q'54 maybe_hw_asid x s)\<rbrace>
 7. \<And>s. (vspace_at_asid a pd and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and unique_table_refs \<circ> caps_of_state and valid_global_objs and valid_vs_lookup and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_arch_state) s \<Longrightarrow> (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and K (a \<noteq> 0 \<and> a \<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:
No subgoals!