theory Example_Valid_State

lemma valid_mdb_s0[simp]:
  "valid_mdb s0_internal" apply (simp add: valid_mdb_def reply_mdb_def) apply (intro conjI) apply (clarsimp simp: mdb_cte_at_def s0_internal_def) apply (force dest: s0_caps_of_state simp: untyped_mdb_def) apply (clarsimp simp: descendants_inc_def) apply (clarsimp simp: no_mloop_def s0_internal_def cdt_parent_defs) apply (clarsimp simp: untyped_inc_def) apply (drule s0_caps_of_state)+ apply ((simp | erule disjE)+)[1] apply (force dest: s0_caps_of_state simp: ut_revocable_def) apply (force dest: s0_caps_of_state simp: irq_revocable_def) apply (clarsimp simp: reply_master_revocable_def) apply (drule s0_caps_of_state) apply ((simp add: is_master_reply_cap_def s0_internal_def s0_ptr_defs | erule disjE)+)[1] apply (force dest: s0_caps_of_state simp: reply_caps_mdb_def) apply (clarsimp simp: reply_masters_mdb_def) apply (simp add: s0_internal_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_mdb s0_internal proof (prove)
goal (1 subgoal):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s0_internal) (cdt s0_internal) \<and> untyped_mdb (cdt s0_internal) (caps_of_state s0_internal) \<and> descendants_inc (cdt s0_internal) (caps_of_state s0_internal) \<and> no_mloop (cdt s0_internal) \<and> untyped_inc (cdt s0_internal) (caps_of_state s0_internal) \<and> ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal) \<and> irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal) \<and> reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal) \<and> reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal) \<and> reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (10 subgoals):
 1. mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s0_internal) (cdt s0_internal)
 2. untyped_mdb (cdt s0_internal) (caps_of_state s0_internal)
 3. descendants_inc (cdt s0_internal) (caps_of_state s0_internal)
 4. no_mloop (cdt s0_internal)
 5. untyped_inc (cdt s0_internal) (caps_of_state s0_internal)
 6. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 7. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 8. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 9. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 10. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (9 subgoals):
 1. untyped_mdb (cdt s0_internal) (caps_of_state s0_internal)
 2. descendants_inc (cdt s0_internal) (caps_of_state s0_internal)
 3. no_mloop (cdt s0_internal)
 4. untyped_inc (cdt s0_internal) (caps_of_state s0_internal)
 5. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 6. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 7. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 8. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 9. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (8 subgoals):
 1. descendants_inc (cdt s0_internal) (caps_of_state s0_internal)
 2. no_mloop (cdt s0_internal)
 3. untyped_inc (cdt s0_internal) (caps_of_state s0_internal)
 4. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 5. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 6. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 7. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 8. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (7 subgoals):
 1. no_mloop (cdt s0_internal)
 2. untyped_inc (cdt s0_internal) (caps_of_state s0_internal)
 3. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 4. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 5. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 6. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 7. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (6 subgoals):
 1. untyped_inc (cdt s0_internal) (caps_of_state s0_internal)
 2. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 3. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 4. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 5. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 6. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba c c'. \<lbrakk>caps_of_state s0_internal (a, b) = Some c; is_untyped_cap c; caps_of_state s0_internal (aa, ba) = Some c'; is_untyped_cap c'\<rbrakk> \<Longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> \<not> untyped_range c \<subset> untyped_range c' \<and> \<not> untyped_range c' \<subset> untyped_range c \<and> (untyped_range c = untyped_range c' \<longrightarrow> a = aa \<and> b = ba)
 2. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 3. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 4. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 5. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 6. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (6 subgoals):
 1. \<And>a b aa ba c c'. \<lbrakk>is_untyped_cap c; is_untyped_cap c'; c = NullCap \<or> ((a, b), c) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}; c' = NullCap \<or> ((aa, ba), c') \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> (untyped_range c \<subseteq> untyped_range c' \<or> untyped_range c' \<subseteq> untyped_range c \<or> untyped_range c \<inter> untyped_range c' = {}) \<and> \<not> untyped_range c \<subset> untyped_range c' \<and> \<not> untyped_range c' \<subset> untyped_range c \<and> (untyped_range c = untyped_range c' \<longrightarrow> a = aa \<and> b = ba)
 2. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 3. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 4. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 5. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 6. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (5 subgoals):
 1. ut_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 2. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 3. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 4. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 5. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (4 subgoals):
 1. irq_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 2. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 3. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 4. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. reply_master_revocable (is_original_cap s0_internal) (caps_of_state s0_internal)
 2. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 3. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>caps_of_state s0_internal (a, b) = Some cap; is_master_reply_cap cap\<rbrakk> \<Longrightarrow> is_original_cap s0_internal (a, b)
 2. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 3. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (3 subgoals):
 1. \<And>a b cap. \<lbrakk>is_master_reply_cap cap; cap = NullCap \<or> ((a, b), cap) \<in> {((Low_cnode_ptr, the_nat_to_bl 10 1), ThreadCap Low_tcb_ptr), ((Low_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((High_cnode_ptr, the_nat_to_bl 10 1), ThreadCap High_tcb_ptr), ((High_cnode_ptr, the_nat_to_bl 10 2), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_cnode_ptr, the_nat_to_bl 10 3), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowRecv}), ((Silc_cnode_ptr, the_nat_to_bl 10 2), CNodeCap Silc_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Silc_cnode_ptr, the_nat_to_bl 10 318), NotificationCap ntfn_ptr 0 {AllowSend}), ((Low_tcb_ptr, tcb_cnode_index 0), CNodeCap Low_cnode_ptr 10 (the_nat_to_bl 10 2)), ((Low_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap Low_pd_ptr (Some Low_asid))), ((Low_tcb_ptr, tcb_cnode_index 2), ReplyCap Low_tcb_ptr True {AllowGrant, AllowWrite}), ((Low_tcb_ptr, tcb_cnode_index 3), NullCap), ((Low_tcb_ptr, tcb_cnode_index 4), NullCap), ((High_tcb_ptr, tcb_cnode_index 0), CNodeCap High_cnode_ptr 10 (the_nat_to_bl 10 2)), ((High_tcb_ptr, tcb_cnode_index 1), ArchObjectCap (PageDirectoryCap High_pd_ptr (Some High_asid))), ((High_tcb_ptr, tcb_cnode_index 2), ReplyCap High_tcb_ptr True {AllowGrant, AllowWrite}), ((High_tcb_ptr, tcb_cnode_index 3), NullCap), ((High_tcb_ptr, tcb_cnode_index 4), NullCap)}\<rbrakk> \<Longrightarrow> is_original_cap s0_internal (a, b)
 2. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 3. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (2 subgoals):
 1. reply_caps_mdb (cdt s0_internal) (caps_of_state s0_internal)
 2. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (1 subgoal):
 1. reply_masters_mdb (cdt s0_internal) (caps_of_state s0_internal) proof (prove)
goal (1 subgoal):
 1. \<And>a b t rights. caps_of_state s0_internal (a, b) = Some (ReplyCap t True rights) \<Longrightarrow> cdt s0_internal (a, b) = None proof (prove)
goal:
No subgoals!