theory Ipc_R

lemma doIPCTransfer_corres:
  "corres dc
     (tcb_at s and tcb_at r and valid_objs and pspace_aligned
        and valid_list
        and pspace_distinct and valid_mdb and cur_tcb
        and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at x s | _ \<Rightarrow> True))
     (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb'
        and (\<lambda>s. case ep of Some x \<Rightarrow> ep_at' x s | _ \<Rightarrow> True))
     (do_ipc_transfer s ep bg grt r)
     (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and>
                       pspace_aligned sa \<and> tcb_at r sa \<and>
                       cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and>
                       (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and>
                       case_option (\<lambda>_. True) in_user_frame receiveBuffer sa \<and>
                       obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb
                                    \<comment> \<open>\<exists>ft. tcb_fault tcb = Some ft\<close>) s sa"
               in corres_underlying_split) apply (rule corres_guard_imp) apply (rule lookupIPCBuffer_corres') apply auto[2] apply (rule corres_underlying_split [OF _ _ thread_get_sp threadGet_inv]) apply (rule corres_guard_imp) apply (rule threadget_fault_corres) apply simp defer apply (rule corres_guard_imp) apply (subst case_option_If)+ apply (rule corres_if2) apply (simp add: fault_rel_optionation_def) apply (rule corres_split_eqr[OF lookupIPCBuffer_corres']) apply (simp add: dc_def[symmetric]) apply (rule doNormalTransfer_corres) apply (wp | simp add: valid_pspace'_def)+ apply (simp add: dc_def[symmetric]) apply (rule doFaultTransfer_corres) apply (clarsimp simp: obj_at_def) apply (erule ignore_if) apply (wp|simp add: obj_at_def is_tcb valid_pspace'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r) proof (prove)
goal (1 subgoal):
 1. corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) (do recv_buffer <- lookup_ipc_buffer True r;
fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r recv_buffer
od | Some f \<Rightarrow> do_fault_transfer bg s r recv_buffer
od) (do receiveBuffer <- lookupIPCBuffer True r;
fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r receiveBuffer
od | Some v21 \<Rightarrow> doFaultTransfer bg s r receiveBuffer
od) proof (prove)
goal (4 subgoals):
 1. corres ?r' (tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) (lookup_ipc_buffer True r) (lookupIPCBuffer True r)
 2. \<And>rv rv'. ?r' rv rv' \<Longrightarrow> corres dc (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa) (?Q' rv') (do fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv
od) (do fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv'
od)
 3. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 4. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (6 subgoals):
 1. corres ?r' ?Q1 ?Q'1 (lookup_ipc_buffer True r) (lookupIPCBuffer True r)
 2. \<And>sa. (tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) sa \<Longrightarrow> ?Q1 sa
 3. \<And>sa. (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) sa \<Longrightarrow> ?Q'1 sa
 4. \<And>rv rv'. ?r' rv rv' \<Longrightarrow> corres dc (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa) (?Q' rv') (do fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv
od) (do fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv'
od)
 5. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 6. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>sa. (tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) sa \<Longrightarrow> (tcb_at r and valid_objs and pspace_aligned) sa
 2. \<And>sa. (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) sa \<Longrightarrow> (tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj') sa
 3. \<And>rv rv'. rv = rv' \<Longrightarrow> corres dc (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa) (?Q' rv') (do fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv
od) (do fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv'
od)
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres dc (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa) (?Q' rv') (do fault <- thread_get tcb_fault s;
case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv
od) (do fault <- threadGet tcbFault s;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv'
od)
 2. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 3. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres (?r'26 rv rv') (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa) (?Q' rv') (thread_get tcb_fault s) (threadGet tcbFault s)
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; ?r'26 rv rv' fault faulta\<rbrakk> \<Longrightarrow> corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) (?Q' rv') (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 3. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 4. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres (?r'26 rv rv') (?Q33 rv rv') (?Q'33 rv rv') (thread_get tcb_fault s) (threadGet tcbFault s)
 2. \<And>rv rv' sa. \<lbrakk>rv = rv'; tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrakk> \<Longrightarrow> ?Q33 rv rv' sa
 3. \<And>rv rv' s. \<lbrakk>rv = rv'; ?Q' rv' s\<rbrakk> \<Longrightarrow> ?Q'33 rv rv' s
 4. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; ?r'26 rv rv' fault faulta\<rbrakk> \<Longrightarrow> corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) (?Q' rv') (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 5. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 6. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' sa. \<lbrakk>rv = rv'; tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrakk> \<Longrightarrow> tcb_at s sa
 2. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
 3. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) (?Q' rv') (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) (?Q' rv') (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 3. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 4. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> corres dc (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) (?Q' rv') (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 2. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 3. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 4. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> corres dc (?Q38 rv rv' fault faulta) (?Q'38 rv rv' fault faulta) (case fault of None \<Rightarrow> do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od | Some f \<Rightarrow> do_fault_transfer bg s r rv) (case faulta of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od | Some v21 \<Rightarrow> doFaultTransfer bg s r rv')
 2. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> ?Q38 rv rv' fault faulta sa
 3. \<And>rv rv' fault faulta s. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' s\<rbrakk> \<Longrightarrow> ?Q'38 rv rv' fault faulta s
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 6. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> corres dc (?Q49 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'50 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (if fault = None then do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od else do_fault_transfer bg s r rv) (if faulta = None then do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od else doFaultTransfer bg s r rv')
 2. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> ?Q44 rv rv rv' rv' fault fault faulta faulta sa
 3. \<And>rv rv' fault faulta s. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' s\<rbrakk> \<Longrightarrow> ?Q'45 rv rv rv' rv' fault fault faulta faulta s
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 6. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q'50 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'45 rv rv rv' rv' fault fault faulta faulta
\<lambda>rv rv' fault faulta. ?Q49 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q44 rv rv rv' rv' fault fault faulta faulta proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta\<rbrakk> \<Longrightarrow> (fault = None) = (faulta = None)
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> corres dc (?P66 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?P'62 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od) (do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od)
 3. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; faulta \<noteq> None\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv) (doFaultTransfer bg s r rv')
 4. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then ?P68 rv rv rv' rv' fault fault faulta faulta else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 5. \<And>rv rv' fault faulta s. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' s\<rbrakk> \<Longrightarrow> (if faulta = None then ?P'64 rv rv rv' rv' fault fault faulta faulta else ?Q'63 rv rv rv' rv' fault fault faulta faulta) s
 6. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 7. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 8. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?P68 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?P66 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?P'64 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?P'62 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> corres dc (?P66 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?P'62 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do send_buffer <- lookup_ipc_buffer False s;
do_normal_transfer s send_buffer ep bg grt r rv
od) (do sendBuffer <- lookupIPCBuffer False s;
doNormalTransfer s sendBuffer ep bg grt r rv'
od)
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; faulta \<noteq> None\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv) (doFaultTransfer bg s r rv')
 3. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then ?P68 rv rv rv' rv' fault fault faulta faulta else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 4. \<And>rv rv' fault faulta s. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' s\<rbrakk> \<Longrightarrow> (if faulta = None then ?P'64 rv rv rv' rv' fault fault faulta faulta else ?Q'63 rv rv rv' rv' fault fault faulta faulta) s
 5. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 6. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 7. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?P68 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?P66 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?P'64 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?P'62 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' fault faulta rva. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> corres dc (?R72 rv rv' fault faulta rva) (?R'72 rv rv' fault faulta rva) (do_normal_transfer s rva ep bg grt r rv) (doNormalTransfer s rva ep bg grt r rv')
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookup_ipc_buffer False s \<lbrace>?R72 rv rv' fault faulta\<rbrace>
 3. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookupIPCBuffer False s \<lbrace>?R'72 rv rv' fault faulta\<rbrace>
 4. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; faulta \<noteq> None\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv) (doFaultTransfer bg s r rv')
 5. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and ?Q81 rv rv rv' rv' fault fault faulta faulta else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 6. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'79 rv rv rv' rv' fault fault faulta faulta else ?Q'63 rv rv rv' rv' fault fault faulta faulta) sa
 7. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 8. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 9. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q81 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'79 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' fault faulta rva. \<lbrakk>rv = rv'; fault_rel_optionation None faulta; fault = None\<rbrakk> \<Longrightarrow> corres dc (?R72 rv' rv' None faulta rva) (?R'72 rv' rv' None faulta rva) (do_normal_transfer s rva ep bg grt r rv') (doNormalTransfer s rva ep bg grt r rv')
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookup_ipc_buffer False s \<lbrace>?R72 rv rv' fault faulta\<rbrace>
 3. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookupIPCBuffer False s \<lbrace>?R'72 rv rv' fault faulta\<rbrace>
 4. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; faulta \<noteq> None\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv) (doFaultTransfer bg s r rv')
 5. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and ?Q81 rv rv rv' rv' fault fault faulta faulta else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 6. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'79 rv rv rv' rv' fault fault faulta faulta else ?Q'63 rv rv rv' rv' fault fault faulta faulta) sa
 7. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 8. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 9. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q81 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'79 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookup_ipc_buffer False s \<lbrace>\<lambda>a. tcb_at s and tcb_at r and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s) and (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a) and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a)\<rbrace>
 2. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; fault = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>a. tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s) and (case a of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a)\<rbrace>
 3. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; faulta \<noteq> None\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv) (doFaultTransfer bg s r rv')
 4. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and ?Q81 rv rv rv' rv' fault fault faulta faulta else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 5. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'79 rv rv rv' rv' fault fault faulta faulta else ?Q'63 rv rv rv' rv' fault fault faulta faulta) sa
 6. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 7. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 8. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q81 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q80 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'79 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'78 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; \<exists>y. faulta = Some y\<rbrakk> \<Longrightarrow> corres (\<lambda>a b. True) (?Q65 rv' rv' rv' rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv' rv' rv' rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv') (doFaultTransfer bg s r rv')
 2. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and (\<lambda>a. (tcb_at s and tcb_at r and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) a \<and> (valid_objs and tcb_at s) a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a) a) else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 3. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) else ?Q'63 rv rv rv' rv' fault fault faulta faulta) sa
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 6. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' fault faulta. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; \<exists>y. faulta = Some y\<rbrakk> \<Longrightarrow> corres dc (?Q65 rv' rv' rv' rv' rv' rv' fault fault fault faulta faulta faulta) (?Q'61 rv' rv' rv' rv' rv' rv' fault fault fault faulta faulta faulta) (do_fault_transfer bg s r rv') (doFaultTransfer bg s r rv')
 2. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and (\<lambda>a. (tcb_at s and tcb_at r and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) a \<and> (valid_objs and tcb_at s) a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a) a) else ?Q67 rv rv rv' rv' fault fault faulta faulta) sa
 3. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) else ?Q'63 rv rv rv' rv' fault fault faulta faulta) sa
 4. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 5. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 6. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa
flex-flex pairs:
\<lambda>rv rv' fault faulta. ?Q67 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q65 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta
\<lambda>rv rv' fault faulta. ?Q'63 rv rv rv' rv' fault fault faulta faulta \<equiv>\<^sup>? \<lambda>rv rv' fault faulta. ?Q'61 rv rv rv rv' rv' rv' fault fault fault faulta faulta faulta proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; (obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> tcb_fault tcb = fault) s and (\<lambda>sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case rv of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa)) sa\<rbrakk> \<Longrightarrow> (if fault = None then tcb_at s and valid_objs and pspace_aligned and (\<lambda>a. (tcb_at s and tcb_at r and pspace_aligned and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)) a \<and> (valid_objs and tcb_at s) a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a) a) else obj_at (\<lambda>ko. \<exists>tcb ft. ko = TCB tcb \<and> tcb_fault tcb = Some ft) s and tcb_at r and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> in_user_frame a)) sa
 2. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) else tcb_at' s and tcb_at' r and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a)) sa
 3. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 4. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 5. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' fault faulta sa. \<lbrakk>rv = rv'; fault_rel_optionation fault faulta; ?Q' rv' sa\<rbrakk> \<Longrightarrow> (if faulta = None then tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) else tcb_at' s and tcb_at' r and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a)) sa
 2. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 3. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>?Q'\<rbrace>
 4. \<And>rv rv' sa. \<lbrakk>rv = rv'; ?Q' rv' sa\<rbrakk> \<Longrightarrow> tcb_at' s sa proof (prove)
goal (3 subgoals):
 1. \<lbrace>tcb_at s and tcb_at r and valid_objs and pspace_aligned and valid_list and pspace_distinct and valid_mdb and cur_tcb and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x s)\<rbrace> lookup_ipc_buffer True r \<lbrace>\<lambda>receiveBuffer sa. tcb_at s sa \<and> valid_objs sa \<and> pspace_aligned sa \<and> tcb_at r sa \<and> cur_tcb sa \<and> valid_mdb sa \<and> valid_list sa \<and> pspace_distinct sa \<and> (case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at x sa) \<and> (case receiveBuffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> in_user_frame x) sa \<and> obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb) s sa\<rbrace>
 2. \<lbrace>tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)\<rbrace> lookupIPCBuffer True r \<lbrace>\<lambda>rv'. tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) and (tcb_at' s and tcb_at' r and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a))\<rbrace>
 3. \<And>rv rv' sa. \<lbrakk>rv = rv'; (tcb_at' s and valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. (tcb_at' s and tcb_at' r and valid_objs' and pspace_aligned' and pspace_distinct' and cur_tcb' and valid_mdb' and no_0_obj' and (\<lambda>s. case ep of None \<Rightarrow> True | Some x \<Rightarrow> ep_at' x s)) a \<and> valid_objs' a \<and> (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a) a) and (tcb_at' s and tcb_at' r and (case rv' of None \<Rightarrow> \<lambda>_. True | Some a \<Rightarrow> valid_ipc_buffer_ptr' a))) sa\<rbrakk> \<Longrightarrow> tcb_at' s sa proof (prove)
goal:
No subgoals!