theory CNodeInv_R

lemma updateCap_noop_irq_handlers:
  "\<lbrace>valid_irq_handlers' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace>
     updateCap slot cap
   \<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 updateCap_ksInterruptState]) apply wp apply (simp, subst(asm) tree_cte_cteCap_eq[unfolded o_def]) apply (simp split: option.split_asm
                add: modify_map_apply fun_upd_idem) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers' and cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot\<rbrace> updateCap slot cap \<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>cte. cteCap cte = cap) slot\<rbrace> updateCap slot cap \<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> updateCap slot cap \<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' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> updateCap slot cap \<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' (\<lambda>cte. cteCap cte = cap) slot) 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' (\<lambda>cte. cteCap cte = cap) slot) s \<Longrightarrow> \<forall>cap\<in>ran (modify_map (cteCaps_of s) slot (K cap)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal 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> (case cteCaps_of s slot of None \<Rightarrow> False | Some a \<Rightarrow> a = cap) \<Longrightarrow> \<forall>cap\<in>ran (modify_map (cteCaps_of s) slot (\<lambda>y. cap)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!