theory Ipc_C

lemma setMRs_to_setMR:
  "setMRs thread buffer xs
   = (do
    stateAssert (tcb_at' thread) [];
    ys \<leftarrow> zipWithM (setMR thread buffer) [0 ..< msgMaxLength] xs;
    return (of_nat (last (0 # ys)))
  od)" apply (simp add: setMRs_to_setMR' zipWithM_mapM split_def mapM_discarded
              del: last.simps) apply (subst mapM_last_Cons) prefer 3 apply simp apply (simp add: msgMaxLength_unfold) apply (simp add: fst_last_zip_upt) apply (subgoal_tac "msgMaxLength - Suc 0 \<ge> length msgRegisters
                           \<and> of_nat (length xs - Suc 0) = of_nat (length xs) - (1 :: word32)
                           \<and> unat ((1 :: word32) + of_nat (length msgRegisters)) = Suc (length msgRegisters)") apply (simp add: setMR_def split: option.split) apply (intro impI conjI allI) apply clarsimp apply clarsimp apply (clarsimp simp add: msgRegisters_unfold) apply (clarsimp simp: linorder_not_less linorder_not_le) apply (clarsimp simp: msgRegisters_unfold msgMaxLength_def
                          msgLengthBits_def shiftL_nat) apply (clarsimp simp: msgRegisters_unfold msgMaxLength_def
                         msgLengthBits_def shiftL_nat) apply (simp add: msgRegisters_unfold msgMaxLength_unfold) apply (case_tac xs, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setMRs thread buffer xs = do stateAssert (tcb_at' thread) [];
ys <- zipWithM (setMR thread buffer) [0..<msgMaxLength] xs;
return (word_of_nat (last (0 # ys)))
od proof (prove)
goal (1 subgoal):
 1. do y <- stateAssert (tcb_at' thread) [];
_ <- mapM_x (\<lambda>p. setMR thread buffer (fst p) (snd p)) (zip [0..<msgMaxLength] xs);
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od = do y <- stateAssert (tcb_at' thread) [];
ys <- mapM (\<lambda>p. setMR thread buffer (fst p) (snd p)) (zip [0..<msgMaxLength] xs);
return (word_of_nat (last (0 # ys)))
od proof (prove)
goal (3 subgoals):
 1. \<And>y. zip [0..<msgMaxLength] xs = [] \<Longrightarrow> word_of_nat 0 = ?y
 2. \<And>y. zip [0..<msgMaxLength] xs \<noteq> [] \<Longrightarrow> do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return ?y
od
 3. do y <- stateAssert (tcb_at' thread) [];
_ <- mapM_x (\<lambda>p. setMR thread buffer (fst p) (snd p)) (zip [0..<msgMaxLength] xs);
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od = do y <- stateAssert (tcb_at' thread) [];
mapM_x (\<lambda>a. setMR thread buffer (fst a) (snd a)) (zip [0..<msgMaxLength] xs);
return ?y
od proof (prove)
goal (3 subgoals):
 1. do y <- stateAssert (tcb_at' thread) [];
_ <- mapM_x (\<lambda>p. setMR thread buffer (fst p) (snd p)) (zip [0..<msgMaxLength] xs);
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od = do y <- stateAssert (tcb_at' thread) [];
mapM_x (\<lambda>a. setMR thread buffer (fst a) (snd a)) (zip [0..<msgMaxLength] xs);
return ?y
od
 2. \<And>y. zip [0..<msgMaxLength] xs = [] \<Longrightarrow> word_of_nat 0 = ?y
 3. \<And>y. zip [0..<msgMaxLength] xs \<noteq> [] \<Longrightarrow> do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return ?y
od proof (prove)
goal (2 subgoals):
 1. \<And>y. zip [0..<msgMaxLength] xs = [] \<Longrightarrow> word_of_nat 0 = word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters)))))
 2. \<And>y. zip [0..<msgMaxLength] xs \<noteq> [] \<Longrightarrow> do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od proof (prove)
goal (1 subgoal):
 1. \<And>y. zip [0..<msgMaxLength] xs \<noteq> [] \<Longrightarrow> do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (fst (last (zip [0..<msgMaxLength] xs))) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od proof (prove)
goal (1 subgoal):
 1. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> (length xs < msgMaxLength \<longrightarrow> do x <- setMR thread buffer (length xs - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (length xs - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od) \<and> (\<not> length xs < msgMaxLength \<longrightarrow> do x <- setMR thread buffer (msgMaxLength - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (msgMaxLength - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> (length xs < msgMaxLength \<longrightarrow> do x <- setMR thread buffer (length xs - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (length xs - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od) \<and> (\<not> length xs < msgMaxLength \<longrightarrow> do x <- setMR thread buffer (msgMaxLength - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat x)
od = do x <- setMR thread buffer (msgMaxLength - Suc 0) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (case buffer of None \<Rightarrow> 0 | Some a \<Rightarrow> Suc (unat msgMaxLength) - unat (1 + word_of_nat (length TCB_H.msgRegisters))))))
od)
 2. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters)\<rbrakk> \<Longrightarrow> (buffer = None \<longrightarrow> length xs - Suc 0 < length TCB_H.msgRegisters \<longrightarrow> \<not> length xs < msgMaxLength \<longrightarrow> return (word_of_nat (length TCB_H.msgRegisters)) = return (word_of_nat (length xs))) \<and> (\<forall>x2. buffer = Some x2 \<longrightarrow> (length xs - Suc 0 < length TCB_H.msgRegisters \<longrightarrow> \<not> length xs < msgMaxLength \<longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od) \<and> (\<not> length xs - Suc 0 < length TCB_H.msgRegisters \<longrightarrow> (length xs < msgMaxLength \<longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od) \<and> (\<not> length xs < msgMaxLength \<longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od)))
 2. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = None; length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> return (word_of_nat (length TCB_H.msgRegisters)) = return (word_of_nat (length xs))
 2. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od
 3. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 4. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 5. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od
 2. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 3. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 4. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 2. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 3. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xs \<noteq> []; Suc (Suc (Suc (Suc 0))) \<le> msgMaxLength - Suc 0; buffer = Some x2; \<not> length xs - Suc 0 < Suc (Suc (Suc (Suc 0))); length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (Suc (Suc (Suc (Suc (unat msgMaxLength - Suc (Suc (Suc (Suc 0))))))))))
od
 2. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 3. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrakk>xs \<noteq> []; Suc (Suc (Suc (Suc 0))) \<le> msgMaxLength - Suc 0; buffer = Some x2; Suc (Suc (Suc (Suc 0))) \<le> length xs - Suc 0; length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (length xs))
od = do y <- storeWordUser (x2 + word_of_nat (length xs) * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (Suc (Suc (Suc (Suc (unat msgMaxLength - Suc (Suc (Suc (Suc 0))))))))))
od
 2. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 3. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (2 subgoals):
 1. \<And>x2. \<lbrakk>0 < msgMaxLength \<and> xs \<noteq> []; length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters); buffer = Some x2; \<not> length xs - Suc 0 < length TCB_H.msgRegisters; \<not> length xs < msgMaxLength\<rbrakk> \<Longrightarrow> do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat msgMaxLength)
od = do y <- storeWordUser (x2 + word_of_nat msgMaxLength * word_size) (snd (last (zip [0..<msgMaxLength] xs)));
return (word_of_nat (min (length xs) (length TCB_H.msgRegisters + (unat msgMaxLength - length TCB_H.msgRegisters))))
od
 2. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (1 subgoal):
 1. 0 < msgMaxLength \<and> xs \<noteq> [] \<Longrightarrow> length TCB_H.msgRegisters \<le> msgMaxLength - Suc 0 \<and> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 \<and> unat (1 + word_of_nat (length TCB_H.msgRegisters)) = Suc (length TCB_H.msgRegisters) proof (prove)
goal (1 subgoal):
 1. xs \<noteq> [] \<Longrightarrow> word_of_nat (length xs - Suc 0) = word_of_nat (length xs) - 1 proof (prove)
goal:
No subgoals!