theory Ipc_R

lemma doFaultTransfer_corres:
  "corres dc
    (obj_at (\<lambda>ko. \<exists>tcb ft. ko = TCB tcb \<and> tcb_fault tcb = Some ft) sender
     and tcb_at receiver and case_option \<top> in_user_frame recv_buf)
    (tcb_at' sender and tcb_at' receiver and
     case_option \<top> valid_ipc_buffer_ptr' recv_buf)
    (do_fault_transfer badge sender receiver recv_buf)
    (doFaultTransfer badge sender receiver recv_buf)" apply (clarsimp simp: do_fault_transfer_def doFaultTransfer_def split_def
                        ARM_H.badgeRegister_def badge_register_def) apply (rule_tac Q="\<lambda>fault. K (\<exists>f. fault = Some f) and
                             tcb_at sender and tcb_at receiver and
                             case_option \<top> in_user_frame recv_buf"
              and Q'="\<lambda>fault'. tcb_at' sender and tcb_at' receiver and
                               case_option \<top> valid_ipc_buffer_ptr' recv_buf"
               in corres_underlying_split) apply (rule corres_guard_imp) apply (rule threadget_fault_corres) apply (clarsimp simp: obj_at_def is_tcb)+ apply (rule corres_assume_pre) apply (fold assert_opt_def | unfold haskell_fail_def)+ apply (rule corres_assert_opt_assume) apply (clarsimp split: option.splits
                      simp: fault_rel_optionation_def assert_opt_def
                            map_option_case) defer defer apply (clarsimp simp: fault_rel_optionation_def) apply (wp thread_get_wp) apply (clarsimp simp: obj_at_def is_tcb) apply wp apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF makeFaultMessage_corres]) apply (rule corres_split_eqr[OF setMRs_corres [OF refl]]) apply (rule corres_split_nor[OF setMessageInfo_corres]) apply simp apply (rule asUser_setRegister_corres) apply (wp | simp)+ apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF makeFaultMessage_corres]) apply (rule corres_split_eqr[OF setMRs_corres [OF refl]]) apply (rule corres_split_nor[OF setMessageInfo_corres]) apply simp apply (rule asUser_setRegister_corres) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (obj_at (\<lambda>ko. \<exists>tcb ft. ko = TCB tcb \<and> tcb_fault tcb = Some ft) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do_fault_transfer badge sender receiver recv_buf) (doFaultTransfer badge sender receiver recv_buf) proof (prove)
goal (1 subgoal):
 1. corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do fault <- thread_get tcb_fault sender;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do fault <- threadGet tcbFault sender;
f <- case fault of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (4 subgoals):
 1. corres ?r'4 (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (thread_get tcb_fault sender) (threadGet tcbFault sender)
 2. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres dc (K (\<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do f <- case rv of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- case rv' of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 3. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 4. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (6 subgoals):
 1. corres ?r'4 ?Q6 ?Q'6 (thread_get tcb_fault sender) (threadGet tcbFault sender)
 2. \<And>s. (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> ?Q6 s
 3. \<And>s. (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> ?Q'6 s
 4. \<And>rv rv'. ?r'4 rv rv' \<Longrightarrow> corres dc (K (\<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do f <- case rv of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- case rv' of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 5. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 6. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s. (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> tcb_at sender s
 2. \<And>s. (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s \<Longrightarrow> tcb_at' sender s
 3. \<And>rv rv'. fault_rel_optionation rv rv' \<Longrightarrow> corres dc (K (\<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (do f <- case rv of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- case rv' of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 4. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 5. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. fault_rel_optionation rv rv' \<Longrightarrow> corres dc ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do f <- case rv of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- case rv' of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 3. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s s'. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do f <- case rv of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- case rv' of None \<Rightarrow> fail | Some f \<Rightarrow> return f;
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 3. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' s s'. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do f <- assert_opt rv;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do f <- assert_opt rv';
p <- makeFaultMessage f sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 3. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' s s' x. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation; rv' = Some x\<rbrakk> \<Longrightarrow> corres dc ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) (do f <- assert_opt rv;
p <- make_fault_msg f sender;
sent <- set_mrs receiver recv_buf (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage x sender;
sent <- setMRs receiver recv_buf (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>rv rv' s s' sa. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) sa\<rbrakk> \<Longrightarrow> rv' \<noteq> None
 3. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 4. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 3. \<And>rv rv' s s' sa. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) sa\<rbrakk> \<Longrightarrow> rv' \<noteq> None
 4. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 5. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>rv rv' s s' sa. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) sa\<rbrakk> \<Longrightarrow> rv' \<noteq> None
 3. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 4. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 5. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' s s' sa. \<lbrakk>fault_rel_optionation rv rv'; ((\<lambda>y. \<exists>f. rv = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) s'; (s, s') \<in> state_relation; (tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)) sa\<rbrakk> \<Longrightarrow> rv' \<noteq> None
 2. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 3. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 4. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 5. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (4 subgoals):
 1. \<lbrace>obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)\<rbrace> thread_get tcb_fault sender \<lbrace>\<lambda>fault. K (\<exists>f. fault = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)\<rbrace>
 2. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 3. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 4. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s. (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (\<exists>ft. tcb_fault tcb = Some ft)) sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> in_user_frame x2)) s \<Longrightarrow> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> (K (\<exists>f. tcb_fault tcb = Some f) and tcb_at sender and tcb_at receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x)) s) sender s
 2. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 3. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 4. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (3 subgoals):
 1. \<lbrace>tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x2 \<Rightarrow> valid_ipc_buffer_ptr' x2)\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>fault'. tcb_at' sender and tcb_at' receiver and (case recv_buf of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)\<rbrace>
 2. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 3. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver) (tcb_at' sender and tcb_at' receiver) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (?Q110 s s' x2) (?Q'110 s s' x2) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> ?Q110 s s' x2 sa
 3. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> ?Q'110 s s' x2 sa
 4. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (6 subgoals):
 1. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (?R114 s s' x2 p) (?R'114 s s' x2 p) (do sent <- set_mrs receiver None (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do sent <- setMRs receiver None (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q114 s s' x2\<rbrace> make_fault_msg x2 sender \<lbrace>?R114 s s' x2\<rbrace>
 3. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 s s' x2\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>?R'114 s s' x2\<rbrace>
 4. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q114 s s' x2) sa
 5. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'114 s s' x2) sa
 6. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (8 subgoals):
 1. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (?R119 s s' x2 p sent) (?R'119 s s' x2 p sent) (do y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q119 s s' x2 p\<rbrace> set_mrs receiver None (snd p) \<lbrace>?R119 s s' x2 p\<rbrace>
 3. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'119 s s' x2 p\<rbrace> setMRs receiver None (snd p) \<lbrace>?R'119 s s' x2 p\<rbrace>
 4. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q114 s s' x2\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q119 s s' x2 p\<rbrace>
 5. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 s s' x2\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'119 s s' x2 p\<rbrace>
 6. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q114 s s' x2) sa
 7. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'114 s s' x2) sa
 8. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (11 subgoals):
 1. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> Types_H.message_info.MI sent 0 0 (fst p) = message_info_map (Structures_A.message_info.MI sent 0 0 (fst p))
 2. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (?R125 s s' x2 p sent) (?R'125 s s' x2 p sent) (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 3. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q125 s s' x2 p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R125 s s' x2 p sent\<rbrace>
 4. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'125 s s' x2 p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R'125 s s' x2 p sent\<rbrace>
 5. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q119 s s' x2 p\<rbrace> set_mrs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q125 s s' x2 p sent\<rbrace>
 6. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'119 s s' x2 p\<rbrace> setMRs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'125 s s' x2 p sent\<rbrace>
 7. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q114 s s' x2\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q119 s s' x2 p\<rbrace>
 8. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 s s' x2\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'119 s s' x2 p\<rbrace>
 9. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q114 s s' x2) sa
 10. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'114 s s' x2) sa
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> corres dc (?R125 s s' x2 p sent) (?R'125 s s' x2 p sent) (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 2. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q125 s s' x2 p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R125 s s' x2 p sent\<rbrace>
 3. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'125 s s' x2 p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R'125 s s' x2 p sent\<rbrace>
 4. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q119 s s' x2 p\<rbrace> set_mrs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q125 s s' x2 p sent\<rbrace>
 5. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'119 s s' x2 p\<rbrace> setMRs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'125 s s' x2 p sent\<rbrace>
 6. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q114 s s' x2\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q119 s s' x2 p\<rbrace>
 7. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 s s' x2\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'119 s s' x2 p\<rbrace>
 8. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q114 s s' x2) sa
 9. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'114 s s' x2) sa
 10. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (9 subgoals):
 1. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q125 s s' x2 p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. tcb_at receiver\<rbrace>
 2. \<And>s s' x2 p sent. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'125 s s' x2 p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. tcb_at' receiver\<rbrace>
 3. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q119 s s' x2 p\<rbrace> set_mrs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q125 s s' x2 p sent\<rbrace>
 4. \<And>s s' x2 p. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'119 s s' x2 p\<rbrace> setMRs receiver None (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'125 s s' x2 p sent\<rbrace>
 5. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q114 s s' x2\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q119 s s' x2 p\<rbrace>
 6. \<And>s s' x2. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 s s' x2\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case None of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'119 s s' x2 p\<rbrace>
 7. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at sender and tcb_at receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q114 s s' x2) sa
 8. \<And>s s' x2 sa. \<lbrakk>tcb_at receiver s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = None; (tcb_at' sender and tcb_at' receiver) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'114 s s' x2) sa
 9. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (tcb_at sender and tcb_at receiver and in_user_frame x2a) (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (?Q156 s s' x2 x2a) (?Q'156 s s' x2 x2a) (do p <- make_fault_msg x2 sender;
sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do p <- makeFaultMessage (fault_map x2) sender;
sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> ?Q156 s s' x2 x2a sa
 3. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> ?Q'156 s s' x2 x2a sa proof (prove)
goal (5 subgoals):
 1. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (?R160 s s' x2 x2a p) (?R'160 s s' x2 x2a p) (do sent <- set_mrs receiver (Some x2a) (snd p);
y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do sent <- setMRs receiver (Some x2a) (snd p);
y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 s s' x2 x2a\<rbrace> make_fault_msg x2 sender \<lbrace>?R160 s s' x2 x2a\<rbrace>
 3. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'160 s s' x2 x2a\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>?R'160 s s' x2 x2a\<rbrace>
 4. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q160 s s' x2 x2a) sa
 5. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'160 s s' x2 x2a) sa proof (prove)
goal (7 subgoals):
 1. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (?R165 s s' x2 x2a p sent) (?R'165 s s' x2 x2a p sent) (do y <- set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p));
as_user receiver (setRegister ARM.badgeRegister badge)
od) (do y <- setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p));
asUser receiver (setRegister ARM.badgeRegister badge)
od)
 2. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q165 s s' x2 x2a p\<rbrace> set_mrs receiver (Some x2a) (snd p) \<lbrace>?R165 s s' x2 x2a p\<rbrace>
 3. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'165 s s' x2 x2a p\<rbrace> setMRs receiver (Some x2a) (snd p) \<lbrace>?R'165 s s' x2 x2a p\<rbrace>
 4. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 s s' x2 x2a\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q165 s s' x2 x2a p\<rbrace>
 5. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'160 s s' x2 x2a\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'165 s s' x2 x2a p\<rbrace>
 6. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q160 s s' x2 x2a) sa
 7. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'160 s s' x2 x2a) sa proof (prove)
goal (10 subgoals):
 1. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> Types_H.message_info.MI sent 0 0 (fst p) = message_info_map (Structures_A.message_info.MI sent 0 0 (fst p))
 2. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (?R171 s s' x2 x2a p sent) (?R'171 s s' x2 x2a p sent) (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 3. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 s s' x2 x2a p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R171 s s' x2 x2a p sent\<rbrace>
 4. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'171 s s' x2 x2a p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R'171 s s' x2 x2a p sent\<rbrace>
 5. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q165 s s' x2 x2a p\<rbrace> set_mrs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q171 s s' x2 x2a p sent\<rbrace>
 6. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'165 s s' x2 x2a p\<rbrace> setMRs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'171 s s' x2 x2a p sent\<rbrace>
 7. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 s s' x2 x2a\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q165 s s' x2 x2a p\<rbrace>
 8. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'160 s s' x2 x2a\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'165 s s' x2 x2a p\<rbrace>
 9. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q160 s s' x2 x2a) sa
 10. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'160 s s' x2 x2a) sa proof (prove)
goal (9 subgoals):
 1. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> corres dc (?R171 s s' x2 x2a p sent) (?R'171 s s' x2 x2a p sent) (as_user receiver (setRegister ARM.badgeRegister badge)) (asUser receiver (setRegister ARM.badgeRegister badge))
 2. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 s s' x2 x2a p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R171 s s' x2 x2a p sent\<rbrace>
 3. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'171 s s' x2 x2a p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. ?R'171 s s' x2 x2a p sent\<rbrace>
 4. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q165 s s' x2 x2a p\<rbrace> set_mrs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q171 s s' x2 x2a p sent\<rbrace>
 5. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'165 s s' x2 x2a p\<rbrace> setMRs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'171 s s' x2 x2a p sent\<rbrace>
 6. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 s s' x2 x2a\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q165 s s' x2 x2a p\<rbrace>
 7. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'160 s s' x2 x2a\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'165 s s' x2 x2a p\<rbrace>
 8. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q160 s s' x2 x2a) sa
 9. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'160 s s' x2 x2a) sa proof (prove)
goal (8 subgoals):
 1. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q171 s s' x2 x2a p sent\<rbrace> set_message_info receiver (Structures_A.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. tcb_at receiver\<rbrace>
 2. \<And>s s' x2 x2a p sent. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'171 s s' x2 x2a p sent\<rbrace> setMessageInfo receiver (Types_H.message_info.MI sent 0 0 (fst p)) \<lbrace>\<lambda>x. tcb_at' receiver\<rbrace>
 3. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q165 s s' x2 x2a p\<rbrace> set_mrs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at receiver and ?Q171 s s' x2 x2a p sent\<rbrace>
 4. \<And>s s' x2 x2a p. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'165 s s' x2 x2a p\<rbrace> setMRs receiver (Some x2a) (snd p) \<lbrace>\<lambda>sent. tcb_at' receiver and ?Q'171 s s' x2 x2a p sent\<rbrace>
 5. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q160 s s' x2 x2a\<rbrace> make_fault_msg x2 sender \<lbrace>\<lambda>p. tcb_at receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) and ?Q165 s s' x2 x2a p\<rbrace>
 6. \<And>s s' x2 x2a. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'160 s s' x2 x2a\<rbrace> makeFaultMessage (fault_map x2) sender \<lbrace>\<lambda>p. tcb_at' receiver and (case Some x2a of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and ?Q'165 s s' x2 x2a p\<rbrace>
 7. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at sender and tcb_at receiver and in_user_frame x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at sender and ?Q160 s s' x2 x2a) sa
 8. \<And>s s' x2 x2a sa. \<lbrakk>tcb_at receiver s; in_user_frame x2a s; (s, s') \<in> state_relation; tcb_at' sender s'; tcb_at sender s; tcb_at' receiver s'; recv_buf = Some x2a; valid_ipc_buffer_ptr' x2a s'; (tcb_at' sender and tcb_at' receiver and valid_ipc_buffer_ptr' x2a) sa\<rbrakk> \<Longrightarrow> (tcb_at' sender and ?Q'160 s s' x2 x2a) sa proof (prove)
goal:
No subgoals!