theory IsolatedThreadAction

lemma copyMRs_simple:
  "msglen \<le> of_nat (length msgRegisters) \<longrightarrow>
    copyMRs sender sbuf receiver rbuf msglen
        = forM_x (take (unat msglen) msgRegisters)
             (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
                    asUser receiver (setRegister r v) od)
           >>= (\<lambda>rv. return msglen)" apply (clarsimp simp: copyMRs_def mapM_discarded) apply (rule bind_cong[OF refl]) apply (simp add: min_def word_le_nat_alt length_msgRegisters
                   upto_enum_red fromEnum_def enum_register
            split: option.split) apply (simp add: upto_enum_def mapM_Nil) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msglen \<le> word_of_nat (length TCB_H.msgRegisters) \<longrightarrow> copyMRs sender sbuf receiver rbuf msglen = do rv <- forM_x (take (unat msglen) TCB_H.msgRegisters) (\<lambda>r. do v <- asUser sender (getRegister r);
asUser receiver (setRegister r v)
od);
return msglen
od proof (prove)
goal (1 subgoal):
 1. msglen \<le> word_of_nat (length TCB_H.msgRegisters) \<Longrightarrow> do _ <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser receiver (setRegister r v)
od) (take (unat msglen) TCB_H.msgRegisters);
bufferMRs <- case sbuf of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rbuf 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. msglen];
return (min msglen (word_of_nat (min (length TCB_H.msgRegisters) (unat msglen)) + word_of_nat (length bufferMRs)))
od = do rv <- mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser receiver (setRegister r v)
od) (take (unat msglen) TCB_H.msgRegisters);
return msglen
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. \<lbrakk>msglen \<le> word_of_nat (length TCB_H.msgRegisters); (v, s') \<in> fst (mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser receiver (setRegister r v)
od) (take (unat msglen) TCB_H.msgRegisters) s)\<rbrakk> \<Longrightarrow> (do bufferMRs <- case sbuf of None \<Rightarrow> return [] | Some sbPtr \<Rightarrow> case rbuf 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. msglen];
return (min msglen (word_of_nat (min (length TCB_H.msgRegisters) (unat msglen)) + word_of_nat (length bufferMRs)))
od) s' = return msglen s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>unat msglen \<le> 4; ((), s') \<in> fst (mapM_x (\<lambda>r. do v <- asUser sender (getRegister r);
asUser receiver (setRegister r v)
od) (take (unat msglen) TCB_H.msgRegisters) s)\<rbrakk> \<Longrightarrow> \<forall>x2 x2a. rbuf = Some x2a \<longrightarrow> sbuf = Some x2 \<longrightarrow> (do bufferMRs <- mapM (\<lambda>x. loadWordUser (x2 + x * word_of_nat wordSize) >>= storeWordUser (x2a + x * word_of_nat wordSize)) [];
return (if unat msglen \<le> unat (msglen + word_of_nat (length bufferMRs)) then msglen else msglen + word_of_nat (length bufferMRs))
od) s' = return msglen s' proof (prove)
goal:
No subgoals!