theory VSpace_R

lemma findPDForASIDAssert_known_corres:
  "corres r P P' f (g pd) \<Longrightarrow>
  corres r (vspace_at_asid asid pd and pd_at_uniq asid pd
               and valid_vspace_objs and valid_asid_map
               and pspace_aligned and pspace_distinct
               and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits) and P)
           (P' and pspace_aligned' and pspace_distinct' and no_0_obj')
       f (findPDForASIDAssert asid >>= g)" apply (subst return_bind[symmetric]) apply (subst corres_cong [OF refl refl _ refl refl]) apply (rule bind_apply_cong [OF _ refl]) apply clarsimp apply (erule(3) find_pd_for_asid_assert_eq[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[OF findPDForASIDAssert_corres[where pd=pd]]) apply simp apply wp+ apply clarsimp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') f (findPDForASIDAssert asid >>= g) proof (prove)
goal (1 subgoal):
 1. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') (do a <- return ?x;
f
od) (findPDForASIDAssert asid >>= g) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>corres r P P' f (g pd); (s, s') \<in> state_relation; (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s; (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s'\<rbrakk> \<Longrightarrow> (do a <- return ?x;
f
od) s = ?f'1 s
 2. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') ?f'1 (findPDForASIDAssert asid >>= g) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>corres r P P' f (g pd); (s, s') \<in> state_relation; (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s; (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s'\<rbrakk> \<Longrightarrow> return ?x s = ?f'5 s (?s'6 s)
 2. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') (\<lambda>s. (do rv <- ?f'5 s;
f
od) (?s'6 s)) (findPDForASIDAssert asid >>= g) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>corres r P P' f (g pd); (s, s') \<in> state_relation; vspace_at_asid asid pd s; P' s'; pd_at_uniq asid pd s; pspace_aligned' s'; valid_vspace_objs s; pspace_distinct' s'; no_0_obj' s'; valid_asid_map s; pspace_aligned s; pspace_distinct s; asid \<noteq> 0; asid \<le> mask local.asid_bits; P s\<rbrakk> \<Longrightarrow> return ?x s = ?f'5 s (?s'6 s)
 2. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') (\<lambda>s. (do rv <- ?f'5 s;
f
od) (?s'6 s)) (findPDForASIDAssert asid >>= g) proof (prove)
goal (1 subgoal):
 1. corres r P P' f (g pd) \<Longrightarrow> corres r (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) (P' and pspace_aligned' and pspace_distinct' and no_0_obj') (do rv <- find_pd_for_asid_assert asid;
f
od) (findPDForASIDAssert asid >>= g) proof (prove)
goal (3 subgoals):
 1. corres r P P' f (g pd) \<Longrightarrow> corres r ?Q25 ?Q'25 (do rv <- find_pd_for_asid_assert asid;
f
od) (findPDForASIDAssert asid >>= g)
 2. \<And>s. \<lbrakk>corres r P P' f (g pd); (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s\<rbrakk> \<Longrightarrow> ?Q25 s
 3. \<And>s. \<lbrakk>corres r P P' f (g pd); (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrakk> \<Longrightarrow> ?Q'25 s proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>corres r P P' f (g pd); rv = pd \<and> rv' = pd\<rbrakk> \<Longrightarrow> corres r (?R29 rv) (?R'29 rv') f (g rv')
 2. corres r P P' f (g pd) \<Longrightarrow> \<lbrace>?Q29\<rbrace> find_pd_for_asid_assert asid \<lbrace>?R29\<rbrace>
 3. corres r P P' f (g pd) \<Longrightarrow> \<lbrace>?Q'29\<rbrace> findPDForASIDAssert asid \<lbrace>?R'29\<rbrace>
 4. \<And>s. \<lbrakk>corres r P P' f (g pd); (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s\<rbrakk> \<Longrightarrow> (K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd and ?Q29) s
 5. \<And>s. \<lbrakk>corres r P P' f (g pd); (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'29) s proof (prove)
goal (4 subgoals):
 1. corres r P P' f (g pd) \<Longrightarrow> \<lbrace>?Q29\<rbrace> find_pd_for_asid_assert asid \<lbrace>\<lambda>a. P\<rbrace>
 2. corres r P P' f (g pd) \<Longrightarrow> \<lbrace>?Q'29\<rbrace> findPDForASIDAssert asid \<lbrace>\<lambda>a. P'\<rbrace>
 3. \<And>s. \<lbrakk>corres r P P' f (g pd); (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s\<rbrakk> \<Longrightarrow> (K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd and ?Q29) s
 4. \<And>s. \<lbrakk>corres r P P' f (g pd); (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'29) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>corres r P P' f (g pd); (vspace_at_asid asid pd and pd_at_uniq asid pd and valid_vspace_objs and valid_asid_map and pspace_aligned and pspace_distinct and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and P) s\<rbrakk> \<Longrightarrow> (K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_asid_map and vspace_at_asid asid pd and pd_at_uniq asid pd and P) s
 2. \<And>s. \<lbrakk>corres r P P' f (g pd); (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and P') s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>corres r P P' f (g pd); (P' and pspace_aligned' and pspace_distinct' and no_0_obj') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and P') s proof (prove)
goal:
No subgoals!