theory Tcb_C

lemma invokeTCB_SetTLSBase_ccorres:
  notes hoare_weak_lift_imp [wp]
  shows
  "ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_')
   (invs')
   ({s. thread_' s = tcb_ptr_to_ctcb_ptr tcb}
         \<inter> {s. tls_base_' s = tls_base}) []
   (invokeTCB (SetTLSBase tcb tls_base))
   (Call invokeSetTLSBase_'proc)" apply (cinit lift: thread_' tls_base_') apply (simp add: liftE_def bind_assoc
               del: Collect_const) apply (ctac add: setRegister_ccorres) apply (rule ccorres_pre_getCurThread) apply (rename_tac cur_thr) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule_tac R="\<lambda>s. cur_thr = ksCurThread s" in ccorres_when) apply (clarsimp simp: rf_sr_ksCurThread) apply clarsimp apply (ctac (no_vcg) add: rescheduleRequired_ccorres) apply (unfold return_returnOk)[1] apply (rule ccorres_return_CE, simp+)[1] apply (wpsimp wp: hoare_drop_imp simp: guard_is_UNIV_def)+ apply vcg apply (clarsimp simp: tlsBaseRegister_def ARM.tlsBaseRegister_def
                        invs_weak_sch_act_wf invs_queues TLS_BASE_def TPIDRURW_def
                 split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') invs' (\<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr tcb\<rbrace> \<inter> \<lbrace>\<acute>tls_base = tls_base\<rbrace>) [] (invokeTCB (tcbinvocation.SetTLSBase tcb tls_base)) (Call invokeSetTLSBase_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q182 tls_basea thread) (?Q'182 tls_basea thread) [SKIP] (liftE (do y <- asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base);
cur <- getCurThread;
y <- when (tcb = cur) rescheduleRequired;
return []
od)) (CALL setRegister_'proc(thread,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_basea);;
(IF thread = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q182 tls_basea thread s \<and> s' \<in> ?Q'182 tls_basea thread proof (prove)
goal (2 subgoals):
 1. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q182 tls_base (tcb_ptr_to_ctcb_ptr tcb)) (?Q'182 tls_base (tcb_ptr_to_ctcb_ptr tcb)) [SKIP] (do y <- asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base);
cur <- getCurThread;
y <- when (tcb = cur) rescheduleRequired;
return (Inr [])
od) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base);;
(IF tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q182 tls_basea thread s \<and> s' \<in> ?Q'182 tls_basea thread proof (prove)
goal (4 subgoals):
 1. \<And>tls_basea thread rv xfdc. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q193 tls_basea thread rv) (?Q'193 tls_basea thread rv xfdc) [SKIP] (do cur <- getCurThread;
y <- when (tcb = cur) rescheduleRequired;
return (Inr [])
od) (IF tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>?Q193 tls_basea thread\<rbrace>
 3. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'193 tls_basea thread rv (xfdc s)}
 4. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (4 subgoals):
 1. \<And>tls_basea thread rv xfdc cur. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?P233 tls_basea thread rv cur) (?P'232 tls_basea thread rv xfdc cur) [SKIP] (do y <- when (tcb = cur) rescheduleRequired;
return (Inr [])
od) (IF tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ?P233 tls_basea thread a rv b\<rbrace>
 3. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> ?P'232 tls_basea thread rv (xfdc s) rva}}
 4. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (4 subgoals):
 1. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?P233 tls_basea thread rv cur_thr) (?P'232 tls_basea thread rv xfdc cur_thr) [SKIP] (do y <- when (tcb = cur_thr) rescheduleRequired;
return (Inr [])
od) (IF tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ?P233 tls_basea thread a rv b\<rbrace>
 3. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> ?P'232 tls_basea thread rv (xfdc s) rva}}
 4. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (7 subgoals):
 1. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P236 tls_basea thread rv cur_thr) (?P'232 tls_basea thread rv xfdca cur_thr) [] (when (tcb = cur_thr) rescheduleRequired) (IF tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 4. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 5. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> (?P236 tls_basea thread a rv and ?R237 tls_basea thread a rv) b\<rbrace>
 6. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> ?P'232 tls_basea thread rv (xfdc s) rva}}
 7. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (8 subgoals):
 1. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> cur_thr = ksCurThread s \<longrightarrow> (tcb = cur_thr) = (s' \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace>)
 2. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt245 tls_basea thread rv cur_thr) (?Rt242 tls_basea thread rv xfdca cur_thr) [] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 4. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 5. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 6. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> ?Pt245 tls_basea thread a rv s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 7. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> {sa. (sa \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> ?Rt242 tls_basea thread rv (xfdc s) rva) \<and> (sa \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 8. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (7 subgoals):
 1. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt245 tls_basea thread rv cur_thr) (?Rt242 tls_basea thread rv xfdca cur_thr) [] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 4. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 5. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> ?Pt245 tls_basea thread a rv s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 6. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> {sa. (sa \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> ?Rt242 tls_basea thread rv (xfdc s) rva) \<and> (sa \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (7 subgoals):
 1. \<And>xfdca cur_thr. ccorres dc xfdc (?Pt245 tls_base (tcb_ptr_to_ctcb_ptr tcb) () cur_thr) (?Rt242 tls_base (tcb_ptr_to_ctcb_ptr tcb) () xfdca cur_thr) [] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 3. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 4. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 5. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> ?Pt245 tls_basea thread a rv s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 6. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>rva. ksCurThread_' (globals sa) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> sa \<in> {sa. (sa \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> ?Rt242 tls_basea thread rv (xfdc s) rva) \<and> (sa \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> sa \<in> UNIV)}}}
 7. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (6 subgoals):
 1. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (return (Inr [])) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 3. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 4. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 5. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 6. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (6 subgoals):
 1. \<And>tls_basea thread rv xfdc cur_thr y rv'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> (\<lambda>rv rv'. rv = [])) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q235 tls_basea thread rv xfdc cur_thr y) (?Q'235 tls_basea thread rv xfdc cur_thr y rv') [SKIP] (returnOk []) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>?Q235 tls_basea thread rv xfdc cur_thr\<rbrace>
 3. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'235 tls_basea thread rv xfdca cur_thr)
 4. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 5. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 6. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (5 subgoals):
 1. \<And>tls_basea thread rv xfdc cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R237 tls_basea thread rv cur_thr\<rbrace> when (tcb = cur_thr) rescheduleRequired \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>tls_basea thread rv xfdca cur_thr. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. \<lbrace>id (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> [] = []\<rbrace>)
 3. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<lbrace>?R202 tls_base (tcb_ptr_to_ctcb_ptr tcb)\<rbrace> asUser tcb (setRegister TCB_H.tlsBaseRegister tls_base) \<lbrace>\<lambda>a b. \<forall>rv. ksCurThread b = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. tcb = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. tcb \<noteq> rv \<longrightarrow> True) and ?R237 tls_basea thread a rv) b\<rbrace>
 4. \<And>tls_basea thread. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tcb_ptr_to_ctcb_ptr tcb = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> UNIV)}}}
 5. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and ?R202 tls_basea thread) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'195 tls_base (tcb_ptr_to_ctcb_ptr tcb)) CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr tcb,SCAST(32 signed \<rightarrow> 32) TLS_BASE,tls_base) UNIV
 2. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> ?R'195 tls_basea thread proof (prove)
goal (1 subgoal):
 1. \<And>tls_basea thread s s'. \<lbrakk>tls_basea = tls_base; thread = tcb_ptr_to_ctcb_ptr tcb; (s, s') \<in> rf_sr; invs' s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>a. True) and (\<lambda>a. Invariants_H.valid_queues a \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> valid_objs' a)) s \<and> s' \<in> {s. w_'_update (\<lambda>_. tls_basea) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) TLS_BASE) (thread_'_update (\<lambda>_. thread) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.tlsBaseRegister\<rbrace> \<inter> \<lbrace>\<acute>w = tls_basea\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!