theory Access_AC

lemma reply_cap_no_children:
  "\<lbrakk> valid_mdb s; caps_of_state s p = Some (ReplyCap t False r) \<rbrakk> \<Longrightarrow> cdt s p' \<noteq> Some p" apply (clarsimp simp: valid_mdb_def) apply (frule descendants_incD[where p=p' and p'=p]) apply (rule child_descendant) apply (fastforce) apply clarsimp apply (subgoal_tac "caps_of_state s p' \<noteq> None") apply (clarsimp simp: cap_class_reply) apply (simp only: reply_mdb_def reply_caps_mdb_def reply_masters_mdb_def) apply (elim conjE allE[where x=p']) apply simp apply (drule(1) mdb_cte_atD) apply (fastforce simp add: cte_wp_at_def caps_of_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; caps_of_state s p = Some (ReplyCap t False r)\<rbrakk> \<Longrightarrow> cdt s p' \<noteq> Some p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p\<rbrakk> \<Longrightarrow> p' \<in> descendants_of p (cdt s)
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = cap_class (the (caps_of_state s p)) \<and> cap_range (the (caps_of_state s p')) \<subseteq> cap_range (the (caps_of_state s p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p\<rbrakk> \<Longrightarrow> cdt s p' = Some p
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = cap_class (the (caps_of_state s p)) \<and> cap_range (the (caps_of_state s p')) \<subseteq> cap_range (the (caps_of_state s p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = cap_class (the (caps_of_state s p)) \<and> cap_range (the (caps_of_state s p')) \<subseteq> cap_range (the (caps_of_state s p))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r); caps_of_state s p' \<noteq> None\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>ra m. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_range (ReplyCap t m ra) \<subseteq> cap_range (ReplyCap t False r); caps_of_state s p' = Some (ReplyCap t m ra)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>ra m. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); (\<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. cdt s ptr = Some ptr' \<and> caps_of_state s ptr' = Some (ReplyCap t True rights'))) \<and> (\<forall>ptr t rights. caps_of_state s ptr = Some (ReplyCap t True rights) \<longrightarrow> cdt s ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_range (ReplyCap t m ra) \<subseteq> cap_range (ReplyCap t False r); caps_of_state s p' = Some (ReplyCap t m ra)\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal (2 subgoals):
 1. \<And>ra m. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_range (ReplyCap t m ra) \<subseteq> cap_range (ReplyCap t False r); caps_of_state s p' = Some (ReplyCap t m ra); \<forall>t rights. caps_of_state s p' = Some (ReplyCap t False rights) \<longrightarrow> (\<exists>ptr' rights'. cdt s p' = Some ptr' \<and> caps_of_state s ptr' = Some (ReplyCap t True rights')); \<forall>t rights. caps_of_state s p' = Some (ReplyCap t True rights) \<longrightarrow> cdt s p' = None \<and> (\<forall>ptr'\<in>descendants_of p' (cdt s). \<exists>rights'. caps_of_state s ptr' = Some (ReplyCap t False rights'))\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cdt s p' = Some p; cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r)\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ReplyCap t False r); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); cap_class (the (caps_of_state s p')) = ReplyClass t; cap_range (the (caps_of_state s p')) \<subseteq> cap_range (ReplyCap t False r); swp (cte_wp_at ((\<noteq>) NullCap)) s p \<and> swp (cte_wp_at ((\<noteq>) NullCap)) s p'\<rbrakk> \<Longrightarrow> caps_of_state s p' \<noteq> None proof (prove)
goal:
No subgoals!