theory CNodeInv_AI

lemma final_cap_same_objrefs:
  "\<lbrace>is_final_cap' cap and
    cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c \<noteq> {}
                     \<or> cap_irqs cap \<inter> cap_irqs c \<noteq> {}
                     \<or> arch_gen_refs cap \<inter>
                            arch_gen_refs c \<noteq> {}) ptr\<rbrace>
     set_cap cap ptr \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>" apply (simp only: is_final_cap'_def3 pred_conj_def
                    cte_wp_at_caps_of_state) apply wp apply (clarsimp simp del: split_paired_Ex split_paired_All) apply (rule_tac x=ptr in exI) apply (subgoal_tac "(a, b) = ptr") apply clarsimp apply (erule_tac x="ptr" in allE) apply (fastforce simp: gen_obj_refs_Int) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap and cte_wp_at (\<lambda>c. obj_refs cap \<inter> obj_refs c \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs c \<noteq> {} \<or> arch_gen_refs cap \<inter> arch_gen_refs c \<noteq> {}) ptr\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. (\<exists>cref. (\<exists>capa. caps_of_state x cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state x cref' = Some cap \<and> True) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state x cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<and> (\<exists>capa. caps_of_state x ptr = Some capa \<and> (obj_refs cap \<inter> obj_refs capa \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs capa \<noteq> {} \<or> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}))\<rbrace> set_cap cap ptr \<lbrace>\<lambda>rv s. \<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap \<and> True) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cref. (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap \<and> True) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<and> (\<exists>capa. caps_of_state s ptr = Some capa \<and> (obj_refs cap \<inter> obj_refs capa \<noteq> {} \<or> cap_irqs cap \<inter> cap_irqs capa \<noteq> {} \<or> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {})) \<Longrightarrow> \<exists>cref. (\<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (\<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) cref' = Some capa \<and> True) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. ((caps_of_state s)(ptr \<mapsto> cap)) cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa capaa. \<lbrakk>\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = ptr \<longrightarrow> gen_obj_refs cap \<noteq> {} \<and> (\<forall>cref'. cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<and> (cref \<noteq> ptr \<longrightarrow> (\<exists>capa. caps_of_state s cref = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (cref' = ptr \<longrightarrow> gen_obj_refs cap = {}) \<and> (cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> cref \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa capaa. \<lbrakk>\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}\<rbrakk> \<Longrightarrow> (ptr = ptr \<longrightarrow> gen_obj_refs cap \<noteq> {} \<and> (\<forall>cref'. cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<and> (ptr \<noteq> ptr \<longrightarrow> (\<exists>capa. caps_of_state s ptr = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (cref' = ptr \<longrightarrow> gen_obj_refs cap = {}) \<and> (cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> ptr \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})))) proof (prove)
goal (2 subgoals):
 1. \<And>s a b capa capaa. \<lbrakk>\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}; (a, b) = ptr\<rbrakk> \<Longrightarrow> (ptr = ptr \<longrightarrow> gen_obj_refs cap \<noteq> {} \<and> (\<forall>cref'. cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))) \<and> (ptr \<noteq> ptr \<longrightarrow> (\<exists>capa. caps_of_state s ptr = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa \<noteq> {}) \<and> (\<forall>cref'. (cref' = ptr \<longrightarrow> gen_obj_refs cap = {}) \<and> (cref' \<noteq> ptr \<longrightarrow> (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> ptr \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}))))
 2. \<And>s a b capa capaa. \<lbrakk>\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}\<rbrakk> \<Longrightarrow> (a, b) = ptr proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa capaa. \<lbrakk>\<forall>cref'. (\<exists>cap. caps_of_state s cref' = Some cap) \<and> cref' \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s cref' = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {}); caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}\<rbrakk> \<Longrightarrow> (a, b) = ptr proof (prove)
goal (1 subgoal):
 1. \<And>s a b capa capaa. \<lbrakk>caps_of_state s ptr = Some capa; cap_irqs cap \<inter> cap_irqs capa = {} \<longrightarrow> obj_refs cap \<inter> obj_refs capa = {} \<longrightarrow> arch_gen_refs cap \<inter> arch_gen_refs capa \<noteq> {}; caps_of_state s (a, b) = Some capaa; gen_obj_refs cap \<inter> gen_obj_refs capaa \<noteq> {}; (\<exists>cap. caps_of_state s ptr = Some cap) \<and> ptr \<noteq> (a, b) \<longrightarrow> (\<exists>capa. caps_of_state s ptr = Some capa \<and> gen_obj_refs cap \<inter> gen_obj_refs capa = {})\<rbrakk> \<Longrightarrow> (a, b) = ptr proof (prove)
goal:
No subgoals!