theory CNodeInv_AI

lemma cap_move_if_unsafe [wp]:
  "\<And>ptr' cap ptr.
    \<lbrace>cte_wp_at ((=) cap.NullCap) ptr'
          and cte_wp_at (weak_derived cap) ptr
          and K (ptr \<noteq> ptr')
          and if_unsafe_then_cap
          and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr'\<rbrace>
      cap_move cap ptr ptr'
    \<lbrace>\<lambda>rv. if_unsafe_then_cap :: 'state_ext state \<Rightarrow> bool\<rbrace>" subgoal for ptr' cap ptr apply (simp add: cap_move_def) apply (wp | simp)+ apply (rule hoare_post_imp, simp only: if_unsafe_then_cap_def) apply (simp only: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply wp+ apply (clarsimp simp: if_unsafe_then_cap_def
                        ex_cte_cap_wp_to_def cte_wp_at_caps_of_state
              simp del: split_paired_All split_paired_Ex
                   del: allI
             split del: if_split) apply (frule weak_derived_Null) apply (frule weak_derived_cte_refs') apply (frule cap_irqs_appropriateness [OF weak_derived_cap_irqs]) apply (frule weak_derived_appropriate) apply (erule allfEI[where f="id (ptr := ptr', ptr' := ptr)"]) apply (case_tac "cref = ptr'") apply (intro allI impI,
          rule_tac x="(id (ptr := ptr', ptr' := ptr)) (a, b)" in exI) apply fastforce apply (clarsimp split: if_split_asm split del: if_split del: exE
               simp del: split_paired_All split_paired_Ex) apply (erule exfEI[where f="id (ptr := ptr', ptr' := ptr)"]) apply (clarsimp split: if_split_asm) apply fastforce done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr' cap ptr. \<lbrace>cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr'\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and K (ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr'\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and (\<lambda>y. ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr'\<rbrace> do y <- set_cap cap ptr';
y <- set_cap NullCap ptr;
src_p <- gets (\<lambda>s. cdt s ptr);
dest_p <- gets (\<lambda>s. cdt s ptr');
cdt <- gets cdt;
y <- set_cdt (\<lambda>r. if (if r = ptr then None else if r = ptr' then cdt ptr else cdt r) = Some ptr then Some ptr' else if r = ptr then None else if r = ptr' then cdt ptr else cdt r);
y <- do_extended_op (cap_move_ext ptr ptr' src_p dest_p);
is_original <- gets is_original_cap;
y <- set_original ptr' (is_original ptr);
set_original ptr False
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B9 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>ya. if_unsafe_then_cap\<rbrace>
 2. \<lbrace>?Q8\<rbrace> set_cap cap ptr' \<lbrace>?B9\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and (\<lambda>y. ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr') s \<Longrightarrow> ?Q8 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B9 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>rv s. \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) cref s\<rbrace>
 2. \<lbrace>?Q8\<rbrace> set_cap cap ptr' \<lbrace>?B9\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and (\<lambda>y. ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr') s \<Longrightarrow> ?Q8 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B9 ()\<rbrace> set_cap NullCap ptr \<lbrace>\<lambda>rv s. \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s))\<rbrace>
 2. \<lbrace>?Q8\<rbrace> set_cap cap ptr' \<lbrace>?B9\<rbrace>
 3. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and (\<lambda>y. ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr') s \<Longrightarrow> ?Q8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at ((=) NullCap) ptr' and cte_wp_at (weak_derived cap) ptr and (\<lambda>y. ptr \<noteq> ptr') and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr') s \<Longrightarrow> \<forall>cref capa. ((caps_of_state s)(ptr' \<mapsto> cap, ptr \<mapsto> NullCap)) cref = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. ((caps_of_state s)(ptr' \<mapsto> cap, ptr \<mapsto> NullCap)) crefa = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)); caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<forall>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)); caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap)\<rbrakk> \<Longrightarrow> \<forall>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)); caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa\<rbrakk> \<Longrightarrow> \<forall>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)); caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa\<rbrakk> \<Longrightarrow> \<forall>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; \<forall>cref cap. caps_of_state s cref = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)); caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa\<rbrakk> \<Longrightarrow> \<forall>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> \<forall>capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b capaa cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s)); cref = ptr'\<rbrakk> \<Longrightarrow> \<forall>capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s))
 2. \<And>s capa a b capaa cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s)); cref \<noteq> ptr'\<rbrakk> \<Longrightarrow> \<forall>capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (2 subgoals):
 1. \<And>s capa a b capaa cref capb. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s)); cref = ptr'; (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capb; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<exists>capa. (if (id(ptr := ptr', ptr' := ptr)) (a, b) = ptr then Some NullCap else if (id(ptr := ptr', ptr' := ptr)) (a, b) = ptr' then Some cap else caps_of_state s ((id(ptr := ptr', ptr' := ptr)) (a, b))) = Some capa \<and> appropriate_cte_cap capb capa \<and> cref \<in> cte_refs capa (interrupt_irq_node s)
 2. \<And>s capa a b capaa cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s)); cref \<noteq> ptr'\<rbrakk> \<Longrightarrow> \<forall>capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa cref. \<lbrakk>caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap cap capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; \<forall>cap. caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref) = Some cap \<longrightarrow> cap \<noteq> NullCap \<longrightarrow> (\<exists>crefa capa. caps_of_state s crefa = Some capa \<and> appropriate_cte_cap cap capa \<and> (id(ptr := ptr', ptr' := ptr)) cref \<in> cte_refs capa (interrupt_irq_node s)); cref \<noteq> ptr'\<rbrakk> \<Longrightarrow> \<forall>capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<longrightarrow> capa \<noteq> NullCap \<longrightarrow> (\<exists>crefa capb. (if crefa = ptr then Some NullCap else if crefa = ptr' then Some cap else caps_of_state s crefa) = Some capb \<and> appropriate_cte_cap capa capb \<and> cref \<in> cte_refs capb (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa aa ba capb. \<lbrakk>(aa, ba) \<noteq> ptr'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap capa capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; (aa, ba) \<noteq> ptr; \<exists>cref cap. caps_of_state s cref = Some cap \<and> appropriate_cte_cap capb cap \<and> (aa, ba) \<in> cte_refs cap (interrupt_irq_node s); caps_of_state s (aa, ba) = Some capb; capb \<noteq> NullCap\<rbrakk> \<Longrightarrow> \<exists>cref capa. (if cref = ptr then Some NullCap else if cref = ptr' then Some cap else caps_of_state s cref) = Some capa \<and> appropriate_cte_cap capb capa \<and> (aa, ba) \<in> cte_refs capa (interrupt_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa aa ba capb cref. \<lbrakk>(aa, ba) \<noteq> ptr'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap capa capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; (aa, ba) \<noteq> ptr; caps_of_state s (aa, ba) = Some capb; capb \<noteq> NullCap; \<exists>cap. caps_of_state s cref = Some cap \<and> appropriate_cte_cap capb cap \<and> (aa, ba) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> \<exists>capa. (if (id(ptr := ptr', ptr' := ptr)) cref = ptr then Some NullCap else if (id(ptr := ptr', ptr' := ptr)) cref = ptr' then Some cap else caps_of_state s ((id(ptr := ptr', ptr' := ptr)) cref)) = Some capa \<and> appropriate_cte_cap capb capa \<and> (aa, ba) \<in> cte_refs capa (interrupt_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>s capa a b capaa aa ba capb ab bb capc. \<lbrakk>(aa, ba) \<noteq> ptr'; caps_of_state s ptr' = Some NullCap; ptr \<noteq> ptr'; caps_of_state s ptr = Some capa; weak_derived cap capa; caps_of_state s (a, b) = Some capaa; appropriate_cte_cap capa capaa; ptr' \<in> cte_refs capaa (interrupt_irq_node s); (cap = NullCap) = (capa = NullCap); cte_refs cap = cte_refs capa; \<forall>cp. appropriate_cte_cap cp cap = appropriate_cte_cap cp capa; appropriate_cte_cap cap = appropriate_cte_cap capa; (aa, ba) \<noteq> ptr; caps_of_state s (aa, ba) = Some capb; capb \<noteq> NullCap; caps_of_state s (ab, bb) = Some capc; appropriate_cte_cap capb capc; (aa, ba) \<in> cte_refs capc (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> ((ab, bb) = ptr \<longrightarrow> appropriate_cte_cap capb capa \<and> (aa, ba) \<in> cte_refs capa (interrupt_irq_node s)) \<and> ((ab, bb) \<noteq> ptr \<longrightarrow> (ab, bb) \<noteq> ptr') proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!