theory CNodeInv_R

lemma cteMove_irq_handlers' [wp]:
  "\<lbrace>\<lambda>s. valid_irq_handlers' s
      \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s
      \<and> cte_wp_at' (\<lambda>c. cteCap c = NullCap) dest s\<rbrace>
     cteMove cap src dest
   \<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 cteMove_ksInterrupt]) apply (simp add: cteMove_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of ran_def) apply (subst(asm) imp_ex, subst(asm) all_comm) apply (drule_tac x="(id (src := dest, dest := src)) a" in spec) apply (clarsimp simp: modify_map_def split: if_split_asm) apply (auto simp: cteCaps_of_def weak_derived'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_handlers' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> cteMove cap src dest \<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' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s\<rbrace> cteMove cap src dest \<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> cteMove cap src dest \<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. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> cteMove cap src dest \<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. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?P11 (ksInterruptState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> do oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
cte <- getCTE src;
y <- updateCap dest cap;
y <- updateCap src capability.NullCap;
y <- updateMDB dest (const (cteMDBNode cte));
y <- updateMDB src (const nullMDBNode);
y <- updateMDB (mdbPrev (cteMDBNode cte)) (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode cte)) (mdbPrev_update (\<lambda>_. dest))
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. (\<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal) \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> ?P11 (ksInterruptState s) s proof (prove)
goal (1 subgoal):
 1. \<And>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' (\<lambda>c. weak_derived' (cteCap c) cap) src s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) dest s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) dest s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) dest s \<and> (cteCap cte = capability.NullCap \<longrightarrow> mdbPrev (cteMDBNode cte) = nullPointer \<and> mdbNext (cteMDBNode cte) = nullPointer \<longrightarrow> cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (\<forall>cap\<in>ran (modify_map (modify_map (cteCaps_of s) dest (K cap)) src (K capability.NullCap)). \<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. cteCaps_of s a = Some cap) \<longrightarrow> (\<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s src = Some cte; weak_derived' (cteCap cte) cap; cteCap ctea = capability.NullCap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; modify_map (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) a = Some (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a irq. \<lbrakk>\<forall>y x. cteCaps_of s y = Some x \<longrightarrow> (\<forall>irq. x = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); ctes_of s src = Some cte; weak_derived' (cteCap cte) cap; cteCap ctea = capability.NullCap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; modify_map (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) a = Some (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea a irq. \<lbrakk>ctes_of s src = Some cte; weak_derived' (cteCap cte) cap; cteCap ctea = capability.NullCap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; modify_map (modify_map (cteCaps_of s) dest (\<lambda>y. cap)) src (\<lambda>a. capability.NullCap) a = Some (capability.IRQHandlerCap irq); \<forall>x. cteCaps_of s ((id(src := dest, dest := src)) a) = Some x \<longrightarrow> (\<forall>irq. x = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea irq z. \<lbrakk>ctes_of s src = Some cte; weak_derived' (cteCap cte) (capability.IRQHandlerCap irq); cteCap ctea = capability.NullCap; ctes_of s dest = Some ctea; mdbPrev (cteMDBNode ctea) = nullPointer; mdbNext (cteMDBNode ctea) = nullPointer; dest \<noteq> src; \<forall>x. cteCaps_of s src = Some x \<longrightarrow> (\<forall>irq. x = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal); cap = capability.IRQHandlerCap irq; cteCaps_of s dest = Some z\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!