theory Tcb_R

lemma checkCapAt_corres:
  assumes r: "cap_relation cap cap'"
  assumes c: "corres dc Q Q' f f'"
  assumes Q: "\<And>s. P s \<and> cte_wp_at (same_object_as cap) slot s \<Longrightarrow> Q s"
  assumes Q': "\<And>s. P' s \<and> cte_wp_at' (sameObjectAs cap' o cteCap) (cte_map slot) s \<Longrightarrow> Q' s"
  shows "corres dc (P and cte_at slot and invs) (P' and pspace_aligned' and pspace_distinct')
             (check_cap_at cap slot f)
             (checkCapAt cap' (cte_map slot) f')" using r c apply (simp add: check_cap_at_def checkCapAt_def liftM_def when_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_if [unfolded if_apply_def2]) apply (erule(1) sameObject_corres2) apply assumption apply (rule corres_trivial, simp) apply (wp get_cap_wp getCTE_wp')+ apply (fastforce elim: cte_wp_at_weakenE intro: Q) apply (fastforce elim: cte_wp_at_weakenE' intro: Q') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (P and cte_wp_at (\<lambda>_. True) slot and invs) (P' and pspace_aligned' and pspace_distinct') (check_cap_at cap slot f) (checkCapAt cap' (cte_map slot) f') proof (prove)
using this:
cap_relation cap cap'
corres dc Q Q' f f'

goal (1 subgoal):
 1. corres dc (P and cte_wp_at (\<lambda>_. True) slot and invs) (P' and pspace_aligned' and pspace_distinct') (check_cap_at cap slot f) (checkCapAt cap' (cte_map slot) f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> corres dc (P and cte_wp_at (\<lambda>_. True) slot and invs) (P' and pspace_aligned' and pspace_distinct') (do cap' <- get_cap slot;
if same_object_as cap cap' then f else return ()
od) (do x <- getCTE (cte_map slot);
if global.sameObjectAs cap' (cteCap x) then f' else return ()
od) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> corres dc ?Q4 ?Q'4 (do cap' <- get_cap slot;
if same_object_as cap cap' then f else return ()
od) (do x <- getCTE (cte_map slot);
if global.sameObjectAs cap' (cteCap x) then f' else return ()
od)
 2. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> ?Q4 s
 3. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?R8 cap'a) (?R'8 x) (if same_object_as cap cap'a then f else return ()) (if global.sameObjectAs cap' (cteCap x) then f' else return ())
 2. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap slot \<lbrace>?R8\<rbrace>
 3. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map slot) \<lbrace>?R'8\<rbrace>
 4. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q8) s
 5. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> same_object_as cap cap'a = global.sameObjectAs cap' (cteCap x)
 2. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?P15 cap'a) (?P'19 x) f f'
 3. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?Q17 cap'a) (?Q'21 x) (return ()) (return ())
 4. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap slot \<lbrace>\<lambda>cap' x. (same_object_as cap cap' \<longrightarrow> ?P15 cap' x) \<and> (\<not> same_object_as cap cap' \<longrightarrow> ?Q17 cap' x)\<rbrace>
 5. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>x xa. (global.sameObjectAs cap' (cteCap x) \<longrightarrow> ?P'19 x xa) \<and> (\<not> global.sameObjectAs cap' (cteCap x) \<longrightarrow> ?Q'21 x xa)\<rbrace>
 6. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q8) s
 7. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?P15 cap'a) (?P'19 x) f f'
 2. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?Q17 cap'a) (?Q'21 x) (return ()) (return ())
 3. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap slot \<lbrace>\<lambda>cap' x. (same_object_as cap cap' \<longrightarrow> ?P15 cap' x) \<and> (\<not> same_object_as cap cap' \<longrightarrow> ?Q17 cap' x)\<rbrace>
 4. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>x xa. (global.sameObjectAs cap' (cteCap x) \<longrightarrow> ?P'19 x xa) \<and> (\<not> global.sameObjectAs cap' (cteCap x) \<longrightarrow> ?Q'21 x xa)\<rbrace>
 5. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q8) s
 6. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>cap'a x. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; cap_relation cap'a (cteCap x)\<rbrakk> \<Longrightarrow> corres dc (?Q17 cap'a) (?Q'21 x) (return ()) (return ())
 2. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap slot \<lbrace>\<lambda>cap' x. (same_object_as cap cap' \<longrightarrow> Q x) \<and> (\<not> same_object_as cap cap' \<longrightarrow> ?Q17 cap' x)\<rbrace>
 3. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>x xa. (global.sameObjectAs cap' (cteCap x) \<longrightarrow> Q' xa) \<and> (\<not> global.sameObjectAs cap' (cteCap x) \<longrightarrow> ?Q'21 x xa)\<rbrace>
 4. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q8) s
 5. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8\<rbrace> get_cap slot \<lbrace>\<lambda>cap' x. (same_object_as cap cap' \<longrightarrow> Q x) \<and> (\<not> same_object_as cap cap' \<longrightarrow> True)\<rbrace>
 2. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'8\<rbrace> getCTE (cte_map slot) \<lbrace>\<lambda>x xa. (global.sameObjectAs cap' (cteCap x) \<longrightarrow> Q' xa) \<and> (\<not> global.sameObjectAs cap' (cteCap x) \<longrightarrow> True)\<rbrace>
 3. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and ?Q8) s
 4. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P and cte_wp_at (\<lambda>_. True) slot and invs) s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) slot and (\<lambda>s. \<forall>capa. cte_wp_at ((=) capa) slot s \<longrightarrow> (same_object_as cap capa \<longrightarrow> Q s) \<and> (\<not> same_object_as cap capa \<longrightarrow> True))) s
 2. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map slot) s \<longrightarrow> (global.sameObjectAs cap' (cteCap cte) \<longrightarrow> Q' s) \<and> (\<not> global.sameObjectAs cap' (cteCap cte) \<longrightarrow> True))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_relation cap cap'; corres dc Q Q' f f'; (P' and pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map slot) s \<longrightarrow> (global.sameObjectAs cap' (cteCap cte) \<longrightarrow> Q' s) \<and> (\<not> global.sameObjectAs cap' (cteCap cte) \<longrightarrow> True))) s proof (prove)
goal:
No subgoals!