theory Ipc_DR

lemma dcorres_lookup_extra_caps:
  "\<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t;
    valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s;
    not_idle_thread thread s\<rbrakk>
    \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>extra extra'. extra = transform_cap_list extra'))
     \<top> ((=) s)
     (Endpoint_D.lookup_extra_caps thread
                                   (cdl_intent_extras (transform_full_intent (machine_state s) thread t)))
     (Ipc_A.lookup_extra_caps thread buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))" apply (clarsimp simp:lookup_extra_caps_def liftE_bindE Endpoint_D.lookup_extra_caps_def) apply (rule corres_symb_exec_r) apply (rule_tac F = "evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv"
                     in corres_gen_asm2) apply (rule corres_mapME[where S = "{(x,y). x = of_bl y \<and> length y = word_bits}"]) prefer 3 apply simp apply (rule dcorres_lookup_cap_and_slot[simplified]) apply (clarsimp simp:transform_cap_list_def)+ apply wp apply simp apply (case_tac buffer) apply clarsimp apply (simp add:transform_full_intent_def Let_def) apply (rule get_ipc_buffer_words_empty) apply (simp add:obj_at_def) apply (erule get_tcb_SomeD) apply simp apply clarify apply (subst evalMonad_get_extra_cptrs) apply simp+ apply (case_tac buffer) apply clarsimp apply clarify apply (drule evalMonad_get_extra_cptrs) apply (simp del:get_extra_cptrs.simps add: zip_map_eqv[where g = "\<lambda>x. x",simplified])+ apply (simp add: word_bits_def del:get_extra_cptrs.simps) apply (wp evalMonad_wp) apply (case_tac buffer) apply (simp add:get_extra_cptrs_def empty_when_fail_simps)+ apply (simp add:liftM_def) apply (rule empty_when_fail_compose) apply (simp add:empty_when_fail_simps)+ apply (rule empty_when_fail_mapM) apply (simp add:weak_det_spec_load_word_offs empty_when_fail_load_word_offs) apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) apply (case_tac buffer) apply (simp add:get_extra_cptrs_def weak_det_spec_simps)+ apply (simp add:liftM_def) apply (rule weak_det_spec_compose) apply (simp add:weak_det_spec_simps) apply (rule weak_det_spec_mapM) apply (simp add:weak_det_spec_load_word_offs) apply (clarsimp simp:valid_state_def valid_pspace_def cur_tcb_def)+ apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>extra extra'. extra = transform_cap_list extra')) (\<lambda>_. True) ((=) s) (Endpoint_D.lookup_extra_caps thread (cdl_intent_extras (transform_full_intent (machine_state s) thread t))) (Ipc_A.lookup_extra_caps thread buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>extra extra'. extra = transform_cap_list extra')) (\<lambda>_. True) ((=) s) (mapME (CSpace_D.lookup_cap_and_slot thread) (cdl_intent_extras (transform_full_intent (machine_state s) thread t))) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) >>= mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (CSpace_A.lookup_cap_and_slot thread cptr))) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>extra extra'. extra = transform_cap_list extra')) (\<lambda>_. True) (?Q' rv) (mapME (CSpace_D.lookup_cap_and_slot thread) (cdl_intent_extras (transform_full_intent (machine_state s) thread t))) (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (CSpace_A.lookup_cap_and_slot thread cptr)) rv)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>?Q'\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>extra extra'. extra = transform_cap_list extra')) (\<lambda>_. True) (?P'5 rv) (mapME (CSpace_D.lookup_cap_and_slot thread) (cdl_intent_extras (transform_full_intent (machine_state s) thread t))) (mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (CSpace_A.lookup_cap_and_slot thread cptr)) rv)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. ?P'5 rv and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (10 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> [] = transform_cap_list []
 2. \<And>rv x xs y ys. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; xs = transform_cap_list ys; ?r'6 rv x y\<rbrakk> \<Longrightarrow> x # xs = transform_cap_list (y # ys)
 3. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'6 rv) (\<lambda>_. True) (?P'5 rv) (CSpace_D.lookup_cap_and_slot thread x) (cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y))
 4. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.lookup_cap_and_slot thread x \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>?P'5 rv\<rbrace> cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y) \<lbrace>\<lambda>rva. ?P'5 rv\<rbrace>
 6. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 7. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 8. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. ?P'5 rv and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 9. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (10 subgoals):
 1. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'6 rv) (\<lambda>_. True) (?P'5 rv) (CSpace_D.lookup_cap_and_slot thread x) (cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y))
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> [] = transform_cap_list []
 3. \<And>rv x xs y ys. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; xs = transform_cap_list ys; ?r'6 rv x y\<rbrakk> \<Longrightarrow> x # xs = transform_cap_list (y # ys)
 4. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.lookup_cap_and_slot thread x \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>?P'5 rv\<rbrace> cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y) \<lbrace>\<lambda>rva. ?P'5 rv\<rbrace>
 6. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 7. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 8. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. ?P'5 rv and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 9. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (10 subgoals):
 1. \<And>rv y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; length y = word_bits\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> ?r'6 rv) (\<lambda>_. True) (?P'5 rv) (CSpace_D.lookup_cap_and_slot thread (of_bl y)) (cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y))
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> [] = transform_cap_list []
 3. \<And>rv x xs y ys. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; xs = transform_cap_list ys; ?r'6 rv x y\<rbrakk> \<Longrightarrow> x # xs = transform_cap_list (y # ys)
 4. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.lookup_cap_and_slot thread x \<lbrace>\<lambda>rv _. True\<rbrace>
 5. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>?P'5 rv\<rbrace> cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y) \<lbrace>\<lambda>rva. ?P'5 rv\<rbrace>
 6. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 7. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 8. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. ?P'5 rv and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 9. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (11 subgoals):
 1. \<And>rv y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; length y = word_bits\<rbrakk> \<Longrightarrow> of_bl y = of_bl y
 2. \<And>rv y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; length y = word_bits\<rbrakk> \<Longrightarrow> length y = word_bits
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> [] = transform_cap_list []
 4. \<And>rv x xs y ys. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; xs = transform_cap_list ys; fst x = transform_cap (fst y) \<and> snd x = transform_cslot_ptr (snd y)\<rbrakk> \<Longrightarrow> x # xs = transform_cap_list (y # ys)
 5. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> CSpace_D.lookup_cap_and_slot thread x \<lbrace>\<lambda>rv _. True\<rbrace>
 6. \<And>rv x y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; (x, y) \<in> {(x, y). x = of_bl y \<and> length y = word_bits}\<rbrakk> \<Longrightarrow> \<lbrace>not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs\<rbrace> cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs\<rbrace>
 7. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 8. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 9. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 10. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>rv y. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; length y = word_bits\<rbrakk> \<Longrightarrow> \<lbrace>not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs\<rbrace> cap_fault_on_failure (of_bl y) False (CSpace_A.lookup_cap_and_slot thread y) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs\<rbrace>
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>rv y sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; length y = word_bits; (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa\<rbrakk> \<Longrightarrow> not_idle_thread thread sa \<and> valid_global_refs sa \<and> valid_objs sa \<and> valid_irq_node sa \<and> valid_idle sa \<and> valid_etcbs sa \<and> not_idle_thread thread sa \<and> valid_global_refs sa \<and> valid_objs sa \<and> valid_irq_node sa \<and> valid_idle sa \<and> valid_etcbs sa
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = None\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> cdl_intent_extras (transform_full_intent (machine_state s) thread t) = []
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state s) t [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (get_tcb_message_info t))] = []
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> ko_at (TCB t) ?thread64 s
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> evalMonad (lookup_ipc_buffer False ?thread64) s = Some None
 3. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 4. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 6. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> kheap s ?thread64 = Some (TCB t)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> evalMonad (lookup_ipc_buffer False ?thread64) s = Some None
 3. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 4. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 6. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some None; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> evalMonad (lookup_ipc_buffer False thread) s = Some None
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 3. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length rv
 2. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (8 subgoals):
 1. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> evalMonad (lookup_ipc_buffer False (?thread73 rv a)) (?s73 rv a) = Some (Some (?buf73 rv a))
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> get_tcb (?thread73 rv a) (?s73 rv a) = Some (?tcb73 rv a)
 3. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> evalMonad (get_extra_cptrs (Some (?buf73 rv a)) (data_to_message_info (arch_tcb_context_get (tcb_arch (?tcb73 rv a)) msg_info_register))) (?s73 rv a) = Some rv
 4. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> length (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) = length (map to_bl (cdl_intent_extras $ transform_full_intent (machine_state (?s73 rv a)) (?thread73 rv a) (?tcb73 rv a)))
 5. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 7. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>rv. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = None\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 2. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>rv a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a\<rbrakk> \<Longrightarrow> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv) \<subseteq> {(x, y). x = of_bl y \<and> length y = word_bits}
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>rv a aa b. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a; (aa, b) \<in> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv)\<rbrakk> \<Longrightarrow> aa = of_bl b \<and> length b = word_bits
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>rv a aa b. \<lbrakk>get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a; (aa, b) \<in> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv)\<rbrakk> \<Longrightarrow> get_tcb thread s = Some (?tcb83 rv a aa b)
 2. \<And>rv a aa b. \<lbrakk>get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a; (aa, b) \<in> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv)\<rbrakk> \<Longrightarrow> evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch (?tcb83 rv a aa b)) msg_info_register))) s = Some (?a83 rv a aa b)
 3. \<And>rv a aa b. \<lbrakk>get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv; buffer = Some a; (aa, b) \<in> set (zip (cdl_intent_extras (transform_full_intent (machine_state s) thread t)) rv); ?a83 rv a aa b = map to_bl (cdl_intent_extras $ transform_full_intent (machine_state s) thread (?tcb83 rv a aa b))\<rbrakk> \<Longrightarrow> aa = of_bl b \<and> length b = word_bits
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>rv a aa. \<lbrakk>get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; evalMonad (get_extra_cptrs (Some a) (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some (map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread t))); buffer = Some a; aa \<in> set (cdl_intent_extras (transform_full_intent (machine_state s) thread t)); rv = map to_bl (cdl_intent_extras (transform_full_intent (machine_state s) thread t))\<rbrakk> \<Longrightarrow> word_bits = 32
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>rv. not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs and (\<lambda>sa. evalMonad (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) s = Some rv)\<rbrace>
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> empty_when_fail (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> empty_when_fail (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 2. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (liftM (map to_bl) (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))]))
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (do x <- mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))];
return (map to_bl x)
od)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (7 subgoals):
 1. \<And>a r. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (return (map to_bl r))
 2. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 3. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 6. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> empty_when_fail (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 2. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (6 subgoals):
 1. \<And>a P l. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (load_word_offs a l) \<and> empty_when_fail (load_word_offs a l)
 2. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 5. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a P r Pa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec Pa (load_word_offs a r)
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = None\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 2. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (liftM (map to_bl) (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))]))
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (do x <- mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))];
return (map to_bl x)
od)
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (5 subgoals):
 1. \<And>a Q r. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec (Q r) (return (map to_bl r))
 2. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 4. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>a P. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec P (mapM (load_word_offs a) [buffer_cptr_index..<buffer_cptr_index + unat (mi_extra_caps (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)))])
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (4 subgoals):
 1. \<And>a P r Pa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some (Some a); get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; buffer = Some a\<rbrakk> \<Longrightarrow> weak_det_spec Pa (load_word_offs a r)
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 3. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (3 subgoals):
 1. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> (not_idle_thread thread and valid_global_refs and valid_objs and valid_irq_node and valid_idle and valid_etcbs) sa \<and> s = sa
 2. \<And>sa. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; s = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register)) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>evalMonad (lookup_ipc_buffer False thread) s = Some buffer; get_tcb thread s = Some t; valid_global_refs s; valid_objs s; valid_irq_node s; valid_idle s; valid_etcbs s; not_idle_thread thread s; False\<rbrakk> \<Longrightarrow> no_fail ((=) s) (get_extra_cptrs buffer (data_to_message_info (arch_tcb_context_get (tcb_arch t) msg_info_register))) proof (prove)
goal:
No subgoals!