theory TcbAcc_R

lemma get_cap_corres_all_rights_P:
  "cte_ptr' = cte_map cte_ptr \<Longrightarrow>
  corres (\<lambda>x y. cap_relation x y \<and> P x)
         (cte_wp_at P cte_ptr) (pspace_aligned' and pspace_distinct')
         (get_cap cte_ptr) (getSlotCap cte_ptr')" apply (simp add: getSlotCap_def mask_cap_def) apply (subst bind_return [symmetric]) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres_P [where P=P]]) apply (insert cap_relation_masks, simp) apply (wp getCTE_wp')+ apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres (\<lambda>x y. cap_relation x y \<and> P x) (cte_wp_at P cte_ptr) (pspace_aligned' and pspace_distinct') (get_cap cte_ptr) (getSlotCap cte_ptr') proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres (\<lambda>x y. cap_relation x y \<and> P x) (cte_wp_at P cte_ptr) (pspace_aligned' and pspace_distinct') (get_cap cte_ptr) (do cte <- getCTE (cte_map cte_ptr);
return (cteCap cte)
od) proof (prove)
goal (1 subgoal):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres (\<lambda>x y. cap_relation x y \<and> P x) (cte_wp_at P cte_ptr) (pspace_aligned' and pspace_distinct') (get_cap cte_ptr >>= return) (do cte <- getCTE (cte_map cte_ptr);
return (cteCap cte)
od) proof (prove)
goal (3 subgoals):
 1. cte_ptr' = cte_map cte_ptr \<Longrightarrow> corres (\<lambda>x y. cap_relation x y \<and> P x) ?Q1 ?Q'1 (get_cap cte_ptr >>= return) (do cte <- getCTE (cte_map cte_ptr);
return (cteCap cte)
od)
 2. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; cte_wp_at P cte_ptr s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'1 s proof (prove)
goal (5 subgoals):
 1. \<And>rv cte. \<lbrakk>cte_ptr' = cte_map cte_ptr; cap_relation rv (cteCap cte) \<and> P rv\<rbrakk> \<Longrightarrow> corres (\<lambda>x y. cap_relation x y \<and> P x) (?R5 rv) (?R'5 cte) (return rv) (return (cteCap cte))
 2. cte_ptr' = cte_map cte_ptr \<Longrightarrow> \<lbrace>?Q5\<rbrace> get_cap cte_ptr \<lbrace>?R5\<rbrace>
 3. cte_ptr' = cte_map cte_ptr \<Longrightarrow> \<lbrace>?Q'5\<rbrace> getCTE (cte_map cte_ptr) \<lbrace>?R'5\<rbrace>
 4. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; cte_wp_at P cte_ptr s\<rbrakk> \<Longrightarrow> (cte_wp_at P cte_ptr and ?Q5) s
 5. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'5) s proof (prove)
goal (4 subgoals):
 1. \<lbrakk>cte_ptr' = cte_map cte_ptr; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> get_cap cte_ptr \<lbrace>?R5\<rbrace>
 2. \<lbrakk>cte_ptr' = cte_map cte_ptr; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> getCTE (cte_map cte_ptr) \<lbrace>?R'5\<rbrace>
 3. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; cte_wp_at P cte_ptr s; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> (cte_wp_at P cte_ptr and ?Q5) s
 4. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; (pspace_aligned' and pspace_distinct') s; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'5) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; cte_wp_at P cte_ptr s; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> (cte_wp_at P cte_ptr and (\<lambda>s. True)) s
 2. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; (pspace_aligned' and pspace_distinct') s; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map cte_ptr) s \<longrightarrow> True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_ptr' = cte_map cte_ptr; (pspace_aligned' and pspace_distinct') s; \<And>c c' rmask. cap_relation c c' \<Longrightarrow> cap_relation (cap_rights_update (cap_rights c \<inter> rmask) c) (global.maskCapRights (rights_mask_map rmask) c')\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. \<forall>cte. cte_wp_at' ((=) cte) (cte_map cte_ptr) s \<longrightarrow> True)) s proof (prove)
goal:
No subgoals!