theory CNodeInv_AI

lemma final_cap_at_unchanged:
  assumes x: "\<And>P p. \<lbrace>cte_wp_at (\<lambda>c. P (gen_obj_refs c)) p\<rbrace> f
                  \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. P (gen_obj_refs c)) p\<rbrace>"
  assumes y: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> f
                \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace>" proof - have final_cap_at_eq':
    "\<And>p s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s =
    (\<exists>cp. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cp) p s
              \<and> (obj_refs cp \<noteq> {} \<or> cap_irqs cp \<noteq> {} \<or> arch_gen_refs cp \<noteq> {})
       \<and> (\<forall>p'. (cte_at p' s \<and> p' \<noteq> p) \<longrightarrow>
                cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s))" apply (simp add: final_cap_at_eq cte_wp_at_def) apply (rule iffI) apply (clarsimp simp: gen_obj_refs_Int gen_obj_refs_empty gen_obj_refs_eq) apply (rule exI, rule conjI, rule refl) apply clarsimp apply (clarsimp simp: gen_obj_refs_Int gen_obj_refs_empty gen_obj_refs_eq) done show ?thesis apply (simp only: final_cap_at_eq' imp_conv_disj de_Morgan_conj) apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift x hoare_vcg_disj_lift
              valid_cte_at_neg_typ y) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> f \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> f \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s = (\<exists>cp. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cp) p s \<and> (obj_refs cp \<noteq> {} \<or> cap_irqs cp \<noteq> {} \<or> arch_gen_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)) proof (prove)
goal (1 subgoal):
 1. \<And>p s. (\<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) = (\<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))) proof (prove)
goal (2 subgoals):
 1. \<And>p s. \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {}))
 2. \<And>p s. \<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>a b s cp. \<lbrakk>fst (get_cap (a, b) s) = {(cp, s)}; obj_refs cp = {} \<longrightarrow> cap_irqs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}; \<forall>aa ba. (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)}) \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)} \<and> obj_refs cp \<inter> obj_refs cap = {} \<and> cap_irqs cp \<inter> cap_irqs cap = {} \<and> arch_gen_refs cp \<inter> arch_gen_refs cap = {})\<rbrakk> \<Longrightarrow> \<exists>cpa. obj_refs cp = obj_refs cpa \<and> cap_irqs cp = cap_irqs cpa \<and> arch_gen_refs cp = arch_gen_refs cpa \<and> (cap_irqs cpa = {} \<longrightarrow> obj_refs cpa = {} \<longrightarrow> arch_gen_refs cpa \<noteq> {}) \<and> (\<forall>aa ba. (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)}) \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)} \<and> obj_refs cpa \<inter> obj_refs cap = {} \<and> cap_irqs cpa \<inter> cap_irqs cap = {} \<and> arch_gen_refs cpa \<inter> arch_gen_refs cap = {}))
 2. \<And>p s. \<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (2 subgoals):
 1. \<And>a b s cp. \<lbrakk>fst (get_cap (a, b) s) = {(cp, s)}; obj_refs cp = {} \<longrightarrow> cap_irqs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}; \<forall>aa ba. (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)}) \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)} \<and> obj_refs cp \<inter> obj_refs cap = {} \<and> cap_irqs cp \<inter> cap_irqs cap = {} \<and> arch_gen_refs cp \<inter> arch_gen_refs cap = {})\<rbrakk> \<Longrightarrow> cap_irqs cp = cap_irqs cp \<and> arch_gen_refs cp = arch_gen_refs cp \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>aa ba. (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)}) \<and> (aa = a \<longrightarrow> ba \<noteq> b) \<longrightarrow> (\<exists>cap. fst (get_cap (aa, ba) s) = {(cap, s)} \<and> obj_refs cp \<inter> obj_refs cap = {} \<and> cap_irqs cp \<inter> cap_irqs cap = {} \<and> arch_gen_refs cp \<inter> arch_gen_refs cap = {}))
 2. \<And>p s. \<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal (1 subgoal):
 1. \<And>p s. \<exists>cp. (\<exists>cap. fst (get_cap p s) = {(cap, s)} \<and> gen_obj_refs cap = gen_obj_refs cp) \<and> (cap_irqs cp = {} \<longrightarrow> obj_refs cp = {} \<longrightarrow> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) \<Longrightarrow> \<exists>cp. fst (get_cap p s) = {(cp, s)} \<and> gen_obj_refs cp \<noteq> {} \<and> (\<forall>a b. (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)}) \<and> (a, b) \<noteq> p \<longrightarrow> (\<exists>cap. fst (get_cap (a, b) s) = {(cap, s)} \<and> gen_obj_refs cp \<inter> gen_obj_refs cap = {})) proof (prove)
goal:
No subgoals! proof (state)
this:
cte_wp_at (\<lambda>c. is_final_cap' c ?s) ?p ?s = (\<exists>cp. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cp) ?p ?s \<and> (obj_refs cp \<noteq> {} \<or> cap_irqs cp \<noteq> {} \<or> arch_gen_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))

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> f \<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. is_final_cap' c s) p s\<rbrace> f \<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. \<exists>cp. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cp) p s \<and> (obj_refs cp \<noteq> {} \<or> cap_irqs cp \<noteq> {} \<or> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>p'. (\<not> cte_wp_at (\<lambda>_. True) p' s \<or> \<not> p' \<noteq> p) \<or> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s)\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cp. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cp) p s \<and> (obj_refs cp \<noteq> {} \<or> cap_irqs cp \<noteq> {} \<or> arch_gen_refs cp \<noteq> {}) \<and> (\<forall>p'. (\<not> cte_wp_at (\<lambda>_. True) p' s \<or> \<not> p' \<noteq> p) \<or> cte_wp_at (\<lambda>c. gen_obj_refs cp \<inter> gen_obj_refs c = {}) p' s)\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace> f \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s\<rbrace>

goal:
No subgoals!