theory Intent_DR

lemma lookup_ipc_buffer_SomeB_evalMonad:
  "evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf)
    \<Longrightarrow> \<exists>b rs sz obj.  AllowRead \<in>  rs \<and> (\<not> in_receive \<or> (AllowWrite \<in> rs))
    \<and> ipc_frame_cte_at thread b rs sz sa \<and> ko_at (TCB obj) thread sa
    \<and> (buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))" apply (simp add:lookup_ipc_buffer_def) apply (subst (asm) evalMonad_compose) apply (clarsimp simp:empty_when_fail_thread_get weak_det_spec_thread_get)+ apply wp apply (clarsimp split:option.splits dest!:evalMonad_thread_get) apply (subst (asm) evalMonad_compose) apply (clarsimp simp:empty_when_fail_get_cap weak_det_spec_get_cap)+ apply wp apply (clarsimp simp:evalMonad_get_cap split:option.splits) apply (clarsimp dest!:caps_of_state_cteD get_tcb_SomeD simp:obj_at_def split:cap.splits arch_cap.splits if_splits) apply (clarsimp simp:cte_wp_at_cases) apply (fastforce simp: obj_at_def vm_read_only_def vm_read_write_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (lookup_ipc_buffer in_receive thread) sa = Some (Some buf) \<Longrightarrow> \<exists>b rs sz obj. AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs) \<and> ipc_frame_cte_at thread b rs sz sa \<and> ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)) proof (prove)
goal (1 subgoal):
 1. evalMonad (do buffer_ptr <- thread_get tcb_ipc_buffer thread;
CSpaceAcc_A.get_cap (thread, 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) sa = Some (Some buf) \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (4 subgoals):
 1. empty_when_fail (thread_get tcb_ipc_buffer thread)
 2. weak_det_spec ((=) sa) (thread_get tcb_ipc_buffer thread)
 3. \<And>s. \<lbrace>(=) s\<rbrace> thread_get tcb_ipc_buffer thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. (case evalMonad (thread_get tcb_ipc_buffer thread) sa of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (thread, 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))) sa) = Some (Some buf) \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> thread_get tcb_ipc_buffer thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. (case evalMonad (thread_get tcb_ipc_buffer thread) sa of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (thread, 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))) sa) = Some (Some buf) \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (1 subgoal):
 1. (case evalMonad (thread_get tcb_ipc_buffer thread) sa of None \<Rightarrow> None | Some r \<Rightarrow> evalMonad (CSpaceAcc_A.get_cap (thread, 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))) sa) = Some (Some buf) \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>evalMonad (CSpaceAcc_A.get_cap (thread, 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 tcb && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) sa = Some (Some buf); get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (4 subgoals):
 1. \<And>tcb. get_tcb thread sa = Some tcb \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4))
 2. \<And>tcb. get_tcb thread sa = Some tcb \<Longrightarrow> weak_det_spec ((=) sa) (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4))
 3. \<And>tcb s. get_tcb thread sa = Some tcb \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4)) sa 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 tcb && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) sa) = Some (Some buf); get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. get_tcb thread sa = Some tcb \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4)) sa 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 tcb && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) sa) = Some (Some buf); get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>(case evalMonad (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4)) sa 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 tcb && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) sa) = Some (Some buf); get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>get_tcb thread sa = Some tcb; caps_of_state sa (thread, tcb_cnode_index 4) = Some x2; 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 tcb && mask (pageBitsForSize vms)) else return None | ArchObjectCap _ \<Rightarrow> return None | _ \<Rightarrow> return None) sa = Some (Some buf)\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> (\<exists>obj. ko_at (TCB obj) thread sa \<and> buf = b + (tcb_ipc_buffer obj && mask (pageBitsForSize sz)))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x32 x33 x34 x35. \<lbrakk>vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> in_receive; buf = x32 + (tcb_ipc_buffer tcb && mask (pageBitsForSize x34)); kheap sa thread = Some (TCB tcb); cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 x35))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. ipc_frame_cte_at thread b rs sz sa \<and> x32 + (tcb_ipc_buffer tcb && mask (pageBitsForSize x34)) = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x31 x32 x33 x34 x35. \<lbrakk>vm_read_write \<subseteq> x33 \<or> vm_read_only \<subseteq> x33 \<and> \<not> in_receive; buf = x32 + (tcb_ipc_buffer tcb && mask (pageBitsForSize x34)); kheap sa thread = Some (TCB tcb); ArchObjectCap (PageCap x31 x32 x33 x34 x35) = tcb_ipcframe tcb\<rbrakk> \<Longrightarrow> \<exists>b rs. AllowRead \<in> rs \<and> (in_receive \<longrightarrow> AllowWrite \<in> rs) \<and> (\<exists>sz. (\<exists>mapdata dev. ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe tcb) \<and> x32 + (tcb_ipc_buffer tcb && mask (pageBitsForSize x34)) = b + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz))) proof (prove)
goal:
No subgoals!