theory Syscall_R

lemma handleReply_sane:
  "\<lbrace>sch_act_sane\<rbrace> handleReply \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>" apply (simp add: handleReply_def getSlotCap_def getThreadCallerSlot_def locateSlot_conv) apply (rule hoare_pre) apply (wp haskell_assert_wp doReplyTransfer_sane getCTE_wp'| wpc)+ apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> handleReply \<lbrace>\<lambda>rv. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> do thread <- getCurThread;
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. sch_act_sane\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q2\<rbrace> do thread <- getCurThread;
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. sch_act_sane\<rbrace>
 2. \<And>s. sch_act_sane s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_sane s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot) s \<longrightarrow> (\<forall>x. cteCap cte = capability.ThreadCap x \<longrightarrow> sch_act_sane s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> sch_act_sane s) \<and> (\<forall>x xa xb xc. cteCap cte = capability.NotificationCap x xa xb xc \<longrightarrow> sch_act_sane s) \<and> (\<forall>x. cteCap cte = capability.IRQHandlerCap x \<longrightarrow> sch_act_sane s) \<and> (\<forall>x xa xb xc xd xe. cteCap cte = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> sch_act_sane s) \<and> (cteCap cte = capability.DomainCap \<longrightarrow> sch_act_sane s) \<and> (\<forall>x xa xb. cteCap cte = capability.Zombie x xa xb \<longrightarrow> sch_act_sane s) \<and> (\<forall>x. cteCap cte = capability.ArchObjectCap x \<longrightarrow> sch_act_sane s) \<and> (\<forall>x xa xb. cteCap cte = capability.ReplyCap x xa xb \<longrightarrow> (xa = True \<longrightarrow> sch_act_sane s) \<and> (xa = False \<longrightarrow> x \<noteq> ksCurThread s \<longrightarrow> sch_act_sane s \<and> x \<noteq> ksCurThread s)) \<and> (\<forall>x xa xb xc. cteCap cte = capability.UntypedCap x xa xb xc \<longrightarrow> sch_act_sane s) \<and> (\<forall>x xa xb xc. cteCap cte = capability.CNodeCap x xa xb xc \<longrightarrow> sch_act_sane s) \<and> (cteCap cte = capability.IRQControlCap \<longrightarrow> sch_act_sane s) proof (prove)
goal:
No subgoals!