theory CNodeInv_R

lemma cteSwap_valid_irq_handlers[wp]:
  "\<lbrace>valid_irq_handlers' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1
           and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace>
     cteSwap c c1 c' c2
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: valid_irq_handlers'_def irq_issued'_def) apply (rule hoare_pre) apply (rule hoare_use_eq [where f=ksInterruptState, OF cteSwap_ksInterrupt]) apply (simp add: cteSwap_def) apply wp apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def ran_def) apply (clarsimp simp add: modify_map_def split: if_split_asm) apply (auto simp add: weak_derived'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers' and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2) s \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> cteSwap c c1 c' c2 \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable f irq = irqstate.IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2) s \<Longrightarrow> ?P11 (ksInterruptState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> do cte1 <- getCTE c1;
y <- updateCap c1 c';
y <- updateCap c2 c;
y <- updateMDB (mdbPrev (cteMDBNode cte1)) (mdbNext_update (\<lambda>_. c2));
y <- updateMDB (mdbNext (cteMDBNode cte1)) (mdbPrev_update (\<lambda>_. c2));
cte2 <- getCTE c2;
y <- updateMDB c1 (const (cteMDBNode cte2));
y <- updateMDB c2 (const (cteMDBNode cte1));
y <- updateMDB (mdbPrev (cteMDBNode cte2)) (mdbNext_update (\<lambda>_. c1));
updateMDB (mdbNext (cteMDBNode cte2)) (mdbPrev_update (\<lambda>_. c1))
od \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable f irq = irqstate.IRQSignal\<rbrace>
 2. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2) s \<Longrightarrow> ?P11 (ksInterruptState s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) and cte_wp_at' (weak_derived' c \<circ> cteCap) c1 and cte_wp_at' (weak_derived' c' \<circ> cteCap) c2) s \<Longrightarrow> \<forall>cap\<in>ran (modify_map (modify_map (cteCaps_of s) c1 (K c')) c2 (K c)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a irq. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s c1 = Some cte; weak_derived' c (cteCap cte); ctes_of s c2 = Some ctea; weak_derived' c' (cteCap ctea); modify_map (modify_map (map_option cteCap \<circ> ctes_of s) c1 (\<lambda>y. c')) c2 (\<lambda>a. c) a = Some (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal (4 subgoals):
 1. \<And>s ctea irq. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s c1 = Some ctea; weak_derived' (capability.IRQHandlerCap irq) (cteCap ctea); weak_derived' c' (cteCap ctea); c2 = c1; c = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal
 2. \<And>s cte ctea irq. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s c1 = Some cte; weak_derived' (capability.IRQHandlerCap irq) (cteCap cte); ctes_of s c2 = Some ctea; weak_derived' c' (cteCap ctea); c2 \<noteq> c1; c = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal
 3. \<And>s cte ctea irq. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s c1 = Some cte; weak_derived' c (cteCap cte); ctes_of s c2 = Some ctea; weak_derived' (capability.IRQHandlerCap irq) (cteCap ctea); c1 \<noteq> c2; c' = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal
 4. \<And>s cte ctea a irq z. \<lbrakk>\<forall>cap. (\<exists>a z. ctes_of s a = Some z \<and> cteCap z = cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s c1 = Some cte; weak_derived' c (cteCap cte); ctes_of s c2 = Some ctea; weak_derived' c' (cteCap ctea); a \<noteq> c2; a \<noteq> c1; ctes_of s a = Some z; cteCap z = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!