theory VSpace_C

lemma setMessageInfo_ccorres:
  "ccorres dc xfdc (tcb_at' thread)
           (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs
           (setMessageInfo thread mi)
           (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo(mi');;
            CALL setRegister(tcb_ptr_to_ctcb_ptr thread, scast Kernel_C.msgInfoRegister, \<acute>ret__unsigned_long))" unfolding setMessageInfo_def apply (rule ccorres_guard_imp2) apply ctac apply simp apply (ctac add: setRegister_ccorres) apply wp apply vcg apply (simp add: ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
                   Kernel_C.msgInfoRegister_def Kernel_C.R1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs (setMessageInfo thread mi) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi');;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread) (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs (do x <- return (wordFromMessageInfo mi);
asUser thread $ setRegister TCB_H.msgInfoRegister x
od) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi');;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q ?Q' hs (do x <- return (wordFromMessageInfo mi);
asUser thread $ setRegister TCB_H.msgInfoRegister x
od) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi');;
CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> ?Q' proof (prove)
goal (4 subgoals):
 1. \<And>rv ret__unsigned_long. rv = ret__unsigned_long \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 rv ret__unsigned_long) hs (asUser thread $ setRegister TCB_H.msgInfoRegister rv) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,ret__unsigned_long))
 2. \<lbrace>?R5\<rbrace> return (wordFromMessageInfo mi) \<lbrace>?Q5\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'5 \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi') {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'5 rv (ret__unsigned_long_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. mi_'_update (\<lambda>_. mi') s \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'5 proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres dc xfdc (?Q5 rv) (?Q'5 rv rv) hs (asUser thread (setRegister TCB_H.msgInfoRegister rv)) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,rv))
 2. \<lbrace>?R5\<rbrace> return (wordFromMessageInfo mi) \<lbrace>?Q5\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'5 \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi') {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'5 rv (ret__unsigned_long_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. mi_'_update (\<lambda>_. mi') s \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'5 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R5\<rbrace> return (wordFromMessageInfo mi) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'5 \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi') {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace> \<inter> \<lbrace>\<acute>w = \<^bsup>s\<^esup>ret__unsigned_long\<rbrace>}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R5) s \<and> s' \<in> {s. mi_'_update (\<lambda>_. mi') s \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'5 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'5 \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(mi') {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace> \<inter> \<lbrace>\<acute>w = \<^bsup>s\<^esup>ret__unsigned_long\<rbrace>}}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s \<and> s' \<in> {s. mi_'_update (\<lambda>_. mi') s \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'5 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; s' \<in> UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s \<and> s' \<in> {s. mi_'_update (\<lambda>_. mi') s \<in> \<lbrace>mi = message_info_to_H \<acute>mi\<rbrace>} \<inter> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift mi') << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift mi') << 9) || (extraCaps_CL (seL4_MessageInfo_lift mi') << 7) || length_CL (seL4_MessageInfo_lift mi') \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister = register_from_H TCB_H.msgInfoRegister\<rbrace> proof (prove)
goal:
No subgoals!