theory CNodeInv_AI

lemma cap_swap_ex_cte_cap[wp]:
  "\<lbrace>ex_cte_cap_wp_to P p
          and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c
                             \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a
          and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c'
                             \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b\<rbrace>
     cap_swap c a c' b
   \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" apply (simp add: cap_swap_def ex_cte_cap_wp_to_def
                   cte_wp_at_caps_of_state
              del: split_paired_Ex) apply (wp get_cap_wp | simp split del: if_split del: split_paired_Ex)+ apply (simp del: split_paired_Ex | intro allI impI | erule conjE)+ apply (erule exfEI [where f="id ( a := b, b := a )"]) apply (clarsimp simp: cte_wp_at_caps_of_state | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c' \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a and cte_wp_at (\<lambda>x. cte_refs x = cte_refs c' \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) \<and> cte_wp_at (\<lambda>x. cte_refs x = cte_refs c \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a s \<and> cte_wp_at (\<lambda>x. cte_refs x = cte_refs c' \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b s \<Longrightarrow> \<exists>cref cap. (if cref = b then Some c else if cref = a then Some c' else caps_of_state s cref) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s); cte_wp_at (\<lambda>x. cte_refs x = cte_refs c \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a s; cte_wp_at (\<lambda>x. cte_refs x = cte_refs c' \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b s\<rbrakk> \<Longrightarrow> \<exists>cref. (cref = a \<longrightarrow> (a = b \<longrightarrow> P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) \<and> (a \<noteq> b \<longrightarrow> P c' \<and> p \<in> cte_refs c' (interrupt_irq_node s))) \<and> (cref \<noteq> a \<longrightarrow> (cref = b \<longrightarrow> P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) \<and> (cref \<noteq> b \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref. \<lbrakk>cte_wp_at (\<lambda>x. cte_refs x = cte_refs c \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c)) a s; cte_wp_at (\<lambda>x. cte_refs x = cte_refs c' \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P c')) b s; \<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> ((id(a := b, b := a)) cref = a \<longrightarrow> (a = b \<longrightarrow> P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) \<and> (a \<noteq> b \<longrightarrow> P c' \<and> p \<in> cte_refs c' (interrupt_irq_node s))) \<and> ((id(a := b, b := a)) cref \<noteq> a \<longrightarrow> ((id(a := b, b := a)) cref = b \<longrightarrow> P c \<and> p \<in> cte_refs c (interrupt_irq_node s)) \<and> ((id(a := b, b := a)) cref \<noteq> b \<longrightarrow> (\<exists>cap. caps_of_state s ((id(a := b, b := a)) cref) = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal:
No subgoals!