theory Ipc_DR

lemma evalMonad_lookup_ipc_buffer_wp:
assumes cte_wp:"\<And>P slot. (\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c)
  \<Longrightarrow> \<lbrace>cte_wp_at (P and (\<noteq>) cap.NullCap) slot\<rbrace> f \<lbrace>\<lambda>r. cte_wp_at P slot\<rbrace>"
assumes tcb_wp:"\<And>buf t. \<lbrace>ipc_buffer_wp_at buf t\<rbrace> f \<lbrace>\<lambda>r. ipc_buffer_wp_at buf t \<rbrace>"
shows "\<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace>" apply (simp add:valid_def lookup_ipc_buffer_def) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_thread_get weak_det_spec_thread_get)+ apply wp apply (clarsimp split:option.split_asm simp:evalMonad_thread_get_eq) apply (frule use_valid[OF _ tcb_wp]) apply (clarsimp dest!:get_tcb_SomeD simp:ipc_buffer_wp_at_def obj_at_def) apply (fastforce) apply (clarsimp simp:ipc_buffer_wp_at_def obj_at_def dest!:get_tcb_rev) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_thread_get weak_det_spec_thread_get)+ apply wp apply (subst (asm) evalMonad_compose) apply (simp add:empty_when_fail_get_cap weak_det_spec_get_cap)+ apply wp apply (clarsimp simp:evalMonad_get_cap split:option.split_asm cap.split_asm) apply (drule caps_of_state_cteD) apply (rename_tac arch_cap) apply (frule_tac P1 = "(=) (cap.ArchObjectCap arch_cap)" in use_valid[OF _ cte_wp]) apply (clarsimp simp:is_cap_simps) apply (erule cte_wp_at_weakenE) apply clarsimp apply (clarsimp simp:cte_wp_at_caps_of_state evalMonad_thread_get_eq) apply (subst evalMonad_compose) apply (simp add:empty_when_fail_get_cap weak_det_spec_get_cap)+ apply wp apply (simp add:evalMonad_get_cap) apply (case_tac arch_cap) apply simp_all apply (clarsimp simp:evalMonad_def return_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer in_receive x) s = Some (Some buf)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) s = Some (Some buf) \<longrightarrow> (\<forall>xa\<in>fst (f s). case xa of (r, s') \<Rightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) s' = Some (Some buf)) proof (prove)
goal (4 subgoals):
 1. \<And>s. empty_when_fail (thread_get tcb_ipc_buffer x)
 2. \<And>s. weak_det_spec ((=) s) (thread_get tcb_ipc_buffer x)
 3. \<And>s sa. \<lbrace>(=) sa\<rbrace> thread_get tcb_ipc_buffer x \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<forall>s. (case evalMonad (thread_get tcb_ipc_buffer x) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s) = Some (Some buf) \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) s' = Some (Some buf)) proof (prove)
goal (2 subgoals):
 1. \<And>sa. \<lbrace>(=) sa\<rbrace> thread_get tcb_ipc_buffer x \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<forall>s. (case evalMonad (thread_get tcb_ipc_buffer x) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s) = Some (Some buf) \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) s' = Some (Some buf)) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (case evalMonad (thread_get tcb_ipc_buffer x) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s) = Some (Some buf) \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) s' = Some (Some buf)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a\<rbrakk> \<Longrightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) b = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a\<rbrakk> \<Longrightarrow> ipc_buffer_wp_at (?buf38 s a b x2a) (?t38 s a b x2a) s
 2. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; ipc_buffer_wp_at (?buf38 s a b x2a) (?t38 s a b x2a) b\<rbrakk> \<Longrightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) b = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); kheap s x = Some (TCB x2a)\<rbrakk> \<Longrightarrow> \<exists>ko. kheap s (?t38 s a b x2a) = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> tcb_ipc_buffer tcb = ?buf38 s a b x2a)
 2. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; ipc_buffer_wp_at (?buf38 s a b x2a) (?t38 s a b x2a) b\<rbrakk> \<Longrightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) b = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; ipc_buffer_wp_at (tcb_ipc_buffer x2a) x b\<rbrakk> \<Longrightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) b = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer x;
CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (buffer_ptr && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))
od) b = Some (Some buf) proof (prove)
goal (4 subgoals):
 1. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> empty_when_fail (thread_get tcb_ipc_buffer x)
 2. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec ((=) b) (thread_get tcb_ipc_buffer x)
 3. \<And>s a b x2a tcb sa. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> thread_get tcb_ipc_buffer x \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb sa. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> thread_get tcb_ipc_buffer x \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) s = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (4 subgoals):
 1. \<And>s a b x2a tcb. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 2. \<And>s a b x2a tcb. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> weak_det_spec ((=) s) (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 3. \<And>s a b x2a tcb sa. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s a b x2a tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) s) = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb sa. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>s a b x2a tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) s) = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) s of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) s) = Some (Some buf); (a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb x12. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap x12); evalMonad (case x12 of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf)\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb x12. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case x12 of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap x12)) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (3 subgoals):
 1. \<And>s a b x2a tcb arch_cap c. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; ArchObjectCap arch_cap = c\<rbrakk> \<Longrightarrow> \<not> Structures_A.is_untyped_cap c
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap arch_cap) and (\<noteq>) cap.NullCap) (?slot144 s a b x2a tcb arch_cap) s
 3. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; cte_wp_at ((=) (ArchObjectCap arch_cap)) (?slot144 s a b x2a tcb arch_cap) b\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap arch_cap) and (\<noteq>) cap.NullCap) (?slot144 s a b x2a tcb arch_cap) s
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; cte_wp_at ((=) (ArchObjectCap arch_cap)) (?slot144 s a b x2a tcb arch_cap) b\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb arch_cap c. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); ArchObjectCap arch_cap = c\<rbrakk> \<Longrightarrow> ((=) (ArchObjectCap arch_cap) and (\<noteq>) cap.NullCap) c
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) b\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) b\<rbrakk> \<Longrightarrow> (case evalMonad (thread_get tcb_ipc_buffer x) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) >>= case_cap (return None) (\<lambda>bool word nat1 nat2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word bool set. return None) (\<lambda>word nat list. return None) (\<lambda>word. return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>word option nat. return None) (case_arch_cap (\<lambda>word1 word2. return None) (return None) (\<lambda>x p R vms xa. if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b = Some (Some buf) proof (prove)
goal (4 subgoals):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> weak_det_spec ((=) b) (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 3. \<And>s a b x2a tcb arch_cap sa. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> (case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) b) = Some (Some buf) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb arch_cap sa. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> CSpaceAcc_A.get_cap (x, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) sa\<rbrace>
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> (case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> (case evalMonad (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4)) b of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (case r of ArchObjectCap (PageCap xa p R vms xaa) \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) b) = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap)\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf) proof (prove)
goal (5 subgoals):
 1. \<And>s a b x2a tcb arch_cap x11 x12. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf)
 2. \<And>s a b x2a tcb arch_cap. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf)
 3. \<And>s a b x2a tcb arch_cap x31 x32 x33 x34 x35. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf)
 4. \<And>s a b x2a tcb arch_cap x41 x42. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf)
 5. \<And>s a b x2a tcb arch_cap x51 x52. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap arch_cap); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> evalMonad (case arch_cap of PageCap x p R vms xa \<Rightarrow> if vm_read_write \<subseteq> R \<or> vm_read_only \<subseteq> R \<and> \<not> in_receive then return $ Some $ p + (tcb_ipc_buffer x2a && mask (pageBitsForSize vms)) else return None | _ \<Rightarrow> return None) b = Some (Some buf) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb arch_cap x31 x32 x33 x34 x35. \<lbrakk>(a, b) \<in> fst (f s); get_tcb x s = Some x2a; tcb_ipc_buffer tcb = tcb_ipc_buffer x2a; get_tcb x b = Some tcb; evalMonad (if vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> in_receive then return $ Some $ x32 + (tcb_ipc_buffer x2a && mask (pageBitsForSize x34)) else return None) s = Some (Some buf); caps_of_state s (x, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); caps_of_state b (x, tcb_cnode_index 4) = Some (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> x33 \<longrightarrow> x32 + (tcb_ipc_buffer x2a && mask (pageBitsForSize x34)) = buf) \<and> (vm_read_only \<subseteq> x33 \<and> \<not> in_receive \<longrightarrow> x32 + (tcb_ipc_buffer x2a && mask (pageBitsForSize x34)) = buf) \<and> (vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> in_receive) proof (prove)
goal:
No subgoals!