theory CSpace_R

lemma pspace_relation_no_reply_caps:
  assumes pspace: "pspace_relation (kheap s) (ksPSpace s')"
  and       invs: "invs s"
  and        tcb: "tcb_at t s"
  and     m_cte': "cte_wp_at' ((=) cte) sl' s'"
  and     m_null: "cteCap cte = capability.NullCap"
  and       m_sl: "sl' = cte_map (t, tcb_cnode_index 2)"
  shows           "noReplyCapsFor t s'" proof - from tcb have m_cte: "cte_at (t, tcb_cnode_index 2) s" by (clarsimp elim!: tcb_at_cte_at) have m_cte_null:
    "cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s" using pspace invs apply (frule_tac pspace_relation_cte_wp_atI') apply (rule assms) apply clarsimp apply (clarsimp simp: m_sl) apply (frule cte_map_inj_eq) apply (rule m_cte) apply (erule cte_wp_cte_at) apply clarsimp+ apply (clarsimp elim!: cte_wp_at_weakenE simp: m_null) done have no_reply_caps:
    "\<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s" by (rule no_reply_caps_for_thread [OF invs tcb m_cte_null]) hence noReplyCaps:
    "\<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t m r) sl s'" apply (intro allI) apply (clarsimp simp: cte_wp_at_neg2 cte_wp_at_ctes_of simp del: split_paired_All) apply (frule pspace_relation_cte_wp_atI [OF pspace _ invs_valid_objs [OF invs]]) apply (clarsimp simp: cte_wp_at_neg2 simp del: split_paired_All) apply (drule_tac x="(a, b)" in spec) apply (clarsimp simp: cte_wp_cte_at cte_wp_at_caps_of_state) apply (case_tac c, simp_all) apply fastforce done thus ?thesis by (simp add: noReplyCapsFor_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. noReplyCapsFor t s' proof (state)
goal (1 subgoal):
 1. noReplyCapsFor t s' proof (chain)
picking this:
tcb_at t s proof (prove)
using this:
tcb_at t s

goal (1 subgoal):
 1. cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s proof (state)
this:
cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. noReplyCapsFor t s' proof (prove)
goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
using this:
pspace_relation (kheap s) (ksPSpace s')
invs s

goal (1 subgoal):
 1. cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s\<rbrakk> \<Longrightarrow> cte_wp_at' ((=) ?cte2) ?x2 s'
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap ?cte2) \<and> ?x2 = cte_map slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> sl' = cte_map slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> sl' = cte_map slot\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (6 subgoals):
 1. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) (?s11 c a b)
 2. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) (?s11 c a b)
 3. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> valid_objs (?s11 c a b)
 4. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_aligned (?s11 c a b)
 5. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_distinct (?s11 c a b)
 6. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b); (t, tcb_cnode_index 2) = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (5 subgoals):
 1. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s
 2. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_aligned s
 4. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_distinct s
 5. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b); (t, tcb_cnode_index 2) = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (4 subgoals):
 1. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_aligned s
 3. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b)\<rbrakk> \<Longrightarrow> pspace_distinct s
 4. \<And>c a b. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (a, b) s; cap_relation c (cteCap cte); cte_map (t, tcb_cnode_index 2) = cte_map (a, b); (t, tcb_cnode_index 2) = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>pspace_relation (kheap s) (ksPSpace s'); invs s; cte_wp_at ((=) c) (t, tcb_cnode_index 2) s; cap_relation c (cteCap cte)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals! proof (state)
this:
cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. noReplyCapsFor t s' proof (prove)
goal (1 subgoal):
 1. \<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s proof (state)
this:
\<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s

goal (1 subgoal):
 1. noReplyCapsFor t s' proof (prove)
using this:
\<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s

goal (1 subgoal):
 1. \<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) sl s' proof (prove)
goal (1 subgoal):
 1. \<And>sl m r. \<forall>sl m r. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m r) sl s \<Longrightarrow> \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) sl s' proof (prove)
goal (1 subgoal):
 1. \<And>sl m r cte. \<lbrakk>\<forall>sl. cte_wp_at (\<lambda>_. True) sl s \<longrightarrow> (\<forall>m r. cte_wp_at (\<lambda>cap. cap \<noteq> cap.ReplyCap t m r) sl s); ctes_of s' sl = Some cte; cteCap cte = capability.ReplyCap t m r\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>sl m r cte. \<lbrakk>\<forall>sl. cte_wp_at (\<lambda>_. True) sl s \<longrightarrow> (\<forall>m r. cte_wp_at (\<lambda>cap. cap \<noteq> cap.ReplyCap t m r) sl s); ctes_of s' sl = Some cte; cteCap cte = capability.ReplyCap t m r; \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap cte) \<and> sl = cte_map slot\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>m r cte c a b. \<lbrakk>\<forall>sl. cte_wp_at (\<lambda>_. True) sl s \<longrightarrow> (\<forall>m r. cte_wp_at (\<lambda>cap. cap \<noteq> cap.ReplyCap t m r) sl s); ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; cte_wp_at ((=) c) (a, b) s; cap_relation c (capability.ReplyCap t m r)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>m r cte c a b. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; cte_wp_at ((=) c) (a, b) s; cap_relation c (capability.ReplyCap t m r); cte_wp_at (\<lambda>_. True) (a, b) s \<longrightarrow> (\<forall>m r. cte_wp_at (\<lambda>cap. cap \<noteq> cap.ReplyCap t m r) (a, b) s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>m r cte c a b. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m r; caps_of_state s (a, b) = Some c; cap_relation c (capability.ReplyCap t m r); \<forall>m r. c \<noteq> cap.ReplyCap t m r\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>m r cte c a b x53. \<lbrakk>ctes_of s' (cte_map (a, b)) = Some cte; cteCap cte = capability.ReplyCap t m (AllowGrant \<in> x53); caps_of_state s (a, b) = Some (cap.ReplyCap t m x53); r = (AllowGrant \<in> x53); \<forall>ma. m = (\<not> ma); c = cap.ReplyCap t m x53\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) sl s'

goal (1 subgoal):
 1. noReplyCapsFor t s' proof (prove)
using this:
\<forall>sl m r. \<not> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t m r) sl s'

goal (1 subgoal):
 1. noReplyCapsFor t s' proof (state)
this:
noReplyCapsFor t s'

goal:
No subgoals!