theory Syscall_R

lemma performInv_invs'[wp]:
  "\<lbrace>invs' and sch_act_simple
          and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))
          and ct_active' and valid_invocation' i\<rbrace>
     RetypeDecls_H.performInvocation block call i \<lbrace>\<lambda>rv. invs'\<rbrace>" unfolding performInvocation_def apply (cases i) apply ((clarsimp simp: simple_sane_strg sch_act_simple_def
                         ct_not_ksQ sch_act_sane_def
                  | wp tcbinv_invs' arch_performInvocation_invs'
                       setDomain_invs'
                  | rule conjI | erule active_ex_cap')+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> global.performInvocation block call i \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. i = Invocations_H.invocation.InvokeUntyped x1 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 2. \<And>x21 x22 x23 x24. i = Invocations_H.invocation.InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 3. \<And>x31 x32. i = Invocations_H.invocation.InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 4. \<And>x41 x42 x43. i = Invocations_H.invocation.InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 5. \<And>x51 x52. i = Invocations_H.invocation.InvokeDomain x51 x52 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 6. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 7. \<And>x7. i = Invocations_H.invocation.InvokeCNode x7 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 8. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 9. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace>
 10. \<And>x10. i = Invocations_H.invocation.InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' i\<rbrace> case i 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 block 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. invs'\<rbrace> proof (prove)
goal:
No subgoals!