theory Tcb_C

lemma decodeSetTLSBase_ccorres:
  "ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and sch_act_simple
              and (\<lambda>s. ksCurThread s = thread) and ct_active' and K (isThreadCap cp)
              and valid_cap' cp and (\<lambda>s. \<forall>x \<in> zobj_refs' cp. ex_nonz_cap_to' x s)
              and sysargs_rel args buffer)
       (UNIV
            \<inter> {s. ccap_relation cp (cap_' s)}
            \<inter> {s. unat (length___unsigned_long_' s) = length args}
            \<inter> {s. buffer_' s = option_to_ptr buffer}) []
     (decodeSetTLSBase args cp
            >>= invocationCatch thread isBlocking isCall InvokeTCB)
     (Call decodeSetTLSBase_'proc)" apply (cinit' lift: cap_' length___unsigned_long_' buffer_'
                simp: decodeSetTLSBase_def) apply wpc apply (simp add: throwError_bind invocationCatch_def) apply (rule ccorres_from_vcg_split_throws[where P=\<top> and P'=UNIV]) apply vcg apply (rule conseqPre, vcg) apply (clarsimp simp: throwError_def return_def
                          exception_defs syscall_error_rel_def
                          syscall_error_to_H_cases) apply (rule ccorres_cond_false_seq; simp) apply (rule ccorres_add_return,
          ctac add: getSyscallArg_ccorres_foo'[where args=args and n=0 and buffer=buffer]) apply (simp add: invocationCatch_use_injection_handler
                      bindE_assoc injection_handler_returnOk
                      ccorres_invocationCatch_Inr performInvocation_def) apply (ctac add: setThreadState_ccorres) apply csymbr apply (ctac (no_vcg) add: invokeTCB_SetTLSBase_ccorres) apply simp apply (rule ccorres_alternative2) apply (rule ccorres_return_CE, simp+)[1] apply (rule ccorres_return_C_errorE, simp+)[1] apply (wpsimp wp: sts_invs_minor')+ apply (vcg exspec=setThreadState_modifies) apply wp apply vcg apply (clarsimp simp: Collect_const_mem) apply (rule conjI) apply (clarsimp simp: ct_in_state'_def sysargs_rel_n_def n_msgRegisters_def) apply (auto simp: valid_tcb_state'_def
              elim!: pred_tcb'_weakenE)[1] apply (simp add: StrictC'_thread_state_defs mask_eq_iff_w2p word_size) apply (frule rf_sr_ksCurThread) apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (auto simp: unat_eq_0 le_max_word_ucast_id)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and K (isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) (UNIV \<inter> \<lbrace>ccap_relation cp \<acute>cap\<rbrace> \<inter> \<lbrace>unat \<acute>length___unsigned_long = length args\<rbrace> \<inter> \<lbrace>\<acute>buffer = option_to_ptr buffer\<rbrace>) [] (decodeSetTLSBase args cp >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (Call decodeSetTLSBase_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>buffera length___unsigned_long cap. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q788 buffera length___unsigned_long cap) (?Q'788 buffera length___unsigned_long cap) [SKIP] ((case args of [] \<Rightarrow> throw Fault_H.syscall_error.TruncatedMessage | tls_base # x \<Rightarrow> returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) tls_base) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 2. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q788 buffera length___unsigned_long cap s \<and> s' \<in> ?Q'788 buffera length___unsigned_long cap proof (prove)
goal (3 subgoals):
 1. \<And>buffera length___unsigned_long cap. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R803 buffera length___unsigned_long cap) (?R''805 buffera length___unsigned_long cap) [SKIP] (throw Fault_H.syscall_error.TruncatedMessage >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 3. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> ?R803 buffera length___unsigned_long cap s) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> ?R''805 buffera length___unsigned_long cap} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (3 subgoals):
 1. \<And>buffera length___unsigned_long cap. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = 0; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R803 (option_to_ptr buffer) length___unsigned_long cap) (?R''805 (option_to_ptr buffer) length___unsigned_long cap) [SKIP] (throwError (Inl Fault_H.syscall_error.TruncatedMessage)) (Cond (if length___unsigned_long = 0 then UNIV else {}) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)) SKIP;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 3. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> ?R803 buffera length___unsigned_long cap s) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> ?R''805 buffera length___unsigned_long cap} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (4 subgoals):
 1. \<And>buffera length___unsigned_long cap. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = 0; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'813 (option_to_ptr buffer) length___unsigned_long cap) Cond (if length___unsigned_long = 0 then UNIV else {}) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)) SKIP {},UNIV
 2. \<And>buffera length___unsigned_long cap \<sigma>. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = 0; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} Cond (if length___unsigned_long = 0 then UNIV else {}) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)) SKIP UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.TruncatedMessage) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 3. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 4. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> ?R'813 buffera length___unsigned_long cap} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (3 subgoals):
 1. \<And>buffera length___unsigned_long cap \<sigma>. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = 0; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} Cond (if length___unsigned_long = 0 then UNIV else {}) (\<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)) SKIP UNIV,{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.TruncatedMessage) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 3. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (3 subgoals):
 1. \<And>buffera length___unsigned_long cap \<sigma>. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = 0; ccap_relation cp cap; args = []\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (throwError (Inl Fault_H.syscall_error.TruncatedMessage) \<sigma>). (\<sigma>', globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) (current_syscall_error_' (globals s)))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (globals_update (current_syscall_error_'_update (\<lambda>_. type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) (current_syscall_error_' (globals s)))) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr>)))) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True)}
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 3. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (2 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 buffera length___unsigned_long cap x21 x22) (?R''806 buffera length___unsigned_long cap x21 x22) [SKIP] ((returnOk $ tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (IF length___unsigned_long = 0 THEN
  \<acute>current_syscall_error :== type_C_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_TruncatedMessage) \<acute>current_syscall_error;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR)
FI;;
(\<acute>tls_base :== CALL getSyscallArg_'proc(SCAST(32 signed \<rightarrow> 32) 0,buffera);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned),\<acute>tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))))
 2. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R''806 buffera length___unsigned_long cap x xa}}} proof (prove)
goal (2 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?R804 (option_to_ptr buffer) length___unsigned_long cap x21 x22) (?R'851 (option_to_ptr buffer) length___unsigned_long cap x21 x22) [SKIP] (returnOk (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (\<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer);;
(CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))))
 2. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> ?R804 buffera length___unsigned_long cap x xa s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> ?R'851 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 rv tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = UCAST(32 \<rightarrow> 32) (args ! 0)\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q872 buffera length___unsigned_long cap x21 x22 rv) (?Q'872 buffera length___unsigned_long cap x21 x22 rv tls_base) [SKIP] (returnOk (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) >>= invocationCatch thread isBlocking isCall Invocations_H.invocation.InvokeTCB) (CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr \<acute>ret__unsigned,tls_base);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>?Q872 buffera length___unsigned_long cap x21 x22\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> ?Q'872 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 4. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q872 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()) (?Q'872 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) [SKIP] (do _ <- setThreadState Structures_H.thread_state.Restart thread;
doE reply <- invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE
od) (CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart);;
(\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr \<acute>ret__unsigned,x21);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')))
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>?Q872 buffera length___unsigned_long cap x21 x22\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> ?Q'872 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 4. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1009 buffera length___unsigned_long cap x21 x22 tls_base rv) (?Q'1009 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc) [SKIP] (doE reply <- invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE) (\<acute>ret__unsigned :== CALL cap_thread_cap_get_capTCBPtr_'proc(cap);;
(\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr \<acute>ret__unsigned,x21);;
return_C ret__unsigned_long_'_update ret__unsigned_long_'))
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>?Q1009 buffera length___unsigned_long cap x21 x22 tls_base\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'1009 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s)}
 4. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 6. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1009 buffera length___unsigned_long cap x21 x22 tls_base rv) (?G'1053 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned) [SKIP] (doE reply <- invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21);
if reply = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread reply isCall)
odE) (\<acute>ret__unsigned_long :== CALL invokeSetTLSBase_'proc(tcb_Ptr ret__unsigned,x21);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>?Q1009 buffera length___unsigned_long cap x21 x22 tls_base\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> ?G'1053 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 4. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 6. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (8 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned rva ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); rva = []; id ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned rva) (?Q'1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned rva ret__unsigned_long) [SKIP] (if rva = [] then liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk () else liftE (replyOnRestart thread rva isCall)) (return_C ret__unsigned_long_'_update (\<lambda>s. ret__unsigned_long))
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err) (?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>s. rv'))
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1123 buffera length___unsigned_long cap x21 x22 tls_base rv\<rbrace> invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) \<lbrace>?Q1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>, \<lbrace>?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>
 4. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and ?R1123 buffera length___unsigned_long cap x21 x22 tls_base a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {s. tls_base_'_update (\<lambda>x. x21) (thread_'_update (\<lambda>_. tcb_Ptr v) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>tls_base = x21\<rbrace>} \<inter> {sa. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v rva (ret__unsigned_long_' t))) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate t) \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v err (ret__unsigned_long_' t) (errstate t)))}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 6. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 7. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 8. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (8 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base xfdc ret__unsigned rva ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); rva = []; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1121 (option_to_ptr buffer) length___unsigned_long cap x21 x22 x21 () xfdc (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) []) (?Q'1121 (option_to_ptr buffer) length___unsigned_long cap x21 x22 x21 () xfdc (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) [] (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (liftE (replyOnRestart thread [] isCall) \<sqinter> returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err) (?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>s. rv'))
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1123 buffera length___unsigned_long cap x21 x22 tls_base rv\<rbrace> invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) \<lbrace>?Q1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>, \<lbrace>?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>
 4. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and ?R1123 buffera length___unsigned_long cap x21 x22 tls_base a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {s. tls_base_'_update (\<lambda>x. x21) (thread_'_update (\<lambda>_. tcb_Ptr v) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>tls_base = x21\<rbrace>} \<inter> {sa. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v rva (ret__unsigned_long_' t))) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate t) \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v err (ret__unsigned_long_' t) (errstate t)))}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 6. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 7. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 8. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (8 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base xfdc ret__unsigned rva ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); rva = []; ret__unsigned_long = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q1164 (option_to_ptr buffer) length___unsigned_long cap x21 x21 x22 () xfdc (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) []) (?Q'1166 (option_to_ptr buffer) length___unsigned_long cap x21 x21 x22 () xfdc (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) [] (SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) [SKIP] (returnOk ()) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err) (?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>s. rv'))
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1123 buffera length___unsigned_long cap x21 x22 tls_base rv\<rbrace> invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) \<lbrace>?Q1164 buffera length___unsigned_long cap x21 tls_base x22 rv xfdc ret__unsigned\<rbrace>, \<lbrace>?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>
 4. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and ?R1123 buffera length___unsigned_long cap x21 x22 tls_base a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {s. tls_base_'_update (\<lambda>x. x21) (thread_'_update (\<lambda>_. tcb_Ptr v) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>tls_base = x21\<rbrace>} \<inter> {sa. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'1166 buffera length___unsigned_long cap x21 tls_base x22 rv (xfdc s) v rva (ret__unsigned_long_' t))) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate t) \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v err (ret__unsigned_long_' t) (errstate t)))}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 6. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 7. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 8. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (7 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap); id rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; cintr err (id rv') ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err) (?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned err rv' ret__unsigned_long) [SKIP] (throwError err) (return_C ret__unsigned_long_'_update (\<lambda>s. rv'))
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1123 buffera length___unsigned_long cap x21 x22 tls_base rv\<rbrace> invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>?QE1121 buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and ?R1123 buffera length___unsigned_long cap x21 x22 tls_base a\<rbrace>
 4. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) sa))) \<longrightarrow> sa\<lparr>ret__unsigned_' := v\<rparr> \<in> {sa. sa \<in> {s. tls_base_'_update (\<lambda>x. x21) (thread_'_update (\<lambda>_. tcb_Ptr v) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>tls_base = x21\<rbrace>} \<inter> {sa. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> \<lbrace>id \<^bsup>t\<^esup>ret__unsigned_long = \<^bsup>t\<^esup>ret__unsigned_long \<and> dc rv (K rv \<^bsup>t\<^esup>ret__unsigned_long)\<rbrace>)) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate t) \<longrightarrow> sa\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q''1121 buffera length___unsigned_long cap x21 x22 tls_base rv (xfdc s) v err (ret__unsigned_long_' t) (errstate t)))}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 5. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 6. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 7. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (6 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22 tls_base rv xfdc ret__unsigned. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21; dc rv xfdc; ret__unsigned = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rbrakk> \<Longrightarrow> \<lbrace>?R1123 buffera length___unsigned_long cap x21 x22 tls_base rv\<rbrace> invokeTCB (tcbinvocation.SetTLSBase (capTCBPtr cp) x21) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>err _. True\<rbrace>
 2. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<lbrace>?R1017 (option_to_ptr buffer) length___unsigned_long cap x21 x22 ()\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>a. invs' and ?R1123 buffera length___unsigned_long cap x21 x22 tls_base a\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22 tls_base. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22; tls_base = x21\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v v'. v = cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift (cap_' (cap_'_update (\<lambda>_. cap) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. tls_base_'_update (\<lambda>x. x21) (thread_'_update (\<lambda>_. tcb_Ptr v) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr (capTCBPtr cp)\<rbrace> \<inter> \<lbrace>\<acute>tls_base = x21\<rbrace>} \<inter> {s. \<forall>t. (id (ret__unsigned_long_' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rva. rva = [] \<longrightarrow> s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> \<lbrace>id \<^bsup>t\<^esup>ret__unsigned_long = \<^bsup>t\<^esup>ret__unsigned_long \<and> dc rv (K rv \<^bsup>t\<^esup>ret__unsigned_long)\<rbrace>)) \<and> (id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. cintr err (id (ret__unsigned_long_' t)) (errstate t) \<longrightarrow> s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. id (ret__unsigned_long_' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> (intr_and_se_rel \<circ> Inr) err (id (ret__unsigned_long_' t)) (errstate s)}))}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. cap) s)) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap}}
 4. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and ?R1017 buffera length___unsigned_long cap x21 x22 a\<rbrace>
 5. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 6. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (4 subgoals):
 1. \<And>length___unsigned_long cap x21 x22. \<lbrakk>unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'1010 (option_to_ptr buffer) length___unsigned_long cap x21 x22 () x21) CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) {s. s\<lparr>ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {}) \<and> s \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {})}
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> True \<and> True)\<rbrace>
 3. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'1010 buffera length___unsigned_long cap x21 x22 rv (tls_base_' s)}
 4. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (3 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<lbrace>?R880 (option_to_ptr buffer) length___unsigned_long cap x21 x22\<rbrace> return () \<lbrace>\<lambda>a. (\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> True \<and> True)\<rbrace>
 2. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s. \<forall>t. s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {}) \<and> s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {})}}
 3. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ?R880 buffera length___unsigned_long cap x xa) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (2 subgoals):
 1. \<And>buffera length___unsigned_long cap x21 x22. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = Suc (length x22); ccap_relation cp cap; args = x21 # x22\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'873 (option_to_ptr buffer) length___unsigned_long cap x21 x22) \<acute>tls_base :== CALL getSyscallArg_'proc(0,option_to_ptr buffer) {s. \<forall>rv. tls_base_' s = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) ThreadState_Restart) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s. \<forall>t. s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {}) \<and> s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {})}}
 2. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> True \<and> True))) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> ?R'873 buffera length___unsigned_long cap x xa \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (1 subgoal):
 1. \<And>buffera length___unsigned_long cap s s'. \<lbrakk>buffera = option_to_ptr buffer; unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; (invs' and sch_act_simple and (\<lambda>s. ksCurThread s = thread) and ct_active' and (\<lambda>y. isThreadCap cp) and valid_cap' cp and (\<lambda>s. \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s) and sysargs_rel args buffer) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((args = [] \<longrightarrow> True) \<and> (\<forall>x xa. args = x # xa \<longrightarrow> (sysargs_rel args buffer and sysargs_rel_n args buffer 0 and ((\<lambda>a. tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> valid_tcb_state' Structures_H.thread_state.Restart a \<and> (ksSchedulerAction a = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (\<forall>p. thread \<in> set (ksReadyQueues a p) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> sch_act_wf (ksSchedulerAction a) a) and (\<lambda>a. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') a \<and> True \<and> True))) s)) \<and> s' \<in> {s. args = [] \<longrightarrow> s \<in> UNIV \<inter> {s. (s \<in> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> True) \<and> (s \<notin> (if length___unsigned_long = 0 then UNIV else {}) \<longrightarrow> False)}} \<inter> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. args = x # xa \<longrightarrow> s \<in> {s. ipc_buffer_'_update (\<lambda>_. buffera) (i_'_update (\<lambda>_. 0) s) \<in> UNIV \<inter> \<lbrace>unat \<acute>i = 0\<rbrace> \<inter> \<lbrace>\<acute>ipc_buffer = buffera\<rbrace>} \<inter> {s. (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> 0 < SCAST(32 signed \<rightarrow> 32) 4 \<longrightarrow> kernel_all_global_addresses.msgRegisters.[unat 0] < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[unat 0])] = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> (\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4\<rparr>, fl)) \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. s\<lparr>tls_base_' := UCAST(32 \<rightarrow> 32) (args ! 0), globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {}) \<and> s\<lparr>tls_base_' := UCAST(32 \<rightarrow> 32) (args ! 0), globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {}))) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion' buffera (uint (0 + SCAST(32 signed \<rightarrow> 32) 1)) False (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> s \<Turnstile>\<^sub>c (buffera +\<^sub>p uint (0 + SCAST(32 signed \<rightarrow> 32) 1)) \<longrightarrow> ptr_add_assertion' buffera (uint (0 + SCAST(32 signed \<rightarrow> 32) 1)) True (hrs_htd (t_hrs_' (globals s))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s))) (buffera +\<^sub>p uint (0 + SCAST(32 signed \<rightarrow> 32) 1)) = UCAST(32 \<rightarrow> 32) (args ! 0) \<longrightarrow> (\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Restart (cl\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4\<rparr>, fl)) \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. s\<lparr>tls_base_' := UCAST(32 \<rightarrow> 32) (args ! 0), globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>, ret__unsigned_' := cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)\<rparr> \<in> (if tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) then UNIV else {}) \<and> s\<lparr>tls_base_' := UCAST(32 \<rightarrow> 32) (args ! 0), globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), ksSchedulerAction_' := ksSchedulerAction_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr> \<in> (if cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap then UNIV else {})))} \<inter> - \<lbrace>length___unsigned_long = 0\<rbrace>}}} proof (prove)
goal (1 subgoal):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> (\<forall>x xa. args = x # xa \<longrightarrow> sysargs_rel (x # xa) buffer s \<and> sysargs_rel_n (x # xa) buffer 0 s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s)) \<and> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> \<forall>x xa. args = x # xa \<longrightarrow> sysargs_rel (x # xa) buffer s \<and> sysargs_rel_n (x # xa) buffer 0 s \<and> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s)
 2. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (2 subgoals):
 1. \<And>length___unsigned_long cap s s' x xa. \<lbrakk>unat length___unsigned_long = Suc (length xa); ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; st_tcb_at' active' (ksCurThread s) s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel (x # xa) buffer s; args = x # xa\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> sch_act_wf (ksSchedulerAction s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s)
 2. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<and> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; ccap_relation cp cap; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; isThreadCap cp; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c ksCurThread_' (globals s') \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(ksCurThread_' (globals s')\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>length___unsigned_long cap s s'. \<lbrakk>unat length___unsigned_long = length args; (s, s') \<in> rf_sr; invs' s; sch_act_simple s; thread = ksCurThread s; ct_active' s; cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap; valid_cap' cp s; \<forall>x\<in>zobj_refs' cp. ex_nonz_cap_to' x s; sysargs_rel args buffer s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); cp = capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap))))\<rbrakk> \<Longrightarrow> (args = [] \<longrightarrow> length___unsigned_long = 0) \<and> (\<forall>x. (\<exists>xa. args = x # xa) \<longrightarrow> (0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> kernel_all_global_addresses.msgRegisters.[0] < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr (ksCurThread s) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])).[unat (kernel_all_global_addresses.msgRegisters.[0])] = x \<longrightarrow> tcb_ptr_to_ctcb_ptr (ksCurThread s) = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> SCAST(32 signed \<rightarrow> 32) cap_thread_cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> (\<not> 0 < SCAST(32 signed \<rightarrow> 32) n_msgRegisters \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 False (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> s' \<Turnstile>\<^sub>c (option_to_ptr buffer +\<^sub>p 1) \<longrightarrow> ptr_add_assertion (option_to_ptr buffer) 1 True (hrs_htd (t_hrs_' (globals s'))) \<longrightarrow> h_val (hrs_mem (t_hrs_' (globals s'))) (option_to_ptr buffer +\<^sub>p 1) = x \<longrightarrow> tcb_ptr_to_ctcb_ptr (ksCurThread s) = tcb_ptr_to_ctcb_ptr (ksCurThread s) \<and> tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap)) = tcb_ptr_to_ctcb_ptr (capTCBPtr cp) \<and> SCAST(32 signed \<rightarrow> 32) cap_thread_cap = SCAST(32 signed \<rightarrow> 32) cap_thread_cap) \<and> length___unsigned_long \<noteq> 0) proof (prove)
goal:
No subgoals!