theory Ipc_DR

lemma evalMonad_lookup_ipc_buffer_wp':
assumes cte_wp:"\<And>P slot. \<lbrace>cte_wp_at P 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 buf\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer in_receive x) s = 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 simp:get_tcb_ko_at 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 (case_tac buf) apply clarsimp apply (clarsimp split:option.splits simp:evalMonad_get_cap dest!:caps_of_state_cteD) apply (frule use_valid[OF _ cte_wp]) apply simp apply (clarsimp simp:evalMonad_get_cap 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 (clarsimp simp:evalMonad_get_cap) apply (clarsimp split:cap.splits arch_cap.splits) apply (fastforce simp:evalMonad_def return_def) 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 (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 buf\<rbrace> f \<lbrace>\<lambda>rv s. evalMonad (lookup_ipc_buffer in_receive x) s = 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 buf proof (prove)
goal (2 subgoals):
 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 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; buf = None\<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 buf
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 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 None; (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; buf = None\<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 None
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; cte_wp_at ((=) x2) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> (\<exists>y. evalMonad (thread_get tcb_ipc_buffer x) b = Some y) \<and> (\<forall>x2. evalMonad (thread_get tcb_ipc_buffer x) b = Some x2 \<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 + (x2 && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b = Some None)
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (3 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; cte_wp_at ((=) x2) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> cte_wp_at (?P86 s a b x2a tcb x2) (?slot86 s a b x2a tcb x2) s
 2. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; cte_wp_at ((=) x2) (x, tcb_cnode_index 4) s; cte_wp_at (?P86 s a b x2a tcb x2) (?slot86 s a b x2a tcb x2) b\<rbrakk> \<Longrightarrow> (\<exists>y. evalMonad (thread_get tcb_ipc_buffer x) b = Some y) \<and> (\<forall>x2. evalMonad (thread_get tcb_ipc_buffer x) b = Some x2 \<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 + (x2 && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b = Some None)
 3. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; cte_wp_at ((=) x2) (x, tcb_cnode_index 4) s; cte_wp_at ((=) x2) (x, tcb_cnode_index 4) b\<rbrakk> \<Longrightarrow> (\<exists>y. evalMonad (thread_get tcb_ipc_buffer x) b = Some y) \<and> (\<forall>x2. evalMonad (thread_get tcb_ipc_buffer x) b = Some x2 \<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 + (x2 && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) b = Some None)
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 None
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (5 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<rbrakk> \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 2. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<rbrakk> \<Longrightarrow> weak_det_spec ((=) b) (CSpaceAcc_A.get_cap (x, tcb_cnode_index 4))
 3. \<And>s a b x2a tcb x2 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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 None
 5. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (3 subgoals):
 1. \<And>s a b x2a tcb x2 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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 None
 3. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<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 None
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x2. \<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; buf = None; evalMonad (case x2 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 None; caps_of_state s (x, tcb_cnode_index 4) = Some x2; caps_of_state b (x, tcb_cnode_index 4) = Some x2\<rbrakk> \<Longrightarrow> evalMonad (case x2 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 None
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb x31 x32 x33 x34 x35 x31a x32a x33a x34a. \<lbrakk>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)); (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; buf = None; 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 None\<rbrakk> \<Longrightarrow> (vm_read_write \<subseteq> x33a \<longrightarrow> x34 = x34a \<longrightarrow> x33 = x33a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a)) \<and> (vm_read_only \<subseteq> x33a \<and> \<not> in_receive \<longrightarrow> x34 = x34a \<longrightarrow> x33 = x33a \<longrightarrow> x32 = x32a \<longrightarrow> x31 = (\<not> x31a))
 2. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa. \<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 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; buf = Some aa\<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 buf proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa)\<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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (ArchObjectCap arch_cap)) (?slot327 s a b x2a tcb aa arch_cap) s
 2. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); cte_wp_at ((=) (ArchObjectCap arch_cap)) (x, tcb_cnode_index 4) s; cte_wp_at ((=) (ArchObjectCap arch_cap)) (?slot327 s a b x2a tcb aa 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 aa) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); ArchObjectCap arch_cap = c\<rbrakk> \<Longrightarrow> ArchObjectCap arch_cap = c
 2. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (4 subgoals):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa 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; buf = Some aa; 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 aa); 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 aa 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; buf = Some aa; 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 aa); 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 aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (2 subgoals):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (5 subgoals):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa)
 2. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa)
 3. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa)
 4. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa)
 5. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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 aa) proof (prove)
goal (1 subgoal):
 1. \<And>s a b x2a tcb aa 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; buf = Some aa; 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 aa); 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)) = aa) \<and> (vm_read_only \<subseteq> x33 \<and> \<not> in_receive \<longrightarrow> x32 + (tcb_ipc_buffer x2a && mask (pageBitsForSize x34)) = aa) \<and> (vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> in_receive) proof (prove)
goal:
No subgoals!