theory Intent_DR

lemma cdl_get_ipc_buffer_Some:
  "\<lbrakk>ipc_frame_cte_at thread b rs sz s';valid_etcbs s';tcb_at thread s';not_idle_thread thread s';AllowRead \<in>  rs \<and> (\<not> in_receive \<or> (AllowWrite \<in> rs))\<rbrakk>  \<Longrightarrow>
  \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = Some b\<rbrace>" apply (clarsimp simp: tcb_at_def not_idle_thread_def) apply (drule(1) valid_etcbs_get_tcb_get_etcb) apply (clarsimp simp:get_ipc_buffer_def gets_the_def gets_def bind_assoc valid_def) apply (clarsimp simp:get_def bind_def assert_opt_def) apply (subst (asm) opt_cap_tcb,simp +) apply (clarsimp simp:return_def cte_wp_at_cases dest!:get_tcb_SomeD get_etcb_SomeD) apply (drule sym) apply (clarsimp simp:transform_cap_def return_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ipc_frame_cte_at thread b rs sz s'; valid_etcbs s'; tcb_at thread s'; not_idle_thread thread s'; AllowRead \<in> rs \<and> (\<not> in_receive \<or> AllowWrite \<in> rs)\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = Some b\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev. \<lbrakk>valid_etcbs s'; thread \<noteq> idle_thread s'; get_tcb thread s' = Some tcb; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = Some b\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev. \<lbrakk>thread \<noteq> idle_thread s'; get_tcb thread s' = Some tcb; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; \<exists>etcb. get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = Some b\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev a ba etcb. \<lbrakk>thread \<noteq> idle_thread s'; get_tcb thread s' = Some tcb; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; (a, ba) \<in> fst ((do x <- get;
assert_opt (opt_cap (thread, tcb_ipcbuffer_slot) x) >>= case_cdl_cap (return None) (\<lambda>bool set1 set2. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word1 word2 set. return None) (\<lambda>word set. return None) (\<lambda>word. return None) (\<lambda>word1 word2 nat1 nat2. return None) (\<lambda>word. return None) (return None) (\<lambda>word1 word2 bool1 bool2 bool3 bool4. return None) (\<lambda>word bool1 bool2. return None) (\<lambda>word. return None) (return None) (return None) (return None) (\<lambda>word. return None) (\<lambda>x a rights xa xb xc. if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then return (Some a) else return None) (\<lambda>word cdl_frame_cap_type option. return None) (\<lambda>word cdl_frame_cap_type option. return None) (return None) (\<lambda>word nat. return None) (\<lambda>word set. return None) (return None) (\<lambda>word. return None) (\<lambda>word. return None) (\<lambda>word. return None) (\<lambda>word. return None)
od) (transform s')); get_etcb thread s' = Some etcb\<rbrakk> \<Longrightarrow> a = Some b proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev a ba etcb aa bb. \<lbrakk>thread \<noteq> idle_thread s'; get_tcb thread s' = Some tcb; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; get_etcb thread s' = Some etcb; (aa, bb) \<in> fst ((case opt_cap (thread, tcb_ipcbuffer_slot) (transform s') of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (transform s')); (a, ba) \<in> fst ((case aa of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then return (Some a) else return None | _ \<Rightarrow> return None) bb)\<rbrakk> \<Longrightarrow> a = Some b proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev a ba etcb aa baa. \<lbrakk>thread \<noteq> idle_thread s'; get_tcb thread s' = Some tcb; cte_wp_at ((=) (ArchObjectCap (PageCap dev b rs sz mapdata))) (thread, tcb_cnode_index 4) s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; get_etcb thread s' = Some etcb; (aa, baa) \<in> fst (return (transform_cap (tcb_ipcframe tcb)) (transform s')); (a, ba) \<in> fst ((case aa of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then return (Some a) else return None | _ \<Rightarrow> return None) baa)\<rbrakk> \<Longrightarrow> a = Some b proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev a ba etcb. \<lbrakk>thread \<noteq> idle_thread s'; ArchObjectCap (PageCap dev b rs sz mapdata) = tcb_ipcframe tcb; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; (a, ba) \<in> fst ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then return (Some a) else return None | _ \<Rightarrow> return None) (transform s')); ekheap s' thread = Some etcb; kheap s' thread = Some (TCB tcb)\<rbrakk> \<Longrightarrow> a = Some b proof (prove)
goal (1 subgoal):
 1. \<And>mapdata tcb dev a ba etcb. \<lbrakk>thread \<noteq> idle_thread s'; AllowRead \<in> rs; in_receive \<longrightarrow> AllowWrite \<in> rs; (a, ba) \<in> fst ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> in_receive then return (Some a) else return None | _ \<Rightarrow> return None) (transform s')); ekheap s' thread = Some etcb; kheap s' thread = Some (TCB tcb); tcb_ipcframe tcb = ArchObjectCap (PageCap dev b rs sz mapdata)\<rbrakk> \<Longrightarrow> a = Some b proof (prove)
goal:
No subgoals!