theory Ipc_C

lemma replyFromKernel_success_empty_ccorres [corres]:
  "ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
     (replyFromKernel thread (0, []))
     (Call replyFromKernel_success_empty_'proc)" apply (subst replyFromKernel_success_empty) apply (cinit lift: thread_') apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_lookupIPCBuffer]) apply (ctac add: setRegister_ccorres) apply (unfold setMessageInfo_def) apply csymbr apply ctac apply (simp only: fun_app_def) apply (ctac add: setRegister_ccorres) apply wp apply vcg apply wp apply vcg apply wp+ apply (simp add: ARM_H.msgInfoRegister_def ARM.msgInfoRegister_def
                   Kernel_C.msgInfoRegister_def Kernel_C.R1_def
                   ARM_H.badgeRegister_def ARM.badgeRegister_def
                   Kernel_C.badgeRegister_def Kernel_C.R0_def
                   message_info_to_H_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs (replyFromKernel thread (0, [])) (Call replyFromKernel_success_empty_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs (replyFromKernel_success_empty thread) (Call replyFromKernel_success_empty_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q114 threada) (?Q'114 threada) (SKIP # hs) (do y <- lookupIPCBuffer True thread;
y <- asUser thread (setRegister Notification_H.badgeRegister 0);
setMessageInfo thread (Types_H.message_info.MI 0 0 0 0)
od) (CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))
 2. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> ?Q'114 threada proof (prove)
goal (4 subgoals):
 1. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q120 threada y) (?Q'120 threada y) (SKIP # hs) (do y <- asUser thread (setRegister Notification_H.badgeRegister 0);
setMessageInfo thread (Types_H.message_info.MI 0 0 0 0)
od) (CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))))
 2. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>?Q120 threada\<rbrace>
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q120 threada rv s \<longrightarrow> s' \<in> ?Q'120 threada rv} proof (prove)
goal (6 subgoals):
 1. \<And>threada y rv xfdca. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 threada y rv) (?Q'130 threada y rv xfdca) (SKIP # hs) (setMessageInfo thread (Types_H.message_info.MI 0 0 0 0)) (\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))
 2. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>?Q130 threada y\<rbrace>
 3. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 threada y rv (xfdc s)}
 4. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (6 subgoals):
 1. \<And>threada y rv xfdca. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 threada y rv) (?Q'130 threada y rv xfdca) (SKIP # hs) (do x <- return (wordFromMessageInfo (Types_H.message_info.MI 0 0 0 0));
asUser thread $ setRegister TCB_H.msgInfoRegister x
od) (\<acute>ret__struct_seL4_MessageInfo_C :== CALL seL4_MessageInfo_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) 0);;
(\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(\<acute>ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long)))
 2. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>?Q130 threada y\<rbrace>
 3. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'130 threada y rv (xfdc s)}
 4. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (6 subgoals):
 1. \<And>threada y rv xfdca ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q130 threada y rv) (?G'157 threada y rv xfdca ret__struct_seL4_MessageInfo_C) (SKIP # hs) (do x <- return (wordFromMessageInfo (Types_H.message_info.MI 0 0 0 0));
asUser thread $ setRegister TCB_H.msgInfoRegister x
od) (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C);;
CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,\<acute>ret__unsigned_long))
 2. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>?Q130 threada y\<rbrace>
 3. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> ?G'157 threada y rv (xfdc s) v}}
 4. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (8 subgoals):
 1. \<And>threada y rv xfdca ret__struct_seL4_MessageInfo_C rva ret__unsigned_long. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>; rva = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 threada y rv xfdca ret__struct_seL4_MessageInfo_C rva) (?Q'223 threada y rv xfdca ret__struct_seL4_MessageInfo_C rva ret__unsigned_long) (SKIP # hs) (asUser thread $ setRegister TCB_H.msgInfoRegister rva) (CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,ret__unsigned_long))
 2. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R225 threada y rv\<rbrace> return (wordFromMessageInfo (Types_H.message_info.MI 0 0 0 0)) \<lbrace>?Q223 threada y rv xfdc ret__struct_seL4_MessageInfo_C\<rbrace>
 3. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C) \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C) {s. \<forall>rva. rva = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C rva (ret__unsigned_long_' s)}
 4. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R225 threada y rv\<rbrace>
 5. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'223 threada y rv (xfdc s) v}}
 6. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (8 subgoals):
 1. \<And>threada y rv xfdca ret__struct_seL4_MessageInfo_C rva ret__unsigned_long. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdca; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>; rva = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q223 (tcb_ptr_to_ctcb_ptr thread) y rv xfdca ret__struct_seL4_MessageInfo_C ret__unsigned_long) (?Q'223 (tcb_ptr_to_ctcb_ptr thread) y rv xfdca ret__struct_seL4_MessageInfo_C ret__unsigned_long ret__unsigned_long) (SKIP # hs) (asUser thread (setRegister TCB_H.msgInfoRegister ret__unsigned_long)) (CALL setRegister_'proc(tcb_ptr_to_ctcb_ptr thread,SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister,ret__unsigned_long))
 2. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R225 threada y rv\<rbrace> return (wordFromMessageInfo (Types_H.message_info.MI 0 0 0 0)) \<lbrace>?Q223 threada y rv xfdc ret__struct_seL4_MessageInfo_C\<rbrace>
 3. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C) \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C) {s. \<forall>rva. rva = ret__unsigned_long_' s \<longrightarrow> s \<in> ?Q'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C rva (ret__unsigned_long_' s)}
 4. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R225 threada y rv\<rbrace>
 5. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'223 threada y rv (xfdc s) v}}
 6. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 8. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (7 subgoals):
 1. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<lbrace>?R225 threada y rv\<rbrace> return (wordFromMessageInfo (Types_H.message_info.MI 0 0 0 0)) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C) \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C) {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>_. threada) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<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>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R225 threada y rv\<rbrace>
 4. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'223 threada y rv (xfdc s) v}}
 5. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 7. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (6 subgoals):
 1. \<And>threada y rv xfdc ret__struct_seL4_MessageInfo_C. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; dc rv xfdc; seL4_MessageInfo_lift ret__struct_seL4_MessageInfo_C = \<lparr>label_CL = 0, capsUnwrapped_CL = 0, extraCaps_CL = 0, length_CL = 0\<rparr>\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'223 threada y rv xfdc ret__struct_seL4_MessageInfo_C) \<acute>ret__unsigned_long :== CALL wordFromMessageInfo_'proc(ret__struct_seL4_MessageInfo_C) {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>_. threada) sa)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = threada\<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>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 3. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {sa. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) sa)))) && mask 7\<rparr> \<longrightarrow> sa\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> ?R'223 threada y rv (xfdc s) v}}
 4. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 6. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (5 subgoals):
 1. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R130 threada y\<rbrace> asUser thread (setRegister Notification_H.badgeRegister 0) \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>a. True)\<rbrace>
 2. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift v) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift v) << 9) || (extraCaps_CL (seL4_MessageInfo_lift v) << 7) || length_CL (seL4_MessageInfo_lift v) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister = register_from_H TCB_H.msgInfoRegister\<rbrace>}}
 3. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and ?R130 threada y\<rbrace>
 5. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and ?R130 threada rv) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (4 subgoals):
 1. \<And>threada y. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'130 threada y) CALL setRegister_'proc(threada,SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister,SCAST(32 signed \<rightarrow> 32) 0) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. \<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = label_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 20, capsUnwrapped_CL = capsUnwrapped_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 3, extraCaps_CL = extraCaps_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 2, length_CL = length_' (length_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (extraCaps_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (capsUnwrapped_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (label_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) s)))) && mask 7\<rparr> \<longrightarrow> s\<lparr>ret__struct_seL4_MessageInfo_C_' := v\<rparr> \<in> {s. mi_'_update (\<lambda>_. v) s \<in> \<lbrace>Types_H.message_info.MI 0 0 0 0 = message_info_to_H \<acute>mi\<rbrace>} \<inter> \<lbrace>\<forall>t. \<^bsup>t\<^esup>ret__unsigned_long = (label_CL (seL4_MessageInfo_lift v) << 12) || (capsUnwrapped_CL (seL4_MessageInfo_lift v) << 9) || (extraCaps_CL (seL4_MessageInfo_lift v) << 7) || length_CL (seL4_MessageInfo_lift v) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister = register_from_H TCB_H.msgInfoRegister\<rbrace>}}
 2. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>s. True \<and> True)\<rbrace>
 4. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> ?R'130 threada rv} proof (prove)
goal (3 subgoals):
 1. \<And>threada s. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>threada. threada = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Q114 threada\<rbrace> lookupIPCBuffer True thread \<lbrace>\<lambda>y. (\<lambda>_. True) and (\<lambda>s. True \<and> True)\<rbrace>
 3. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q114 threada s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c threada \<longrightarrow> (\<forall>rv. dc rv (xfdc (s\<lparr>globals := t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister)) (SCAST(32 signed \<rightarrow> 32) 0)))) (globals s)\<rparr>)) \<longrightarrow> (\<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> \<longrightarrow> Types_H.message_info.MI 0 0 0 0 = message_info_to_H v \<and> (\<forall>t. ret__unsigned_long_' t = (label_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 12) || (capsUnwrapped_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 9) || (extraCaps_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 7) || length_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister = register_from_H TCB_H.msgInfoRegister)))}} proof (prove)
goal (1 subgoal):
 1. \<And>threada s s'. \<lbrakk>threada = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s \<longrightarrow> s' \<in> {s. w_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) 0) (reg_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister) (thread_'_update (\<lambda>_. threada) s)) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H Notification_H.badgeRegister\<rbrace> \<inter> \<lbrace>\<acute>w = 0\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c threada \<longrightarrow> (\<forall>rv. dc rv (xfdc (s\<lparr>globals := t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(threada\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat (SCAST(32 signed \<rightarrow> 32) Kernel_C.badgeRegister)) (SCAST(32 signed \<rightarrow> 32) 0)))) (globals s)\<rparr>)) \<longrightarrow> (\<forall>v. seL4_MessageInfo_lift v = \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> \<longrightarrow> Types_H.message_info.MI 0 0 0 0 = message_info_to_H v \<and> (\<forall>t. ret__unsigned_long_' t = (label_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 12) || (capsUnwrapped_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 9) || (extraCaps_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> << 7) || length_CL \<lparr>label_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 20, capsUnwrapped_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 3, extraCaps_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 2, length_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 7\<rparr> \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.msgInfoRegister = register_from_H TCB_H.msgInfoRegister)))}} proof (prove)
goal:
No subgoals!