theory Untyped_R

lemma insertNewCap_valid_irq_handlers:
  "\<lbrace>valid_irq_handlers' and (\<lambda>s. \<forall>irq. cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace>
     insertNewCap parent slot cap
   \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: insertNewCap_def valid_irq_handlers'_def irq_issued'_def) apply (wp | wp (once) hoare_use_eq[where f=ksInterruptState, OF updateNewFreeIndex_ksInterrupt])+ apply (simp add: cteCaps_of_def) apply (wp | wp (once) hoare_use_eq[where f=ksInterruptState, OF setCTE_ksInterruptState]
               getCTE_wp)+ apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of ran_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers' and (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> irq_issued' irq s)\<rbrace> insertNewCap parent 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 (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<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 (5 subgoals):
 1. \<And>next oldCTE y. \<lbrace>?B11 next oldCTE y\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>ya s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace>
 2. \<And>next oldCTE. \<lbrace>?B10 next oldCTE\<rbrace> assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer) \<lbrace>?B11 next oldCTE\<rbrace>
 3. \<And>next. \<lbrace>?B9 next\<rbrace> getCTE slot \<lbrace>?B10 next\<rbrace>
 4. \<lbrace>?Q8\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?B9\<rbrace>
 5. \<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 (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)) s \<Longrightarrow> ?Q8 s proof (prove)
goal (5 subgoals):
 1. \<And>next oldCTE. \<lbrace>?B11 next oldCTE ()\<rbrace> setCTE slot (CTE cap (MDB next parent True True)) \<lbrace>\<lambda>ya s. \<forall>cap\<in>ran (\<lambda>a. map_option cteCap (ctes_of s a)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace>
 2. \<And>next oldCTE. \<lbrace>?B10 next oldCTE\<rbrace> assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer) \<lbrace>?B11 next oldCTE\<rbrace>
 3. \<And>next. \<lbrace>?B9 next\<rbrace> getCTE slot \<lbrace>?B10 next\<rbrace>
 4. \<lbrace>?Q8\<rbrace> liftM (mdbNext \<circ> cteMDBNode) (getCTE parent) \<lbrace>?B9\<rbrace>
 5. \<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 (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)) s \<Longrightarrow> ?Q8 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 (\<lambda>s. \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) parent s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) parent s \<and> ((\<lambda>next s. cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (cteCap cte = capability.NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer \<longrightarrow> (\<forall>cap\<in>ran (\<lambda>a. map_option cteCap (((ctes_of s)(slot \<mapsto> CTE cap (MDB next parent True True))) a)). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal)))) \<circ> (mdbNext \<circ> cteMDBNode)) cte s) 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); \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal; ctes_of s parent = Some cte; ctes_of s slot = Some ctea; cteCap ctea = capability.NullCap; mdbNext (cteMDBNode ctea) = nullPointer; mdbPrev (cteMDBNode ctea) = nullPointer; a = slot \<longrightarrow> cap = capability.IRQHandlerCap irq; a \<noteq> slot \<longrightarrow> (\<exists>z. ctes_of s a = Some z \<and> cteCap z = capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal proof (prove)
goal:
No subgoals!