theory Syscall_R

lemma pinv_tcb'[wp]:
  "\<lbrace>invs' and st_tcb_at' active' tptr
          and valid_invocation' i and ct_active'\<rbrace>
     RetypeDecls_H.performInvocation block call i
   \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>" apply (simp add: performInvocation_def) apply (case_tac i, simp_all) apply (wp invokeArch_tcb_at' | clarsimp simp: pred_tcb_at')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' active' tptr and valid_invocation' i and ct_active'\<rbrace> global.performInvocation block call i \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' active' tptr and valid_invocation' i and ct_active'\<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. tcb_at' tptr\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>x1. i = Invocations_H.invocation.InvokeUntyped x1 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and valid_untyped_inv' x1 and ct_active'\<rbrace> doE y <- invokeUntyped x1;
returnOk []
odE \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 2. \<And>x21 x22 x23 x24. i = Invocations_H.invocation.InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and (ep_at' x21 and ex_nonz_cap_to' x21) and ct_active'\<rbrace> liftE (do thread <- getCurThread;
y <- sendIPC block call x22 x23 x24 thread x21;
return []
od) \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 3. \<And>x31 x32. i = Invocations_H.invocation.InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and (ntfn_at' x31 and ex_nonz_cap_to' x31) and ct_active'\<rbrace> doE y <- liftE (sendSignal x31 x32);
returnOk []
odE \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 4. \<And>x41 x42 x43. i = Invocations_H.invocation.InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and (tcb_at' x41 and cte_wp_at' (\<lambda>cte. \<exists>gr. cteCap cte = capability.ReplyCap x41 False gr) x42) and ct_active'\<rbrace> liftE (do sender <- getCurThread;
y <- doReplyTransfer sender x41 x42 x43;
return []
od) \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 5. \<And>x51 x52. i = Invocations_H.invocation.InvokeDomain x51 x52 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and (tcb_at' x51 and (\<lambda>y. x52 \<le> maxDomain)) and ct_active'\<rbrace> liftE (do y <- setDomain x51 x52;
return []
od) \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 6. \<And>x6. i = Invocations_H.invocation.InvokeTCB x6 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and tcb_inv_wf' x6 and ct_active'\<rbrace> invokeTCB x6 \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 7. \<And>x7. i = Invocations_H.invocation.InvokeCNode x7 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and valid_cnode_inv' x7 and ct_active'\<rbrace> doE y <- invokeCNode x7;
returnOk []
odE \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 8. \<And>x8. i = Invocations_H.invocation.InvokeIRQControl x8 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and irq_control_inv_valid' x8 and ct_active'\<rbrace> doE y <- global.performIRQControl x8;
returnOk []
odE \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 9. \<And>x9. i = Invocations_H.invocation.InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and irq_handler_inv_valid' x9 and ct_active'\<rbrace> doE y <- liftE (InterruptDecls_H.invokeIRQHandler x9);
returnOk []
odE \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace>
 10. \<And>x10. i = Invocations_H.invocation.InvokeArchObject x10 \<Longrightarrow> \<lbrace>invs' and st_tcb_at' active' tptr and valid_arch_inv' x10 and ct_active'\<rbrace> Arch.performInvocation x10 \<lbrace>\<lambda>rv. tcb_at' tptr\<rbrace> proof (prove)
goal:
No subgoals!