kings-crown/FVELER_Isabelle huggingface dataset:
theory Ipc_R

lemma sts_valid_pspace_hangers:
  "\<lbrace>valid_pspace' and tcb_at' t and
   valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs'\<rbrace>"
  "\<lbrace>valid_pspace' and tcb_at' t and
   valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
  "\<lbrace>valid_pspace' and tcb_at' t and
   valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
  "\<lbrace>valid_pspace' and tcb_at' t and
   valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>"
  "\<lbrace>valid_pspace' and tcb_at' t and
   valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>" by (safe intro!: hoare_strengthen_post [OF sts'_valid_pspace'_inv])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_objs'\<rbrace> &&& \<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>) &&& \<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> &&& \<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. valid_mdb'\<rbrace> &&& \<lbrace>valid_pspace' and tcb_at' t and valid_tcb_state' st\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>
theory Ipc_R

lemma getThreadReplySlot_tcb_at'[wp]:
  "\<lbrace>tcb_at' t\<rbrace> getThreadReplySlot tcb \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" by (simp add: getThreadReplySlot_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> getThreadReplySlot tcb \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
theory Ipc_R

lemma setupCallerCap_tcb_at'[wp]:
  "\<lbrace>tcb_at' t\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. tcb_at' t\<rbrace>" by (simp add: setupCallerCap_def, wp hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> setupCallerCap sender receiver grant \<lbrace>\<lambda>_. tcb_at' t\<rbrace>
theory Ipc_R

lemma cteInsert_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
     cteInsert newCap srcSlot destSlot
   \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" by (wp sch_act_wf_lift tcb_in_cur_domain'_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>
theory Ipc_R

lemma setupCallerCap_sch_act [wp]:
  "\<lbrace>\<lambda>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
  setupCallerCap t r g \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: setupCallerCap_def getSlotCap_def getThreadCallerSlot_def
            getThreadReplySlot_def locateSlot_conv) apply (wp getCTE_wp' sts_sch_act' hoare_drop_imps hoare_vcg_all_lift) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> setupCallerCap t r g \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply t;
masterCTE <- getCTE (t + 2 ^ cte_level_bits * tcbReplySlot);
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = t);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
cte <- getCTE (r + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap t False g) (t + 2 ^ cte_level_bits * tcbReplySlot) (r + 2 ^ cte_level_bits * tcbCallerSlot)
od \<lbrace>\<lambda>_ s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_not t s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> \<forall>x xa. (\<not> runnable' Structures_H.thread_state.BlockedOnReply \<longrightarrow> sch_act_not t s) \<and> sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma possibleSwitchTo_weak_sch_act_wf[wp]:
  "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
      possibleSwitchTo t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: possibleSwitchTo_def setSchedulerAction_def threadGet_def curDomain_def
                   bitmap_fun_defs) apply (wp rescheduleRequired_weak_sch_act_wf
            weak_sch_act_wf_lift_linear[where f="tcbSchedEnqueue t"]
            getObject_tcb_wp hoare_weak_lift_imp
           | wpc)+ apply (clarsimp simp: obj_at'_def projectKOs weak_sch_act_wf_def ps_clear_def tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- liftM tcbDomain (getObject t);
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else modify (ksSchedulerAction_update (\<lambda>_. SwitchToThread t))
od \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. weak_sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> ((\<lambda>targetDom sa. (targetDom \<noteq> ksCurDomain s \<longrightarrow> weak_sch_act_wf (ksSchedulerAction sa) sa) \<and> (\<not> targetDom \<noteq> ksCurDomain s \<longrightarrow> (ksSchedulerAction sa \<noteq> ResumeCurrentThread \<longrightarrow> True) \<and> (\<not> ksSchedulerAction sa \<noteq> ResumeCurrentThread \<longrightarrow> weak_sch_act_wf (ksSchedulerAction (sa\<lparr>ksSchedulerAction := SwitchToThread t\<rparr>)) (sa\<lparr>ksSchedulerAction := SwitchToThread t\<rparr>)))) \<circ> tcbDomain) ta s) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setSchedulerAction_ct_in_domain:
 "\<lbrace>\<lambda>s. ct_idle_or_in_cur_domain' s
   \<and>  p \<noteq> ResumeCurrentThread \<rbrace> setSchedulerAction p
  \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" by (simp add:setSchedulerAction_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ct_idle_or_in_cur_domain' s \<and> p \<noteq> ResumeCurrentThread\<rbrace> setSchedulerAction p \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>
theory Ipc_R

lemma valid_sched_weak_strg:
  "valid_sched s \<longrightarrow> weak_valid_sched_action s" by (simp add: valid_sched_def valid_sched_action_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched s \<longrightarrow> weak_valid_sched_action s
theory Ipc_R

lemma valid_Running'[simp]:
  "valid_tcb_state' Running = \<top>" by (rule ext, simp add: valid_tcb_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb_state' Structures_H.thread_state.Running = (\<lambda>_. True)
theory Ipc_R

lemma possibleSwitchTo_sch_act[wp]:
  "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace>
     possibleSwitchTo t
   \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs) apply (wp hoare_weak_lift_imp threadSet_sch_act setQueue_sch_act threadGet_wp
       | simp add: unless_def | wpc)+ apply (auto simp: obj_at'_def projectKOs tcb_in_cur_domain'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> (tcbDomain tcb = ksCurDomain s \<longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> tcb_in_cur_domain' t s)) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma possibleSwitchTo_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace>
   possibleSwitchTo t
   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs) apply (wp hoare_drop_imps | wpc | simp)+ apply (auto simp: valid_tcb'_def weak_sch_act_wf_def
              dest: pred_tcb_at'
             elim!: valid_objs_valid_tcbE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<Longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma possibleSwitchTo_ksQ':
  "\<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and K(t' \<noteq> t)\<rbrace>
     possibleSwitchTo t
   \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs) apply (wp hoare_weak_lift_imp rescheduleRequired_ksQ' tcbSchedEnqueue_ksQ threadGet_wp
         | wpc
         | simp split del: if_split)+ apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and K (t' \<noteq> t)\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s) and (\<lambda>y. t' \<noteq> t)\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>_ s. t' \<notin> set (ksReadyQueues s p)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. t' \<notin> set (ksReadyQueues s p) \<and> sch_act_not t' s \<and> t' \<noteq> t \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma possibleSwitchTo_valid_queues'[wp]:
  "\<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)
                  and st_tcb_at' runnable' t\<rbrace>
   possibleSwitchTo t
   \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: possibleSwitchTo_def curDomain_def bitmap_fun_defs) apply (wp hoare_weak_lift_imp threadGet_wp | wpc | simp)+ apply (auto simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else setSchedulerAction (SwitchToThread t)
od \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' runnable' t s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>tcb. ko_at' tcb t s \<and> (tcbDomain tcb = ksCurDomain s \<longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> weak_sch_act_wf (ksSchedulerAction s) s)) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma sts_running_valid_queues:
  "runnable' st \<Longrightarrow> \<lbrace> Invariants_H.valid_queues \<rbrace> setThreadState st t \<lbrace>\<lambda>_. Invariants_H.valid_queues \<rbrace>" by (wp sts_valid_queues, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. runnable' st \<Longrightarrow> \<lbrace>Invariants_H.valid_queues\<rbrace> setThreadState st t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory Ipc_R

lemma ct_in_state_activatable_imp_simple'[simp]:
  "ct_in_state' activatable' s \<Longrightarrow> ct_in_state' simple' s" apply (simp add: ct_in_state'_def) apply (erule pred_tcb'_weakenE) apply (case_tac st; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state' activatable' s \<Longrightarrow> ct_in_state' simple' s proof (prove)
goal (1 subgoal):
 1. st_tcb_at' activatable' (ksCurThread s) s \<Longrightarrow> st_tcb_at' simple' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>st. activatable' st \<Longrightarrow> simple' st proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cancelIPC_nonz_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp add: cancelIPC_def getThreadReplySlot_def Let_def
                   capHasProperty_def) apply (wp threadSet_cap_to'
       | wpc
       | simp
       | clarsimp elim!: cte_wp_at_weakenE'
       | rule hoare_post_imp[where Q="\<lambda>rv. ex_nonz_cap_to' p"])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> do state <- getThreadState t;
case state of Structures_H.thread_state.BlockedOnReceive x xa \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | Structures_H.thread_state.BlockedOnReply \<Rightarrow> do y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
slot <- locateSlotTCB t tcbReplySlot;
callerCap <- liftM (mdbNext \<circ> cteMDBNode) (getCTE slot);
when (callerCap \<noteq> nullPointer) (do y <- stateAssert (cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<and> \<not> capReplyMaster (cteCap c)) callerCap) [];
cteDeleteOne callerCap
od)
od | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> cancelSignal t (waitingOnNotification state) | Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<Rightarrow> do ep <- getEndpoint (blockingObject state);
y <- assert (\<not> (case ep of Structures_H.endpoint.IdleEP \<Rightarrow> True | _ \<Rightarrow> False));
ep' <- case remove1 t (epQueue ep) of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ epQueue_update (\<lambda>_. remove1 t (epQueue ep)) ep;
y <- setEndpoint (blockingObject state) ep';
setThreadState Structures_H.thread_state.Inactive t
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma rfk_invs':
  "\<lbrace>invs' and tcb_at' t\<rbrace> replyFromKernel t r \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: replyFromKernel_def) apply (cases r) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> replyFromKernel t r \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> case r of (resultLabel, resultData) \<Rightarrow> do destIPCBuffer <- lookupIPCBuffer True t;
y <- asUser t (setRegister Notification_H.badgeRegister 0);
len <- setMRs t destIPCBuffer resultData;
setMessageInfo t (Types_H.message_info.MI len 0 0 resultLabel)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. r = (a, b) \<Longrightarrow> \<lbrace>invs' and tcb_at' t\<rbrace> case r of (resultLabel, resultData) \<Rightarrow> do destIPCBuffer <- lookupIPCBuffer True t;
y <- asUser t (setRegister Notification_H.badgeRegister 0);
len <- setMRs t destIPCBuffer resultData;
setMessageInfo t (Types_H.message_info.MI len 0 0 resultLabel)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma doNBRecvFailedTransfer_corres:
  "corres dc (tcb_at thread)
            (tcb_at' thread)
            (do_nbrecv_failed_transfer thread)
            (doNBRecvFailedTransfer thread)" unfolding do_nbrecv_failed_transfer_def doNBRecvFailedTransfer_def by (simp add: badgeRegister_def badge_register_def, rule asUser_setRegister_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at thread) (tcb_at' thread) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at thread) (tcb_at' thread) (do as_user thread $ setRegister badge_register 0;
return ()
od) (asUser thread $ setRegister Notification_H.badgeRegister 0)
theory Ipc_R

lemma tg_sp':
  "\<lbrace>P\<rbrace> threadGet f p \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f t' = t) p and P\<rbrace>" including no_pre apply (simp add: threadGet_def) apply wp apply (rule hoare_strengthen_post) apply (rule getObject_tcb_sp) apply clarsimp apply (erule obj_at'_weakenE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> threadGet f p \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f t' = t) p and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> threadGet f p \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f t' = t) p and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> liftM f (getObject p) \<lbrace>\<lambda>t. obj_at' (\<lambda>t'. f t' = t) p and P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getObject p \<lbrace>(\<lambda>t s. obj_at' (\<lambda>t'. f t' = t) p s \<and> P s) \<circ> f\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> getObject p \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> ((\<lambda>t s. obj_at' (\<lambda>t'. f t' = t) p s \<and> P s) \<circ> f) rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (P and ko_at' rv p) s \<Longrightarrow> ((\<lambda>t s. obj_at' (\<lambda>t'. f t' = t) p s \<and> P s) \<circ> f) rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>P s; ko_at' rv p s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>t'. f t' = f rv) p s proof (prove)
goal (1 subgoal):
 1. \<And>rv s k. \<lbrakk>P s; k = rv\<rbrakk> \<Longrightarrow> f k = f rv proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma gets_the_noop_corres:
  assumes P: "\<And>s. P s \<Longrightarrow> f s \<noteq> None"
  shows "corres dc P P' (gets_the f) (return x)" apply (clarsimp simp: corres_underlying_def gets_the_def
                        return_def gets_def bind_def get_def) apply (clarsimp simp: assert_opt_def return_def dest!: P) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc P P' (gets_the f) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> state_relation; P a; P' b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (assert_opt (f a) a). case x of (r, t) \<Rightarrow> (t, b) \<in> state_relation proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setupCallerCap_state_refs_of[wp]:
  "\<lbrace>\<lambda>s. P ((state_refs_of' s) (sender := {r \<in> state_refs_of' s sender. snd r = TCBBound}))\<rbrace>
     setupCallerCap sender rcvr grant
   \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (simp add: setupCallerCap_def getThreadCallerSlot_def
                   getThreadReplySlot_def) apply (wp hoare_drop_imps) apply (simp add: fun_upd_def cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(sender := {r \<in> state_refs_of' s sender. snd r = TCBBound}))\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((state_refs_of' s)(sender := {r \<in> state_refs_of' s sender. snd r = TCBBound}))\<rbrace> do y <- setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- locateSlotTCB sender tcbReplySlot;
masterCTE <- getCTE replySlot;
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = sender);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
callerSlot <- locateSlotTCB rcvr tcbCallerSlot;
callerCap <- getSlotCap callerSlot;
y <- assert (callerCap = capability.NullCap);
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((state_refs_of' s)(sender := {r \<in> state_refs_of' s sender. snd r = TCBBound})) \<Longrightarrow> P ((state_refs_of' s)(sender := tcb_st_refs_of' Structures_H.thread_state.BlockedOnReply \<union> {r \<in> state_refs_of' s sender. snd r = TCBBound})) proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma setCTE_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" by (wp valid_queues_lift setCTE_pred_tcb_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> setCTE ptr val \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>