theory Ipc_C

lemma handleFaultReply':
  notes option.case_cong_weak [cong] wordSize_def'[simp] take_append[simp del]
  assumes neq: "s \<noteq> r"
  shows "monadic_rewrite True False (tcb_at' s and tcb_at' r) (do
    tag \<leftarrow> getMessageInfo s;
    sb \<leftarrow> lookupIPCBuffer False s;
    msg \<leftarrow> getMRs s sb tag;
    handleFaultReply f r (msgLabel tag) msg
  od) (handleFaultReply' f s r)" supply empty_fail_cond[simp] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def
                bit_def msgLengthBits_def msgRegisters_unfold
                fromIntegral_simp1 fromIntegral_simp2
                shiftL_word) apply (simp add: bind_assoc) apply (rule monadic_rewrite_bind_tail) apply (clarsimp simp: mapM_def sequence_def bind_assoc asUser_bind_distrib
                         asUser_return submonad_asUser.fn_stateAssert) apply (case_tac f, simp_all add: handleFaultReply_def zipWithM_x_mapM_x zip_take) 
   (* UserException *)
       apply (clarsimp simp: handleFaultReply_def zipWithM_x_mapM_x
                            zip_Cons ARM_H.exceptionMessage_def
                            ARM.exceptionMessage_def
                            mapM_x_Cons mapM_x_Nil) apply (rule monadic_rewrite_symb_exec_l) apply (rule_tac P="tcb_at' s and tcb_at' r" in monadic_rewrite_inst) apply (case_tac sb; (case_tac "msgLength tag < scast n_msgRegisters",
                 (erule disjE[OF word_less_cases],
                   ( clarsimp simp: n_msgRegisters_def asUser_bind_distrib
                                    mapM_x_Cons mapM_x_Nil bind_assoc
                                    asUser_mapMloadWordUser_getSanitiseRegisterInfo_comm
                                    asUser_getRegister_getSanitiseRegisterInfo_comm
                                    asUser_getRegister_discarded asUser_mapMloadWordUser_threadGet_comm
                                    asUser_comm[OF neq] asUser_getRegister_threadGet_comm
                                    bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
                                    word_le_nat_alt[of 4, simplified linorder_not_less[symmetric, of 4]]
                                    asUser_return submonad_asUser.fn_stateAssert
                   | rule monadic_rewrite_bind_tail monadic_rewrite_refl
                          monadic_rewrite_symb_exec_l[OF _ stateAssert_inv]
                          monadic_rewrite_symb_exec_l[OF _ mapM_x_mapM_valid[OF mapM_x_wp']]
                   | wp)+)+)) apply wp+ 
     (* capFault *)
      apply (repeat 5 \<open>rule monadic_rewrite_symb_exec_l\<close>)  (* until case sb *)
                     apply (case_tac sb) apply (clarsimp
                           | rule monadic_rewrite_bind_tail monadic_rewrite_refl
                                  monadic_rewrite_symb_exec_l[OF _ mapM_x_mapM_valid[OF mapM_x_wp']]
                           | wp mapM_x_mapM_valid[OF mapM_x_wp'[OF loadWordUser_inv]]
                                empty_fail_loadWordUser)+ 
    (* UnknownSyscallExceptio *)
     apply (simp add: zip_append2 mapM_x_append asUser_bind_distrib split_def bind_assoc) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans[rotated]) apply (rule monadic_rewrite_do_flip) apply (rule monadic_rewrite_bind_tail) apply (rule_tac P="inj (case_bool s r)" in monadic_rewrite_gen_asm) apply (rule monadic_rewrite_trans[OF _ monadic_rewrite_transverse]) apply (rule monadic_rewrite_weaken_flags[where F=False and E=True], simp) apply (rule isolate_thread_actions_rewrite_bind
                     bool.simps setRegister_simple
                     zipWithM_setRegister_simple
                     thread_actions_isolatable_bind lookupIPCBuffer_isolatable
                     lookupIPCBuffer_isolatable[THEN thread_actions_isolatableD]
                     copy_registers_isolate_general thread_actions_isolatable_return
                     thread_actions_isolatable_return[THEN thread_actions_isolatableD]
               | assumption
               | wp assert_inv)+ apply (rule monadic_rewrite_isolate_final[where P="\<top>"]) apply simp+ apply wp 
     (* swap ends *)
      apply (clarsimp simp: handleFaultReply_def zipWithM_x_mapM_x
                            zip_Cons syscallMessage_unfold
                            n_syscallMessage_def
                            upto_enum_word mapM_x_Cons mapM_x_Nil) apply (simp add: getSanitiseRegisterInfo_moreMapM_comm asUser_getRegister_getSanitiseRegisterInfo_comm getSanitiseRegisterInfo_lookupIPCBuffer_comm) apply (rule monadic_rewrite_bind_tail) apply (rule monadic_rewrite_bind_tail [where Q="\<lambda>_. tcb_at' r"]) apply (case_tac sb) apply (case_tac "msgLength tag < scast n_msgRegisters") apply (erule disjE[OF word_less_cases],
                  ( clarsimp simp: n_msgRegisters_def asUser_bind_distrib
                                   mapM_x_Cons mapM_x_Nil bind_assoc
                                   asUser_getRegister_discarded
                                   asUser_comm[OF neq] take_zip
                                   word_le_nat_alt[of 4, simplified linorder_not_less[symmetric, of 4]]
                                   asUser_return submonad_asUser.fn_stateAssert
                  | rule monadic_rewrite_bind_tail monadic_rewrite_refl
                         monadic_rewrite_symb_exec_l[OF _ stateAssert_inv]
                  | wp)+)+ apply (case_tac "msgLength tag < scast n_msgRegisters") apply (erule disjE[OF word_less_cases],
                  ( clarsimp simp: n_msgRegisters_def asUser_bind_distrib
                                   mapM_x_Cons mapM_x_Nil bind_assoc
                                   zipWithM_x_Nil
                                   asUser_getRegister_discarded
                                   asUser_comm[OF neq] take_zip
                                   bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
                                   asUser_return submonad_asUser.fn_stateAssert
                  | rule monadic_rewrite_bind_tail monadic_rewrite_refl
                         monadic_rewrite_symb_exec_l[OF _ mapM_x_mapM_valid[OF mapM_x_wp']]
                         monadic_rewrite_symb_exec_l[OF _ stateAssert_inv]
                  | wp mapM_wp')+)+ apply (simp add: n_msgRegisters_def word_le_nat_alt n_syscallMessage_def
                        linorder_not_less syscallMessage_unfold) apply (clarsimp | frule neq0_conv[THEN iffD2, THEN not0_implies_Suc,
                                         OF order_less_le_trans, rotated])+ apply (subgoal_tac "\<forall>n :: word32. n \<le> scast n_syscallMessage \<longrightarrow> [n .e. msgMaxLength]
                                 = [n .e. scast n_syscallMessage]
                                     @ [scast n_syscallMessage + 1 .e. msgMaxLength]") apply (simp only: upto_enum_word[where y="scast n_syscallMessage :: word32"]
                          upto_enum_word[where y="scast n_syscallMessage + 1 :: word32"]) apply (clarsimp simp: bind_assoc asUser_bind_distrib
                              mapM_x_Cons mapM_x_Nil
                              asUser_comm [OF neq] asUser_getRegister_discarded
                              submonad_asUser.fn_stateAssert take_zip
                              bind_subst_lift [OF submonad_asUser.stateAssert_fn]
                              word_less_nat_alt ARM_H.sanitiseRegister_def
                              split_def n_msgRegisters_def msgMaxLength_def
                              bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
                              word_size msgLengthBits_def n_syscallMessage_def
                   split del: if_split
                        cong: if_weak_cong) apply (rule monadic_rewrite_bind_tail)+ apply (subst (2) upto_enum_word) apply (case_tac "ma < unat n_syscallMessage - 4") apply (erule disjE[OF nat_less_cases'],
                        ( clarsimp simp: n_syscallMessage_def bind_assoc asUser_bind_distrib
                                         mapM_x_Cons mapM_x_Nil zipWithM_x_mapM_x mapM_Cons
                                         bind_comm_mapM_comm [OF asUser_loadWordUser_comm, symmetric]
                                         asUser_loadWordUser_comm loadWordUser_discarded asUser_return
                                         zip_take_triv2 msgMaxLength_def
                                   cong: if_weak_cong
                        | simp
                        | rule monadic_rewrite_bind_tail
                               monadic_rewrite_refl
                               monadic_rewrite_symb_exec_l[OF _ stateAssert_inv]
                               monadic_rewrite_symb_exec_l[OF _ mapM_x_mapM_valid[OF mapM_x_wp']]
                        | wp empty_fail_loadWordUser)+)+ apply (clarsimp simp: upto_enum_word word_le_nat_alt simp del: upt.simps cong: if_weak_cong) apply (cut_tac i="unat n" and j="Suc (unat (scast n_syscallMessage :: word32))"
                                 and k="Suc msgMaxLength" in upt_add_eq_append') apply (simp add: n_syscallMessage_def) apply (simp add: n_syscallMessage_def msgMaxLength_unfold) apply (simp add: n_syscallMessage_def msgMaxLength_def
                        msgLengthBits_def shiftL_nat
                   del: upt.simps upt_rec_numeral) apply (simp add: upto_enum_word cong: if_weak_cong) apply wp+ 
    (* ArchFault *)
     apply (simp add: neq inj_case_bool split: bool.split) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_is_refl) apply (rule ext) apply (unfold handleArchFaultReply'[symmetric] getMRs_def msgMaxLength_def
                  bit_def msgLengthBits_def msgRegisters_unfold
                  fromIntegral_simp1 fromIntegral_simp2 shiftL_word) apply (clarsimp simp: mapM_def sequence_def bind_assoc asUser_bind_distrib
                          asUser_return submonad_asUser.fn_stateAssert) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' s and tcb_at' r) (do tag <- getMessageInfo s;
sb <- lookupIPCBuffer False s;
getMRs s sb tag >>= handleFaultReply f r (msgLabel tag)
od) (handleFaultReply' f s r) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' s and tcb_at' r) (do tag <- getMessageInfo s;
sb <- lookupIPCBuffer False s;
getMRs s sb tag >>= handleFaultReply f r (msgLabel tag)
od) (handleFaultReply' f s r) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' s and tcb_at' r) (do tag <- getMessageInfo s;
sb <- lookupIPCBuffer False s;
do intSize <- return (word_of_nat wordSize);
hardwareMRs <- return (map Register [register.R2, register.R3, register.R4, register.R5]);
hardwareMRValues <- asUser s $ mapM getRegister hardwareMRs;
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * intSize)) [word_of_nat $ length hardwareMRs + 1 .e. 0x78]) >>= mapM loadWordUser;
values <- return (hardwareMRValues @ bufferMRValues);
return $ take (unat $ msgLength tag) values
od >>= handleFaultReply f r (msgLabel tag)
od) (do tag <- getMessageInfo s;
label <- return $ msgLabel tag;
mlen <- return $ msgLength tag;
case f of Fault_H.fault.UserException x xa \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat mlen) FaultHandler_H.exceptionMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
return (label = 0)
od | Fault_H.fault.CapFault x xa xb \<Rightarrow> return True | Fault_H.fault.UnknownSyscallException x \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat mlen) FaultHandler_H.syscallMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
sendBuf <- lookupIPCBuffer False s;
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) regs);
return (label = 0)
od | Fault_H.fault.ArchFault af \<Rightarrow> handleArchFaultReply' af s r tag
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (tcb_at' s and tcb_at' r) (do tag <- getMessageInfo s;
sb <- lookupIPCBuffer False s;
hardwareMRValues <- asUser s (mapM getRegister [register.R2, register.R3, register.R4, register.R5]);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) (hardwareMRValues @ bufferMRValues))
od) (do tag <- getMessageInfo s;
case f of Fault_H.fault.UserException x xa \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.exceptionMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
return (msgLabel tag = 0)
od | Fault_H.fault.CapFault x xa xb \<Rightarrow> return True | Fault_H.fault.UnknownSyscallException x \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.syscallMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
sendBuf <- lookupIPCBuffer False s;
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) regs);
return (msgLabel tag = 0)
od | Fault_H.fault.ArchFault af \<Rightarrow> handleArchFaultReply' af s r tag
od) proof (prove)
goal (2 subgoals):
 1. \<And>tag. monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
hardwareMRValues <- asUser s (mapM getRegister [register.R2, register.R3, register.R4, register.R5]);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) (hardwareMRValues @ bufferMRValues))
od) (case f of Fault_H.fault.UserException x xa \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.exceptionMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
return (msgLabel tag = 0)
od | Fault_H.fault.CapFault x xa xb \<Rightarrow> return True | Fault_H.fault.UnknownSyscallException x \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.syscallMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
sendBuf <- lookupIPCBuffer False s;
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) regs);
return (msgLabel tag = 0)
od | Fault_H.fault.ArchFault af \<Rightarrow> handleArchFaultReply' af s r tag)
 2. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tag. monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (case f of Fault_H.fault.UserException x xa \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.exceptionMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
return (msgLabel tag = 0)
od | Fault_H.fault.CapFault x xa xb \<Rightarrow> return True | Fault_H.fault.UnknownSyscallException x \<Rightarrow> do t <- local.getSanitiseRegisterInfo r;
regs <- return $ take (unat (msgLength tag)) FaultHandler_H.syscallMessage;
zipWithM_x (\<lambda>rs rd. do v <- asUser s $ getRegister rs;
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) (map Register [register.R2, register.R3, register.R4, register.R5]) regs;
sendBuf <- lookupIPCBuffer False s;
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) regs);
return (msgLabel tag = 0)
od | Fault_H.fault.ArchFault af \<Rightarrow> handleArchFaultReply' af s r tag)
 2. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.exceptionMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.exceptionMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.exceptionMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.exceptionMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) [(register.FaultIP, rv), (register.SP, rva), (register.CPSR, rvb)]));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) [(register.R2, register.FaultIP), (register.R3, register.SP), (register.R4, register.CPSR)]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x11 x12 sb. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> monadic_rewrite True False (?Q9 tag x11 x12 sb) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) [(register.FaultIP, rv), (register.SP, rva), (register.CPSR, rvb)]));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) [(register.R2, register.FaultIP), (register.R3, register.SP), (register.R4, register.CPSR)]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x11 x12 P. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>P\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> empty_fail (lookupIPCBuffer False s)
 4. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>?Q1 tag\<rbrace> lookupIPCBuffer False s \<lbrace>?Q9 tag x11 x12\<rbrace>
 5. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 6. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x11 x12 sb. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) [(register.FaultIP, rv), (register.SP, rva), (register.CPSR, rvb)]));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) [(register.R2, register.FaultIP), (register.R3, register.SP), (register.R4, register.CPSR)]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x11 x12 P. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>P\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> empty_fail (lookupIPCBuffer False s)
 4. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>?Q1 tag\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>sb. tcb_at' s and tcb_at' r\<rbrace>
 5. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 6. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x11 x12 P. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>P\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> empty_fail (lookupIPCBuffer False s)
 3. \<And>tag x11 x12. f = Fault_H.fault.UserException x11 x12 \<Longrightarrow> \<lbrace>?Q1 tag\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>sb. tcb_at' s and tcb_at' r\<rbrace>
 4. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q1 tag) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>?Q1\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x21 x22 x23. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rv <- asUser s (getRegister register.R3);
rv <- asUser s (getRegister register.R4);
rv <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (19 subgoals):
 1. \<And>tag x21 x22 x23 sb rv rva rvb rvc. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q675 tag x21 x22 x23 sb rv rva rvb rvc) (do bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 2. \<And>tag x21 x22 x23 sb rv rva rvb P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R5) \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R5))
 4. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q670 tag x21 x22 x23 sb rv rva rvb\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q675 tag x21 x22 x23 sb rv rva rvb\<rbrace>
 5. \<And>tag x21 x22 x23 sb rv rva P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R4) \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R4))
 7. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q665 tag x21 x22 x23 sb rv rva\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q670 tag x21 x22 x23 sb rv rva\<rbrace>
 8. \<And>tag x21 x22 x23 sb rv P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R3) \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>tag x21 x22 x23 sb rv. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R3))
 10. \<And>tag x21 x22 x23 sb rv. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q660 tag x21 x22 x23 sb rv\<rbrace> asUser s (getRegister register.R3) \<lbrace>?Q665 tag x21 x22 x23 sb rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (19 subgoals):
 1. \<And>tag x21 x22 x23 sb rv rva rvb rvc. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> monadic_rewrite True False (?Q675 tag x21 x22 x23 sb rv rva rvb rvc) (do bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 2. \<And>tag x21 x22 x23 sb rv rva rvb P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R5) \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R5))
 4. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q670 tag x21 x22 x23 sb rv rva rvb\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q675 tag x21 x22 x23 sb rv rva rvb\<rbrace>
 5. \<And>tag x21 x22 x23 sb rv rva P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R4) \<lbrace>\<lambda>_. P\<rbrace>
 6. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R4))
 7. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q665 tag x21 x22 x23 sb rv rva\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q670 tag x21 x22 x23 sb rv rva\<rbrace>
 8. \<And>tag x21 x22 x23 sb rv P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R3) \<lbrace>\<lambda>_. P\<rbrace>
 9. \<And>tag x21 x22 x23 sb rv. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R3))
 10. \<And>tag x21 x22 x23 sb rv. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q660 tag x21 x22 x23 sb rv\<rbrace> asUser s (getRegister register.R3) \<lbrace>?Q665 tag x21 x22 x23 sb rv\<rbrace>
A total of 19 subgoals... proof (prove)
goal (20 subgoals):
 1. \<And>tag x21 x22 x23 sb rv rva rvb rvc. \<lbrakk>f = Fault_H.fault.CapFault x21 x22 x23; sb = None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q675 tag x21 x22 x23 sb rv rva rvb rvc) (do bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 2. \<And>tag x21 x22 x23 sb rv rva rvb rvc a. \<lbrakk>f = Fault_H.fault.CapFault x21 x22 x23; sb = Some a\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q675 tag x21 x22 x23 sb rv rva rvb rvc) (do bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) (return True)
 3. \<And>tag x21 x22 x23 sb rv rva rvb P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R5) \<lbrace>\<lambda>_. P\<rbrace>
 4. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R5))
 5. \<And>tag x21 x22 x23 sb rv rva rvb. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q670 tag x21 x22 x23 sb rv rva rvb\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q675 tag x21 x22 x23 sb rv rva rvb\<rbrace>
 6. \<And>tag x21 x22 x23 sb rv rva P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R4) \<lbrace>\<lambda>_. P\<rbrace>
 7. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R4))
 8. \<And>tag x21 x22 x23 sb rv rva. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>?Q665 tag x21 x22 x23 sb rv rva\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q670 tag x21 x22 x23 sb rv rva\<rbrace>
 9. \<And>tag x21 x22 x23 sb rv P. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> \<lbrace>P\<rbrace> asUser s (getRegister register.R3) \<lbrace>\<lambda>_. P\<rbrace>
 10. \<And>tag x21 x22 x23 sb rv. f = Fault_H.fault.CapFault x21 x22 x23 \<Longrightarrow> empty_fail (asUser s (getRegister register.R3))
A total of 20 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>(x, y). setRegister x (local.sanitiseRegister b x y)) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>(x, y). do v <- asUser s (getRegister x);
asUser r (setRegister y (local.sanitiseRegister t y v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister t (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q767 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister t (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> ?Q767 tag x3 sa
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q770 tag x3) (?g770 tag x3) (do t <- local.getSanitiseRegisterInfo r;
y <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister t (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
sendBuf <- lookupIPCBuffer False s;
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister t rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (?g770 tag x3)
 3. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q770 tag x3) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
return (a, c)
od) (do c <- local.getSanitiseRegisterInfo r;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
a <- lookupIPCBuffer False s;
return (a, c)
od)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 c. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q775 tag x3 c) (do a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
return (a, c)
od) (do b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
a <- lookupIPCBuffer False s;
return (a, c)
od)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q775 tag x3\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q778 tag x3 c) (do a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
return (a, c)
od) (do b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
a <- lookupIPCBuffer False s;
return (a, c)
od)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and ?Q778 tag x3 c\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P779 tag x3 c) (do a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
return (a, c)
od) (?g779 tag x3 c)
 2. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite False True (?Q780 tag x3 c) (do b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
a <- lookupIPCBuffer False s;
return (a, c)
od) (?b780 tag x3 c)
 3. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P780 tag x3 c) (?g779 tag x3 c) (?b780 tag x3 c)
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and (?P779 tag x3 c and (?P780 tag x3 c and ?Q780 tag x3 c))\<rbrace>
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 6. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite False True (?P779 tag x3 c) (do a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
return (a, c)
od) (?g779 tag x3 c)
 2. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite False True (?Q780 tag x3 c) (do b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
a <- lookupIPCBuffer False s;
return (a, c)
od) (?b780 tag x3 c)
 3. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P780 tag x3 c) (?g779 tag x3 c) (?b780 tag x3 c)
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and (?P779 tag x3 c and (?P780 tag x3 c and ?Q780 tag x3 c))\<rbrace>
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 6. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?P780 tag x3 c) (isolate_thread_actions (case_bool s r) (do x <- lookupIPCBuffer False s;
xa <- return ();
return (x, c)
od) (id \<circ> foldr (\<lambda>r. copy_register_tsrs True False (fst r) (snd r) (local.sanitiseRegister c (snd r))) (rev (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage))) \<circ> id) (id \<circ> id \<circ> id)) (isolate_thread_actions (case_bool s r) (do x <- return ();
xa <- lookupIPCBuffer False s;
return (xa, c)
od) (id \<circ> id \<circ> foldr (\<lambda>r. copy_register_tsrs True False (fst r) (snd r) (local.sanitiseRegister c (snd r))) (rev (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage)))) (id \<circ> id \<circ> id))
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and ((\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa) and (?P780 tag x3 c and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa)))\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x3 c. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r)\<rbrakk> \<Longrightarrow> do x <- lookupIPCBuffer False s;
xa <- return ();
return (x, c)
od = do x <- return ();
xa <- lookupIPCBuffer False s;
return (xa, c)
od
 2. \<And>tag x3 c sa tsrs. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r); True; tsrs = get_tcb_state_regs \<circ> ksPSpace sa \<circ> case_bool s r\<rbrakk> \<Longrightarrow> (id \<circ> foldr (\<lambda>r. copy_register_tsrs True False (fst r) (snd r) (local.sanitiseRegister c (snd r))) (rev (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage))) \<circ> id) tsrs = (id \<circ> id \<circ> foldr (\<lambda>r. copy_register_tsrs True False (fst r) (snd r) (local.sanitiseRegister c (snd r))) (rev (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage)))) tsrs
 3. \<And>tag x3 c sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; inj (case_bool s r); True\<rbrakk> \<Longrightarrow> (id \<circ> id \<circ> id) (ksSchedulerAction sa) = (id \<circ> id \<circ> id) (ksSchedulerAction sa)
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and ((\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa) and ((\<lambda>_. True) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa)))\<rbrace>
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 6. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>\<lambda>c. (\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa)\<rbrace>
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ?Q770 tag x3) sa
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) (zip FaultHandler_H.syscallMessage (rv # rva # rvb # rvc # bufferMRValues))));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) (zip [register.R2, register.R3, register.R4, register.R5] FaultHandler_H.syscallMessage));
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
b <- local.getSanitiseRegisterInfo r;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?P770 tag x3) (do b <- local.getSanitiseRegisterInfo r;
sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do c <- local.getSanitiseRegisterInfo r;
a <- lookupIPCBuffer False s;
b <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister c (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister c rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 3. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 4. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (?Q900 tag x3 b) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do a <- lookupIPCBuffer False s;
ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case a of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 3. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 b sb. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 b sb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; sb = None\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b sb a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; sb = Some a\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x3 b sb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; sb = None; msgLength tag < SCAST(32 signed \<rightarrow> 32) n_msgRegisters\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b sb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; sb = None; \<not> msgLength tag < SCAST(32 signed \<rightarrow> 32) n_msgRegisters\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 b sb a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; sb = Some a\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> zipWithM_x (\<lambda>i rd. do v <- loadWordUser (bufferPtr + PPtr (i * 4));
asUser r $ setRegister rd $ local.sanitiseRegister b rd v
od) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop (unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)) (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 4. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 6. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 b a. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop 4 (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 b a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; msgLength tag < SCAST(32 signed \<rightarrow> 32) n_msgRegisters\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop 4 (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; \<not> msgLength tag < SCAST(32 signed \<rightarrow> 32) n_msgRegisters\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop 4 (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 b a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; \<not> msgLength tag < 4\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) (take (unat (msgLength tag)) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)]);
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] (drop 4 (take (unat (msgLength tag)) FaultHandler_H.syscallMessage));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 b a. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; 4 \<le> unat (msgLength tag)\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) (take (unat (msgLength tag)) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)];
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. 0xC] (drop 4 (take (unat (msgLength tag)) [register.R0, register.R1, register.R2, register.R3, register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]));
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # take ma (zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)];
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. 0xC] (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # take ma (zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)];
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. 0xC] (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = map word_of_nat [unat n..<Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- mapM loadWordUser (map (\<lambda>x. a + x * 4) [5 .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (local.sanitiseRegister b (fst p) (snd p))) ((register.R0, rv) # (register.R1, rva) # (register.R2, rvb) # (register.R3, rvc) # take ma (zip [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR] bufferMRValues)));
return (msgLabel tag = 0)
od) (do ba <- mapM_x (\<lambda>p. do v <- asUser s (getRegister (fst p));
asUser r (setRegister (snd p) (local.sanitiseRegister b (snd p) v))
od) [(register.R2, register.R0), (register.R3, register.R1), (register.R4, register.R2), (register.R5, register.R3)];
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (local.sanitiseRegister b rd v))
od) [5 .e. 0xC] (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> monadic_rewrite True False (tcb_at' r) (do rv <- asUser s (getRegister register.R2);
rv <- asUser r (setRegister register.R0 rv);
rv <- asUser s (getRegister register.R3);
rv <- asUser r (setRegister register.R1 rv);
rv <- asUser s (getRegister register.R4);
rv <- asUser r (setRegister register.R2 rv);
rv <- asUser s (getRegister register.R5);
rv <- asUser r (setRegister register.R3 rv);
bufferMRValues <- mapM loadWordUser ((a + 0x14) # (a + 0x18) # (a + 0x1C) # (a + 0x20) # (a + 0x24) # (a + 0x28) # (a + 0x2C) # (a + 0x30) # map (\<lambda>x. a + x * 4) [0xD .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (case fst p of register.CPSR \<Rightarrow> snd p && 0xF8000000 || 0x150 | _ \<Rightarrow> snd p)) (zip (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]) (take ma bufferMRValues)));
return (msgLabel tag = 0)
od) (do v <- asUser s (getRegister register.R2);
y <- asUser r (setRegister register.R0 v);
v <- asUser s (getRegister register.R3);
y <- asUser r (setRegister register.R1 v);
v <- asUser s (getRegister register.R4);
y <- asUser r (setRegister register.R2 v);
v <- asUser s (getRegister register.R5);
b <- asUser r (setRegister register.R3 v);
y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (case rd of register.CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))
od) [5 .e. 0xC] (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (15 subgoals):
 1. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf rvg. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q1508 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (do bufferMRValues <- mapM loadWordUser ((a + 0x14) # (a + 0x18) # (a + 0x1C) # (a + 0x20) # (a + 0x24) # (a + 0x28) # (a + 0x2C) # (a + 0x30) # map (\<lambda>x. a + x * 4) [0xD .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (case fst p of register.CPSR \<Rightarrow> snd p && 0xF8000000 || 0x150 | _ \<Rightarrow> snd p)) (zip (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]) (take ma bufferMRValues)));
return (msgLabel tag = 0)
od) (do y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (case rd of register.CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))
od) [5 .e. 0xC] (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve rvf\<rbrace> asUser r (setRegister register.R3 rvf) \<lbrace>?Q1508 tag x3 a ma rv rva rvb rvc rvd rve rvf\<rbrace>
 3. \<And>tag x3 a ma rv rva rvb rvc rvd rve. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace>
 4. \<And>tag x3 a ma rv rva rvb rvc rvd. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc rvd\<rbrace> asUser r (setRegister register.R2 rvd) \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd\<rbrace>
 5. \<And>tag x3 a ma rv rva rvb rvc. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1496 tag x3 a ma rv rva rvb rvc\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc\<rbrace>
 6. \<And>tag x3 a ma rv rva rvb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1493 tag x3 a ma rv rva rvb\<rbrace> asUser r (setRegister register.R1 rvb) \<lbrace>?Q1496 tag x3 a ma rv rva rvb\<rbrace>
 7. \<And>tag x3 a ma rv rva. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1490 tag x3 a ma rv rva\<rbrace> asUser s (getRegister register.R3) \<lbrace>?Q1493 tag x3 a ma rv rva\<rbrace>
 8. \<And>tag x3 a ma rv. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1487 tag x3 a ma rv\<rbrace> asUser r (setRegister register.R0 rv) \<lbrace>?Q1490 tag x3 a ma rv\<rbrace>
 9. \<And>tag x3 a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' r\<rbrace> asUser s (getRegister register.R2) \<lbrace>?Q1487 tag x3 a ma\<rbrace>
 10. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf rvg. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q1513 tag tag x3 a ma rv rva rvb rvc rvd rve rvf rvg (?x3.1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) a ma (?rv1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rva1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvb1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvc1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvd1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rve1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvf1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvg1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg)) (do bufferMRValues <- mapM loadWordUser ((a + 0x14) # (a + 0x18) # (a + 0x1C) # (a + 0x20) # (a + 0x24) # (a + 0x28) # (a + 0x2C) # (a + 0x30) # map (\<lambda>x. a + x * 4) [0xD .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (case fst p of register.CPSR \<Rightarrow> snd p && 0xF8000000 || 0x150 | _ \<Rightarrow> snd p)) (zip (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]) (take ma bufferMRValues)));
return (msgLabel tag = 0)
od) (do y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (case rd of register.CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))
od) (map word_of_nat [unat 5..<Suc (unat 0xC)]) (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve rvf\<rbrace> asUser r (setRegister register.R3 rvf) \<lbrace>\<lambda>rvg. ?Q1513 tag tag x3 a ma rv rva rvb rvc rvd rve rvf rvg (?x3.1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) a ma (?rv1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rva1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvb1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvc1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvd1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rve1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvf1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvg1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg)\<rbrace>
 3. \<And>tag x3 a ma rv rva rvb rvc rvd rve. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace>
 4. \<And>tag x3 a ma rv rva rvb rvc rvd. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc rvd\<rbrace> asUser r (setRegister register.R2 rvd) \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd\<rbrace>
 5. \<And>tag x3 a ma rv rva rvb rvc. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1496 tag x3 a ma rv rva rvb rvc\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc\<rbrace>
 6. \<And>tag x3 a ma rv rva rvb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1493 tag x3 a ma rv rva rvb\<rbrace> asUser r (setRegister register.R1 rvb) \<lbrace>?Q1496 tag x3 a ma rv rva rvb\<rbrace>
 7. \<And>tag x3 a ma rv rva. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1490 tag x3 a ma rv rva\<rbrace> asUser s (getRegister register.R3) \<lbrace>?Q1493 tag x3 a ma rv rva\<rbrace>
 8. \<And>tag x3 a ma rv. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1487 tag x3 a ma rv\<rbrace> asUser r (setRegister register.R0 rv) \<lbrace>?Q1490 tag x3 a ma rv\<rbrace>
 9. \<And>tag x3 a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' r\<rbrace> asUser s (getRegister register.R2) \<lbrace>?Q1487 tag x3 a ma\<rbrace>
 10. \<And>tag x3 b a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma)))\<rbrakk> \<Longrightarrow> \<forall>n\<le>SCAST(32 signed \<rightarrow> 32) n_syscallMessage. [n .e. msgMaxLength] = [n .e. SCAST(32 signed \<rightarrow> 32) n_syscallMessage] @ [SCAST(32 signed \<rightarrow> 32) n_syscallMessage + 1 .e. msgMaxLength]
A total of 15 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf rvg. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]; ma < unat n_syscallMessage - 4\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q1513 tag tag x3 a ma rv rva rvb rvc rvd rve rvf rvg (?x3.1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) a ma (?rv1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rva1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvb1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvc1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvd1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rve1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvf1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvg1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg)) (do bufferMRValues <- mapM loadWordUser ((a + 0x14) # (a + 0x18) # (a + 0x1C) # (a + 0x20) # (a + 0x24) # (a + 0x28) # (a + 0x2C) # (a + 0x30) # map (\<lambda>x. a + x * 4) [0xD .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (case fst p of register.CPSR \<Rightarrow> snd p && 0xF8000000 || 0x150 | _ \<Rightarrow> snd p)) (zip (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]) (take ma bufferMRValues)));
return (msgLabel tag = 0)
od) (do y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (case rd of register.CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))
od) (map word_of_nat [unat 5..<Suc (unat 0xC)]) (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 2. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf rvg. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]; \<not> ma < unat n_syscallMessage - 4\<rbrakk> \<Longrightarrow> monadic_rewrite True False (?Q1513 tag tag x3 a ma rv rva rvb rvc rvd rve rvf rvg (?x3.1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) a ma (?rv1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rva1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvb1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvc1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvd1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rve1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvf1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvg1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg)) (do bufferMRValues <- mapM loadWordUser ((a + 0x14) # (a + 0x18) # (a + 0x1C) # (a + 0x20) # (a + 0x24) # (a + 0x28) # (a + 0x2C) # (a + 0x30) # map (\<lambda>x. a + x * 4) [0xD .e. 0x78]);
y <- asUser r (mapM_x (\<lambda>p. setRegister (fst p) (case fst p of register.CPSR \<Rightarrow> snd p && 0xF8000000 || 0x150 | _ \<Rightarrow> snd p)) (zip (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]) (take ma bufferMRValues)));
return (msgLabel tag = 0)
od) (do y <- zipWithM_x (\<lambda>i rd. do v <- loadWordUser (a + i * 4);
asUser r (setRegister rd (case rd of register.CPSR \<Rightarrow> v && 0xF8000000 || 0x150 | _ \<Rightarrow> v))
od) (map word_of_nat [unat 5..<Suc (unat 0xC)]) (take ma [register.R4, register.R5, register.R6, register.R7, register.FaultIP, register.SP, register.LR, register.CPSR]);
return (msgLabel tag = 0)
od)
 3. \<And>tag x3 a ma rv rva rvb rvc rvd rve rvf. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve rvf\<rbrace> asUser r (setRegister register.R3 rvf) \<lbrace>\<lambda>rvg. ?Q1513 tag tag x3 a ma rv rva rvb rvc rvd rve rvf rvg (?x3.1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) a ma (?rv1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rva1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvb1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvc1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvd1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rve1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvf1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg) (?rvg1512 tag x3 a ma rv rva rvb rvc rvd rve rvf rvg)\<rbrace>
 4. \<And>tag x3 a ma rv rva rvb rvc rvd rve. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace> asUser s (getRegister register.R5) \<lbrace>?Q1505 tag x3 a ma rv rva rvb rvc rvd rve\<rbrace>
 5. \<And>tag x3 a ma rv rva rvb rvc rvd. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc rvd\<rbrace> asUser r (setRegister register.R2 rvd) \<lbrace>?Q1502 tag x3 a ma rv rva rvb rvc rvd\<rbrace>
 6. \<And>tag x3 a ma rv rva rvb rvc. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1496 tag x3 a ma rv rva rvb rvc\<rbrace> asUser s (getRegister register.R4) \<lbrace>?Q1499 tag x3 a ma rv rva rvb rvc\<rbrace>
 7. \<And>tag x3 a ma rv rva rvb. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1493 tag x3 a ma rv rva rvb\<rbrace> asUser r (setRegister register.R1 rvb) \<lbrace>?Q1496 tag x3 a ma rv rva rvb\<rbrace>
 8. \<And>tag x3 a ma rv rva. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1490 tag x3 a ma rv rva\<rbrace> asUser s (getRegister register.R3) \<lbrace>?Q1493 tag x3 a ma rv rva\<rbrace>
 9. \<And>tag x3 a ma rv. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>?Q1487 tag x3 a ma rv\<rbrace> asUser r (setRegister register.R0 rv) \<lbrace>?Q1490 tag x3 a ma rv\<rbrace>
 10. \<And>tag x3 a ma. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); \<forall>n\<le>0xC. [n .e. 0x78] = map word_of_nat [unat n..<13] @ [0xD .e. 0x78]\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' r\<rbrace> asUser s (getRegister register.R2) \<lbrace>?Q1487 tag x3 a ma\<rbrace>
A total of 16 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); n \<le> 0xC\<rbrakk> \<Longrightarrow> [n .e. 0x78] = [n .e. 0xC] @ [0xD .e. 0x78]
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12\<rbrakk> \<Longrightarrow> map word_of_nat [unat n..<121] = map word_of_nat [unat n..<13] @ [0xD, 0xE, 0xF, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1A, 0x1B, 0x1C, 0x1D, 0x1E, 0x1F, 0x20, 0x21, 0x22, 0x23, 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2A, 0x2B, 0x2C, 0x2D, 0x2E, 0x2F, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39, 0x3A, 0x3B, 0x3C, 0x3D, 0x3E, 0x3F, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48, 0x49, 0x4A, 0x4B, 0x4C, 0x4D, 0x4E, 0x4F, 0x50, 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5A, 0x5B, 0x5C, 0x5D, 0x5E, 0x5F, 0x60, 0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6A, 0x6B, 0x6C, 0x6D, 0x6E, 0x6F, 0x70, 0x71, 0x72, 0x73, 0x74, 0x75, 0x76, 0x77, 0x78]
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12\<rbrakk> \<Longrightarrow> unat n \<le> Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))
 2. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12\<rbrakk> \<Longrightarrow> Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage)) \<le> Suc msgMaxLength
 3. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12; [unat n..<Suc msgMaxLength] = [unat n..<Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))] @ [Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))..<Suc msgMaxLength]\<rbrakk> \<Longrightarrow> map word_of_nat [unat n..<121] = map word_of_nat [unat n..<13] @ [0xD, 0xE, 0xF, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1A, 0x1B, 0x1C, 0x1D, 0x1E, 0x1F, 0x20, 0x21, 0x22, 0x23, 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2A, 0x2B, 0x2C, 0x2D, 0x2E, 0x2F, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39, 0x3A, 0x3B, 0x3C, 0x3D, 0x3E, 0x3F, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48, 0x49, 0x4A, 0x4B, 0x4C, 0x4D, 0x4E, 0x4F, 0x50, 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5A, 0x5B, 0x5C, 0x5D, 0x5E, 0x5F, 0x60, 0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6A, 0x6B, 0x6C, 0x6D, 0x6E, 0x6F, 0x70, 0x71, 0x72, 0x73, 0x74, 0x75, 0x76, 0x77, 0x78]
 4. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 5. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 6. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 7. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 8. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12\<rbrakk> \<Longrightarrow> Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage)) \<le> Suc msgMaxLength
 2. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12; [unat n..<Suc msgMaxLength] = [unat n..<Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))] @ [Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))..<Suc msgMaxLength]\<rbrakk> \<Longrightarrow> map word_of_nat [unat n..<121] = map word_of_nat [unat n..<13] @ [0xD, 0xE, 0xF, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1A, 0x1B, 0x1C, 0x1D, 0x1E, 0x1F, 0x20, 0x21, 0x22, 0x23, 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2A, 0x2B, 0x2C, 0x2D, 0x2E, 0x2F, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39, 0x3A, 0x3B, 0x3C, 0x3D, 0x3E, 0x3F, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48, 0x49, 0x4A, 0x4B, 0x4C, 0x4D, 0x4E, 0x4F, 0x50, 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5A, 0x5B, 0x5C, 0x5D, 0x5E, 0x5F, 0x60, 0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6A, 0x6B, 0x6C, 0x6D, 0x6E, 0x6F, 0x70, 0x71, 0x72, 0x73, 0x74, 0x75, 0x76, 0x77, 0x78]
 3. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 4. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 5. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 6. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 7. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12; [unat n..<Suc msgMaxLength] = [unat n..<Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))] @ [Suc (unat (SCAST(32 signed \<rightarrow> 32) n_syscallMessage))..<Suc msgMaxLength]\<rbrakk> \<Longrightarrow> map word_of_nat [unat n..<121] = map word_of_nat [unat n..<13] @ [0xD, 0xE, 0xF, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1A, 0x1B, 0x1C, 0x1D, 0x1E, 0x1F, 0x20, 0x21, 0x22, 0x23, 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2A, 0x2B, 0x2C, 0x2D, 0x2E, 0x2F, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39, 0x3A, 0x3B, 0x3C, 0x3D, 0x3E, 0x3F, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48, 0x49, 0x4A, 0x4B, 0x4C, 0x4D, 0x4E, 0x4F, 0x50, 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5A, 0x5B, 0x5C, 0x5D, 0x5E, 0x5F, 0x60, 0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6A, 0x6B, 0x6C, 0x6D, 0x6E, 0x6F, 0x70, 0x71, 0x72, 0x73, 0x74, 0x75, 0x76, 0x77, 0x78]
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>tag x3 ma n. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; unat (msgLength tag) = Suc (Suc (Suc (Suc ma))); unat n \<le> 12; [unat n..<121] = [unat n..<13] @ [13..<121]\<rbrakk> \<Longrightarrow> map word_of_nat [13..<121] = [0xD, 0xE, 0xF, 0x10, 0x11, 0x12, 0x13, 0x14, 0x15, 0x16, 0x17, 0x18, 0x19, 0x1A, 0x1B, 0x1C, 0x1D, 0x1E, 0x1F, 0x20, 0x21, 0x22, 0x23, 0x24, 0x25, 0x26, 0x27, 0x28, 0x29, 0x2A, 0x2B, 0x2C, 0x2D, 0x2E, 0x2F, 0x30, 0x31, 0x32, 0x33, 0x34, 0x35, 0x36, 0x37, 0x38, 0x39, 0x3A, 0x3B, 0x3C, 0x3D, 0x3E, 0x3F, 0x40, 0x41, 0x42, 0x43, 0x44, 0x45, 0x46, 0x47, 0x48, 0x49, 0x4A, 0x4B, 0x4C, 0x4D, 0x4E, 0x4F, 0x50, 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5A, 0x5B, 0x5C, 0x5D, 0x5E, 0x5F, 0x60, 0x61, 0x62, 0x63, 0x64, 0x65, 0x66, 0x67, 0x68, 0x69, 0x6A, 0x6B, 0x6C, 0x6D, 0x6E, 0x6F, 0x70, 0x71, 0x72, 0x73, 0x74, 0x75, 0x76, 0x77, 0x78]
 2. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 3. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 4. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 5. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 6. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tag x3 b. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?Q900 tag x3 b\<rbrace> lookupIPCBuffer False s \<lbrace>\<lambda>_. tcb_at' r\<rbrace>
 2. \<And>tag x3. f = Fault_H.fault.UnknownSyscallException x3 \<Longrightarrow> \<lbrace>?P770 tag x3\<rbrace> local.getSanitiseRegisterInfo r \<lbrace>?Q900 tag x3\<rbrace>
 3. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (?P770 tag x3 and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 4. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 5. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (tcb_at' r and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 2. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x3 sa. \<lbrakk>f = Fault_H.fault.UnknownSyscallException x3; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> (tcb_at' r and ((\<lambda>_. inj (case_bool s r)) and (\<lambda>sa. \<forall>x. tcb_at' (case x of True \<Rightarrow> s | False \<Rightarrow> r) sa))) sa
 2. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (tcb_at' s and tcb_at' r) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 2. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> monadic_rewrite True False (?Q3241 tag x4) (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) (handleArchFaultReply' x4 s r tag)
 2. \<And>tag x4 sa. \<lbrakk>f = Fault_H.fault.ArchFault x4; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> ?Q3241 tag x4 sa
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x4. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od = handleArchFaultReply' x4 s r tag
 2. \<And>tag x4 sa. \<lbrakk>f = Fault_H.fault.ArchFault x4; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> True
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x4 x. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) x = handleArchFaultReply' x4 s r tag x
 2. \<And>tag x4 sa. \<lbrakk>f = Fault_H.fault.ArchFault x4; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> True
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tag x4 x. f = Fault_H.fault.ArchFault x4 \<Longrightarrow> (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply x4 r (msgLabel tag) (take (unat (msgLength tag)) (rv # rva # rvb # rvc # bufferMRValues))
od) x = (do sb <- lookupIPCBuffer False s;
do intSize <- return (word_of_nat wordSize);
hardwareMRs <- return (map Register [register.R2, register.R3, register.R4, register.R5]);
hardwareMRValues <- asUser s $ mapM getRegister hardwareMRs;
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * intSize)) [word_of_nat $ length hardwareMRs + 1 .e. 0x78]) >>= mapM loadWordUser;
values <- return (hardwareMRValues @ bufferMRValues);
return $ take (unat $ msgLength tag) values
od >>= handleArchFaultReply x4 r (msgLabel tag)
od) x
 2. \<And>tag x4 sa. \<lbrakk>f = Fault_H.fault.ArchFault x4; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> True
 3. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>tag x4 sa. \<lbrakk>f = Fault_H.fault.ArchFault x4; (tcb_at' s and tcb_at' r) sa\<rbrakk> \<Longrightarrow> True
 2. \<lbrace>tcb_at' s and tcb_at' r\<rbrace> getMessageInfo s \<lbrace>\<lambda>tag. tcb_at' s and tcb_at' r\<rbrace> proof (prove)
goal:
No subgoals!