theory CNodeInv_R

lemma cteMove_ex:
  "\<lbrace>ex_cte_cap_to' ptr and
    cte_wp_at' (weak_derived' cap o cteCap) p and
    cte_wp_at' ((=) NullCap o cteCap) p' and
    K (p \<noteq> p') \<rbrace>
  cteMove cap p p'
  \<lbrace>\<lambda>_. ex_cte_cap_to' ptr\<rbrace>" unfolding ex_cte_cap_to'_def apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF cteMove_ksInterrupt]) apply (wp hoare_vcg_ex_lift cteMove_cte_wp_at) apply (clarsimp simp: cte_wp_at_ctes_of) apply (case_tac "cref = p") apply simp apply (rule_tac x=p' in exI) apply (clarsimp simp: weak_derived'_def dest!: capMaster_same_refs) apply (rule_tac x=cref in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True) ptr and cte_wp_at' (weak_derived' cap \<circ> cteCap) p and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) p' and K (p \<noteq> p')\<rbrace> cteMove cap p p' \<lbrace>\<lambda>_. ex_cte_cap_wp_to' (\<lambda>_. True) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (weak_derived' cap \<circ> cteCap) p and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) p' and K (p \<noteq> p')\<rbrace> cteMove cap p p' \<lbrace>\<lambda>_ s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteMove cap p p' \<lbrace>\<lambda>_ s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (weak_derived' cap \<circ> cteCap) p and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) p' and K (p \<noteq> p')) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> cteMove cap p p' \<lbrace>\<lambda>_ s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (weak_derived' cap \<circ> cteCap) p and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) p' and K (p \<noteq> p')) s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. True \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s) and cte_wp_at' (weak_derived' cap \<circ> cteCap) p and cte_wp_at' ((=) capability.NullCap \<circ> cteCap) p' and K (p \<noteq> p')) s \<Longrightarrow> \<exists>x. cte_wp_at' (\<lambda>_. True) x s \<and> (if p = x then True \<and> ptr \<in> cte_refs' capability.NullCap (irq_node' s) else if p' = x then True \<and> ptr \<in> cte_refs' cap (irq_node' s) else cte_wp_at' ((\<lambda>a. True \<and> ptr \<in> cte_refs' a (irq_node' s)) \<circ> cteCap) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref = p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s))))
 2. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctea = cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some cte; weak_derived' cap (cteCap cte); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref = p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s))))
 2. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctea = cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some cte; weak_derived' cap (cteCap cte); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref = p\<rbrakk> \<Longrightarrow> (p' = p' \<longrightarrow> p \<noteq> p' \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cte. ctes_of s p' = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> p' \<longrightarrow> p \<noteq> p' \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cte. ctes_of s p' = Some cte) \<and> (\<exists>cte. ctes_of s p' = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s))))
 2. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref \<noteq> p\<rbrakk> \<Longrightarrow> \<exists>x. (p' = x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> x \<longrightarrow> p \<noteq> x \<and> (p \<noteq> x \<longrightarrow> (\<exists>cte. ctes_of s x = Some cte) \<and> (\<exists>cte. ctes_of s x = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cte ctea cteb. \<lbrakk>ctes_of s cref = Some cte; ptr \<in> cte_refs' (cteCap cte) (irq_node' s); p \<noteq> p'; ctes_of s p = Some ctea; weak_derived' cap (cteCap ctea); ctes_of s p' = Some cteb; capability.NullCap = cteCap cteb; cref \<noteq> p\<rbrakk> \<Longrightarrow> (p' = cref \<longrightarrow> p \<noteq> cref \<and> (p \<noteq> cref \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte) \<and> ptr \<in> cte_refs' cap (irq_node' s))) \<and> (p' \<noteq> cref \<longrightarrow> p \<noteq> cref \<and> (p \<noteq> cref \<longrightarrow> (\<exists>cte. ctes_of s cref = Some cte) \<and> (\<exists>cte. ctes_of s cref = Some cte \<and> ptr \<in> cte_refs' (cteCap cte) (irq_node' s)))) proof (prove)
goal:
No subgoals!