theory Ipc_DR

lemma dcorres_set_mrs':
  "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)
    (set_mrs recv rv msgs)" supply if_cong[cong] apply (rule dcorres_expand_pfx) apply (clarsimp simp:corrupt_ipc_buffer_def) apply (case_tac rv) apply (rule corres_symb_exec_l) apply (rule_tac F = " rva = None " in corres_gen_asm) apply (clarsimp simp:copy_mrs_def) apply (rule corres_guard_imp[OF set_mrs_corres_no_recv_buffer]) apply simp+ 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:not_idle_thread_def) apply (rule opt_cap_valid_etcbs, clarsimp+) apply (simp split:cdl_cap.splits) apply (rule hoare_pre, wp hoare_vcg_prop[where P=True] cdl_get_ipc_buffer_None) apply simp+ apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply clarsimp apply (rule corres_symb_exec_l) apply (rule_tac F = "rva = Some b" in corres_gen_asm) apply clarsimp apply (rule corrupt_frame_include_self) apply (rule corres_guard_imp[OF set_mrs_corres]) 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: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 dest!:get_tcb_rev) apply (clarsimp simp:get_ipc_buffer_def gets_the_def exs_valid_def gets_def not_idle_thread_def
      get_def bind_def return_def assert_opt_def fail_def split:option.splits | rule conjI)+ apply (rule opt_cap_valid_etcbs, clarsimp+) apply (simp split:cdl_cap.splits) apply wp apply (wp 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) (set_mrs recv rv msgs) 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) (set_mrs recv rv msgs) 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) (set_mrs recv rv msgs) 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) (set_mrs recv rv msgs) 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) (set_mrs recv rv msgs)
 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) (set_mrs recv rv msgs) proof (prove)
goal (5 subgoals):
 1. \<And>s' rva. \<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' rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (set_mrs recv rv msgs)
 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> \<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>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>?Q12 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (5 subgoals):
 1. \<And>s' rva. \<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; rva = None\<rbrakk> \<Longrightarrow> dcorres dc (?P17 s' rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (set_mrs recv rv msgs)
 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> \<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>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (5 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 (?P17 s' None) ((=) s') (corrupt_tcb_intent recv) (set_mrs recv None msgs)
 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> \<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>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) 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; ?P17 s' None s\<rbrakk> \<Longrightarrow> True
 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; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread recv and valid_etcbs) 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; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 s' rv and (\<lambda>s. rv = None)\<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; False\<rbrakk> \<Longrightarrow> no_fail ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (4 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; 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (5 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None; valid_idle s'; thread \<noteq> idle_thread s'; recv \<noteq> idle_thread 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (4 subgoals):
 1. \<And>s' x2. \<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; 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\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) proof (prove)
goal (3 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>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. ?P17 s' rv and (\<lambda>s. rv = None)\<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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) 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> evalMonad (lookup_ipc_buffer in_receive recv) s' = Some None
 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> transform s' = s
 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 ((=) (transform s')) (get_ipc_buffer recv in_receive)
 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) (set_mrs recv rv msgs) 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) (set_mrs recv (Some a) msgs) 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) (set_mrs recv (Some a) msgs) 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) (set_mrs recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) msgs) proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev rva. \<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 (?Q87 s' b rs sz mapdata obj dev rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (set_mrs recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) msgs)
 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>?Q87 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 rva. \<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'; rva = Some b\<rbrakk> \<Longrightarrow> dcorres dc (?P92 s' b rs sz mapdata obj dev rva) ((=) s') (case rva of None \<Rightarrow> corrupt_tcb_intent recv | Some x \<Rightarrow> corrupt_frame x) (set_mrs recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) msgs)
 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. ?P92 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 (?P92 s' b rs sz mapdata obj dev (Some b)) ((=) s') (corrupt_frame b) (set_mrs recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) msgs)
 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. ?P92 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'; 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 (\<lambda>_. True) ((=) s') (do corrupt_tcb_intent (?y98 s' b rs sz mapdata obj dev);
corrupt_frame b
od) (set_mrs recv (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) msgs)
 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'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b (?y98 s' b rs sz mapdata obj dev) s \<and> not_idle_thread (?y98 s' b rs sz mapdata obj dev) s \<and> valid_etcbs s
 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'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<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'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) 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 (6 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'; True\<rbrakk> \<Longrightarrow> True
 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'; 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
 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> ipc_frame_ptr_at b recv s \<and> not_idle_thread recv s \<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. (\<lambda>a. True) 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 (5 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'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b recv s \<and> not_idle_thread recv s \<and> valid_etcbs s
 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'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<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'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) 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 (5 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'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b recv s \<and> not_idle_thread recv s \<and> valid_etcbs s
 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'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<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'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) 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 (5 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'; s' = s\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b recv s \<and> not_idle_thread recv s \<and> valid_etcbs s
 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'; transform s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<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'\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) 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 (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; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (recv, tcb_cnode_index 4) s; kheap s recv = Some (TCB obj)\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at b 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. (\<lambda>a. True) 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
 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. (\<lambda>a. True) 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
 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. (\<lambda>a. True) 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. \<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)\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) (transform 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. (\<lambda>a. True) 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 (3 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'; get_tcb recv s' = Some obj\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer recv in_receive \<exists>\<lbrace>\<lambda>r. (=) (transform 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. (\<lambda>a. True) 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'; 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'; 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'; 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'; get_tcb recv s' = Some obj\<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. (\<lambda>a. True) 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 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'; get_tcb recv s' = Some obj; 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. (\<lambda>a. True) 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. (\<lambda>a. True) 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 (3 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>?P'164 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer recv in_receive \<lbrace>\<lambda>rv s. rv = Some b\<rbrace>
 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> True \<and> ?P'164 s' b rs sz mapdata obj dev 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'; 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 (?rs168 s' b rs sz mapdata obj dev) (?sz168 s' b rs sz mapdata obj dev) (?s'168 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'168 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'168 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'168 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> ?rs168 s' b rs sz mapdata obj dev \<and> (\<not> in_receive \<or> AllowWrite \<in> ?rs168 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'168 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)