theory Intent_DR

lemma cdl_get_ipc_buffer_None:
  "\<lbrakk> valid_etcbs s'; not_idle_thread thread s';
    evalMonad(lookup_ipc_buffer in_receive thread) s' = Some None \<rbrakk> \<Longrightarrow>
  \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = None\<rbrace>" supply if_cong[cong] apply (drule lookup_ipc_buffer_None_evalMonad) apply (clarsimp simp: valid_def get_ipc_buffer_def gets_the_def gets_def bind_def get_def return_def) apply (subst (asm) opt_cap_tcb) apply (simp add: obj_at_def get_tcb_rev not_idle_thread_def |
            drule(1) valid_etcbs_tcb_etcb |
            fastforce simp: get_etcb_rev)+ apply (clarsimp simp: assert_opt_def return_def split: cdl_cap.splits) apply (clarsimp simp: transform_cap_def split: cap.splits arch_cap.splits) by (auto simp: cte_wp_at_cases split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s'; not_idle_thread thread s'; evalMonad (lookup_ipc_buffer in_receive thread) s' = Some None\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s'; not_idle_thread thread s'; \<exists>obj. ko_at (TCB obj) thread s' \<and> (\<forall>b rs sz. ipc_frame_cte_at thread b rs sz s' \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<notin> rs \<or> AllowRead \<notin> rs))\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> get_ipc_buffer thread in_receive \<lbrace>\<lambda>r s. r = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba obj. \<lbrakk>valid_etcbs s'; not_idle_thread thread s'; (a, b) \<in> fst (assert_opt (opt_cap (thread, tcb_ipcbuffer_slot) (transform s')) (transform s')); (aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); ko_at (TCB obj) thread s'\<rbrakk> \<Longrightarrow> aa = None proof (prove)
goal (4 subgoals):
 1. \<And>a b aa ba obj. \<lbrakk>(aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); ko_at (TCB obj) thread s'; valid_etcbs s'; not_idle_thread thread s'\<rbrakk> \<Longrightarrow> get_tcb thread s' = Some (?tcb31 a b aa ba obj)
 2. \<And>a b aa ba obj. \<lbrakk>(aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); ko_at (TCB obj) thread s'; valid_etcbs s'; not_idle_thread thread s'\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb thread s' = Some etcb
 3. \<And>a b aa ba obj. \<lbrakk>(aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); ko_at (TCB obj) thread s'; valid_etcbs s'; not_idle_thread thread s'\<rbrakk> \<Longrightarrow> thread \<noteq> idle_thread s'
 4. \<And>a b aa ba obj. \<lbrakk>valid_etcbs s'; not_idle_thread thread s'; (a, b) \<in> fst (assert_opt (if tcb_ipcbuffer_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF (?tcb31 a b aa ba obj))) (tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot)) else if tcb_ipcbuffer_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op thread (tcb_state (?tcb31 a b aa ba obj))) else if tcb_ipcbuffer_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification (?tcb31 a b aa ba obj))) else None) (transform s')); (aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); ko_at (TCB obj) thread s'\<rbrakk> \<Longrightarrow> aa = None proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba obj. \<lbrakk>thread \<noteq> idle_thread s'; (a, b) \<in> fst (return (transform_cap (tcb_ipcframe obj)) (transform s')); (aa, ba) \<in> fst ((case a 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 \<lambda>s. ({(Some a, s)}, False) else (\<lambda>s. ({(None, s)}, False)) | _ \<Rightarrow> \<lambda>s. ({(None, s)}, False)) b); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); kheap s' thread = Some (TCB obj); \<exists>etcb. ekheap s' thread = Some etcb\<rbrakk> \<Longrightarrow> aa = None proof (prove)
goal (1 subgoal):
 1. \<And>aa ba obj x171 etcb x172 x173 x174 x175 x176. \<lbrakk>\<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); kheap s' thread = Some (TCB obj); thread \<noteq> idle_thread s'; ekheap s' thread = Some etcb; transform_cap (tcb_ipcframe obj) = FrameCap x171 x172 x173 x174 x175 x176; (aa, ba) \<in> fst ((if AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<or> AllowRead \<in> x173 \<and> \<not> in_receive then \<lambda>s. ({(Some x172, s)}, False) else (\<lambda>s. ({(None, s)}, False))) (transform s'))\<rbrakk> \<Longrightarrow> aa = None proof (prove)
goal (2 subgoals):
 1. \<And>aa ba obj x171 etcb x172 x173 x174 x175 x176 x51 x52 x53. \<lbrakk>(aa, ba) \<in> fst ((if AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<or> AllowRead \<in> x173 \<and> \<not> in_receive then \<lambda>s. ({(Some x172, s)}, False) else (\<lambda>s. ({(None, s)}, False))) (transform s')); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); kheap s' thread = Some (TCB obj); thread \<noteq> idle_thread s'; ekheap s' thread = Some etcb; tcb_ipcframe obj = cap.ReplyCap x51 x52 x53; (if x52 then MasterReplyCap x51 else cdl_cap.ReplyCap x51 x53) = FrameCap x171 x172 x173 x174 x175 x176\<rbrakk> \<Longrightarrow> aa = None
 2. \<And>aa ba obj x171 etcb x172 x173 x34 x35. \<lbrakk>(aa, ba) \<in> fst ((if AllowWrite \<in> x173 \<and> AllowRead \<in> x173 \<or> AllowRead \<in> x173 \<and> \<not> in_receive then \<lambda>s. ({(Some x172, s)}, False) else (\<lambda>s. ({(None, s)}, False))) (transform s')); \<forall>b rs. (\<exists>sz. ipc_frame_cte_at thread b rs sz s') \<longrightarrow> AllowRead \<notin> rs \<and> \<not> in_receive \<or> in_receive \<and> (AllowWrite \<in> rs \<longrightarrow> AllowRead \<notin> rs); kheap s' thread = Some (TCB obj); thread \<noteq> idle_thread s'; ekheap s' thread = Some etcb; tcb_ipcframe obj = ArchObjectCap (PageCap x171 x172 x173 x34 x35)\<rbrakk> \<Longrightarrow> aa = None