theory ArchArch_IF

lemma set_mrs_globals_equiv:
  "\<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)\<rbrace>
      set_mrs thread buf msgs
    \<lbrace>\<lambda>_. globals_equiv s\<rbrace>" unfolding set_mrs_def apply (wp | wpc)+ apply (simp add: zipWithM_x_mapM_x) apply (rule conjI) apply (rule impI) apply (rule_tac Q="\<lambda>_. globals_equiv s"
          in hoare_strengthen_post) apply (wp mapM_x_wp') apply (simp add: split_def) apply (wp store_word_offs_globals_equiv) apply (simp) apply (clarsimp) apply (insert length_msg_lt_msg_max) apply (simp) apply (wp set_object_globals_equiv hoare_weak_lift_imp) apply (wp hoare_vcg_all_lift set_object_globals_equiv hoare_weak_lift_imp)+ apply (clarsimp simp:arm_global_pd_not_tcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)\<rbrace> do tcb <- gets_the $ get_tcb thread;
context <- return (arch_tcb_get_registers (tcb_arch tcb));
new_regs <- return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg);
set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>));
remaining_msgs <- return (drop (length msg_registers) msgs);
case buf of None \<Rightarrow> return $ nat_to_len (min (length msg_registers) (length msgs)) | Some pptr \<Rightarrow> do zipWithM_x (store_word_offs pptr) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs;
return $ nat_to_len $ min (length msgs) msg_max_length
od
od \<lbrace>\<lambda>_. globals_equiv s\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>tcb context new_regs x remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<lbrace>?R16 tcb context new_regs x remaining_msgs x2\<rbrace> zipWithM_x (store_word_offs x2) [length msg_registers + 1..<Suc msg_max_length] remaining_msgs \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa sa)\<rbrace>
 3. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 4. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 7. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (7 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> (Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs) \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>) \<and> (\<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>)
 2. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa sa)\<rbrace>
 3. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 4. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 7. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (8 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs) \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 3. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa sa)\<rbrace>
 4. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 5. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 6. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 8. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (8 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length\<rbrakk> \<Longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs) \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 3. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa sa)\<rbrace>
 4. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 5. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 6. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 8. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (9 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length\<rbrakk> \<Longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs remaining_msgs x2 rv sa. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 3. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>?R16 tcb context new_regs () remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 4. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa sa)\<rbrace>
 5. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 6. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 7. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 9. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (9 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2 x. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; x \<in> set (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs)\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> case x of (a, b) \<Rightarrow> store_word_offs x2 a b \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs remaining_msgs x2 rv sa. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 3. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 4. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 5. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 6. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 7. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 9. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 x. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; x \<in> set (zip ([Suc (length msg_registers)..<msg_max_length] @ [msg_max_length]) remaining_msgs)\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> store_word_offs x2 (fst x) (snd x) \<lbrace>\<lambda>_. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs remaining_msgs x2 rv sa. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 3. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 4. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 5. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 6. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 7. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 9. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (8 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2 rv sa. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; globals_equiv s sa\<rbrakk> \<Longrightarrow> globals_equiv s sa
 2. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 3. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 4. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 5. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 6. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 8. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (7 subgoals):
 1. \<And>tcb context new_regs remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<not> Suc (length msg_registers) \<le> msg_max_length \<longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 3. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 4. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 7. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (7 subgoals):
 1. \<And>x2. \<lbrakk>buf = Some x2; \<not> Suc (length msg_registers) \<le> msg_max_length\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 3. \<And>tcb context new_regs. \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 4. \<And>tcb context. \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 5. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 7. \<And>sa. (globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa \<Longrightarrow> ?Q sa proof (prove)
goal (7 subgoals):
 1. \<And>x2. \<lbrakk>buf = Some x2; \<not> Suc (length msg_registers) \<le> msg_max_length; length msg_registers < msg_max_length\<rbrakk> \<Longrightarrow> \<lbrace>globals_equiv s\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) [] \<lbrace>\<lambda>xa. globals_equiv s\<rbrace>
 2. \<And>tcb context new_regs x. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 3. \<And>tcb context new_regs. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 4. \<And>tcb context. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 5. \<And>tcb. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 6. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 7. \<And>sa. \<lbrakk>(globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa; length msg_registers < msg_max_length\<rbrakk> \<Longrightarrow> ?Q sa proof (prove)
goal (6 subgoals):
 1. \<And>tcb context new_regs x. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 2. \<And>tcb context new_regs. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>?B4 tcb context new_regs\<rbrace>
 3. \<And>tcb context. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 4. \<And>tcb. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 5. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 6. \<And>sa. \<lbrakk>(globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa; length msg_registers < msg_max_length\<rbrakk> \<Longrightarrow> ?Q sa proof (prove)
goal (5 subgoals):
 1. \<And>tcb context new_regs. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B3 tcb context new_regs\<rbrace> set_object thread (TCB (tcb\<lparr>tcb_arch := arch_tcb_set_registers new_regs (tcb_arch tcb)\<rparr>)) \<lbrace>\<lambda>x sa. (buf = None \<longrightarrow> globals_equiv s sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> globals_equiv s sa)\<rbrace>
 2. \<And>tcb context. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B2 tcb context\<rbrace> return (\<lambda>reg. if reg \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers reg else context reg) \<lbrace>?B3 tcb context\<rbrace>
 3. \<And>tcb. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 4. length msg_registers < msg_max_length \<Longrightarrow> \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 5. \<And>sa. \<lbrakk>(globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa; length msg_registers < msg_max_length\<rbrakk> \<Longrightarrow> ?Q sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>(globals_equiv s and valid_arch_state and (\<lambda>sa. thread \<noteq> idle_thread sa)) sa; length msg_registers < msg_max_length\<rbrakk> \<Longrightarrow> (buf = None \<longrightarrow> get_tcb thread sa \<noteq> None \<longrightarrow> (globals_equiv s and (\<lambda>s. thread \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. thread = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. TCB (the (get_tcb thread sa)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>a. if a \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers a else arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa))) a) (tcb_arch (the (get_tcb thread sa)))\<rparr>) = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. TCB (the (get_tcb thread sa)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>a. if a \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers a else arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa))) a) (tcb_arch (the (get_tcb thread sa)))\<rparr>) = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))) sa) \<and> (\<forall>x. buf = Some x \<longrightarrow> get_tcb thread sa \<noteq> None \<longrightarrow> (globals_equiv s and (\<lambda>s. thread \<noteq> arm_global_pd (arch_state s)) and (\<lambda>t. thread = idle_thread t \<longrightarrow> (\<forall>tcb. kheap t (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<exists>tcb'. TCB (the (get_tcb thread sa)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>a. if a \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers a else arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa))) a) (tcb_arch (the (get_tcb thread sa)))\<rparr>) = TCB tcb' \<and> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<forall>tcb'. TCB (the (get_tcb thread sa)\<lparr>tcb_arch := arch_tcb_set_registers (\<lambda>a. if a \<in> set (take (length msgs) msg_registers) then msgs ! the_index msg_registers a else arch_tcb_get_registers (tcb_arch (the (get_tcb thread sa))) a) (tcb_arch (the (get_tcb thread sa)))\<rparr>) = TCB tcb' \<longrightarrow> tcb_at (idle_thread t) t))) sa) proof (prove)
goal:
No subgoals!