theory Intent_DR

lemma get_ipc_buffer_words_empty:
  "\<lbrakk>ko_at (TCB obj) thread sa;evalMonad (lookup_ipc_buffer False thread) sa = Some None\<rbrakk> \<Longrightarrow>
  get_ipc_buffer_words (machine_state sa) obj x = []" 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 get_ipc_buffer_words_def dest!:sym[where t = "tcb_ipcframe obj"])+ apply (clarsimp simp:evalMonad_def split:if_splits) apply (clarsimp simp:obj_at_def vm_read_only_def return_def vm_read_write_def)+ apply (clarsimp simp:cte_wp_at_cases get_ipc_buffer_words_def dest!:sym[where t = "tcb_ipcframe obj"])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB obj) thread sa; evalMonad (lookup_ipc_buffer False thread) sa = Some None\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB obj) thread sa; 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 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\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (4 subgoals):
 1. ko_at (TCB obj) thread sa \<Longrightarrow> empty_when_fail (thread_get tcb_ipc_buffer thread)
 2. ko_at (TCB obj) thread sa \<Longrightarrow> weak_det_spec ((=) sa) (thread_get tcb_ipc_buffer thread)
 3. \<And>s. ko_at (TCB obj) thread sa \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get tcb_ipc_buffer thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrakk>ko_at (TCB obj) thread sa; (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 then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) sa) = Some None\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (2 subgoals):
 1. \<And>s. ko_at (TCB obj) thread sa \<Longrightarrow> \<lbrace>(=) s\<rbrace> thread_get tcb_ipc_buffer thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>ko_at (TCB obj) thread sa; (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 then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) sa) = Some None\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at (TCB obj) thread sa; (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 then return $ Some $ p + (r && mask (pageBitsForSize vms)) else return None) (\<lambda>word option. return None) (\<lambda>word option. return None))) sa) = Some None\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ko_at (TCB obj) thread sa; 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 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> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (4 subgoals):
 1. \<And>tcb. \<lbrakk>get_tcb thread sa = Some tcb; ko_at (TCB obj) thread sa\<rbrakk> \<Longrightarrow> empty_when_fail (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4))
 2. \<And>tcb. \<lbrakk>get_tcb thread sa = Some tcb; ko_at (TCB obj) thread sa\<rbrakk> \<Longrightarrow> weak_det_spec ((=) sa) (CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4))
 3. \<And>tcb s. \<lbrakk>get_tcb thread sa = Some tcb; ko_at (TCB obj) thread sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tcb. \<lbrakk>ko_at (TCB obj) thread sa; (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 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> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (2 subgoals):
 1. \<And>tcb s. \<lbrakk>get_tcb thread sa = Some tcb; ko_at (TCB obj) thread sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap (thread, tcb_cnode_index 4) \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>tcb. \<lbrakk>ko_at (TCB obj) thread sa; (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 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> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ko_at (TCB obj) thread sa; (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 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> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (1 subgoal):
 1. \<And>tcb x2. \<lbrakk>get_tcb thread sa = Some tcb; ko_at (TCB obj) thread sa; 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 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> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (16 subgoals):
 1. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) cap.NullCap) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 2. \<And>x21 x22 x23 x24. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (cap.UntypedCap x21 x22 x23 x24)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 3. \<And>x31 x32 x33. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (cap.EndpointCap x31 x32 x33)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 4. \<And>x41 x42 x43. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (cap.NotificationCap x41 x42 x43)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 5. \<And>x51 x52 x53. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (cap.ReplyCap x51 x52 x53)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 6. \<And>x61 x62 x63. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (cap.CNodeCap x61 x62 x63)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 7. \<And>x7. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ThreadCap x7)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 8. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) cap.DomainCap) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 9. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) IRQControlCap) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 10. \<And>x10. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (IRQHandlerCap x10)) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
A total of 16 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>x31 x32 x33 x34 x35 xa xaa. \<lbrakk>kheap sa thread = Some (TCB obj); the (evalMonad (if AllowRead \<in> x33 then mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer obj && mask (pageBitsForSize x34)) + word_of_nat (n * word_size)) x) else return []) (machine_state sa)) \<noteq> []; xa \<in> vm_read_write; xa \<notin> x33; xaa \<in> vm_read_only; tcb_ipcframe obj = ArchObjectCap (PageCap x31 x32 x33 x34 x35)\<rbrakk> \<Longrightarrow> xaa \<in> x33
 2. \<And>x41 x42. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap x41 x42))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 3. \<And>x51 x52. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 xa xaa. \<lbrakk>the None \<noteq> []; xa \<in> vm_read_write; xa \<notin> x33; xaa \<in> vm_read_only; tcb_ipcframe obj = ArchObjectCap (PageCap x31 x32 x33 x34 x35); kheap sa thread = Some (TCB obj); AllowRead \<in> x33; fst (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer obj && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) x) (machine_state sa)) = {}\<rbrakk> \<Longrightarrow> xaa \<in> x33
 2. \<And>x31 x32 x33 x34 x35 x xa. \<lbrakk>the None \<noteq> []; x \<in> vm_read_write; x \<notin> x33; xa \<in> vm_read_only; tcb_ipcframe obj = ArchObjectCap (PageCap x31 x32 x33 x34 x35); kheap sa thread = Some (TCB obj); AllowRead \<notin> x33; fst (return [] (machine_state sa)) = {}\<rbrakk> \<Longrightarrow> xa \<in> x33
 3. \<And>x31 x32 x33 x34 x35 xa xaa. \<lbrakk>pick (fst ` fst (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer obj && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) x) (machine_state sa))) \<noteq> []; xa \<in> vm_read_write; xa \<notin> x33; xaa \<in> vm_read_only; tcb_ipcframe obj = ArchObjectCap (PageCap x31 x32 x33 x34 x35); kheap sa thread = Some (TCB obj); AllowRead \<in> x33; fst (mapM loadWord (map (\<lambda>n. x32 + (tcb_ipc_buffer obj && mask (pageBitsForSize x34)) + word_of_nat n * word_of_nat word_size) x) (machine_state sa)) \<noteq> {}\<rbrakk> \<Longrightarrow> xaa \<in> x33
 4. \<And>x31 x32 x33 x34 x35 x xa. \<lbrakk>pick (fst ` fst (return [] (machine_state sa))) \<noteq> []; x \<in> vm_read_write; x \<notin> x33; xa \<in> vm_read_only; tcb_ipcframe obj = ArchObjectCap (PageCap x31 x32 x33 x34 x35); kheap sa thread = Some (TCB obj); AllowRead \<notin> x33; fst (return [] (machine_state sa)) \<noteq> {}\<rbrakk> \<Longrightarrow> xa \<in> x33
 5. \<And>x41 x42. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap x41 x42))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 6. \<And>x51 x52. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageTableCap x41 x42))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = []
 2. \<And>x51 x52. \<lbrakk>kheap sa thread = Some (TCB obj); cte_wp_at ((=) (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52))) (thread, tcb_cnode_index 4) sa\<rbrakk> \<Longrightarrow> get_ipc_buffer_words (machine_state sa) obj x = [] proof (prove)
goal:
No subgoals!