theory Ipc_R

lemma copy_mrs_invs'[wp]:
  "\<lbrace> invs' and tcb_at' s and tcb_at' r \<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. invs' \<rbrace>" including no_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord|
         simp add: split_def) apply (case_tac sb, simp_all)[1] apply wp+ apply (case_tac rb, simp_all)[1] apply (wp mapM_wp dmo_invs' no_irq_mapM no_irq_storeWord no_irq_loadWord) apply blast apply (rule hoare_strengthen_post) apply (rule mapM_wp) apply (wp | simp | blast)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> copyMRs s sb r rb n \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> do y <- mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters);
bufferMRs <- case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * word_of_nat wordSize) >>= storeWordUser (rbPtr + x * word_of_nat wordSize)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n];
return (min n (word_of_nat (min (length TCB_H.msgRegisters) (unat n)) + word_of_nat (length bufferMRs)))
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?B6 x\<rbrace> case sb of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (sbPtr + x * word_of_nat wordSize) >>= storeWordUser (rbPtr + x * word_of_nat wordSize)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n] \<lbrace>\<lambda>bufferMRs. invs'\<rbrace>
 2. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>?B6\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. sb = None \<Longrightarrow> \<lbrace>?B6 x\<rbrace> return [] \<lbrace>\<lambda>bufferMRs. invs'\<rbrace>
 2. \<And>x a. sb = Some a \<Longrightarrow> \<lbrace>?B6 x\<rbrace> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (a + x * word_of_nat wordSize) >>= storeWordUser (rbPtr + x * word_of_nat wordSize)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n] \<lbrace>\<lambda>bufferMRs. invs'\<rbrace>
 3. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>?B6\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x a. sb = Some a \<Longrightarrow> \<lbrace>invs'\<rbrace> case rb of None \<Rightarrow> return [] | Some rbPtr \<Rightarrow> mapM (\<lambda>x. loadWordUser (a + x * word_of_nat wordSize) >>= storeWordUser (rbPtr + x * word_of_nat wordSize)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n] \<lbrace>\<lambda>bufferMRs. invs'\<rbrace>
 2. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> \<lbrace>invs'\<rbrace> mapM (\<lambda>x. loadWordUser (a + x * word_of_nat wordSize) >>= storeWordUser (aa + x * word_of_nat wordSize)) [1 + word_of_nat (length TCB_H.msgRegisters) .e. n] \<lbrace>\<lambda>bufferMRs. invs'\<rbrace>
 2. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a aa. \<lbrakk>sb = Some a; rb = Some aa\<rbrakk> \<Longrightarrow> set [1 + word_of_nat (length TCB_H.msgRegisters) .e. n] \<subseteq> ?S19 a aa
 2. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>\<lambda>x. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> mapM (\<lambda>ra. do v <- asUser s (getRegister ra);
asUser r (setRegister ra v)
od) (take (unat n) TCB_H.msgRegisters) \<lbrace>?Q27\<rbrace>
 2. \<And>rv s. ?Q27 rv s \<Longrightarrow> invs' s proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> ?S30 \<Longrightarrow> \<lbrace>invs' and tcb_at' s and tcb_at' r\<rbrace> do v <- asUser s (getRegister x);
asUser r (setRegister x v)
od \<lbrace>\<lambda>rv. invs' and tcb_at' s and tcb_at' r\<rbrace>
 2. set (take (unat n) TCB_H.msgRegisters) \<subseteq> ?S30
 3. \<And>rv sa. (invs' and tcb_at' s and tcb_at' r) sa \<Longrightarrow> invs' sa proof (prove)
goal:
No subgoals!