theory CNodeInv_AI

lemma duplicate_creation:
  "\<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p
     and cte_at p' and K (p \<noteq> p')\<rbrace>
     set_cap cap p'
  \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_post_imp [where Q="\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p
                                        and cte_wp_at ((=) cap) p'"]) apply (clarsimp simp: cte_wp_at_def) apply (case_tac "\<exists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa") apply (elim exE conjE) apply (frule (4) final_cap_duplicate_obj_ref) apply simp apply (case_tac "\<exists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa") apply (elim exE conjE) apply (frule (4) final_cap_duplicate_irq, simp) apply (case_tac "\<exists>x. x \<in> arch_gen_refs cap \<and> x \<in> arch_gen_refs capa") apply (elim exE conjE) apply (frule (4) final_cap_duplicate_arch_refs, simp) apply (simp add: is_final_cap'_def gen_obj_refs_eq gen_obj_refs_Int) apply (wp set_cap_cte_wp_at) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p' and K (p \<noteq> p')\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv s. cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>p \<noteq> p'; (cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p') s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<not> is_final_cap' cap s) p s
 2. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s\<rbrakk> \<Longrightarrow> False
 2. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<exists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa x. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; x \<in> obj_refs cap; x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa x. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; x \<in> obj_refs cap; x \<in> obj_refs capa; x \<notin> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa\<rbrakk> \<Longrightarrow> False
 2. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<exists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa x. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; x \<in> cap_irqs cap; x \<in> cap_irqs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa\<rbrakk> \<Longrightarrow> False
 2. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa; \<exists>x. x \<in> arch_gen_refs cap \<and> x \<in> arch_gen_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa; \<nexists>x. x \<in> arch_gen_refs cap \<and> x \<in> arch_gen_refs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s capa x. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa; x \<in> arch_gen_refs cap; x \<in> arch_gen_refs capa\<rbrakk> \<Longrightarrow> False
 2. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa; \<nexists>x. x \<in> arch_gen_refs cap \<and> x \<in> arch_gen_refs capa\<rbrakk> \<Longrightarrow> False
 3. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s capa. \<lbrakk>p \<noteq> p'; fst (get_cap p' s) = {(cap, s)}; fst (get_cap p s) = {(capa, s)}; gen_obj_refs capa = gen_obj_refs cap; is_final_cap' capa s; \<nexists>x. x \<in> obj_refs cap \<and> x \<in> obj_refs capa; \<nexists>x. x \<in> cap_irqs cap \<and> x \<in> cap_irqs capa; \<nexists>x. x \<in> arch_gen_refs cap \<and> x \<in> arch_gen_refs capa\<rbrakk> \<Longrightarrow> False
 2. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> p' \<Longrightarrow> \<lbrace>cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at ((=) cap) p'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> p'; (cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p and cte_wp_at (\<lambda>_. True) p') s\<rbrakk> \<Longrightarrow> ((\<lambda>s. if p = p' then gen_obj_refs cap = gen_obj_refs cap else cte_wp_at (\<lambda>c. gen_obj_refs c = gen_obj_refs cap) p s) and cte_wp_at (\<lambda>_. True) p') s \<and> ((\<lambda>s. if p' = p' then cap = cap else cte_wp_at ((=) cap) p' s) and cte_wp_at (\<lambda>_. True) p') s proof (prove)
goal:
No subgoals!