theory Ipc_C

lemma Arch_setMRs_fault_ccorres:
  "ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_'
           (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender
                          and K (ft = ArchFault aft)
                          and (case buffer of Some x \<Rightarrow> valid_ipc_buffer_ptr' x | None \<Rightarrow> \<top>)
                          and K (buffer \<noteq> Some 0)
                          and K (sender \<noteq> receiver))
           (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace>
                 \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace>
                 \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft \<rbrace>
                 \<inter> \<lbrace>\<acute>receiveIPCBuffer = Ptr (option_to_0 buffer)\<rbrace>) hs
    (makeArchFaultMessage aft sender >>= (\<lambda>ms. setMRs receiver buffer (snd ms)))
    (Call Arch_setMRs_fault_'proc)" proof - let ?obj_at_ft = "obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV
          [where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV] show ?thesis apply (unfold K_def) using [[goals_limit = 1]] apply (intro ccorres_gen_asm) apply (cinit' lift: sender_' receiver_' faultType_' receiveIPCBuffer_') apply (simp only: makeArchFaultMessage_def setMRs_to_setMR
                 del:  Collect_const split del: if_split) apply (rule_tac P="ft = ArchFault aft" in ccorres_gen_asm) apply wpc apply (rename_tac list) apply (rule_tac P="zip [Suc (Suc 0) ..< msgMaxLength] list = [(2, hd list), (3, hd (tl list))]"
                     in ccorres_gen_asm) apply (simp add: Collect_True Collect_False ccorres_cond_iffs
                      zip_upt_Cons msgMaxLength_unfold
                      zipWithM_mapM mapM_Cons bind_assoc
                      seL4_Fault_tag_defs
                 del: Collect_const) apply (rule ccorres_rhs_assoc)+ apply (ctac (no_vcg)) apply (rule ccorres_stateAssert) apply (ctac(no_vcg) add: setMR_ccorres_dc) apply (rule ccorres_move_c_guard_tcb) apply (rule_tac val="vmFaultAddress aft" in symb_exec_r_fault) apply (rule conseqPre, vcg, clarsimp) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: ctcb_relation_def typ_heap_simps
                                   cfault_rel_def seL4_Fault_lift_def
                                   seL4_Fault_VMFault_lift_def Let_def
                            split: if_split_asm) apply ceqv apply (ctac(no_vcg) add: setMR_ccorres_dc) apply (rule_tac val="hd (vmFaultArchData aft)" in symb_exec_r_fault) apply (rule conseqPre, vcg, clarsimp) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps') apply (clarsimp simp: ctcb_relation_def
                                     cfault_rel_def seL4_Fault_lift_def
                                     seL4_Fault_VMFault_lift_def Let_def
                              split: if_split_asm) apply ceqv apply (ctac(no_vcg) add: setMR_ccorres_dc) apply (rule_tac val="vmFaultArchData aft ! 1" in symb_exec_r_fault) apply (rule conseqPre, vcg, clarsimp) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps') apply (clarsimp simp: ctcb_relation_def
                                    cfault_rel_def seL4_Fault_lift_def
                                    seL4_Fault_VMFault_lift_def Let_def
                             split: if_split_asm) apply ceqv apply (ctac(no_vcg) add: setMR_ccorres) apply (simp add: mapM_Nil) apply (rule ccorres_return_C, simp+)[1] apply wp apply (clarsimp simp: option_to_ptr_def) apply (subgoal_tac "case list of [a, b] \<Rightarrow> True | _ \<Rightarrow> True") apply (simp add: zip_upt_Cons guard_is_UNIVI seL4_VMFault_FSR_def split: list.split_asm) apply (simp split: list.split) apply (wp setMR_tcbFault_obj_at asUser_inv[OF getRestartPC_inv]
                       hoare_case_option_wp
                     | simp add: option_to_ptr_def guard_is_UNIVI
                                 seL4_VMFault_PrefetchFault_def
                                 seL4_VMFault_Addr_def
                                 seL4_VMFault_IP_def
                                 msgMaxLength_def
                            del: Collect_const split del: if_split)+ apply clarsimp apply (drule(1) obj_at_cslift_tcb[where thread=sender]) apply (clarsimp simp: obj_at'_def projectKOs objBits_simps) apply (clarsimp simp: ctcb_relation_def cfault_rel_def seL4_Fault_lift_def
                        Let_def zip_upt_Cons
                  split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (state)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (state)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (state)
this:
\<lbrakk>\<And>s. ?\<Gamma>\<turnstile> (UNIV \<inter> {s'. obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender s \<and> (s, s') \<in> ?sr}) ?m ({s'. (s, s') \<in> ?sr} \<inter> \<lbrace>\<acute>ret__unsigned = ?val\<rbrace>); \<And>rv' t t'. ceqv ?\<Gamma> ret__unsigned_' rv' t t' ?y (?y' rv'); ccorres_underlying ?sr ?\<Gamma> ?r ?xf ?arrel ?axf ?P ?Q ?hs ?a (?y' ?val); guard_is_UNIV (\<lambda>rv rv'. rv' = ?val) ret__unsigned_' (\<lambda>rv rv'. ?Q)\<rbrakk> \<Longrightarrow> ccorres_underlying ?sr ?\<Gamma> ?r ?xf ?arrel ?axf (?P and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender) UNIV ?hs ?a (?m;;
?y)

goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and (\<lambda>y. ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>y. buffer \<noteq> Some 0) and (\<lambda>y. sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and (\<lambda>y. ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>y. buffer \<noteq> Some 0) and (\<lambda>y. sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and (\<lambda>y. ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q1346 receiveIPCBuffer faultType receivera sendera) (?Q'1346 receiveIPCBuffer faultType receivera sendera) (SKIP # hs) (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (IF faultType = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(sendera);;
CALL setMR_'proc(receivera,receiveIPCBuffer,SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(receivera,receiveIPCBuffer,SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(receivera,receiveIPCBuffer,SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c sendera} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(sendera\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(receivera,receiveIPCBuffer,SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q1346 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?Q'1346 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (SKIP # hs) (do ms <- case aft of ARM_H.VMFault vptr archData \<Rightarrow> do pc <- asUser sender getRestartPC;
return (5, pc # fromVPtr vptr # archData)
od;
stateAssert (tcb_at' receiver) [];
ys <- zipWithM (setMR receiver buffer) [0..<msgMaxLength] (snd ms);
return (word_of_nat (last (0 # ys)))
od) (IF fault_to_fault_tag ft = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault aft\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?G1355 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (?Q'1346 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender)) (SKIP # hs) (do ms <- case aft of ARM_H.VMFault vptr archData \<Rightarrow> do pc <- asUser sender getRestartPC;
return (5, pc # fromVPtr vptr # archData)
od;
stateAssert (tcb_at' receiver) [];
ys <- zipWithM (setMR receiver buffer) [0..<msgMaxLength] (snd ms);
return (word_of_nat (last (0 # ys)))
od) (IF fault_to_fault_tag ft = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 x2. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault aft; aft = ARM_H.VMFault x1 x2\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (\<lambda>a. ?R1368 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) a x1 x2) (?R''1369 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 x2) (SKIP # hs) (do a <- do pc <- asUser sender getRestartPC;
return (5, pc # fromVPtr x1 # x2)
od;
stateAssert (tcb_at' receiver) [];
ys <- zipWithM (setMR receiver buffer) [0..<msgMaxLength] (snd a);
return (word_of_nat (last (0 # ys)))
od) (IF fault_to_fault_tag ft = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault aft; aft = ARM_H.VMFault x1 list\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (\<lambda>a. ?R1368 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) a x1 list) (?R''1369 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (SKIP # hs) (do a <- do pc <- asUser sender getRestartPC;
return (5, pc # fromVPtr x1 # list)
od;
stateAssert (tcb_at' receiver) [];
ys <- zipWithM (setMR receiver buffer) [0..<msgMaxLength] (snd a);
return (word_of_nat (last (0 # ys)))
od) (IF fault_to_fault_tag ft = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = fault_to_fault_tag ft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault aft; aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<msgMaxLength] list = [(2, hd list), (3, hd (tl list))]\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?G1375 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (?R''1369 (PTR(32 word) (option_to_0 buffer)) (fault_to_fault_tag ft) (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (SKIP # hs) (do a <- do pc <- asUser sender getRestartPC;
return (5, pc # fromVPtr x1 # list)
od;
stateAssert (tcb_at' receiver) [];
ys <- zipWithM (setMR receiver buffer) [0..<msgMaxLength] (snd a);
return (word_of_nat (last (0 # ys)))
od) (IF fault_to_fault_tag ft = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault THEN
  \<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'
ELSE
  Guard DontReach {} SKIP
FI)
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?G1375 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (?R''1369 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (SKIP # hs) (do pc <- asUser sender getRestartPC;
a <- stateAssert (tcb_at' receiver) [];
y <- setMR receiver buffer 0 pc;
y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (\<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')
A total of 2 subgoals... proof (prove)
goal (2 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?G1375 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (?R''1369 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list) (SKIP # hs) (do pc <- asUser sender getRestartPC;
a <- stateAssert (tcb_at' receiver) [];
y <- setMR receiver buffer 0 pc;
y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (\<acute>ret__unsigned_long :== CALL getRestartPC_'proc(tcb_ptr_to_ctcb_ptr sender);;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,\<acute>ret__unsigned_long);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))))))))
A total of 2 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q1421 receiveIPCBuffer faultType receivera sendera x1 list rv) (?Q'1436 x1 list rv ret__unsigned_long) (SKIP # hs) (do a <- stateAssert (tcb_at' receiver) [];
y <- setMR receiver buffer 0 rv;
y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,ret__unsigned_long);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')))))))
A total of 3 subgoals...
flex-flex pairs:
\<lambda>x1 list t rv. ?Q'1436 x1 list rv (ret__unsigned_long_' t) \<equiv>\<^sup>? ?Q'1435 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) proof (prove)
goal (3 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?P1748 receiveIPCBuffer faultType receivera sendera x1 list rv) (?Q'1436 x1 list rv ret__unsigned_long) (SKIP # hs) (do y <- setMR receiver buffer 0 rv;
y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>a. case a of (a, b) \<Rightarrow> setMR receiver buffer a b) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_IP,ret__unsigned_long);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')))))))
A total of 3 subgoals...
flex-flex pairs:
\<lambda>x1 list t rv. ?Q'1436 x1 list rv (ret__unsigned_long_' t) \<equiv>\<^sup>? ?Q'1435 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q1754 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva) (?Q'1772 x1 list rv ret__unsigned_long rva xfdc) (SKIP # hs) (do y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))))))
A total of 4 subgoals...
flex-flex pairs:
?Q'1773 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) \<equiv>\<^sup>? \<lambda>x1 list t rv ta rva. ?Q'1772 x1 list rv (ret__unsigned_long_' t) rva (xfdc ta) proof (prove)
goal (4 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?A1816 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva) (?C'1814 x1 list rv ret__unsigned_long rva xfdc) (SKIP # hs) (do y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))))))
A total of 4 subgoals...
flex-flex pairs:
\<lambda>x1 list t rv ta rva. ?C'1814 x1 list rv (ret__unsigned_long_' t) rva (xfdc ta) \<equiv>\<^sup>? ?C'1813 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc s. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender s \<and> (s, s') \<in> rf_sr}) \<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_address_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__unsigned = vmFaultAddress aft\<rbrace>)
A total of 7 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; obj_at' (\<lambda>tcb. tcbFault tcb = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list))) sender s; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = seL4_Fault_VMFault_CL.address_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> seL4_Fault_VMFault_CL.address_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = x1)
A total of 7 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; (s, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko sender s \<and> tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list)) \<and> cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = seL4_Fault_VMFault_CL.address_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> seL4_Fault_VMFault_CL.address_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = x1)
A total of 7 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc rv' t t'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))))) (?y'1818 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc rv')
A total of 6 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?P1822 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva) (?Q1818 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdc) (SKIP # hs) (do y <- setMR receiver buffer (Suc 0) x1;
y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_Addr,vmFaultAddress aft);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')))))
A total of 5 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q2226 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb) (?Q'2226 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc) (SKIP # hs) (do y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))))
A total of 6 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc s. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender s \<and> (s, s') \<in> rf_sr}) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_instructionFault_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__unsigned = hd (vmFaultArchData aft)\<rbrace>)
A total of 9 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; obj_at' (\<lambda>tcb. tcbFault tcb = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list))) sender s; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = instructionFault_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> instructionFault_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = hd list)
A total of 9 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; (s, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko sender s \<and> tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list)) \<and> cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = instructionFault_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> instructionFault_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = hd list)
A total of 9 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x1 list s x ko ko'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; (s, x) \<in> rf_sr; ko_at' ko sender s; tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list)); cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> seL4_Fault_get_tag (tcbFault_C ko') = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = instructionFault_CL (seL4_Fault_VMFault_lift (tcbFault_C ko'))) \<longrightarrow> instructionFault_CL (seL4_Fault_VMFault_lift (tcbFault_C ko')) = hd list)
A total of 9 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc rv' t t'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,\<acute>ret__unsigned);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))) (?y'2261 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc rv')
A total of 8 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?P2263 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb) (?Q2261 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc) (SKIP # hs) (do y <- setMR receiver buffer 2 (hd list);
y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_PrefetchFault,hd (vmFaultArchData aft));;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')))
A total of 7 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q2495 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc) (?Q'2495 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc) (SKIP # hs) (do y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))));;
(\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_'))
A total of 8 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc s. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (UNIV \<inter> {s'. obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender s \<and> (s, s') \<in> rf_sr}) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender} (\<acute>ret__unsigned :== CALL seL4_Fault_VMFault_get_FSR_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) ({s'. (s, s') \<in> rf_sr} \<inter> \<lbrace>\<acute>ret__unsigned = vmFaultArchData aft ! 1\<rbrace>)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; obj_at' (\<lambda>tcb. tcbFault tcb = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list))) sender s; (s, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = FSR_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> FSR_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = list ! Suc 0)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 list s x. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; (s, x) \<in> rf_sr; \<exists>ko ko'. ko_at' ko sender s \<and> tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list)) \<and> cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> x \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr sender \<and> seL4_Fault_get_tag (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))) = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = FSR_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C'']))))) \<longrightarrow> FSR_CL (seL4_Fault_VMFault_lift (h_val (hrs_mem (t_hrs_' (globals x))) (PTR(seL4_Fault_C) &(tcb_ptr_to_ctcb_ptr sender\<rightarrow>[''tcbFault_C''])))) = list ! Suc 0)
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x1 list s x ko ko'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; (s, x) \<in> rf_sr; ko_at' ko sender s; tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x1 list)); cslift x (tcb_ptr_to_ctcb_ptr sender) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> seL4_Fault_get_tag (tcbFault_C ko') = SCAST(32 signed \<rightarrow> 32) seL4_Fault_VMFault \<and> ((\<exists>t. ret__unsigned_' t = FSR_CL (seL4_Fault_VMFault_lift (tcbFault_C ko'))) \<longrightarrow> FSR_CL (seL4_Fault_VMFault_lift (tcbFault_C ko')) = list ! Suc 0)
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rv' t t'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ret__unsigned_' rv' t t' (\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,\<acute>ret__unsigned);;
return_C ret__unsigned_long_'_update unsigned_eret_2_') (?y'2531 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rv')
A total of 10 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?P2533 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc) (?Q2531 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc) (SKIP # hs) (do y <- setMR receiver buffer 3 (hd (drop (Suc 0) list));
ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then y else last ys))
od) (\<acute>unsigned_eret_2 :== CALL setMR_'proc(tcb_ptr_to_ctcb_ptr receiver,PTR(32 word) (option_to_0 buffer),SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR,vmFaultArchData aft ! 1);;
return_C ret__unsigned_long_'_update unsigned_eret_2_')
A total of 9 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rvd unsigned_eret_2. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc; rvd = unat (unsigned_eret_2 && mask msgLengthBits)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q2742 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rvd) (?Q'2742 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rvd unsigned_eret_2) (SKIP # hs) (do ys <- mapM (\<lambda>(x, y). setMR receiver buffer x y) [];
return (word_of_nat (if ys = [] then rvd else last ys))
od) (return_C ret__unsigned_long_'_update (\<lambda>s. unsigned_eret_2))
A total of 10 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc rvd unsigned_eret_2. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; rvd = unat (unsigned_eret_2 && mask msgLengthBits)\<rbrakk> \<Longrightarrow> ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (?Q2742 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list ret__unsigned_long ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc (unat (unsigned_eret_2 && mask msgLengthBits))) (?Q'2742 (PTR(32 word) (option_to_0 buffer)) 5 (tcb_ptr_to_ctcb_ptr receiver) (tcb_ptr_to_ctcb_ptr sender) x1 list ret__unsigned_long ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc (unat (unsigned_eret_2 && mask msgLengthBits)) unsigned_eret_2) (SKIP # hs) (return (unsigned_eret_2 && mask msgLengthBits)) (return_C ret__unsigned_long_'_update (\<lambda>s. unsigned_eret_2))
A total of 10 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2744 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc\<rbrace> setMR receiver buffer 3 (hd (drop (Suc 0) list)) \<lbrace>\<lambda>a b. True\<rbrace>
A total of 9 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdcb rvc xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdcb; dc rvc xfdc\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = vmFaultArchData aft ! 1) ret__unsigned_' (\<lambda>rv rv'. {s. reg_'_update (\<lambda>_. vmFaultArchData aft ! 1) (offset_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR) (receiveIPCBuffer_'_update (\<lambda>_. PTR(32 word) (option_to_0 buffer)) (receiver_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr receiver) s))) \<in> UNIV \<inter> \<lbrace>\<acute>offset = word_of_nat 3\<rbrace> \<inter> \<lbrace>\<acute>reg = hd (drop (Suc 0) list)\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = option_to_ptr buffer\<rbrace>} \<inter> {s'. \<forall>t rv. rv = unat (ret__unsigned_' t && mask msgLengthBits) \<longrightarrow> s'\<lparr>globals := globals t, unsigned_eret_2_' := ret__unsigned_' t\<rparr> \<in> \<lbrace>\<^bsup>t\<^esup>ret__unsigned && mask msgLengthBits = \<^bsup>t\<^esup>ret__unsigned && mask msgLengthBits\<rbrace>})
A total of 8 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = list ! Suc 0) ret__unsigned_' (\<lambda>rv rv'. if SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR = 3 \<and> list ! Suc 0 = hd (drop (Suc 0) list) then UNIV else {})
A total of 8 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; case list of [] \<Rightarrow> True | [a] \<Rightarrow> True | [a, b] \<Rightarrow> True | a # b # _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. rv' = list ! Suc 0) ret__unsigned_' (\<lambda>rv rv'. if SCAST(32 signed \<rightarrow> 32) seL4_VMFault_FSR = 3 \<and> list ! Suc 0 = hd (drop (Suc 0) list) then UNIV else {})
A total of 9 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>x1 list. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]\<rbrakk> \<Longrightarrow> case list of [] \<Rightarrow> True | [a] \<Rightarrow> True | [a, b] \<Rightarrow> True | a # b # _ \<Rightarrow> True
A total of 8 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb xfdc. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = 5; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x1 list); aft = ARM_H.VMFault x1 list; zip [Suc (Suc 0)..<120] list = [(2, hd list), (3, hd (drop (Suc 0) list))]; rv = ret__unsigned_long; dc rva xfdca; dc rvb xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R2497 receiveIPCBuffer faultType receivera sendera x1 list rv ret__unsigned_long rva xfdca rvb\<rbrace> setMR receiver buffer 2 (hd list) \<lbrace>\<lambda>rvc. valid_pspace' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>s. 3 < msgMaxLength) and (\<lambda>_. True) and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender\<rbrace>
A total of 7 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>receiveIPCBuffer faultType receivera sendera s s'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; receiveIPCBuffer = PTR(32 word) (option_to_0 buffer); faultType = arch_fault_to_fault_tag aft; receivera = tcb_ptr_to_ctcb_ptr receiver; sendera = tcb_ptr_to_ctcb_ptr sender; (s, s') \<in> rf_sr; valid_pspace' s \<and> obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender s \<and> ft = Fault_H.fault.ArchFault aft \<and> (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s\<rbrakk> \<Longrightarrow> \<forall>x xa. aft = ARM_H.VMFault x xa \<longrightarrow> (tcb_at' receiver s \<longrightarrow> obj_at' (\<lambda>tcb. tcbFault tcb = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x xa))) sender s \<and> tcb_at' sender s) \<and> zip [Suc (Suc 0)..<120] xa = [(2, hd xa), (3, hd (drop (Suc 0) xa))] proof (prove)
goal (1 subgoal):
 1. \<And>s s' x xa. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; (s, s') \<in> rf_sr; valid_pspace' s; obj_at' (\<lambda>tcb. tcbFault tcb = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x xa))) sender s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x xa); aft = ARM_H.VMFault x xa\<rbrakk> \<Longrightarrow> (tcb_at' receiver s \<longrightarrow> tcb_at' sender s) \<and> zip [Suc (Suc 0)..<120] xa = [(2, hd xa), (3, hd (drop (Suc 0) xa))] proof (prove)
goal (1 subgoal):
 1. \<And>s s' x xa. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; (s, s') \<in> rf_sr; valid_pspace' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x xa); aft = ARM_H.VMFault x xa; \<exists>ko ko'. ko_at' ko sender s \<and> tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x xa)) \<and> cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (tcb_at' receiver s \<longrightarrow> tcb_at' sender s) \<and> zip [Suc (Suc 0)..<120] xa = [(2, hd xa), (3, hd (drop (Suc 0) xa))] proof (prove)
goal (1 subgoal):
 1. \<And>s s' x xa ko ko'. \<lbrakk>sender \<noteq> receiver; buffer \<noteq> Some 0; (s, s') \<in> rf_sr; valid_pspace' s; (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) s; ft = Fault_H.fault.ArchFault (ARM_H.VMFault x xa); aft = ARM_H.VMFault x xa; ksPSpace s sender = Some (KOTCB ko); is_aligned sender tcbBlockSizeBits; ps_clear sender tcbBlockSizeBits s; tcbFault ko = Some (Fault_H.fault.ArchFault (ARM_H.VMFault x xa)); cslift s' (tcb_ptr_to_ctcb_ptr sender) = Some ko'; ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> zip [Suc (Suc 0)..<120] xa = [(2, hd xa), (3, hd (drop (Suc 0) xa))] proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres (\<lambda>r r'. r = r' && mask msgLengthBits) ret__unsigned_long_' (valid_pspace' and obj_at' (\<lambda>tcb. tcbFault tcb = Some ft) sender and K (ft = Fault_H.fault.ArchFault aft) and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (buffer \<noteq> Some 0) and K (sender \<noteq> receiver)) (UNIV \<inter> \<lbrace>\<acute>sender = tcb_ptr_to_ctcb_ptr sender\<rbrace> \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr receiver\<rbrace> \<inter> \<lbrace>\<acute>faultType = fault_to_fault_tag ft\<rbrace> \<inter> \<lbrace>\<acute>receiveIPCBuffer = PTR(32 word) (option_to_0 buffer)\<rbrace>) hs (do ms <- makeArchFaultMessage aft sender;
setMRs receiver buffer (snd ms)
od) (Call Arch_setMRs_fault_'proc)

goal:
No subgoals!