theory Syscall_R

lemma hr_ct_active'[wp]:
  "\<lbrace>invs' and ct_active'\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active'\<rbrace>" apply (simp add: handleReply_def getSlotCap_def getCurThread_def
                   getThreadCallerSlot_def locateSlot_conv) apply (rule hoare_seq_ext) apply (rule_tac t=thread in ct_in_state'_decomp) apply ((wp hoare_drop_imps | wpc | simp)+)[1] apply (subst haskell_assert_def) apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active
        | wpc | simp)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def
                  dest: ctes_of_valid') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active'\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active'\<rbrace> do thread <- gets ksCurThread;
cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte 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 (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. ct_active'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?B2 thread\<rbrace> do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte 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 (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. ct_active'\<rbrace>
 2. \<lbrace>invs' and ct_active'\<rbrace> gets ksCurThread \<lbrace>?B2\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>\<lambda>s. thread = ksCurThread s\<rbrace> do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte 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 (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv s. thread = ksCurThread s\<rbrace>
 2. \<And>thread. \<lbrace>?Pre5 thread\<rbrace> do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte 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 (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. st_tcb_at' active' thread\<rbrace>
 3. \<lbrace>invs' and ct_active'\<rbrace> gets ksCurThread \<lbrace>\<lambda>thread s. ?Pre5 thread s \<and> thread = ksCurThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?Pre5 thread\<rbrace> do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte 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 (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. st_tcb_at' active' thread\<rbrace>
 2. \<lbrace>invs' and ct_active'\<rbrace> gets ksCurThread \<lbrace>\<lambda>thread s. ?Pre5 thread s \<and> thread = ksCurThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>?Pre163 thread thread\<rbrace> do cte <- getCTE (thread + 2 ^ cte_level_bits * tcbCallerSlot);
case cteCap cte of capability.NullCap \<Rightarrow> return () | capability.ReplyCap caller True canGrant \<Rightarrow> haskell_fail [] | capability.ReplyCap caller False canGrant \<Rightarrow> do assert (caller \<noteq> thread);
doReplyTransfer thread caller (thread + 2 ^ cte_level_bits * tcbCallerSlot) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. st_tcb_at' active' thread\<rbrace>
 2. \<lbrace>invs' and ct_active'\<rbrace> gets ksCurThread \<lbrace>\<lambda>thread s. ?Pre163 thread thread s \<and> thread = ksCurThread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<forall>x. \<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (cteCap cte = capability.ThreadCap x \<longrightarrow> st_tcb_at' active' (ksCurThread s) s))) \<and> (cte_wp_at' (\<lambda>_. True) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (cteCap cte = capability.NullCap \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.NotificationCap x xa xb xc) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x. cteCap cte = capability.IRQHandlerCap x) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x xa xb. cteCap cte = capability.Zombie x xa xb) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x. cteCap cte = capability.ArchObjectCap x) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> (xa \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> (\<not> xa \<longrightarrow> x \<noteq> ksCurThread s \<longrightarrow> st_tcb_at' active' (ksCurThread s) s \<and> tcb_at' x s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap x False xb) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s)) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> ((\<exists>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc) \<longrightarrow> st_tcb_at' active' (ksCurThread s) s) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> st_tcb_at' active' (ksCurThread s) s))) proof (prove)
goal:
No subgoals!