theory ArchIpc_IF

lemma set_mrs_equiv_but_for_labels[Ipc_IF_assms]:
  "\<lbrace>equiv_but_for_labels (aag :: 'a subject_label PAS) L st and
    K (pasObjectAbs aag thread \<in> L \<and>
       (case buf of (Some buf') \<Rightarrow> is_aligned buf' msg_align_bits \<and>
                                   (\<forall>x \<in> ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)
                            | _ \<Rightarrow> True))\<rbrace>
   set_mrs thread buf msgs
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding set_mrs_def apply (wp | wpc)+ apply (subst zipWithM_x_mapM_x) apply (rule_tac Q="\<lambda>_. equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L  \<and>
                               (case buf of (Some buf') \<Rightarrow> is_aligned buf' msg_align_bits \<and>
                                                           (\<forall>x \<in> ptr_range buf' msg_align_bits.
                                                              pasObjectAbs aag x \<in> L)
                                                    | _ \<Rightarrow> True))" in hoare_strengthen_post) apply (wp mapM_x_wp' store_word_offs_equiv_but_for_labels | simp add: split_def)+ apply (case_tac xa, clarsimp split: if_split_asm elim!: in_set_zipE) apply (clarsimp simp: for_each_byte_of_word_def) apply (erule bspec) apply (clarsimp simp: ptr_range_def) apply (rule conjI) apply (erule order_trans[rotated]) apply (erule is_aligned_no_wrap') apply (rule mul_word_size_lt_msg_align_bits_ofnat) apply (fastforce simp: msg_max_length_def msg_align_bits') apply (erule order_trans) apply (subst p_assoc_help) apply (simp add: add.assoc) apply (rule word_plus_mono_right) apply (rule word_less_sub_1) apply (rule_tac y="of_nat msg_max_length * of_nat word_size + (word_size - 1)"
                       in le_less_trans) apply (rule word_plus_mono_left) apply (rule word_mult_le_mono1) apply (erule disjE) apply (rule word_of_nat_le) apply (simp add: msg_max_length_def) apply clarsimp apply (rule word_of_nat_le) apply (simp add: msg_max_length_def) apply (simp add: word_size_def) apply (simp add: msg_max_length_def word_size_def) apply (simp add: msg_max_length_def word_size_def) apply (rule mul_add_word_size_lt_msg_align_bits_ofnat) apply (simp add: msg_max_length_def msg_align_bits') apply (simp add: word_size_def) apply (erule is_aligned_no_overflow') apply simp apply (wp set_object_equiv_but_for_labels hoare_vcg_all_lift hoare_weak_lift_imp | simp)+ apply (fastforce dest: get_tcb_not_asid_pool_at)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))\<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>_. equiv_but_for_labels aag L st\<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. equiv_but_for_labels aag L st\<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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R16 tcb context new_regs x remaining_msgs xa s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>tcb context new_regs x remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<lbrace>?R29 tcb context new_regs x remaining_msgs x2 (?tcb29 tcb context new_regs x remaining_msgs x2) (?context29 tcb context new_regs x remaining_msgs x2) (?new_regs29 tcb context new_regs x remaining_msgs x2) (?x29 tcb context new_regs x remaining_msgs x2) remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip [length msg_registers + 1..<Suc msg_max_length] remaining_msgs) \<lbrace>\<lambda>xa. equiv_but_for_labels aag L st\<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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R29 tcb context new_regs x remaining_msgs xa (?tcb29 tcb context new_regs x remaining_msgs xa) (?context29 tcb context new_regs x remaining_msgs xa) (?new_regs29 tcb context new_regs x remaining_msgs xa) (?x29 tcb context new_regs x remaining_msgs xa) remaining_msgs xa s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>tcb context new_regs x remaining_msgs x2. buf = Some x2 \<Longrightarrow> \<lbrace>?R29 tcb context new_regs x remaining_msgs x2 (?tcb29 tcb context new_regs x remaining_msgs x2) (?context29 tcb context new_regs x remaining_msgs x2) (?new_regs29 tcb context new_regs x remaining_msgs x2) (?x29 tcb context new_regs x remaining_msgs x2) remaining_msgs x2\<rbrace> mapM_x (\<lambda>(x, y). store_word_offs x2 x y) (zip [length msg_registers + 1..<Suc msg_max_length] remaining_msgs) \<lbrace>\<lambda>_. equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))\<rbrace>
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>xa. buf = Some xa \<longrightarrow> ?R29 tcb context new_regs x remaining_msgs xa (?tcb29 tcb context new_regs x remaining_msgs xa) (?context29 tcb context new_regs x remaining_msgs xa) (?new_regs29 tcb context new_regs x remaining_msgs xa) (?x29 tcb context new_regs x remaining_msgs xa) remaining_msgs xa s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 xa s. \<lbrakk>buf = Some x2; xa \<in> set (zip (if Suc (length msg_registers) \<le> msg_max_length then [Suc (length msg_registers)..<msg_max_length] @ [msg_max_length] else []) remaining_msgs); equiv_but_for_labels aag L st s \<and> pasObjectAbs aag thread \<in> L \<and> is_aligned x2 msg_align_bits \<and> (\<forall>x\<in>ptr_range x2 msg_align_bits. pasObjectAbs aag x \<in> L)\<rbrakk> \<Longrightarrow> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (x2 + word_of_nat (fst xa) * word_of_nat word_size)
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; \<forall>x\<in>ptr_range x2 msg_align_bits. pasObjectAbs aag x \<in> L; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs\<rbrakk> \<Longrightarrow> for_each_byte_of_word (\<lambda>x. pasObjectAbs aag x \<in> L) (x2 + word_of_nat aa * word_of_nat word_size)
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; \<forall>x\<in>ptr_range x2 msg_align_bits. pasObjectAbs aag x \<in> L; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> pasObjectAbs aag y \<in> L
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<in> ptr_range x2 msg_align_bits
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> x2 \<le> y \<and> y \<le> x2 + 2 ^ msg_align_bits - 1
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> x2 \<le> y
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<le> x2 + 2 ^ msg_align_bits - 1
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> x2 \<le> x2 + word_of_nat aa * word_of_nat word_size
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<le> x2 + 2 ^ msg_align_bits - 1
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> word_of_nat aa * word_of_nat word_size < 2 ^ msg_align_bits
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<le> x2 + 2 ^ msg_align_bits - 1
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> aa < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<le> x2 + 2 ^ msg_align_bits - 1
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; y \<le> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1)\<rbrakk> \<Longrightarrow> y \<le> x2 + 2 ^ msg_align_bits - 1
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1) \<le> x2 + 2 ^ msg_align_bits - 1
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 + word_of_nat aa * word_of_nat word_size + (word_size - 1) \<le> x2 + (2 ^ msg_align_bits - 1)
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 + (word_of_nat aa * word_of_nat word_size + (word_size - 1)) \<le> x2 + (2 ^ msg_align_bits - 1)
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat aa * word_of_nat word_size + (word_size - 1) \<le> 2 ^ msg_align_bits - 1
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat aa * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat aa * word_of_nat word_size + (word_size - 1) \<le> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 4. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 5. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 6. \<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>
 7. \<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>
 8. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 10. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (11 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat aa * word_of_nat word_size \<le> word_of_nat msg_max_length * word_of_nat word_size
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 5. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 6. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 7. \<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>
 8. \<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>
 9. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 10. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 7. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 8. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 9. \<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>
 10. \<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>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; aa = msg_max_length\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 7. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 8. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 9. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 10. \<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>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; aa = msg_max_length\<rbrakk> \<Longrightarrow> aa \<le> unat (word_of_nat msg_max_length)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 7. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 8. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 9. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 10. \<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>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 7. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 8. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 9. \<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>
 10. \<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>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; Suc (length msg_registers) \<le> aa; aa < msg_max_length\<rbrakk> \<Longrightarrow> word_of_nat aa \<le> word_of_nat msg_max_length
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 7. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 8. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 9. \<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>
 10. \<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>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y; Suc (length msg_registers) \<le> aa; aa < msg_max_length\<rbrakk> \<Longrightarrow> aa \<le> unat (word_of_nat msg_max_length)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 6. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 7. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 8. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 9. \<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>
 10. \<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>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> 0 < word_of_nat word_size
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 5. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 6. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 7. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 8. \<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>
 9. \<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>
 10. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> unat (word_of_nat msg_max_length) * unat (word_of_nat word_size) < 2 ^ LENGTH(32)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 4. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 5. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 6. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 7. \<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>
 8. \<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>
 9. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 10. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 \<le> word_size - 1 + word_of_nat msg_max_length * word_of_nat word_size
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 4. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 5. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 6. \<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>
 7. \<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>
 8. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 10. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_of_nat msg_max_length * word_of_nat word_size + (word_size - 1) < 2 ^ msg_align_bits
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> msg_max_length < 2 ^ (msg_align_bits - word_size_bits)
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 < word_size
 3. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 4. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 5. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 6. \<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>
 7. \<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>
 8. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 9. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 10. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> word_size - 1 < word_size
 2. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 3. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>remaining_msgs x2 s aa ba y. \<lbrakk>buf = Some x2; Suc (length msg_registers) \<le> msg_max_length; equiv_but_for_labels aag L st s; pasObjectAbs aag thread \<in> L; is_aligned x2 msg_align_bits; aa = msg_max_length \<or> Suc (length msg_registers) \<le> aa \<and> aa < msg_max_length; ba \<in> set remaining_msgs; x2 + word_of_nat aa * word_of_nat word_size \<le> y\<rbrakk> \<Longrightarrow> x2 \<le> x2 + (2 ^ msg_align_bits - 1)
 2. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>tcb context new_regs x remaining_msgs x2 rv s. \<lbrakk>buf = Some x2; (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s\<rbrakk> \<Longrightarrow> equiv_but_for_labels aag L st s
 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 s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<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>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>tcb context new_regs x. \<lbrace>?B4 tcb context new_regs x\<rbrace> return (drop (length msg_registers) msgs) \<lbrace>\<lambda>remaining_msgs s. (buf = None \<longrightarrow> equiv_but_for_labels aag L st s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s)\<rbrace>
 2. \<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>
 3. \<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>
 4. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> return (arch_tcb_get_registers (tcb_arch tcb)) \<lbrace>?B2 tcb\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets_the $ get_tcb thread \<lbrace>?B1\<rbrace>
 6. \<And>s. (equiv_but_for_labels aag L st and K (pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. equiv_but_for_labels aag L st s \<and> pasObjectAbs aag thread \<in> L \<and> (case buf of None \<Rightarrow> True | Some buf' \<Rightarrow> is_aligned buf' msg_align_bits \<and> (\<forall>x\<in>ptr_range buf' msg_align_bits. pasObjectAbs aag x \<in> L)) \<Longrightarrow> (buf = None \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> \<not> typ_at (AArch AASIDPool) thread s) \<and> (\<forall>x. buf = Some x \<longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> \<not> typ_at (AArch AASIDPool) thread s \<and> is_aligned x msg_align_bits \<and> (\<forall>x\<in>ptr_range x msg_align_bits. pasObjectAbs aag x \<in> L)) proof (prove)
goal:
No subgoals!