theory IsolatedThreadAction

lemma doIPCTransfer_simple_rewrite:
  "monadic_rewrite True True
   ((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0
               \<and> msgLength (messageInfoFromWord msgInfo)
                      \<le> of_nat (length msgRegisters))
      and obj_at' (\<lambda>tcb. tcbFault tcb = None
               \<and> (atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender)
   (doIPCTransfer sender ep badge grant rcvr)
   (do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
                             asUser rcvr (setRegister r v)
                          od)
               (take (unat (msgLength (messageInfoFromWord msgInfo))) msgRegisters);
         y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
         asUser rcvr (setRegister badgeRegister badge)
      od)" supply if_cong[cong] apply (rule monadic_rewrite_gen_asm) apply (simp add: doIPCTransfer_def bind_assoc doNormalTransfer_def
                   getMessageInfo_def
             cong: option.case_cong) apply (rule monadic_rewrite_guard_imp) apply (rule monadic_rewrite_trans) apply (rule monadic_rewrite_bind_tail) apply (monadic_rewrite_symb_exec_l_known None, simp) apply (rule monadic_rewrite_bind_tail) apply (monadic_rewrite_symb_exec_l_known msgInfo) apply (simp add: lookupExtraCaps_simple_rewrite returnOk_catch_bind) apply (rule monadic_rewrite_bind) apply (rule monadic_rewrite_from_simple, rule copyMRs_simple) apply (rule monadic_rewrite_bind_head) apply (rule transferCaps_simple_rewrite) apply (wp threadGet_const user_getreg_rv asUser_inv)+ apply (simp add: bind_assoc) apply (rule monadic_rewrite_symb_exec_l_drop[OF _ lookupIPC_inv empty_fail_lookupIPCBuffer]
               monadic_rewrite_symb_exec_l_drop[OF _ threadGet_inv empty_fail_threadGet]
               monadic_rewrite_symb_exec_l_drop[OF _ user_getreg_inv' empty_fail_user_getreg]
               monadic_rewrite_bind_head monadic_rewrite_bind_tail)+ apply (case_tac "messageInfoFromWord msgInfo") apply simp apply (rule monadic_rewrite_refl) apply wp apply clarsimp apply (auto elim!: obj_at'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender) (doIPCTransfer sender ep badge grant rcvr) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True ((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender) (doIPCTransfer sender ep badge grant rcvr) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) proof (prove)
goal (1 subgoal):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender) (doIPCTransfer sender ep badge grant rcvr) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) proof (prove)
goal (1 subgoal):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender) (do receiveBuffer <- lookupIPCBuffer True rcvr;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od | Some v21 \<Rightarrow> doFaultTransfer badge sender rcvr receiveBuffer
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) proof (prove)
goal (2 subgoals):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q10 (do receiveBuffer <- lookupIPCBuffer True rcvr;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od | Some v21 \<Rightarrow> doFaultTransfer badge sender rcvr receiveBuffer
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ?Q10 s proof (prove)
goal (3 subgoals):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?P13 (do receiveBuffer <- lookupIPCBuffer True rcvr;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od | Some v21 \<Rightarrow> doFaultTransfer badge sender rcvr receiveBuffer
od) ?g13
 2. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 ?g13 (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 3. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (4 subgoals):
 1. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q16 receiveBuffer) (do fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od | Some v21 \<Rightarrow> doFaultTransfer badge sender rcvr receiveBuffer
od) (?j16 receiveBuffer)
 2. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>?Q16\<rbrace>
 3. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (lookupIPCBuffer True rcvr >>= ?j16) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 4. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (5 subgoals):
 1. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q20 receiveBuffer) (do sendBuffer <- lookupIPCBuffer False sender;
x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j16 receiveBuffer)
 2. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 3. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 4. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (lookupIPCBuffer True rcvr >>= ?j16) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 5. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (6 subgoals):
 1. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q42 receiveBuffer sendBuffer) (do x <- asUser sender (getRegister TCB_H.msgInfoRegister);
caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord x) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord x));
tag' <- transferCaps (messageInfoFromWord x) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j42 receiveBuffer sendBuffer)
 2. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>?Q42 receiveBuffer\<rbrace>
 3. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 4. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 5. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
lookupIPCBuffer False sender >>= ?j42 x
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 6. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (7 subgoals):
 1. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q46 receiveBuffer sendBuffer) (do caps <- if grant then lookupExtraCaps sender sendBuffer (messageInfoFromWord msgInfo) <catch> const (return []) else return [];
msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord msgInfo));
tag' <- transferCaps (messageInfoFromWord msgInfo) caps ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j42 receiveBuffer sendBuffer)
 2. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 3. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and ?Q46 receiveBuffer sendBuffer\<rbrace>
 4. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 5. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 6. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
lookupIPCBuffer False sender >>= ?j42 x
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 7. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (7 subgoals):
 1. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q46 receiveBuffer sendBuffer) (do msgTransferred <- copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord msgInfo));
tag' <- transferCaps (messageInfoFromWord msgInfo) [] ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgTransferred) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j42 receiveBuffer sendBuffer)
 2. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 3. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and ?Q46 receiveBuffer sendBuffer\<rbrace>
 4. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 5. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 6. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
lookupIPCBuffer False sender >>= ?j42 x
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 7. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (9 subgoals):
 1. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?P67 receiveBuffer sendBuffer) (copyMRs sender sendBuffer rcvr receiveBuffer (msgLength (messageInfoFromWord msgInfo))) (?g67 receiveBuffer sendBuffer)
 2. \<And>receiveBuffer sendBuffer x. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q67 receiveBuffer sendBuffer x) (do tag' <- transferCaps (messageInfoFromWord msgInfo) [] ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. x) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j67 receiveBuffer sendBuffer x)
 3. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?R67 receiveBuffer sendBuffer\<rbrace> ?g67 receiveBuffer sendBuffer \<lbrace>?Q67 receiveBuffer sendBuffer\<rbrace>
 4. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 5. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and (?P67 receiveBuffer sendBuffer and ?R67 receiveBuffer sendBuffer)\<rbrace>
 6. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 7. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 8. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
xa <- lookupIPCBuffer False sender;
?g67 x xa >>= ?j67 x xa
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 9. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (8 subgoals):
 1. \<And>receiveBuffer sendBuffer x. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q67 receiveBuffer sendBuffer x) (do tag' <- transferCaps (messageInfoFromWord msgInfo) [] ep rcvr receiveBuffer;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. x) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (?j67 receiveBuffer sendBuffer x)
 2. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?R67 receiveBuffer sendBuffer\<rbrace> do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od \<lbrace>?Q67 receiveBuffer sendBuffer\<rbrace>
 3. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 4. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and ?R67 receiveBuffer sendBuffer)\<rbrace>
 5. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 6. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 7. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
xa <- lookupIPCBuffer False sender;
do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od >>= ?j67 x xa
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 8. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (8 subgoals):
 1. \<And>receiveBuffer sendBuffer x. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q67 receiveBuffer sendBuffer x) (transferCaps (messageInfoFromWord msgInfo) [] ep rcvr receiveBuffer) (?g75 receiveBuffer sendBuffer x)
 2. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?R67 receiveBuffer sendBuffer\<rbrace> do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od \<lbrace>?Q67 receiveBuffer sendBuffer\<rbrace>
 3. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 4. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and ?R67 receiveBuffer sendBuffer)\<rbrace>
 5. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 6. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 7. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
xa <- lookupIPCBuffer False sender;
xb <- do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od;
tag' <- ?g75 x xa xb;
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. xb) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 8. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (7 subgoals):
 1. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?R67 receiveBuffer sendBuffer\<rbrace> do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od \<lbrace>\<lambda>x. (\<lambda>_. [] = []) and (\<lambda>_. True)\<rbrace>
 2. \<And>receiveBuffer sendBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P46 receiveBuffer sendBuffer\<rbrace> asUser sender (getRegister TCB_H.msgInfoRegister) \<lbrace>\<lambda>rv' _. rv' = msgInfo\<rbrace>
 3. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q20 receiveBuffer\<rbrace> lookupIPCBuffer False sender \<lbrace>\<lambda>sendBuffer. ?P46 receiveBuffer sendBuffer and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and ?R67 receiveBuffer sendBuffer)\<rbrace>
 4. \<And>receiveBuffer. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P20 receiveBuffer\<rbrace> threadGet tcbFault sender \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 5. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?P13\<rbrace> lookupIPCBuffer True rcvr \<lbrace>\<lambda>receiveBuffer. ?P20 receiveBuffer and ?Q20 receiveBuffer\<rbrace>
 6. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
x <- lookupIPCBuffer False sender;
x <- do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od;
tag' <- return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (messageInfoFromWord msgInfo)));
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. x) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 7. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> (?P13 and ?Q13) s proof (prove)
goal (2 subgoals):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
x <- lookupIPCBuffer False sender;
x <- do rv <- forM_x (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od);
return (msgLength (messageInfoFromWord msgInfo))
od;
tag' <- return (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (messageInfoFromWord msgInfo)));
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. x) tag');
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (2 subgoals):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True ?Q13 (do x <- lookupIPCBuffer True rcvr;
x <- lookupIPCBuffer False sender;
rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgLength_update (\<lambda>_. msgLength (messageInfoFromWord msgInfo)) (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (messageInfoFromWord msgInfo))));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od) (do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters);
y <- setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo));
asUser rcvr (setRegister Notification_H.badgeRegister badge)
od)
 2. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (3 subgoals):
 1. \<And>rv. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> monadic_rewrite True True (?Q107 rv) (setMessageInfo rcvr (msgLength_update (\<lambda>_. msgLength (messageInfoFromWord msgInfo)) (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (messageInfoFromWord msgInfo))))) (setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo)))
 2. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q13\<rbrace> mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) \<lbrace>?Q107\<rbrace>
 3. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (3 subgoals):
 1. \<And>rv x1 x2 x3 x4. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); messageInfoFromWord msgInfo = Types_H.message_info.MI x1 x2 x3 x4\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q107 rv) (setMessageInfo rcvr (msgLength_update (\<lambda>_. msgLength (messageInfoFromWord msgInfo)) (msgCapsUnwrapped_update (\<lambda>_. 0) (msgExtraCaps_update (\<lambda>_. 0) (messageInfoFromWord msgInfo))))) (setMessageInfo rcvr (msgCapsUnwrapped_update (\<lambda>_. 0) (messageInfoFromWord msgInfo)))
 2. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q13\<rbrace> mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) \<lbrace>?Q107\<rbrace>
 3. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (3 subgoals):
 1. \<And>x1 x3 x4. \<lbrakk>x1 \<le> word_of_nat (length TCB_H.msgRegisters); messageInfoFromWord msgInfo = Types_H.message_info.MI x1 0 x3 x4\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q107 ()) (setMessageInfo rcvr (Types_H.message_info.MI x1 0 0 x4)) (setMessageInfo rcvr (Types_H.message_info.MI x1 0 0 x4))
 2. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q13\<rbrace> mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) \<lbrace>?Q107\<rbrace>
 3. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (2 subgoals):
 1. msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> \<lbrace>?Q13\<rbrace> mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od) (take (unat (msgLength (messageInfoFromWord msgInfo))) TCB_H.msgRegisters) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and ?Q13) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>msgExtraCaps (messageInfoFromWord msgInfo) = 0 \<and> msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters); obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s\<rbrakk> \<Longrightarrow> ((\<lambda>s. tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) and (obj_at' (\<lambda>tcb. (atcbContextGet \<circ> tcbArch) tcb TCB_H.msgInfoRegister = msgInfo) sender and ((\<lambda>_. msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)) and (\<lambda>s. [] = [] \<and> True))) and (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_at' (\<lambda>tcb. tcbFault tcb = None \<and> atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s; msgExtraCaps (messageInfoFromWord msgInfo) = 0; msgLength (messageInfoFromWord msgInfo) \<le> word_of_nat (length TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> (tcb_at' sender s \<longrightarrow> obj_at' ((\<lambda>rv. rv = None) \<circ> tcbFault) sender s) \<and> obj_at' (\<lambda>tcb. atcbContextGet (tcbArch tcb) TCB_H.msgInfoRegister = msgInfo) sender s proof (prove)
goal:
No subgoals!