theory Intent_DR

lemma lookup_ipc_buffer_None_evalMonad:
  "evalMonad (lookup_ipc_buffer in_receive thread) sa = Some None
    \<Longrightarrow> \<exists>obj. ko_at (TCB obj) thread sa \<and> (\<forall>b rs sz. ipc_frame_cte_at thread b rs sz sa
    \<longrightarrow> ((AllowRead \<notin> rs \<and> \<not> in_receive) \<or>  (in_receive \<and> (AllowWrite \<notin> rs \<or> AllowRead\<notin> rs)))) " 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) apply (simp add:obj_at_def cte_wp_at_cases split:cap.splits arch_cap.splits if_splits) apply (clarsimp simp: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 None \<Longrightarrow> \<exists>obj. ko_at (TCB obj) thread sa \<and> (\<forall>b rs sz. ipc_frame_cte_at thread b rs sz sa \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<notin> rs \<or> AllowRead \<notin> rs)) 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 None \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None; get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None; get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None; get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None; get_tcb thread sa = Some tcb\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) 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 None\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>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 None; kheap sa thread = Some (TCB tcb); cte_wp_at ((=) x2) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> (\<exists>obj. ko_at (TCB obj) thread sa) \<and> (\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz sa) \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2 x12 x31 x32 x33 x34 x35. \<lbrakk>kheap sa thread = Some (TCB tcb); x2 = ArchObjectCap (PageCap x31 x32 x33 x34 x35); tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); x12 = PageCap x31 x32 x33 x34 x35; \<not> vm_read_write \<subseteq> x33 \<and> (vm_read_only \<subseteq> x33 \<longrightarrow> in_receive)\<rbrakk> \<Longrightarrow> AllowRead \<notin> x33 \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) proof (prove)
goal:
No subgoals!