theory Ipc_DR

lemma dcorres_set_extra_badge:
  "rcv = thread \<Longrightarrow> dcorres dc \<top>
           (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread thread and
            (\<lambda>s. evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some rcv_buffer) \<and>
                 2 + msg_max_length + n < max_ipc_length) and valid_etcbs)
           (corrupt_ipc_buffer rcv in_receive)
           (set_extra_badge rcv_buffer w n)" supply if_cong[cong] apply (clarsimp simp:set_extra_badge_def corrupt_ipc_buffer_def) apply (rule dcorres_expand_pfx) apply clarsimp apply (frule lookup_ipc_buffer_SomeB_evalMonad) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_symb_exec_l) apply (rule_tac F = "rv = Some b" in corres_gen_asm) apply (clarsimp) apply (rule dcorres_store_word_offs_spec) apply (drule_tac x = "buffer_cptr_index + n" and sz = sz in within_page_ipc_buf) apply (simp)+ apply (simp add:obj_at_def cte_wp_at_cases) apply (drule_tac t = "tcb_ipcframe obj" in sym) apply (fastforce simp:ipc_frame_wp_at_def obj_at_def) apply (simp add:obj_at_def cte_wp_at_cases) apply (drule_tac t = "tcb_ipcframe obj" in sym) apply (fastforce simp:ipc_frame_wp_at_def obj_at_def) apply (simp add:ipc_buffer_wp_at_def obj_at_def) apply (clarsimp simp: msg_max_length_def max_ipc_length_unfold buffer_cptr_index_def
                              msg_align_bits) 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 (subgoal_tac "s = transform s'") prefer 2 apply simp+ apply (rule exI) apply (clarsimp simp: obj_at_def, frule(1) valid_etcbs_tcb_etcb) apply (subst opt_cap_tcb) apply (rule get_tcb_rev, simp) apply (clarsimp simp: get_etcb_def) apply (simp add:obj_at_def not_idle_thread_def)+ apply (simp split:cdl_cap.splits) apply (wp cdl_get_ipc_buffer_Some) apply (drule lookup_ipc_buffer_SomeB_evalMonad) apply (fastforce simp:cte_wp_at_def) apply (clarsimp simp:tcb_at_def get_tcb_SomeD obj_at_def not_idle_thread_def)+ apply (clarsimp simp:cte_wp_at_cases obj_at_def) apply (drule_tac t = "tcb_ipcframe obj" in sym) apply (fastforce simp:ipc_frame_wp_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rcv = thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread thread and (\<lambda>s. evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some rcv_buffer) \<and> 2 + msg_max_length + n < max_ipc_length) and valid_etcbs) (corrupt_ipc_buffer rcv in_receive) (set_extra_badge rcv_buffer w n) proof (prove)
goal (1 subgoal):
 1. rcv = thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread thread and (\<lambda>s. evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some rcv_buffer) \<and> 2 + msg_max_length + n < max_ipc_length) and valid_etcbs) (corrupt_ipc_buffer rcv in_receive) (set_extra_badge rcv_buffer w n) proof (prove)
goal (1 subgoal):
 1. rcv = thread \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread thread and (\<lambda>s. evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some rcv_buffer) \<and> Suc (Suc (msg_max_length + n)) < max_ipc_length) and valid_etcbs) (do buffer <- get_ipc_buffer thread in_receive;
case buffer of None \<Rightarrow> corrupt_tcb_intent thread | Some a \<Rightarrow> corrupt_frame a
od) (store_word_offs rcv_buffer (buffer_cptr_index + n) w) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>rcv = thread; s = transform s'; True; (valid_idle and valid_objs and pspace_aligned and pspace_distinct and not_idle_thread thread and (\<lambda>s. evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some rcv_buffer) \<and> Suc (Suc (msg_max_length + n)) < max_ipc_length) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do buffer <- get_ipc_buffer thread in_receive;
case buffer of None \<Rightarrow> corrupt_tcb_intent thread | Some a \<Rightarrow> corrupt_frame a
od) (store_word_offs rcv_buffer (buffer_cptr_index + n) w) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some rcv_buffer); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer thread in_receive >>= case_option (corrupt_tcb_intent thread) corrupt_frame) (store_word_offs rcv_buffer (buffer_cptr_index + n) w) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some rcv_buffer); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread b rs sz s' \<and> ko_at (TCB obj) thread s' \<and> rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer thread in_receive >>= case_option (corrupt_tcb_intent thread) corrupt_frame) (store_word_offs rcv_buffer (buffer_cptr_index + n) w) proof (prove)
goal (1 subgoal):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (get_ipc_buffer thread in_receive >>= case_option (corrupt_tcb_intent thread) corrupt_frame) (store_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) (buffer_cptr_index + n) w) proof (prove)
goal (3 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc (?Q25 s' b rs sz mapdata obj dev) (?Q'25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive >>= case_option (corrupt_tcb_intent thread) corrupt_frame) (store_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) (buffer_cptr_index + n) w)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> ?Q'25 s' b rs sz mapdata obj dev s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev rv. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc (?Q29 s' b rs sz mapdata obj dev rv) (?Q'25 s' b rs sz mapdata obj dev) (case rv of None \<Rightarrow> corrupt_tcb_intent thread | Some x \<Rightarrow> corrupt_frame x) (store_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) (buffer_cptr_index + n) w)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>?Q29 s' b rs sz mapdata obj dev\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> ?Q'25 s' b rs sz mapdata obj dev s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev rv. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); rv = Some b\<rbrakk> \<Longrightarrow> dcorres dc (?P34 s' b rs sz mapdata obj dev rv) (?Q'25 s' b rs sz mapdata obj dev) (case rv of None \<Rightarrow> corrupt_tcb_intent thread | Some x \<Rightarrow> corrupt_frame x) (store_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) (buffer_cptr_index + n) w)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. ?P34 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> ?Q'25 s' b rs sz mapdata obj dev s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> dcorres dc (?P34 s' b rs sz mapdata obj dev (Some b)) (?Q'25 s' b rs sz mapdata obj dev) (corrupt_frame b) (store_word_offs (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))) (buffer_cptr_index + n) w)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. ?P34 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> ?Q'25 s' b rs sz mapdata obj dev s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (12 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> pspace_aligned s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> pspace_distinct s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at (?buf42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y42 s' b rs sz mapdata obj dev) s'
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page (?buf42 s' b rs sz mapdata obj dev) (?buf42 s' b rs sz mapdata obj dev + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 10. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at (?buf42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y42 s' b rs sz mapdata obj dev) s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page (?buf42 s' b rs sz mapdata obj dev) (?buf42 s' b rs sz mapdata obj dev + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 8. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 10. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (10 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe obj; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at (?buf42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y42 s' b rs sz mapdata obj dev) s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page (?buf42 s' b rs sz mapdata obj dev) (?buf42 s' b rs sz mapdata obj dev + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 8. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 10. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (10 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ipc_frame_ptr_at (?buf42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?y42 s' b rs sz mapdata obj dev) s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) (?y42 s' b rs sz mapdata obj dev) s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page (?buf42 s' b rs sz mapdata obj dev) (?buf42 s' b rs sz mapdata obj dev + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 8. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 10. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) thread s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe obj; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) thread s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz thread s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) thread s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (8 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?bptr42 s' b rs sz mapdata obj dev) thread s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (?bptr42 s' b rs sz mapdata obj dev && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (7 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> buffer_cptr_index + n < 2 ^ (msg_align_bits - 2)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat (buffer_cptr_index + n) * word_of_nat word_size) sz\<rbrakk> \<Longrightarrow> within_page b (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) + word_of_nat ((buffer_cptr_index + n) * word_size)) (?sz40 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at (?sz40 s' b rs sz mapdata obj dev) (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (5 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get_ipc_buffer thread in_receive \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (thread, tcb_ipcbuffer_slot) s = Some y
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (7 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s; s = transform s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (thread, tcb_ipcbuffer_slot) s = Some y
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> s = transform s'
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (7 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> s = transform s'
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s; s = transform s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (thread, tcb_ipcbuffer_slot) s = Some y
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); ?Q25 s' b rs sz mapdata obj dev s\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 s' b rs sz mapdata obj dev\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (?Q25 s' b rs sz mapdata obj dev) (get_ipc_buffer thread in_receive)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> ?Q25 s' b rs sz mapdata obj dev s
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (thread, tcb_ipcbuffer_slot) (transform s') = Some y
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_ipcbuffer_slot) (transform s') = Some (?y68 s' b rs sz mapdata obj dev s)
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (6 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> opt_cap (thread, tcb_ipcbuffer_slot) (transform s') = Some (?y68 s' b rs sz mapdata obj dev (transform s'))
 2. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> get_tcb thread s' = Some (?tcb77 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb thread s' = Some etcb
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> (if tcb_ipcbuffer_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF (?tcb77 s' b rs sz mapdata obj dev))) (tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot)) else if tcb_ipcbuffer_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state (?tcb77 s' b rs sz mapdata obj dev))) else if tcb_ipcbuffer_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification (?tcb77 s' b rs sz mapdata obj dev))) else None) = Some (?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s'))
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>rv. (\<lambda>a. True) and (\<lambda>s. rv = Some b)\<rbrace>
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s
flex-flex pairs:
\<lambda>s' b rs sz mapdata obj dev. ?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s') \<equiv>\<^sup>? \<lambda>s' b rs sz mapdata obj dev. ?y68 s' b rs sz mapdata obj dev (transform s') proof (prove)
goal (8 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb thread s' = Some etcb
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> (if tcb_ipcbuffer_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF obj)) (tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot)) else if tcb_ipcbuffer_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state obj)) else if tcb_ipcbuffer_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification obj)) else None) = Some (?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s'))
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s
flex-flex pairs:
\<lambda>s' b rs sz mapdata obj dev. ?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s') \<equiv>\<^sup>? \<lambda>s' b rs sz mapdata obj dev. ?y68 s' b rs sz mapdata obj dev (transform s') proof (prove)
goal (7 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> (if tcb_ipcbuffer_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF obj)) (tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot)) else if tcb_ipcbuffer_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state obj)) else if tcb_ipcbuffer_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification obj)) else None) = Some (?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s'))
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, tcb_ipcbuffer_slot) 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)) s). case x of (rv, x) \<Rightarrow> s = x)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s
flex-flex pairs:
\<lambda>s' b rs sz mapdata obj dev. ?y78 s' s' b rs sz mapdata obj dev (?b77 s' b rs sz mapdata obj dev) (?rs77 s' b rs sz mapdata obj dev) (?sz77 s' b rs sz mapdata obj dev) (?mapdata77 s' b rs sz mapdata obj dev) (?obj77 s' b rs sz mapdata obj dev) (?dev77 s' b rs sz mapdata obj dev) (transform s') \<equiv>\<^sup>? \<lambda>s' b rs sz mapdata obj dev. ?y68 s' b rs sz mapdata obj dev (transform s') proof (prove)
goal (5 subgoals):
 1. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; thread \<noteq> idle_thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; kheap s' thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> \<forall>x2. opt_cap (thread, 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)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (4 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. s = transform s'\<rbrace> get_ipc_buffer thread 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>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 3. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 4. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_cte_at thread b (?rs109 s' b rs sz mapdata obj dev) (?sz109 s' b rs sz mapdata obj dev) (?s'109 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> valid_etcbs (?s'109 s' b rs sz mapdata obj dev)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> tcb_at thread (?s'109 s' b rs sz mapdata obj dev)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> not_idle_thread thread (?s'109 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> AllowRead \<in> ?rs109 s' b rs sz mapdata obj dev \<and> (\<not> in_receive \<or> AllowWrite \<in> ?rs109 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> True \<and> transform (?s'109 s' b rs sz mapdata obj dev) = s
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (9 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); \<exists>ba rs sza obja. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread ba rs sza s' \<and> ko_at (TCB obja) thread s' \<and> b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) = ba + (tcb_ipc_buffer obja && mask (pageBitsForSize sza))\<rbrakk> \<Longrightarrow> ipc_frame_cte_at thread b (?rs109 s' b rs sz mapdata obj dev) (?sz109 s' b rs sz mapdata obj dev) (?s'109 s' b rs sz mapdata obj dev)
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> valid_etcbs (?s'109 s' b rs sz mapdata obj dev)
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> tcb_at thread (?s'109 s' b rs sz mapdata obj dev)
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> not_idle_thread thread (?s'109 s' b rs sz mapdata obj dev)
 5. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> AllowRead \<in> ?rs109 s' b rs sz mapdata obj dev \<and> (\<not> in_receive \<or> AllowWrite \<in> ?rs109 s' b rs sz mapdata obj dev)
 6. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> True \<and> transform (?s'109 s' b rs sz mapdata obj dev) = s
 7. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 9. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (8 subgoals):
 1. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> valid_etcbs s'
 2. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> tcb_at thread s'
 3. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> not_idle_thread thread s'
 4. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs)
 5. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s = transform s'\<rbrakk> \<Longrightarrow> True \<and> transform s' = s
 6. \<And>s' b rs sz mapdata obj dev. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. s = transform s') (get_ipc_buffer thread in_receive)
 7. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); transform s' = s\<rbrakk> \<Longrightarrow> s = transform s'
 8. \<And>s' b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s'; valid_objs s'; pspace_aligned s'; pspace_distinct s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; ko_at (TCB obj) thread s'; rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_sz_at sz (?s_id40 s' b rs sz mapdata obj dev) and ipc_frame_ptr_at b (?s_id40 s' b rs sz mapdata obj dev) and valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s; valid_objs s; pspace_aligned s; pspace_distinct s; thread \<noteq> idle_thread s; evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s; kheap s thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?s_id40 s b rs sz mapdata obj dev) s \<and> ipc_frame_ptr_at b (?s_id40 s b rs sz mapdata obj dev) s proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s; valid_objs s; pspace_aligned s; pspace_distinct s; thread \<noteq> idle_thread s; evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe obj; kheap s thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz))\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?s_id40 s b rs sz mapdata obj dev) s \<and> ipc_frame_ptr_at b (?s_id40 s b rs sz mapdata obj dev) s proof (prove)
goal (1 subgoal):
 1. \<And>b rs sz mapdata obj dev s. \<lbrakk>rcv = thread; valid_idle s; valid_objs s; pspace_aligned s; pspace_distinct s; thread \<noteq> idle_thread s; evalMonad (lookup_ipc_buffer in_receive thread) s = Some (Some (b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))); Suc (Suc (msg_max_length + n)) < max_ipc_length; valid_etcbs s; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; kheap s thread = Some (TCB obj); rcv_buffer = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)); tcb_ipcframe obj = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> ipc_frame_sz_at sz (?s_id40 s b rs sz mapdata obj dev) s \<and> ipc_frame_ptr_at b (?s_id40 s b rs sz mapdata obj dev) s proof (prove)
goal:
No subgoals!