theory Syscall_R

lemma retype_pi_IRQInactive:
  "\<lbrace>valid_irq_states'\<rbrace> RetypeDecls_H.performInvocation blocking call v
   -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace>" apply (simp add: Retype_H.performInvocation_def) apply (rule hoare_pre) apply (wpc |
          wp inv_tcb_IRQInactive inv_cnode_IRQInactive inv_irq_IRQInactive
             inv_untyped_IRQInactive inv_arch_IRQInactive |
          simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> global.performInvocation blocking call v -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> case v of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC blocking call badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok -, \<lbrace>\<lambda>rv s. intStateIRQTable (ksInterruptState s) rv \<noteq> irqstate.IRQInactive\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> case v of Invocations_H.invocation.InvokeUntyped invok \<Rightarrow> doE invokeUntyped invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeEndpoint ep badge canGrant canGrantReply \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
sendIPC blocking call badge canGrant canGrantReply thread ep;
return $ []
od | Invocations_H.invocation.InvokeNotification ep badge \<Rightarrow> doE withoutPreemption $ sendSignal ep badge;
returnOk $ []
odE | Invocations_H.invocation.InvokeReply thread slot canGrant \<Rightarrow> withoutPreemption $ do sender <- getCurThread;
doReplyTransfer sender thread slot canGrant;
return $ []
od | Invocations_H.invocation.InvokeDomain thread domain \<Rightarrow> withoutPreemption $ do setDomain thread domain;
return $ []
od | Invocations_H.invocation.InvokeTCB invok \<Rightarrow> invokeTCB invok | Invocations_H.invocation.InvokeCNode invok \<Rightarrow> doE invokeCNode invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQControl invok \<Rightarrow> doE global.performIRQControl invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeIRQHandler invok \<Rightarrow> doE withoutPreemption $ InterruptDecls_H.invokeIRQHandler invok;
returnOk $ []
odE | Invocations_H.invocation.InvokeArchObject invok \<Rightarrow> Arch.performInvocation invok -, \<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!