theory Invoke_C

lemma invokeCNodeSaveCaller_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (valid_mdb' and pspace_aligned' and cur_tcb')
       (UNIV \<inter> {s. destSlot_' s = Ptr destSlot}) []
       (invokeCNode (SaveCaller destSlot))
  (Call invokeCNodeSaveCaller_'proc)" apply (cinit lift: destSlot_'  simp del: return_bind cong:call_ignore_cong) apply (simp add: Collect_True split del: if_split  del: Collect_const cong:call_ignore_cong) apply (simp only: liftE_def) apply (rule ccorres_Guard_Seq)+ apply (simp only: bind_assoc) apply (rule ccorres_pre_getCurThread) apply (simp only: getThreadCallerSlot_def locateSlot_conv) apply (rule_tac P="\<lambda>s. rv=ksCurThread s \<and> is_aligned rv tcbBlockSizeBits" and r'="\<lambda> a c. c = Ptr a"
                   and xf'="srcSlot_'" and P'=UNIV in ccorres_split_nothrow) apply (rule ccorres_return) apply vcg apply clarsimp apply (simp add: cte_level_bits_def size_of_def of_nat_def) apply (simp add: rf_sr_def cstate_relation_def Kernel_C.tcbCaller_def tcbCallerSlot_def) apply (clarsimp simp: Let_def objBits_defs) apply (subst ptr_val_tcb_ptr_mask2[simplified mask_def objBits_defs, simplified]) apply assumption apply simp apply ceqv apply (simp del: Collect_const cong: call_ignore_cong) apply (rule ccorres_getSlotCap_cte_at) apply (rule ccorres_move_c_guard_cte) apply (ctac (no_vcg)) apply csymbr apply (wpc, simp_all add: cap_get_tag_isCap isCap_simps
                                 Collect_False Collect_True
                            del: Collect_const)[1] apply (rule ccorres_fail)+
                  \<comment> \<open>NullCap case\<close> apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply clarsimp apply (simp add: return_def) apply (rule ccorres_fail)+
          \<comment> \<open>ReplyCap case\<close> apply (rule ccorres_rhs_assoc) apply csymbr apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (simp add: cap_get_tag_ReplyCap) apply (case_tac " (capReplyMaster_CL (cap_reply_cap_lift cap))=0", simp_all add: to_bool_def)[1] apply (ctac (no_vcg) add: cteMove_ccorres) apply (rule ccorres_return_CE [unfolded returnOk_def,simplified], simp+)[1] apply wp apply (rule ccorres_fail') apply (rule ccorres_fail)+ apply (wp getSlotCap_wp) apply (clarsimp simp: cap_get_tag_isCap isCap_simps) apply wp apply vcg apply (clarsimp simp: word_sle_def cte_wp_at_ctes_of
                        tcb_aligned' cur_tcb'_def
                        tcb_cnode_index_defs ptr_add_assertion_positive) apply (frule(1) rf_sr_tcb_ctes_array_assertion2[rotated]) apply (simp add: tcb_cnode_index_defs array_assertion_shrink_right
                   rf_sr_ksCurThread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (valid_mdb' and pspace_aligned' and cur_tcb') (UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace>) [] (invokeCNode (SaveCaller destSlot)) (Call invokeCNodeSaveCaller_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>destSlota. destSlota = cte_Ptr destSlot \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q577 destSlota) (?Q'577 destSlota) [SKIP] (liftE (do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od)) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,destSlota)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q577 destSlota s \<and> s' \<in> ?Q'577 destSlota proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q577 (cte_Ptr destSlot)) (?Q'577 (cte_Ptr destSlot)) [SKIP] (liftE (do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od)) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q577 destSlota s \<and> s' \<in> ?Q'577 destSlota proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q577 (cte_Ptr destSlot)) (?Q'577 (cte_Ptr destSlot)) [SKIP] (do r <- do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od;
return (Inr r)
od) (Guard MemorySafety \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q577 destSlota s \<and> s' \<in> ?Q'577 destSlota proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q577 (cte_Ptr destSlot)) (?C'590 (cte_Ptr destSlot)) [SKIP] (do r <- do thread <- getCurThread;
srcSlot <- getThreadCallerSlot thread;
cap <- getSlotCap srcSlot;
case cap of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove cap srcSlot destSlot | _ \<Rightarrow> haskell_fail []
od;
return (Inr r)
od) (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q577 destSlota s \<and> s' \<in> ?C'590 destSlota \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (2 subgoals):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q577 (cte_Ptr destSlot)) (?C'590 (cte_Ptr destSlot)) [SKIP] (do x <- getCurThread;
x <- getThreadCallerSlot x;
xa <- getSlotCap x;
r <- case xa of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xb True xaa \<Rightarrow> haskell_fail [] | capability.ReplyCap xb False xaa \<Rightarrow> cteMove xa x destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q577 destSlota s \<and> s' \<in> ?C'590 destSlota \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?P594 (cte_Ptr destSlot) a rv) (?P'595 (cte_Ptr destSlot) rv) [SKIP] (do x <- getThreadCallerSlot rv;
xa <- getSlotCap x;
r <- case xa of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xb bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove xa x destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P594 destSlota s rv) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'595 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>a. ?P594 (cte_Ptr destSlot) a rv) (?P'595 (cte_Ptr destSlot) rv) [SKIP] (do x <- return (rv + 2 ^ cte_level_bits * tcbCallerSlot);
xa <- getSlotCap x;
r <- case xa of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xb bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove xa x destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P594 destSlota s rv) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'595 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv. ccorres (\<lambda>a c. c = cte_Ptr a) srcSlot_' (\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) UNIV [SKIP] (return (rv + 2 ^ cte_level_bits * tcbCallerSlot)) (\<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))))
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. (s, s') \<in> rf_sr}) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s'. (s, s') \<in> rf_sr \<and> srcSlot_' s' = cte_Ptr (rv + 2 ^ cte_level_bits * tcbCallerSlot)}
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s. is_aligned (ksCurThread s) tcbBlockSizeBits \<Longrightarrow> UNIV \<inter> {s'. (s, s') \<in> rf_sr} \<subseteq> {sa. (s, srcSlot_'_update (\<lambda>_. cte_Ptr ((ptr_val (ksCurThread_' (globals sa)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)))) sa) \<in> rf_sr \<and> cte_Ptr ((ptr_val (ksCurThread_' (globals sa)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr (ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot)}
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) tcbBlockSizeBits; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ptr_val (ksCurThread_' (globals x)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C)) = ksCurThread s + 2 ^ cte_level_bits * tcbCallerSlot
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) tcbBlockSizeBits; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (ptr_val (ksCurThread_' (globals x)) && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * 0x10 = ksCurThread s + 0x10 * tcbCallerSlot
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) tcbBlockSizeBits; let cheap = t_hrs_' (globals x) in cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) cheap \<and> cready_queues_relation (clift cheap) (ksReadyQueues_' (globals x)) (ksReadyQueues s) \<and> zero_ranges_are_zero (gsUntypedZeroRanges s) cheap \<and> cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s) \<and> cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s) \<and> ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s) \<and> cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)) \<and> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals x)) \<and> carch_state_relation (ksArchState s) (globals x) \<and> cmachine_state_relation (ksMachineState s) (globals x) \<and> cvariable_array_map_relation (gsCNodes s) ((^) 2) cte_Ptr (hrs_htd cheap) \<and> cvariable_array_map_relation (map_to_tcbs (ksPSpace s)) (\<lambda>x. 5) cte_Ptr (hrs_htd cheap) \<and> apsnd fst (ghost'state_' (globals x)) = (gsUserPages s, gsCNodes s) \<and> ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s) \<and> ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s \<and> hrs_htd cheap \<Turnstile>\<^sub>t intStateIRQNode_array_Ptr \<and> {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs \<and> hrs_htd cheap \<Turnstile>\<^sub>t armKSGlobalPD_Ptr \<and> {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs \<and> htd_safe domain (hrs_htd cheap) \<and> - domain \<subseteq> kernel_data_refs \<and> globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list \<and> cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule \<and> ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s) \<and> ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s) \<and> ksDomainTime_' (globals x) = ksDomainTime s\<rbrakk> \<Longrightarrow> ptr_val (ksCurThread_' (globals x)) && 0xFFFFFE00 = ksCurThread s
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) 9; cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState s) (globals x); cmachine_state_relation (ksMachineState s) (globals x); cte_array_relation s (globals x); tcb_cte_array_relation s (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals x) = ksDomainTime s\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr (ksCurThread s)) && 0xFFFFFE00 = ksCurThread s
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) 9; cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState s) (globals x); cmachine_state_relation (ksMachineState s) (globals x); cte_array_relation s (globals x); tcb_cte_array_relation s (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals x) = ksDomainTime s\<rbrakk> \<Longrightarrow> is_aligned (ksCurThread s) 9
 2. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) 9; cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState s) (globals x); cmachine_state_relation (ksMachineState s) (globals x); cte_array_relation s (globals x); tcb_cte_array_relation s (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals x) = ksDomainTime s\<rbrakk> \<Longrightarrow> ksCurThread s = ksCurThread s
 3. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 4. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 5. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 6. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 7. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned (ksCurThread s) 9; cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals x)); cready_queues_relation (cslift x) (ksReadyQueues_' (globals x)) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals x)); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals x)) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals x)) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals x) = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals x)); cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals x)); carch_state_relation (ksArchState s) (globals x); cmachine_state_relation (ksMachineState s) (globals x); cte_array_relation s (globals x); tcb_cte_array_relation s (globals x); apsnd fst (ghost'state_' (globals x)) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals x)) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals x) = ksWorkUnitsCompleted s; x \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; x \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals x))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals x) = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals x) = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals x) = ksDomainTime s\<rbrakk> \<Longrightarrow> ksCurThread s = ksCurThread s
 2. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 3. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' t t'. ceqv \<Gamma> srcSlot_' rv' t t' (Guard C_Guard {s. s \<Turnstile>\<^sub>c srcSlot_' s} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(\<acute>srcSlot\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,\<acute>srcSlot,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))) (?d'598 rv rv')
 2. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (?d'598 rv rv')
 3. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 4. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 5. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva rv'. rv' = cte_Ptr rva \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva rv') [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa bool1 xaa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr r)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c rv'} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(rv'\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,rv',cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 3. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 4. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q598 rv rva) (?Q'598 rv rva (cte_Ptr rva)) [SKIP] (do x <- getSlotCap rva;
r <- case x of capability.NullCap \<Rightarrow> return () | capability.ReplyCap xa True xaa \<Rightarrow> haskell_fail [] | capability.ReplyCap xa False xaa \<Rightarrow> cteMove x rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr ())
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr rva} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rva\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,cte_Ptr rva,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q598 rv\<rbrace>
 3. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 4. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?G823 rv rva) (?Q'598 rv rva (cte_Ptr rva)) [SKIP] (do a <- getSlotCap rva;
r <- case a of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x bool1 xa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove a rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr ())
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr rva} (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rva\<rightarrow>[''cap_C''])));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,cte_Ptr rva,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ?G823 rv rva s\<rbrace>
 3. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?Q'598 rv rva (srcSlot_' s)}
 4. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?A825 rv rva) (?C'826 rv rva (cte_Ptr rva)) [SKIP] (do a <- getSlotCap rva;
r <- case a of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x bool1 xa \<Rightarrow> case bool1 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove a rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr ())
od) (\<acute>cap :== h_val (hrs_mem \<acute>t_hrs) (cap_Ptr &(cte_Ptr rva\<rightarrow>[''cap_C'']));;
(\<acute>ret__unsigned :== CALL cap_get_capType_'proc(\<acute>cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(\<acute>cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(\<acute>cap,cte_Ptr rva,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> (?A825 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 3. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rva. srcSlot_' s = cte_Ptr rva \<longrightarrow> s \<in> ?C'826 rv rva (srcSlot_' s) \<inter> \<lbrace>True\<rbrace>}
 4. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rva rvb cap. ccap_relation rvb cap \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q830 rv rva rvb) (?Q'830 rv rva rvb cap) [SKIP] (do r <- case rvb of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove rvb rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_get_capType_'proc(cap);;
(IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>?Q830 rv rva\<rbrace>
 3. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> ?Q'830 rv rva rvb (cap_' s)
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation rvb cap; ret__unsigned = cap_get_tag cap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q830 rv rva rvb) (?G'1000 rv rva rvb cap ret__unsigned) [SKIP] (do r <- case rvb of capability.NullCap \<Rightarrow> return () | capability.ReplyCap x True xa \<Rightarrow> haskell_fail [] | capability.ReplyCap x False xa \<Rightarrow> cteMove rvb rva destSlot | _ \<Rightarrow> haskell_fail [];
return (Inr ())
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_null_cap THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) cap_reply_cap THEN
  \<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI
ELSE
  Guard DontReach {} SKIP
FI
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>?Q830 rv rva\<rbrace>
 3. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> ?G'1000 rv rva rvb (cap_' s) v}
 4. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 5. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (17 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned x1. \<lbrakk>ccap_relation (capability.ThreadCap x1) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1158 rv rva (capability.ThreadCap x1) x1) (?R''1156 rv rva (capability.ThreadCap x1) cap (cap_get_tag cap) x1) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.NullCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1159 rv rva capability.NullCap) (?R''1154 rv rva capability.NullCap cap (cap_get_tag cap)) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.NullCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.NullCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1159 rv rva capability.NullCap) (?R''1154 rv rva capability.NullCap cap (cap_get_tag cap)) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.NullCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.NullCap\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned \<sigma>. \<lbrakk>ccap_relation capability.NullCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.NullCap\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 16 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>cap \<sigma> x. \<lbrakk>ccap_relation capability.NullCap cap; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (return (Inr ()) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (\<lambda>y. ()) ret__unsigned_long_' (x\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 16 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) cap; ret__unsigned = cap_get_tag cap; rvb = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1160 rv rva (capability.NotificationCap x31 x32 x33 x34) x31 x32 x33 x34) (?R''1153 rv rva (capability.NotificationCap x31 x32 x33 x34) cap (cap_get_tag cap) x31 x32 x33 x34) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x4. \<lbrakk>ccap_relation (capability.IRQHandlerCap x4) cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1161 rv rva (capability.IRQHandlerCap x4) x4) (?R''1148 rv rva (capability.IRQHandlerCap x4) cap (cap_get_tag cap) x4) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x51 x52 x53 x54 x55 x56. \<lbrakk>ccap_relation (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap; ret__unsigned = cap_get_tag cap; rvb = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1162 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) x51 x52 x53 x54 x55 x56) (?R''1146 rv rva (capability.EndpointCap x51 x52 x53 x54 x55 x56) cap (cap_get_tag cap) x51 x52 x53 x54 x55 x56) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.DomainCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.DomainCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1163 rv rva capability.DomainCap) (?R''1139 rv rva capability.DomainCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned x71 x72 x73. \<lbrakk>ccap_relation (capability.Zombie x71 x72 x73) cap; ret__unsigned = cap_get_tag cap; rvb = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1164 rv rva (capability.Zombie x71 x72 x73) x71 x72 x73) (?R''1138 rv rva (capability.Zombie x71 x72 x73) cap (cap_get_tag cap) x71 x72 x73) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned x8. \<lbrakk>ccap_relation (capability.ArchObjectCap x8) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1165 rv rva (capability.ArchObjectCap x8) x8) (?R''1134 rv rva (capability.ArchObjectCap x8) cap (cap_get_tag cap) x8) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 8. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 9. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 10. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
A total of 15 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> ?R''1132 rv rva rvb (cap_' s) v x xa xb}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned x91 x92 x93. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigned = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?R''1132 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (\<acute>ret__unsigned :== CALL cap_reply_cap_get_capReplyMaster_'proc(cap);;
(IF \<acute>ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> ?R''1132 rv rva rvb (cap_' s) v x xa xb}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 x92 x93 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigneda = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93; ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?G'1227 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93 ret__unsigned) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (IF ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> ?G'1227 rv rva rvb (cap_' s) v x xa xb va}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 x92 x93 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap x91 x92 x93) cap; ret__unsigneda = cap_get_tag cap; rvb = capability.ReplyCap x91 x92 x93; ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_reply_cap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap x91 x92 x93) x91 x92 x93) (?G'1227 rv rva (capability.ReplyCap x91 x92 x93) cap (cap_get_tag cap) x91 x92 x93 ret__unsigned) [SKIP] (do r <- case x92 of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (IF ret__unsigned = 0 THEN
  CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> ?G'1227 rv rva rvb (cap_' s) v x xa xb va}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap)))) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap))); ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap)))) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap)))) (?G'1227 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap)))) cap (cap_get_tag cap) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap))) (to_bool (capReplyCanGrant_CL (cap_reply_cap_lift cap))) (capReplyMaster_CL (cap_reply_cap_lift cap))) [SKIP] (do r <- case to_bool (capReplyMaster_CL (cap_reply_cap_lift cap)) of True \<Rightarrow> haskell_fail [] | False \<Rightarrow> cteMove rvb rva destSlot;
return (Inr ())
od) (Cond (if capReplyMaster_CL (cap_reply_cap_lift cap) = 0 then UNIV else {}) (CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot)) SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> ?G'1227 rv rva rvb (cap_' s) v x xa xb va}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = 0; x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) = 0\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (?G'1227 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap (cap_get_tag cap) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0) 0) [SKIP] (do r <- cteMove (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) rva destSlot;
return (Inr ())
od) (CALL cteMove_'proc(cap,cte_Ptr rva,cte_Ptr destSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1166 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (?G'1227 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap (cap_get_tag cap) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0) (capReplyMaster_CL (cap_reply_cap_lift cap))) [SKIP] fail (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> ?R1166 rv rva rvb x xa xb s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 7. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> ?G'1227 rv rva rvb (cap_' s) v x xa xb va}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 8. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 9. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 10. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (11 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned rvc xfdc. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = 0; x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) = 0; dc rvc xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1315 rv rva rvb cap ret__unsigneda x91 ret__unsigned rvc) (?Q'1329 rv rva cap rvc xfdc) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = 0; x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1323 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)\<rbrace> cteMove (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) rva destSlot \<lbrace>?Q1315 rv rva rvb cap ret__unsigneda x91 ret__unsigned\<rbrace>
 3. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (valid_mdb' and pspace_aligned' and ?R1323 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) ({s. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rvb. dc rvb (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1328 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap (cap_get_tag cap) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0) (capReplyMaster_CL (cap_reply_cap_lift cap)) t rvb}) [SKIP] fail (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 7. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R1323 rv rva rvb x xa xb) s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 8. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>va v'. va = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := va\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rvc. dc rvc (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'1328 rv rva rvb (cap_' s) v x xa xb va t rvc}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 9. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 10. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
A total of 11 subgoals...
flex-flex pairs:
\<lambda>rv rva cap t rvb. ?Q'1329 rv rva cap rvb (xfdc t) \<equiv>\<^sup>? \<lambda>rv rva cap. ?Q'1328 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap (cap_get_tag cap) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0) 0 proof (prove)
goal (10 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = 0; x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) = 0\<rbrakk> \<Longrightarrow> \<lbrace>?R1323 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)\<rbrace> cteMove (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) False (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) rva destSlot \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (valid_mdb' and pspace_aligned' and ?R1323 rv rva (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) ({s. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}) [SKIP] fail (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 6. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and ?R1323 rv rva rvb x xa xb) s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 7. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 8. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 9. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 10. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>rv rva rvb cap ret__unsigneda x91 ret__unsigned. \<lbrakk>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) cap; ret__unsigneda = SCAST(32 signed \<rightarrow> 32) cap_reply_cap; rvb = capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0); ret__unsigned = capReplyMaster_CL (cap_reply_cap_lift cap); x91 = ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap))); capReplyMaster_CL (cap_reply_cap_lift cap) \<noteq> 0\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) ({s. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation (capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap)))) True (capReplyCanGrant_CL (cap_reply_cap_lift cap) \<noteq> 0)) \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}) [SKIP] fail (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 5. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 6. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 7. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 8. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 9. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>rv rva rvb cap ret__unsigned x101 x102 x103 x104. \<lbrakk>ccap_relation (capability.UntypedCap x101 x102 x103 x104) cap; ret__unsigned = cap_get_tag cap; rvb = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1167 rv rva (capability.UntypedCap x101 x102 x103 x104) x101 x102 x103 x104) (?R''1128 rv rva (capability.UntypedCap x101 x102 x103 x104) cap (cap_get_tag cap) x101 x102 x103 x104) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>rv rva rvb cap ret__unsigned x111 x112 x113 x114. \<lbrakk>ccap_relation (capability.CNodeCap x111 x112 x113 x114) cap; ret__unsigned = cap_get_tag cap; rvb = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1168 rv rva (capability.CNodeCap x111 x112 x113 x114) x111 x112 x113 x114) (?R''1123 rv rva (capability.CNodeCap x111 x112 x113 x114) cap (cap_get_tag cap) x111 x112 x113 x114) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>rv rva rvb cap ret__unsigned. \<lbrakk>ccap_relation capability.IRQControlCap cap; ret__unsigned = cap_get_tag cap; rvb = capability.IRQControlCap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R1169 rv rva capability.IRQControlCap) (?R''1118 rv rva capability.IRQControlCap cap (cap_get_tag cap)) [SKIP] fail (Guard DontReach {} SKIP;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> ?R1167 rv rva rvb x xa xb xc s) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> ?R1168 rv rva rvb x xa xb xc s) \<and> (rvb = capability.IRQControlCap \<longrightarrow> ?R1169 rv rva rvb s)\<rbrace>
 5. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> sa \<in> ?R''1128 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> sa \<in> ?R''1123 rv rva rvb (cap_' s) v x xa xb xc}}}}} \<inter> {sa. rvb = capability.IRQControlCap \<longrightarrow> sa \<in> ?R''1118 rv rva rvb (cap_' s) v}))))))))))}
 6. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 7. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 8. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rva. \<lbrace>?R830 rv rva\<rbrace> getSlotCap rva \<lbrace>\<lambda>rvb s. (\<forall>x. rvb = capability.ThreadCap x \<longrightarrow> True) \<and> (rvb = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (rvb = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. rvb = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. rvb = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (rvb = capability.IRQControlCap \<longrightarrow> True)\<rbrace>
 2. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> {s. rvb = capability.IRQControlCap \<longrightarrow> s \<in> UNIV}))))))))))}
 3. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and ?R830 rv rva and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 4. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 5. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rva s rvb. ccap_relation rvb (cap_' s) \<Longrightarrow> s \<in> {sa. \<forall>v. v = cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. \<forall>x. s \<in> {s. rvb = capability.ThreadCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rvb = capability.NullCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.NotificationCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.IRQHandlerCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. \<forall>xe. s \<in> {s. rvb = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> s \<in> UNIV}}}}}}} \<inter> ({s. rvb = capability.DomainCap \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. rvb = capability.Zombie x xa xb \<longrightarrow> s \<in> UNIV}}}} \<inter> ({s. \<forall>x. s \<in> {s. rvb = capability.ArchObjectCap x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. rvb = capability.ReplyCap x xa xb \<longrightarrow> sa \<in> {sa. \<forall>v v'. v = capReplyMaster_CL (cap_reply_cap_lift (cap_' (cap_'_update (\<lambda>_. cap_' s) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {sa. destSlot_'_update (\<lambda>_. cte_Ptr destSlot) (srcSlot_'_update (\<lambda>_. cte_Ptr rva) (newCap_'_update (\<lambda>_. cap_' s) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr rva\<rbrace> \<inter> \<lbrace>ccap_relation rvb \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> dc () (K () (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))\<rbrace>}}} \<inter> {sa. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap_' s) sa)) = SCAST(32 signed \<rightarrow> 32) cap_reply_cap}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.UntypedCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. rvb = capability.CNodeCap x xa xb xc \<longrightarrow> s \<in> UNIV}}}}} \<inter> {s. rvb = capability.IRQControlCap \<longrightarrow> s \<in> UNIV}))))))))))}
 2. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) rva s \<and> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> True) \<and> (cap = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (cap = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (cap = capability.IRQControlCap \<longrightarrow> True)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 3. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 4. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrace>?R603 (cte_Ptr destSlot) rv\<rbrace> return (rv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>rva s. cte_wp_at' (\<lambda>_. True) rva s \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) rva s \<and> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> True) \<and> (cap = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (cap = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (cap = capability.IRQControlCap \<longrightarrow> True)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr rva))) s\<rbrace>
 2. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 3. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and ?R603 destSlota rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<Gamma>\<turnstile>\<^bsub>/?F598 rv\<^esub> (?R'601 (cte_Ptr destSlot) rv) \<acute>srcSlot :== cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) {s. \<forall>rv. srcSlot_' s = cte_Ptr rv \<longrightarrow> s \<in> \<lbrace>\<^bsup>s\<^esup>srcSlot = \<^bsup>s\<^esup>srcSlot\<rbrace> \<inter> \<lbrace>True\<rbrace>}
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and (\<lambda>a. cte_wp_at' (\<lambda>_. True) (rv + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (rv + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> True) \<and> (cap = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (cap = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (cap = capability.IRQControlCap \<longrightarrow> True)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (rv + 2 ^ cte_level_bits * tcbCallerSlot)))) a)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> ?R'601 destSlota rv} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (valid_mdb' and pspace_aligned' and cur_tcb') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s \<and> is_aligned rv tcbBlockSizeBits) and (\<lambda>a. cte_wp_at' (\<lambda>_. True) (rv + 2 ^ cte_level_bits * tcbCallerSlot) a \<longrightarrow> ((\<lambda>_. True) and (\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) (rv + 2 ^ cte_level_bits * tcbCallerSlot) s \<and> (\<forall>x. cap = capability.ThreadCap x \<longrightarrow> True) \<and> (cap = capability.NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.NotificationCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x. cap = capability.IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. cap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> True) \<and> (cap = capability.DomainCap \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. cap = capability.ArchObjectCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. cap = capability.ReplyCap x xa xb \<longrightarrow> (valid_mdb' and pspace_aligned' and (\<lambda>a. True)) s) \<and> (\<forall>x xa xb xc. cap = capability.UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb xc. cap = capability.CNodeCap x xa xb xc \<longrightarrow> True) \<and> (cap = capability.IRQControlCap \<longrightarrow> True)) and cte_wp_at' (\<lambda>_. True) (ptr_val (cte_Ptr (rv + 2 ^ cte_level_bits * tcbCallerSlot)))) a)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>\<forall>rv. cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr rv \<longrightarrow> cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) = cte_Ptr ((ptr_val \<acute>ksCurThread && 0xFFFFFE00) + SCAST(32 signed \<rightarrow> 32) Kernel_C.tcbCaller * word_of_nat (size_of TYPE(cte_C))) \<and> True\<rbrace>} \<inter> \<lbrace>ptr_add_assertion (cte_Ptr (ptr_val \<acute>ksCurThread && 0xFFFFFE00)) (sint Kernel_C.tcbCaller) False (hrs_htd \<acute>t_hrs)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; tcb_at' (ksCurThread s) s\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr (ptr_val (ksCurThread_' (globals s')) && 0xFFFFFE00)) 3 (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_mdb' s; pspace_aligned' s; tcb_at' (ksCurThread s) s; array_assertion (cte_Ptr (ksCurThread s)) (unat tcbCNodeEntries) (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> array_assertion (cte_Ptr (ptr_val (ksCurThread_' (globals s')) && 0xFFFFFE00)) 3 (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!