theory Ipc_DR

lemma dcorres_get_thread_state:
  "dcorres (\<lambda>op ts. op = infer_tcb_pending_op t ts)
     \<top>
     (valid_etcbs and tcb_at t and not_idle_thread t)
     (do tcb <- get_thread t; return (the (cdl_tcb_caps tcb tcb_pending_op_slot)) od)
     (get_thread_state t)" text \<open>Brute force proof. Trying to reuse @{thm thread_get_corres} doesn't
        seem to work, because it expects to have concrete tcbs\<close> apply (simp add: get_thread_state_def) apply (monad_eq simp: corres_underlying_def Bex_def
                        get_thread_def
                        thread_get_def get_tcb_def
                   split: option.splits) apply (rename_tac s ko tcb) apply (case_tac ko; clarsimp) text \<open>These two existential vars refer to the same transformed tcb.
        We skip the first one and instantiate the second first\<close> apply (rule exI) apply (rule conjI) apply (rule_tac x="transform_tcb (machine_state s) t tcb (the (get_etcb t s))" in exI) apply (monad_eq simp: transform_tcb_def) apply (rule conjI) apply (fastforce simp: get_etcb_def cdl_objects_tcb not_idle_thread_def
                     dest: valid_etcbs_tcb_etcb) apply (rule refl) apply (clarsimp simp: infer_tcb_pending_op_def tcb_slot_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>op ts. op = infer_tcb_pending_op t ts) (\<lambda>_. True) (valid_etcbs and tcb_at t and not_idle_thread t) (do tcb <- get_thread t;
return (the (cdl_tcb_caps tcb tcb_pending_op_slot))
od) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>op ts. op = infer_tcb_pending_op t ts) (\<lambda>_. True) (valid_etcbs and tcb_at t and not_idle_thread t) (do tcb <- get_thread t;
return (the (cdl_tcb_caps tcb tcb_pending_op_slot))
od) (get_thread_state t) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>op ts. op = infer_tcb_pending_op t ts) (\<lambda>_. True) (valid_etcbs and tcb_at t and not_idle_thread t) (do tcb <- get_thread t;
return (the (cdl_tcb_caps tcb tcb_pending_op_slot))
od) (thread_get tcb_state t) proof (prove)
goal (1 subgoal):
 1. \<And>b x2 aa. \<lbrakk>valid_etcbs b; tcb_at t b; not_idle_thread t b; kheap b t = Some x2; (case x2 of TCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some aa\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa. cdl_objects (transform b) t = Some aa \<and> (a, transform b) \<in> fst ((case aa of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform b))) \<and> infer_tcb_pending_op t (tcb_state aa) = the (cdl_tcb_caps a tcb_pending_op_slot) proof (prove)
goal (1 subgoal):
 1. \<And>s ko tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some ko; (case ko of TCB x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some tcb\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa. cdl_objects (transform s) t = Some aa \<and> (a, transform s) \<in> fst ((case aa of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))) \<and> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps a tcb_pending_op_slot) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa. cdl_objects (transform s) t = Some aa \<and> (a, transform s) \<in> fst ((case aa of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))) \<and> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps a tcb_pending_op_slot) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>a. (\<exists>aa. cdl_objects (transform s) t = Some aa \<and> (a, transform s) \<in> fst ((case aa of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))) \<and> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps a tcb_pending_op_slot) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> (\<exists>a. cdl_objects (transform s) t = Some a \<and> (?a69 s tcb, transform s) \<in> fst ((case a of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))) \<and> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) t = Some a \<and> (?a69 s tcb, transform s) \<in> fst ((case a of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))
 2. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cdl_objects (transform s) t = Some (transform_tcb (machine_state s) t tcb (the (get_etcb t s))) \<and> (?a69 s tcb, transform s) \<in> fst ((case transform_tcb (machine_state s) t tcb (the (get_etcb t s)) of Tcb x \<Rightarrow> return x | _ \<Rightarrow> fail) (transform s))
 2. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cdl_objects (transform s) t = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr>) \<and> ?a69 s tcb = \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr>
 2. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (3 subgoals):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> cdl_objects (transform s) t = Some (Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr>)
 2. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ?a69 s tcb = \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr>
 3. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (2 subgoals):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> ?a69 s tcb = \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr>
 2. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps (?a69 s tcb) tcb_pending_op_slot) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>valid_etcbs s; tcb_at t s; not_idle_thread t s; kheap s t = Some (TCB tcb)\<rbrakk> \<Longrightarrow> infer_tcb_pending_op t (tcb_state tcb) = the (cdl_tcb_caps \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable tcb), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable tcb), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply tcb), tcb_caller_slot \<mapsto> transform_cap (tcb_caller tcb), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe tcb), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op t (tcb_state tcb), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification tcb)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler tcb), cdl_tcb_intent = transform_full_intent (machine_state s) t tcb, cdl_tcb_has_fault = \<exists>y. tcb_fault tcb = Some y, cdl_tcb_domain = tcb_domain (the (get_etcb t s))\<rparr> tcb_pending_op_slot) proof (prove)
goal:
No subgoals!