theory CSpace_AI

lemma safe_parent_is_parent:
  "\<lbrakk> safe_parent_for m p cap pcap; caps_of_state s p = Some pcap; valid_mdb s \<rbrakk>
  \<Longrightarrow> should_be_parent_of pcap (is_original_cap s p) cap f" apply (clarsimp simp: should_be_parent_of_def safe_parent_for_def valid_mdb_def) apply (erule disjE) apply clarsimp apply (erule (1) irq_revocableD) apply (erule disjE) apply clarsimp apply (drule (2) ut_revocableD) apply (clarsimp simp: is_cap_simps) apply (drule (2) safe_parent_arch_is_parent[where f=f]) apply (clarsimp simp: is_cap_simps should_be_parent_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for m p cap pcap; caps_of_state s p = Some pcap; valid_mdb s\<rbrakk> \<Longrightarrow> should_be_parent_of pcap (is_original_cap s p) cap f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; (\<exists>irq. cap = IRQHandlerCap irq) \<and> pcap = IRQControlCap \<or> is_untyped_cap pcap \<and> descendants_of p m = {} \<or> safe_parent_for_arch cap pcap; 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)\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); (\<exists>irq. cap = IRQHandlerCap irq) \<and> pcap = IRQControlCap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True)
 2. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap \<and> descendants_of p m = {} \<or> safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<And>irq. \<lbrakk>caps_of_state s p = Some IRQControlCap; 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); pcap = IRQControlCap; cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> is_original_cap s p
 2. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap \<and> descendants_of p m = {} \<or> safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap \<and> descendants_of p m = {} \<or> safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap \<and> descendants_of p m = {}\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True)
 2. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap; descendants_of p m = {}\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True)
 2. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); is_untyped_cap pcap; descendants_of p m = {}; is_original_cap s p\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True)
 2. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); safe_parent_for_arch cap pcap\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some pcap; cap_is_device cap = cap_is_device pcap; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); same_region_as pcap cap; 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); should_be_parent_of pcap (is_original_cap s p) cap f\<rbrakk> \<Longrightarrow> is_original_cap s p \<and> (case pcap of EndpointCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | NotificationCap ref badge R \<Rightarrow> badge \<noteq> 0 \<longrightarrow> cap_ep_badge cap = badge \<and> \<not> f | _ \<Rightarrow> True) proof (prove)
goal:
No subgoals!