theory VSpace_R

lemma load_hw_asid_corres2:
  "corres (=)
     (valid_vspace_objs and pspace_distinct and pspace_aligned
       and valid_asid_map and vspace_at_asid a pd
       and valid_vs_lookup and valid_global_objs
       and unique_table_refs o caps_of_state
       and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask asid_bits))
     (pspace_aligned' and pspace_distinct' and no_0_obj')
    (load_hw_asid a) (loadHWASID a)" apply (rule stronger_corres_guard_imp) apply (rule loadHWASID_corres[where pd=pd]) apply (clarsimp simp: pd_at_asid_uniq) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (load_hw_asid a) (loadHWASID a) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (load_hw_asid a) (loadHWASID a)
 2. \<And>s s'. \<lbrakk>(valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s; (pspace_aligned' and pspace_distinct' and no_0_obj') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>(valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s; (pspace_aligned' and pspace_distinct' and no_0_obj') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>(valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s; (pspace_aligned' and pspace_distinct' and no_0_obj') s'; (s, s') \<in> state_relation\<rbrakk> \<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)) s
 2. \<And>s s'. \<lbrakk>(valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s; (pspace_aligned' and pspace_distinct' and no_0_obj') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj') s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(valid_vspace_objs and pspace_distinct and pspace_aligned and valid_asid_map and vspace_at_asid a pd and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) s; (pspace_aligned' and pspace_distinct' and no_0_obj') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj') s' proof (prove)
goal:
No subgoals!