theory CNodeInv_R

lemma inv_cnode_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> invokeCNode cnode_inv
  -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: invokeCNode_def) apply (rule hoare_pre) apply (wp cteRevoke_IRQInactive finaliseSlot_IRQInactive
             cteDelete_IRQInactive
             whenE_wp
           | wpc
           | simp add:  split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> invokeCNode cnode_inv -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> case cnode_inv of Insert cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteInsert cap srcSlot destSlot | Rotate cap1 cap2 slot1 slot2 slot3 \<Rightarrow> withoutPreemption $ if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od | Revoke destSlot \<Rightarrow> cteRevoke destSlot | Move cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteMove cap srcSlot destSlot | CancelBadgedSends (capability.EndpointCap ptr b xa xaa xb xc) \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | CancelBadgedSends _ \<Rightarrow> haskell_fail [] | SaveCaller destSlot \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od | Delete destSlot \<Rightarrow> cteDelete destSlot True -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case cnode_inv of Insert cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteInsert cap srcSlot destSlot | Rotate cap1 cap2 slot1 slot2 slot3 \<Rightarrow> withoutPreemption $ if slot1 = slot3 then cteSwap cap1 slot1 cap2 slot2 else do cteMove cap2 slot2 slot3;
cteMove cap1 slot1 slot2
od | Revoke destSlot \<Rightarrow> cteRevoke destSlot | Move cap srcSlot destSlot \<Rightarrow> withoutPreemption $ cteMove cap srcSlot destSlot | CancelBadgedSends (capability.EndpointCap ptr b xa xaa xb xc) \<Rightarrow> withoutPreemption $ unless (b = 0) $ cancelBadgedSends ptr b | CancelBadgedSends _ \<Rightarrow> haskell_fail [] | SaveCaller destSlot \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od | Delete destSlot \<Rightarrow> cteDelete destSlot True -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!