kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_R

lemma cancelAllIPC_valid_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
   cancelAllIPC ep_ptr
   \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" apply (simp add: cancelAllIPC_def ep'_Idle_case_helper) apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
            cancelAllIPC_mapM_x_valid_queues cancelAllIPC_mapM_x_valid_objs' cancelAllIPC_mapM_x_weak_sch_act
            set_ep_valid_objs' getEndpoint_wp) apply (clarsimp simp: valid_ep'_def) apply (drule (1) ko_at_valid_objs') apply (auto simp: valid_obj'_def valid_ep'_def valid_tcb'_def projectKOs
             split: endpoint.splits
              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. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> cancelAllIPC ep_ptr \<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. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> do ep <- getEndpoint ep_ptr;
if ep = Structures_H.endpoint.IdleEP then return () else do y <- setEndpoint ep_ptr Structures_H.endpoint.IdleEP;
y <- mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) (epQueue ep);
rescheduleRequired
od
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> (\<forall>ep. ko_at' ep ep_ptr s \<longrightarrow> ep = Structures_H.endpoint.IdleEP \<longrightarrow> Invariants_H.valid_queues s) \<and> (\<forall>ep. ko_at' ep ep_ptr s \<longrightarrow> ep \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ((Invariants_H.valid_queues s \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) s) \<and> (\<forall>x\<in>set (epQueue ep). tcb_at' x s)) \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) s \<and> weak_sch_act_wf (ksSchedulerAction s) s) proof (prove)
goal (1 subgoal):
 1. \<And>s ep x. \<lbrakk>Invariants_H.valid_queues s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; ko_at' ep ep_ptr s; ep \<noteq> Structures_H.endpoint.IdleEP; x \<in> set (epQueue ep)\<rbrakk> \<Longrightarrow> tcb_at' x s proof (prove)
goal (2 subgoals):
 1. \<And>s ep x ko. \<lbrakk>Invariants_H.valid_queues s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; ep \<noteq> Structures_H.endpoint.IdleEP; x \<in> set (epQueue ep); projectKO_opt ko = Some ep\<rbrakk> \<Longrightarrow> injectKOS ep = ko
 2. \<And>s ep x. \<lbrakk>Invariants_H.valid_queues s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; ep \<noteq> Structures_H.endpoint.IdleEP; x \<in> set (epQueue ep); valid_obj' (injectKOS ep) s\<rbrakk> \<Longrightarrow> tcb_at' x s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cancelAllSignals_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
     cancelAllSignals epptr
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: cancelAllSignals_def) apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift
          rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at'
          getNotification_wp
     | wpc
     | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cancelAllSignals epptr \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do ntfn <- getNotification epptr;
case ntfnObj ntfn of Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> do setNotification epptr (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn);
forM_x queue (\<lambda>t. do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od);
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindMaybeNotification_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>
     unbindMaybeNotification r
   \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> unbindMaybeNotification r \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do ntfn <- getNotification r;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some t \<Rightarrow> do y <- setNotification r (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None t
od
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_queues[wp]:
  "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
   cteDeleteOne sl
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") apply (simp add: cteDeleteOne_def unless_def split_def) apply (wp isFinalCapability_inv getCTE_wp | rule hoare_drop_imps | simp)+ apply (clarsimp simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> cteDeleteOne sl \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> do cte <- getCTE sl;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) sl \<and> snd p = capability.NullCap);
emptySlot sl capability.NullCap
od)
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) sl s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) sl s) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma emptySlot_valid_inQ_queues [wp]:
  "\<lbrace>valid_inQ_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" unfolding emptySlot_def by (wp opt_return_pres_lift | wpcw | wp valid_inQ_queues_lift | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> do clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
mdbNode <- return (cteMDBNode newCTE);
prev <- return (mdbPrev mdbNode);
next <- return (mdbNext mdbNode);
case cteCap newCTE of capability.NullCap \<Rightarrow> return () | _ \<Rightarrow> do updateMDB prev (mdbNext_update (\<lambda>_. next));
updateMDB next (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged mdbNode) (mdbPrev_update (\<lambda>_. prev) mdb));
updateCap sl capability.NullCap;
updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>
theory Finalise_R

lemma cancelAllIPC_mapM_x_valid_inQ_queues:
  "\<lbrace>valid_inQ_queues\<rbrace>
   mapM_x (\<lambda>t. do
                 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                 tcbSchedEnqueue t
               od) q
   \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" apply (rule mapM_x_wp_inv) apply (wp sts_valid_queues [where st="Structures_H.thread_state.Restart", simplified]
            setThreadState_st_tcb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>valid_inQ_queues\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart x;
tcbSchedEnqueue x
od \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_valid_inQ_queues[wp]:
  "\<lbrace>valid_inQ_queues\<rbrace>
   cteDeleteOne sl
   \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" apply (simp add: cteDeleteOne_def unless_def) apply (wpsimp wp: hoare_drop_imp hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> cteDeleteOne sl \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_inQ_queues\<rbrace> do cte <- getCTE sl;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
(remainder, info) <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable remainder sl \<and> info = capability.NullCap);
emptySlot sl capability.NullCap
od)
od \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteDeleteOne_tcbDomain_obj_at':
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" apply (simp add: cteDeleteOne_def unless_def split_def) apply (wp emptySlot_tcbDomain cancelAllIPC_tcbDomain_obj_at' cancelAllSignals_tcbDomain_obj_at'
          isFinalCapability_inv getCTE_wp
          unbindMaybeNotification_tcbDomain_obj_at'
     | rule hoare_drop_imp
     | simp add: finaliseCapTrue_standin_def Let_def
            split del: if_split
     | wpc)+ apply (clarsimp simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> do cte <- getCTE slot;
when (cteCap cte \<noteq> capability.NullCap) (do final <- isFinalCapability cte;
p <- finaliseCapTrue_standin (cteCap cte) final;
y <- assert (capRemovable (fst p) slot \<and> snd p = capability.NullCap);
emptySlot slot capability.NullCap
od)
od \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (if cteCap cte \<noteq> capability.NullCap then \<lambda>s. (isEndpointCap (cteCap cte) \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' s) \<and> (\<not> isEndpointCap (cteCap cte) \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' s) \<and> (\<not> isNotificationCap (cteCap cte) \<longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' s) \<and> (\<not> isReplyCap (cteCap cte) \<longrightarrow> cteCap cte = capability.DomainCap \<longrightarrow> obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t' s))) else obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t') s) proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma finaliseCap_zombie_cap':
  "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>
     finaliseCap cap fin flag
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl\<rbrace>" apply (rule hoare_strengthen_post) apply (rule finaliseCap_zombie_cap) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl s \<Longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma cteCaps_of_ctes_of_lift:
  "(\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s) \<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace>" unfolding cteCaps_of_def .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (map_option cteCap \<circ> ctes_of s)\<rbrace>
theory Finalise_R

lemma setEndpoint_sch_act_not_ct[wp]:
  "\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace>
   setEndpoint ptr val \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>" by (rule hoare_weaken_pre, wps setEndpoint_ct', wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>
theory Finalise_R

lemma sbn_ct_in_state'[wp]:
  "\<lbrace>ct_in_state' P\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_pre) apply (wps setBoundNotification_ct') apply (wp sbn_st_tcb', clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' P (ksCurThread s) s\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_ s. st_tcb_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_ s. st_tcb_at' P (ksCurThread s) s\<rbrace>
 2. \<And>s. st_tcb_at' P (ksCurThread s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>rv. st_tcb_at' P (ksCurThread prev_s)\<rbrace>
 2. \<And>s. st_tcb_at' P (ksCurThread s) s \<Longrightarrow> ?P3 s s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma set_ntfn_ct_in_state'[wp]:
  "\<lbrace>ct_in_state' P\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_pre) apply (wps setNotification_ksCurThread, wp, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. st_tcb_at' P (ksCurThread s) s\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_ s. st_tcb_at' P (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_ s. st_tcb_at' P (ksCurThread s) s\<rbrace>
 2. \<And>s. st_tcb_at' P (ksCurThread s) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma unbindMaybeNotification_ct_in_state'[wp]:
  "\<lbrace>ct_in_state' P\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" apply (simp add: unbindMaybeNotification_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state' P\<rbrace> do ntfn <- getNotification t;
case ntfnBoundTCB ntfn of None \<Rightarrow> return () | Some ta \<Rightarrow> do y <- setNotification t (ntfnBoundTCB_update (\<lambda>_. None) ntfn);
setBoundNotification None ta
od
od \<lbrace>\<lambda>_. ct_in_state' P\<rbrace> proof (prove)
goal:
No subgoals!
theory Finalise_R

lemma setNotification_sch_act_sane:
  "\<lbrace>sch_act_sane\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" by (wp sch_act_sane_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. sch_act_sane\<rbrace>
theory Ipc_R

lemma getMessageInfo_corres: "corres ((=) \<circ> message_info_map)
                      (tcb_at t) (tcb_at' t)
                      (get_message_info t) (getMessageInfo t)" apply (rule corres_guard_imp) apply (unfold get_message_info_def getMessageInfo_def fun_app_def) apply (simp add: ARM_H.msgInfoRegister_def
             ARM.msgInfoRegister_def ARM_A.msg_info_register_def) apply (rule corres_split_eqr[OF asUser_getRegister_corres]) apply (rule corres_trivial, simp add: message_info_from_data_eqv) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres ((=) \<circ> message_info_map) (tcb_at t) (tcb_at' t) (get_message_info t) (getMessageInfo t) proof (prove)
goal (3 subgoals):
 1. corres ((=) \<circ> message_info_map) ?Q ?Q' (get_message_info t) (getMessageInfo t)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres ((=) \<circ> message_info_map) ?Q ?Q' (do x <- as_user t (getRegister msg_info_register);
return (data_to_message_info x)
od) (do x <- asUser t (getRegister TCB_H.msgInfoRegister);
return (messageInfoFromWord x)
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. corres ((=) \<circ> message_info_map) ?Q ?Q' (do x <- as_user t (getRegister R1);
return (data_to_message_info x)
od) (do x <- asUser t (getRegister R1);
return (messageInfoFromWord x)
od)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>x. corres ((=) \<circ> message_info_map) (?R4 x) (?R'4 x) (return (data_to_message_info x)) (return (messageInfoFromWord x))
 2. \<lbrace>?Q4\<rbrace> as_user t (getRegister R1) \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> asUser t (getRegister R1) \<lbrace>?R'4\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> as_user t (getRegister R1) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> asUser t (getRegister R1) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q4) s
 4. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma cap_relation_mask:
  "\<lbrakk> cap_relation c c'; msk' = rights_mask_map msk \<rbrakk> \<Longrightarrow>
  cap_relation (mask_cap msk c) (maskCapRights msk' c')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_relation c c'; msk' = rights_mask_map msk\<rbrakk> \<Longrightarrow> cap_relation (mask_cap msk c) (global.maskCapRights msk' c')
theory Ipc_R

lemma unifyFailure_wp_E [wp]:
  "\<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>_. E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> unifyFailure f -, \<lbrace>\<lambda>_. E\<rbrace>" unfolding validE_E_def by (erule unifyFailure_wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>_. E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> unifyFailure f -, \<lbrace>\<lambda>_. E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> unifyFailure f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. E\<rbrace>
theory Ipc_R

lemma unifyFailure_wp2 [wp]:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>"
  shows      "\<lbrace>P\<rbrace> unifyFailure f \<lbrace>\<lambda>_. Q\<rbrace>" by (wp x, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> unifyFailure f \<lbrace>\<lambda>_. Q\<rbrace>
theory Ipc_R

lemma valid_ipc_buffer_ptr_aligned_2:
  "\<lbrakk>valid_ipc_buffer_ptr' a s;  is_aligned y 2 \<rbrakk> \<Longrightarrow> is_aligned (a + y) 2" unfolding valid_ipc_buffer_ptr'_def apply clarsimp apply (erule (1) aligned_add_aligned) apply (simp add: msg_align_bits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_ipc_buffer_ptr' a s; is_aligned y 2\<rbrakk> \<Longrightarrow> is_aligned (a + y) 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a msg_align_bits \<and> typ_at' UserDataT (a && ~~ mask pageBits) s; is_aligned y 2\<rbrakk> \<Longrightarrow> is_aligned (a + y) 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y 2; is_aligned a msg_align_bits; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> is_aligned (a + y) 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned y 2; typ_at' UserDataT (a && ~~ mask pageBits) s\<rbrakk> \<Longrightarrow> 2 \<le> msg_align_bits proof (prove)
goal:
No subgoals!
theory Ipc_R

lemma get_recv_slot_inv'[wp]:
  "\<lbrace> P \<rbrace> getReceiveSlots receiver buf \<lbrace>\<lambda>rv'. P \<rbrace>" apply (case_tac buf) apply (simp add: getReceiveSlots_def) apply (simp add: getReceiveSlots_def
                   split_def unlessE_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getReceiveSlots receiver buf \<lbrace>\<lambda>rv'. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. buf = None \<Longrightarrow> \<lbrace>P\<rbrace> getReceiveSlots receiver buf \<lbrace>\<lambda>rv'. P\<rbrace>
 2. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> getReceiveSlots receiver buf \<lbrace>\<lambda>rv'. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> getReceiveSlots receiver buf \<lbrace>\<lambda>rv'. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. buf = Some a \<Longrightarrow> \<lbrace>P\<rbrace> do ct <- loadCapTransfer a;
emptyOnFailure (doE cnode <- unifyFailure (lookupCap receiver (ctReceiveRoot ct));
slot <- unifyFailure (lookupSlotForCNodeOp False cnode (ctReceiveIndex ct) (ctReceiveDepth ct));
cte <- liftE (getCTE slot);
y <- if cteCap cte = capability.NullCap then returnOk () else throwError ();
returnOk [slot]
odE)
od \<lbrace>\<lambda>rv'. P\<rbrace> proof (prove)
goal:
No subgoals!