theory VSpace_R

lemma loadHWASID_corres:
  "corres (=)
          (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 asid_bits))
          (pspace_aligned' and pspace_distinct' and no_0_obj')
          (load_hw_asid a) (loadHWASID a)" apply (simp add: load_hw_asid_def loadHWASID_def) apply (rule_tac r'="(=)" in corres_underlying_split [OF _ _ gets_sp gets_sp]) apply (clarsimp simp: state_relation_def arch_state_relation_def) apply (case_tac "rv' a") apply simp apply (rule corres_guard_imp) apply (rule_tac pd=pd in findPDForASIDAssert_known_corres) apply (rule corres_trivial, simp) apply clarsimp apply clarsimp apply clarsimp apply (rule corres_guard_imp) apply (rule_tac pd=b in findPDForASIDAssert_known_corres) apply (rule corres_trivial, simp) apply (clarsimp simp: valid_arch_state_def valid_asid_map_def) apply (drule subsetD, erule domI) apply (drule bspec, erule graph_ofI) apply clarsimp 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 (\<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)) (pspace_aligned' and pspace_distinct' and no_0_obj') (load_hw_asid a) (loadHWASID a) 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 (\<lambda>s. \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s) and (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (do asid_map <- gets (arm_asid_map \<circ> arch_state);
return (map_option fst (asid_map a))
od) (do asidMap <- gets (armKSASIDMap \<circ> ksArchState);
y <- findPDForASIDAssert a;
return (case asidMap a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (2 subgoals):
 1. corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (gets (arm_asid_map \<circ> arch_state)) (gets (armKSASIDMap \<circ> ksArchState))
 2. \<And>rv rv'. rv = rv' \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. \<lbrakk>rv = rv'; rv' a = None\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od)
 2. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (2 subgoals):
 1. \<And>rv. rv a = None \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv)) (return None) (do y <- findPDForASIDAssert a;
return None
od)
 2. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. rv a = None \<Longrightarrow> corres (=) (?Q28 rv) (?Q'28 rv) (return None) (do y <- findPDForASIDAssert a;
return None
od)
 2. \<And>rv s. \<lbrakk>rv a = None; (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv)) s\<rbrakk> \<Longrightarrow> ?Q28 rv s
 3. \<And>rv s. \<lbrakk>rv a = None; (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv)) s\<rbrakk> \<Longrightarrow> ?Q'28 rv s
 4. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (4 subgoals):
 1. \<And>rv. rv a = None \<Longrightarrow> corres (=) (?P32 rv) (?P'32 rv) (return None) (return None)
 2. \<And>rv s. \<lbrakk>rv a = None; (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv)) s\<rbrakk> \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and ?P32 rv) s
 3. \<And>rv s. \<lbrakk>rv a = None; (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv)) s\<rbrakk> \<Longrightarrow> (?P'32 rv and pspace_aligned' and pspace_distinct' and no_0_obj') s
 4. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>rv a = None; (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv)) s\<rbrakk> \<Longrightarrow> (vspace_at_asid a pd and pd_at_uniq a pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>_. True)) s
 2. \<And>rv s. \<lbrakk>rv a = None; (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s
 3. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>rv a = None; (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s
 2. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv' aa. \<lbrakk>rv = rv'; rv' a = Some aa\<rbrakk> \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. (arm_asid_map \<circ> arch_state) s = rv)) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (armKSASIDMap \<circ> ksArchState) s = rv')) (return (map_option fst (rv a))) (do y <- findPDForASIDAssert a;
return (case rv' a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid)
od) proof (prove)
goal (1 subgoal):
 1. \<And>rv' aa b. rv' a = Some (aa, b) \<Longrightarrow> corres (=) (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv')) (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) (return (Some aa)) (do y <- findPDForASIDAssert a;
return (Some aa)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv' aa b. rv' a = Some (aa, b) \<Longrightarrow> corres (=) (?Q36 rv' aa b) (?Q'36 rv' aa b) (return (Some aa)) (do y <- findPDForASIDAssert a;
return (Some aa)
od)
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv')) s\<rbrakk> \<Longrightarrow> ?Q36 rv' aa b s
 3. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ?Q'36 rv' aa b s proof (prove)
goal (3 subgoals):
 1. \<And>rv' aa b. rv' a = Some (aa, b) \<Longrightarrow> corres (=) (?P40 rv' aa b) (?P'40 rv' aa b) (return (Some aa)) (return (Some aa))
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv')) s\<rbrakk> \<Longrightarrow> (vspace_at_asid a b and pd_at_uniq a b and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and ?P40 rv' aa b) s
 3. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> (?P'40 rv' aa b and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (2 subgoals):
 1. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (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 (\<lambda>y. a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>s. arm_asid_map (arch_state s) = rv')) s\<rbrakk> \<Longrightarrow> (vspace_at_asid a b and pd_at_uniq a b and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits) and (\<lambda>_. True)) s
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (2 subgoals):
 1. \<And>aa b s. \<lbrakk>arm_asid_map (arch_state s) a = Some (aa, b); valid_vspace_objs s; pspace_distinct s; pspace_aligned s; dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid a pd s; \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s; a \<noteq> 0; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> vspace_at_asid a b s \<and> pd_at_uniq a b s
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (2 subgoals):
 1. \<And>aa b s. \<lbrakk>arm_asid_map (arch_state s) a = Some (aa, b); valid_vspace_objs s; pspace_distinct s; pspace_aligned s; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0; vspace_at_asid a pd s; \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s; a \<noteq> 0; a \<le> mask local.asid_bits; a \<in> {0..mask local.asid_bits}\<rbrakk> \<Longrightarrow> vspace_at_asid a b s \<and> pd_at_uniq a b s
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (2 subgoals):
 1. \<And>aa b s. \<lbrakk>arm_asid_map (arch_state s) a = Some (aa, b); valid_vspace_objs s; pspace_distinct s; pspace_aligned s; vspace_at_asid a pd s; \<forall>pd. vspace_at_asid a pd s \<longrightarrow> pd_at_uniq a pd s; a \<noteq> 0; a \<le> mask local.asid_bits; a \<in> {0..mask local.asid_bits}; case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> vspace_at_asid a b s \<and> pd_at_uniq a b s
 2. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal (1 subgoal):
 1. \<And>rv' aa b s. \<lbrakk>rv' a = Some (aa, b); (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. armKSASIDMap (ksArchState s) = rv')) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and pspace_aligned' and pspace_distinct' and no_0_obj') s proof (prove)
goal:
No subgoals!