theory CNodeInv_AI

lemma final_cap_at_same_objrefs:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c.  obj_refs c \<noteq> {} \<and> is_final_cap' c s) p s
      \<and> cte_wp_at (\<lambda>c. gen_obj_refs cap = gen_obj_refs c) ptr s \<and> p \<noteq> ptr\<rbrace>
     set_cap cap ptr \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace>" apply (simp only: final_cap_at_eq cte_wp_at_conj) apply (simp add: cte_wp_at_caps_of_state) apply wp apply (clarsimp simp del: split_paired_All split_paired_Ex
                      simp: gen_obj_refs_Int gen_obj_refs_empty gen_obj_refs_eq) apply fastforce done

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