theory Ipc_C

lemma getMessageInfo_ccorres':
  "ccorres (\<lambda>r r'. r = message_info_to_H r') tag_'
           (tcb_at' sender) UNIV hs (getMessageInfo sender)
           (\<acute>ret__unsigned_long :== CALL getRegister(tcb_ptr_to_ctcb_ptr sender,scast Kernel_C.msgInfoRegister);;
            \<acute>tag :== CALL messageInfoFromWord(\<acute>ret__unsigned_long))" unfolding getMessageInfo_def apply simp apply (rule ccorres_guard_imp2) apply ctac apply ctac apply wp apply vcg apply (frule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
    Kernel_C.msgInfoRegister_def Kernel_C.R1_def dest!: c_guard_clift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = message_info_to_H r') tag_' (tcb_at' sender) UNIV hs (getMessageInfo sender) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
\<acute>tag :== CALL messageInfoFromWord_'proc(\<acute>ret__unsigned_long)) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = message_info_to_H r') tag_' (tcb_at' sender) UNIV hs (do x <- asUser sender $ getRegister TCB_H.msgInfoRegister;
return $ messageInfoFromWord x
od) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
\<acute>tag :== CALL messageInfoFromWord_'proc(\<acute>ret__unsigned_long)) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = message_info_to_H r') tag_' (tcb_at' sender) UNIV hs (do x <- asUser sender (getRegister TCB_H.msgInfoRegister);
return (messageInfoFromWord x)
od) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
\<acute>tag :== CALL messageInfoFromWord_'proc(\<acute>ret__unsigned_long)) proof (prove)
goal (2 subgoals):
 1. ccorres (\<lambda>r r'. r = message_info_to_H r') tag_' ?Q6 ?Q'6 hs (do x <- asUser sender (getRegister TCB_H.msgInfoRegister);
return (messageInfoFromWord x)
od) (\<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister);;
\<acute>tag :== CALL messageInfoFromWord_'proc(\<acute>ret__unsigned_long))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q6 s \<and> s' \<in> ?Q'6 proof (prove)
goal (4 subgoals):
 1. \<And>rv ret__unsigned_long. rv = ret__unsigned_long \<Longrightarrow> ccorres (\<lambda>r r'. r = message_info_to_H r') tag_' (?Q11 rv) (?Q'11 rv ret__unsigned_long) hs (return (messageInfoFromWord rv)) (\<acute>tag :== CALL messageInfoFromWord_'proc(ret__unsigned_long))
 2. \<lbrace>?R11\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>?Q11\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'11 \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'11 rv (ret__unsigned_long_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>} \<inter> ?R'11 proof (prove)
goal (3 subgoals):
 1. \<lbrace>?R11\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'11 \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) sa \<in> \<lbrace>\<acute>w = rv\<rbrace>}}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R11) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>} \<inter> ?R'11 proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> ?R'11 \<acute>ret__unsigned_long :== CALL getRegister_'proc(tcb_ptr_to_ctcb_ptr sender,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) {s. \<forall>rv. rv = ret__unsigned_long_' s \<longrightarrow> s \<in> {sa. w_'_update (\<lambda>_. ret__unsigned_long_' s) sa \<in> \<lbrace>\<acute>w = rv\<rbrace>}}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>} \<inter> ?R'11 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' sender s; s' \<in> UNIV; \<exists>ko ko'. ko_at' ko sender s \<and> True \<and> cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s \<and> s' \<in> {s. reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister) (thread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr sender) s) \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H TCB_H.msgInfoRegister\<rbrace>} \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!