theory Ipc_DR

lemma dcorres_copy_mrs':
  notes hoare_post_taut[wp] if_cong[cong]
  shows
  "dcorres dc \<top> ((\<lambda>s. evalMonad (lookup_ipc_buffer in_receive recv) s = Some rv)
    and valid_idle and not_idle_thread thread and not_idle_thread recv and tcb_at recv
    and valid_objs and pspace_aligned and pspace_distinct and valid_etcbs)
    (corrupt_ipc_buffer recv in_receive)
    (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))" apply (rule dcorres_expand_pfx) apply (clarsimp simp:corrupt_ipc_buffer_def) apply (case_tac rv) apply (rule corres_guard_imp) apply (rule corres_symb_exec_l) apply (rule_tac F = " rvb = None " in corres_gen_asm) apply (clarsimp simp:copy_mrs_def) apply (rule corres_dummy_return_l) apply (rule corres_split[OF set_registers_corres]) apply (rule corres_symb_exec_r)+ apply (rule corres_trivial[OF corres_free_return]) apply (wp | clarsimp split:option.splits)+ prefer 2 apply (wpsimp wp:  hoare_vcg_prop[where P=True] cdl_get_ipc_buffer_None) apply (clarsimp simp:get_ipc_buffer_def gets_the_def exs_valid_def gets_def
               get_def bind_def return_def assert_opt_def fail_def split:option.splits | rule conjI)+ apply (frule(1) tcb_at_is_etcb_at, clarsimp simp: is_etcb_at_def, fold get_etcb_def) apply (clarsimp simp:not_idle_thread_def tcb_at_def opt_cap_tcb)+ apply (simp split:cdl_cap.splits) apply clarsimp apply simp+ apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply clarsimp apply (rule corres_symb_exec_l) apply (rule_tac F = "rvb = Some b" in corres_gen_asm) apply clarsimp apply (rule corres_guard_imp[OF dcorres_copy_mrs]) apply (simp add:data_to_message_info_valid)+ apply (clarsimp simp:ipc_frame_wp_at_def obj_at_def cte_wp_at_cases) apply (drule_tac t = "tcb_ipcframe obj" in sym) apply (clarsimp split:cap.splits simp add:ipc_buffer_wp_at_def obj_at_def) apply (clarsimp simp:get_ipc_buffer_def gets_the_def exs_valid_def gets_def
       get_def bind_def return_def assert_opt_def fail_def split:option.splits | rule conjI)+ apply (clarsimp simp: obj_at_def, frule(1) valid_etcbs_tcb_etcb, fold get_etcb_def) apply (subgoal_tac "get_tcb recv s' = Some obj") apply (clarsimp simp:not_idle_thread_def tcb_at_def opt_cap_tcb get_tcb_def)+ apply (simp split:cdl_cap.splits) apply (rule hoare_pre, wp hoare_vcg_prop[where P=True]  cdl_get_ipc_buffer_Some) apply (fastforce simp:cte_wp_at_def) by clarsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) ((\<lambda>s. evalMonad (lookup_ipc_buffer in_receive recv) s = Some rv) and valid_idle and not_idle_thread thread and not_idle_thread recv and tcb_at recv and valid_objs and pspace_aligned and pspace_distinct and valid_etcbs) (corrupt_ipc_buffer recv in_receive) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; ((\<lambda>s. evalMonad (lookup_ipc_buffer in_receive recv) s = Some rv) and valid_idle and not_idle_thread thread and not_idle_thread recv and tcb_at recv and valid_objs and pspace_aligned and pspace_distinct and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (corrupt_ipc_buffer recv in_receive) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?Q12 s') (?Q'12 s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 3. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 4. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (7 subgoals):
 1. \<And>s' rvb. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?Q16 s' rvb) (?Q'12 s') (case rvb of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>?Q16 s'\<rbrace>
 4. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 6. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 7. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (7 subgoals):
 1. \<And>s' rvb. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; rvb = None\<rbrakk> \<Longrightarrow> dcorres dc (?P21 s' rvb) (?Q'12 s') (case rvb of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P21 s' rv and (\<lambda>s. rv = None)\<rbrace>
 4. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 6. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 7. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?P21 s' None) (?Q'12 s') (corrupt_tcb_intent recv) (do y <- mapM (\<lambda>r. do v <- as_user send (getRegister r);
as_user recv (setRegister r v)
od) (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) msg_registers);
buf_mrs <- case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))];
return (min (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) (word_of_nat (min (length msg_registers) (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P21 s' rv and (\<lambda>s. rv = None)\<rbrace>
 4. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 6. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 7. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> dcorres dc (?P21 s' None) (?Q'12 s') (corrupt_tcb_intent recv >>= return) (do y <- mapM (\<lambda>r. do v <- as_user send (getRegister r);
as_user recv (setRegister r v)
od) (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) msg_registers);
buf_mrs <- case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))];
return (min (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) (word_of_nat (min (length msg_registers) (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P21 s' rv and (\<lambda>s. rv = None)\<rbrace>
 4. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 6. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 7. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (9 subgoals):
 1. \<And>s' x rv'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R29 s' x) (?R'29 s' rv') (return x) (do buf_mrs <- case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))];
return (min (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) (word_of_nat (min (length msg_registers) (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))) + word_of_nat (length buf_mrs)))
od)
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 s' None\<rbrace> corrupt_tcb_intent recv \<lbrace>?R29 s'\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 s'\<rbrace> mapM (\<lambda>r. do v <- as_user send (getRegister r);
as_user recv (setRegister r v)
od) (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) msg_registers) \<lbrace>?R'29 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q32 s' rv and (\<lambda>s. rv = None)\<rbrace>
 6. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 7. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 8. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 9. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (12 subgoals):
 1. \<And>s' x rv' rva. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R29 s' x) (?Q'36 s' x rv' rva) (return x) (return (min (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))) (word_of_nat (min (length msg_registers) (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))) + word_of_nat (length rva))))
 2. \<And>s' x rv'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'29 s' rv'\<rbrace> case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))] \<lbrace>?Q'36 s' x rv'\<rbrace>
 3. \<And>s' x rv' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'; ?R'29 s' rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))] \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' x rv'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'; False\<rbrakk> \<Longrightarrow> no_fail (?R'29 s' rv') (case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))])
 5. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 s' None\<rbrace> corrupt_tcb_intent recv \<lbrace>?R29 s'\<rbrace>
 6. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 s'\<rbrace> mapM (\<lambda>r. do v <- as_user send (getRegister r);
as_user recv (setRegister r v)
od) (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) msg_registers) \<lbrace>?R'29 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q32 s' rv and (\<lambda>s. rv = None)\<rbrace>
 9. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 10. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s' x rv'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'29 s' rv'\<rbrace> case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))] \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>s' x rv' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'; ?R'29 s' rv' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))] \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' x rv'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; dc x rv'; False\<rbrakk> \<Longrightarrow> no_fail (?R'29 s' rv') (case rva of None \<Rightarrow> return [] | Some sb_ptr \<Rightarrow> case None of None \<Rightarrow> return [] | Some rb_ptr \<Rightarrow> mapM (\<lambda>x. load_word_offs sb_ptr x >>= store_word_offs rb_ptr x) [length msg_registers + 1..<Suc (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))])
 4. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 s' None\<rbrace> corrupt_tcb_intent recv \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q'29 s'\<rbrace> mapM (\<lambda>r. do v <- as_user send (getRegister r);
as_user recv (setRegister r v)
od) (take (unat (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) msg_registers) \<lbrace>?R'29 s'\<rbrace>
 6. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q32 s' rv and (\<lambda>s. rv = None)\<rbrace>
 8. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 9. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 10. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
A total of 11 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q32 s' rv and (\<lambda>s. rv = None)\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 6. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s'\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q32 s' rv and (\<lambda>s. rv = None)\<rbrace>
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; ?Q12 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (?Q12 s') (get_ipc_buffer recv in_receive)
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 6. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (5 subgoals):
 1. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; True \<and> True \<and> transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. True \<and> True \<and> transform s' = s) (get_ipc_buffer recv in_receive)
 3. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 5. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2 \<longrightarrow> (\<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x)
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. True \<and> True \<and> transform s' = s) (get_ipc_buffer recv in_receive)
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 6. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (6 subgoals):
 1. \<And>s' y. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; get_etcb recv s' = Some y\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2 \<longrightarrow> (\<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x)
 3. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. True \<and> True \<and> transform s' = s) (get_ipc_buffer recv in_receive)
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 5. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 6. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (5 subgoals):
 1. \<And>s' tcb x2. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; thread \<noteq> idle_thread s'; recv \<noteq> idle_thread s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; get_tcb recv s' = Some tcb; opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x
 2. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. True \<and> True \<and> transform s' = s) (get_ipc_buffer recv in_receive)
 3. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 4. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 5. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. True \<and> True \<and> transform s' = s) (get_ipc_buffer recv in_receive)
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 3. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 4. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (3 subgoals):
 1. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> True \<and> transform s' = s
 2. \<And>s' s. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = None; s' = s\<rbrakk> \<Longrightarrow> (tcb_at recv and valid_idle and not_idle_thread recv and valid_etcbs and ?Q'29 s') s
 3. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some rv; valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv rv (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some (Some a); valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv (Some a) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (1 subgoal):
 1. \<And>s' a. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some a; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at recv b rs sz s' \<and> ko_at (TCB obj) recv s' \<and> a = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv (Some a) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (1 subgoal):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer recv in_receive >>= case_option (corrupt_tcb_intent recv) corrupt_frame) (copy_mrs send rva recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register)))) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev rvb. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q136 s' b rs sz mapdata obj dev rvb) ((=) s') (case rvb of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (copy_mrs send rva recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>?Q136 s' b rs sz mapdata obj dev\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev rvb. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; rvb = Some b\<rbrakk> \<Longrightarrow> dcorres dc (?P141 s' b rs sz mapdata obj dev rvb) ((=) s') (case rvb of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (copy_mrs send rva recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> dcorres dc (?P141 s' b rs sz mapdata obj dev (Some b)) ((=) s') (corrupt_frame b) (copy_mrs send rva recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) (mi_length (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))))
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> valid_message_info (data_to_message_info (arch_tcb_context_get (tcb_arch tcb) msg_info_register))
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; ?P141 s' b rs sz mapdata obj dev (Some b) s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread recv and ipc_frame_ptr_at b recv and ipc_frame_sz_at sz recv and ipc_buffer_wp_at (tcb_ipc_buffer obj) recv and valid_etcbs) s
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s; not_idle_thread thread s; not_idle_thread recv s; tcb_at recv s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_etcbs s; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s; ko_at (TCB obj) recv s; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b recv s \<and> ipc_frame_sz_at sz recv s \<and> ipc_buffer_wp_at (tcb_ipc_buffer obj) recv s
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>b rs sz mapdata obj dev s. \<lbrakk>valid_idle s; not_idle_thread thread s; not_idle_thread recv s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_etcbs s; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe obj; kheap s recv = Some (TCB obj)\<rbrakk> \<Longrightarrow> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> b = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> ipc_buffer_wp_at (tcb_ipc_buffer obj) recv s
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>b rs sz mapdata obj dev s. \<lbrakk>valid_idle s; not_idle_thread thread s; not_idle_thread recv s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_etcbs s; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; kheap s recv = Some (TCB obj); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> b = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> (case tcb_ipcframe obj of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False) \<and> ipc_buffer_wp_at (tcb_ipc_buffer obj) recv s
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (3 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2 \<longrightarrow> (\<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; kheap s' recv = Some (TCB obj); \<exists>etcb. get_etcb recv s' = Some etcb\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2 \<longrightarrow> (\<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (5 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; kheap s' recv = Some (TCB obj); \<exists>etcb. get_etcb recv s' = Some etcb; get_tcb recv s' = Some obj\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; kheap s' recv = Some (TCB obj); \<exists>etcb. get_etcb recv s' = Some etcb\<rbrakk> \<Longrightarrow> get_tcb recv s' = Some obj
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2 \<longrightarrow> (\<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (3 subgoals):
 1. \<And>s' b rs sz mapdata obj dev tcb x2. \<lbrakk>valid_idle s'; thread \<noteq> idle_thread s'; recv \<noteq> idle_thread s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; (case kheap s' recv of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None) = Some tcb; opt_cap (recv, tcb_ipcbuffer_slot) (transform s') = Some x2\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((case x2 of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) (transform s')). case x of (rv, x) \<Rightarrow> transform s' = x
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (2 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P141 s' b rs sz mapdata obj dev rv and (\<lambda>s. rv = Some b)\<rbrace>
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (7 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> ipc_frame_cte_at recv b (?rs202 s' b rs sz mapdata obj dev) (?sz202 s' b rs sz mapdata obj dev) (?s'202 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> valid_etcbs (?s'202 s' b rs sz mapdata obj dev)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> tcb_at recv (?s'202 s' b rs sz mapdata obj dev)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> not_idle_thread recv (?s'202 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> AllowRead \<in> ?rs202 s' b rs sz mapdata obj dev \<and> (\<not> in_receive \<or> AllowWrite \<in> ?rs202 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> transform (?s'202 s' b rs sz mapdata obj dev) = s
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive) proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> valid_etcbs s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> tcb_at recv s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> not_idle_thread recv s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'\<rbrakk> \<Longrightarrow> AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; transform s' = s\<rbrakk> \<Longrightarrow> True \<and> transform s' = s
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>valid_idle s'; not_idle_thread thread s'; not_idle_thread recv s'; tcb_at recv s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; valid_etcbs s'; rv = Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))); AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s'; ko_at (TCB obj) recv s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive)