theory Syscall_R

lemma handleReply_ct_not_ksQ:
  "\<lbrace>invs' and sch_act_simple
           and ct_in_state' simple'
           and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   handleReply
   \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: handleReply_def del: split_paired_All) apply (subst haskell_assert_def) apply (wp | wpc)+ apply (wp doReplyTransfer_ct_not_ksQ getThreadCallerSlot_inv)+ apply (rule_tac Q="\<lambda>cap.
                              (\<lambda>s. \<forall>p. ksCurThread s \<notin> set(ksReadyQueues s p))
                          and invs'
                          and sch_act_simple
                          and (\<lambda>s. thread = ksCurThread s)
                          and tcb_at' thread
                          and ct_in_state' simple'
                          and cte_wp_at' (\<lambda>c. cteCap c = cap) callerSlot"
             in hoare_post_imp) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def
                           cte_wp_at_ctes_of valid_cap'_def
                    dest!: ctes_of_valid') apply (wp getSlotCap_cte_wp_at getThreadCallerSlot_inv)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> handleReply \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do thread <- getCurThread;
callerSlot <- getThreadCallerSlot thread;
callerCap <- getSlotCap callerSlot;
case callerCap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap caller True canGrant \<Rightarrow> haskell_fail [] | capability.ReplyCap caller False canGrant \<Rightarrow> do haskell_assert (caller \<noteq> thread) [];
doReplyTransfer thread caller callerSlot canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> do thread <- getCurThread;
callerSlot <- getThreadCallerSlot thread;
getSlotCap callerSlot >>= case_capability (\<lambda>word. haskell_fail []) (return ()) (\<lambda>word1 word2 bool1 bool2. haskell_fail []) (\<lambda>word. haskell_fail []) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. haskell_fail []) (haskell_fail []) (\<lambda>word zombie_type nat. haskell_fail []) (\<lambda>arch_capability. haskell_fail []) (\<lambda>caller bool1 canGrant. case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> do assert (caller \<noteq> thread);
doReplyTransfer thread caller callerSlot canGrant
od) (\<lambda>bool word nat1 nat2. haskell_fail []) (\<lambda>word1 nat1 word2 nat2. haskell_fail []) (haskell_fail [])
od \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>thread callerSlot x x91 x92 x93 xa. \<lbrakk>x = capability.ReplyCap x91 x92 x93; x92 = False\<rbrakk> \<Longrightarrow> \<lbrace>?B105 thread callerSlot x x91 x92 x93 xa\<rbrace> doReplyTransfer thread x91 callerSlot x93 \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 2. \<And>thread callerSlot x x91 x92 x93. \<lbrakk>x = capability.ReplyCap x91 x92 x93; x92 = False\<rbrakk> \<Longrightarrow> \<lbrace>?R97 thread callerSlot x x91 x92 x93\<rbrace> assert (x91 \<noteq> thread) \<lbrace>?B105 thread callerSlot x x91 x92 x93\<rbrace>
 3. \<And>thread callerSlot x x101 x102 x103 x104. x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>?R28 thread callerSlot x x101 x102 x103 x104\<rbrace> haskell_fail [] \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 4. \<And>thread callerSlot x x111 x112 x113 x114. x = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>?R23 thread callerSlot x x111 x112 x113 x114\<rbrace> haskell_fail [] \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 5. \<And>thread callerSlot x. x = capability.IRQControlCap \<Longrightarrow> \<lbrace>?R18 thread callerSlot x\<rbrace> haskell_fail [] \<lbrace>\<lambda>rv s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>
 6. \<And>thread callerSlot. \<lbrace>?B2 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>x s. (\<forall>xa. x = capability.ThreadCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (x = capability.NullCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc xd. x = capability.NotificationCap xa xb xc xd \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa. x = capability.IRQHandlerCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc xd xe xf. x = capability.EndpointCap xa xb xc xd xe xf \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (x = capability.DomainCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc. x = capability.Zombie xa xb xc \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa. x = capability.ArchObjectCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc. x = capability.ReplyCap xa xb xc \<longrightarrow> (xb = True \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (xb = False \<longrightarrow> ?R97 thread callerSlot x xa xb xc s)) \<and> (\<forall>xa xb xc xd. x = capability.UntypedCap xa xb xc xd \<longrightarrow> ?R28 thread callerSlot x xa xb xc xd s) \<and> (\<forall>xa xb xc xd. x = capability.CNodeCap xa xb xc xd \<longrightarrow> ?R23 thread callerSlot x xa xb xc xd s) \<and> (x = capability.IRQControlCap \<longrightarrow> ?R18 thread callerSlot x s)\<rbrace>
 7. \<And>thread. \<lbrace>?B1 thread\<rbrace> getThreadCallerSlot thread \<lbrace>?B2 thread\<rbrace>
 8. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 9. \<And>s. (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread callerSlot. \<lbrace>?B2 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>x s. (\<forall>xa. x = capability.ThreadCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (x = capability.NullCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc xd. x = capability.NotificationCap xa xb xc xd \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa. x = capability.IRQHandlerCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc xd xe xf. x = capability.EndpointCap xa xb xc xd xe xf \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (x = capability.DomainCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc. x = capability.Zombie xa xb xc \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa. x = capability.ArchObjectCap xa \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc. x = capability.ReplyCap xa xb xc \<longrightarrow> (xb = True \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (xb = False \<longrightarrow> xa \<noteq> thread \<longrightarrow> (invs' and sch_act_simple and tcb_at' thread and tcb_at' xa and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> xa) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s)) \<and> (\<forall>xa xb xc xd. x = capability.UntypedCap xa xb xc xd \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>xa xb xc xd. x = capability.CNodeCap xa xb xc xd \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (x = capability.IRQControlCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))\<rbrace>
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> getThreadCallerSlot thread \<lbrace>?B2 thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread callerSlot rv s. ((\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and invs' and sch_act_simple and (\<lambda>s. thread = ksCurThread s) and tcb_at' thread and ct_in_state' simple' and cte_wp_at' (\<lambda>c. cteCap c = rv) callerSlot) s \<Longrightarrow> (\<forall>x. rv = capability.ThreadCap x \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (rv = capability.NullCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x. rv = capability.IRQHandlerCap x \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x xa xb xc xd xe. rv = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (rv = capability.DomainCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x xa xb. rv = capability.Zombie x xa xb \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x. rv = capability.ArchObjectCap x \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x xa xb. rv = capability.ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (xa = False \<longrightarrow> x \<noteq> thread \<longrightarrow> (invs' and sch_act_simple and tcb_at' thread and tcb_at' x and ct_in_state' simple' and (\<lambda>s. ksCurThread s \<noteq> x) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s)) \<and> (\<forall>x xa xb xc. rv = capability.UntypedCap x xa xb xc \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (\<forall>x xa xb xc. rv = capability.CNodeCap x xa xb xc \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) \<and> (rv = capability.IRQControlCap \<longrightarrow> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)))
 2. \<And>thread callerSlot. \<lbrace>?B2 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>cap. (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and invs' and sch_act_simple and (\<lambda>s. thread = ksCurThread s) and tcb_at' thread and ct_in_state' simple' and cte_wp_at' (\<lambda>c. cteCap c = cap) callerSlot\<rbrace>
 3. \<And>thread. \<lbrace>?B1 thread\<rbrace> getThreadCallerSlot thread \<lbrace>?B2 thread\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread callerSlot. \<lbrace>?B2 thread callerSlot\<rbrace> getSlotCap callerSlot \<lbrace>\<lambda>cap. (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and invs' and sch_act_simple and (\<lambda>s. thread = ksCurThread s) and tcb_at' thread and ct_in_state' simple' and cte_wp_at' (\<lambda>c. cteCap c = cap) callerSlot\<rbrace>
 2. \<And>thread. \<lbrace>?B1 thread\<rbrace> getThreadCallerSlot thread \<lbrace>?B2 thread\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and ct_in_state' simple' and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))) s \<Longrightarrow> ((\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and invs' and sch_act_simple and (\<lambda>sa. ksCurThread s = ksCurThread sa) and tcb_at' (ksCurThread s) and ct_in_state' simple') s \<and> True proof (prove)
goal:
No subgoals!