theory KHeap_DR

lemma ep_waiting_set_send_lift:
  "\<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow>
   get_waiting_sync_send_threads epptr (transform s) =
   ep_waiting_set_send epptr s" apply (rule set_eqI) apply (clarsimp simp: get_waiting_sync_send_threads_def) apply (rule iffI) apply (clarsimp simp: ep_waiting_set_send_def
                         transform_def transform_objects_def restrict_map_Some_iff) apply (clarsimp simp: infer_tcb_pending_op_def transform_object_def
                         transform_tcb_def tcb_slots infer_tcb_bound_notification_def
                   split: Structures_A.kernel_object.splits nat.splits
                          Structures_A.thread_state.splits | drule(1) valid_etcbs_tcb_etcb)+ apply (simp split: arch_kernel_obj.splits) apply (clarsimp simp: ep_waiting_set_send_def map_add_def
                        transform_def transform_objects_def
                  split: option.splits if_splits) apply (clarsimp simp: restrict_map_Some_iff) apply (rule conjI) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (drule(1) valid_etcbs_tcb_etcb) apply (clarsimp simp: infer_tcb_pending_op_def transform_tcb_def tcb_slots) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> get_waiting_sync_send_threads epptr (transform s) = ep_waiting_set_send epptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (x \<in> get_waiting_sync_send_threads epptr (transform s)) = (x \<in> ep_waiting_set_send epptr s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault))) = (x \<in> ep_waiting_set_send epptr s) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault))\<rbrakk> \<Longrightarrow> x \<in> ep_waiting_set_send epptr s
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ep_waiting_set_send epptr s\<rbrakk> \<Longrightarrow> \<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)) proof (prove)
goal (2 subgoals):
 1. \<And>x fault a b call can_grant can_grant_reply z. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault); kheap s x = Some z; x \<noteq> idle_thread s; transform_object (machine_state s) x (ekheap s x) z = Tcb a\<rbrakk> \<Longrightarrow> \<exists>t. z = TCB t \<and> (\<exists>payload. tcb_state t = BlockedOnSend epptr payload)
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ep_waiting_set_send epptr s\<rbrakk> \<Longrightarrow> \<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)) proof (prove)
goal (2 subgoals):
 1. \<And>x fault a b call can_grant can_grant_reply x5. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault); kheap s x = Some (ArchObj x5); x \<noteq> idle_thread s; (case x5 of ASIDPool ap \<Rightarrow> AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents ap\<rparr> | arch_kernel_obj.PageTable ptx \<Rightarrow> cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents ptx\<rparr> | arch_kernel_obj.PageDirectory pd \<Rightarrow> cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents pd\<rparr> | DataPage dev sz \<Rightarrow> Frame \<lparr>cdl_frame_size_bits = pageBitsForSize sz\<rparr>) = Tcb a\<rbrakk> \<Longrightarrow> False
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ep_waiting_set_send epptr s\<rbrakk> \<Longrightarrow> \<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ep_waiting_set_send epptr s\<rbrakk> \<Longrightarrow> \<exists>fault a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)) proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> ((kheap s |` (- {idle_thread s})) x = None \<longrightarrow> (\<exists>fault a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s})) x = Some (Tcb a) \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)))) \<and> (\<forall>x2. (kheap s |` (- {idle_thread s})) x = Some x2 \<longrightarrow> (\<exists>fault a. transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x) x2 = Tcb a \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)))) proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s \<and> (x \<noteq> idle_thread s \<longrightarrow> (\<exists>fault a. (case ekheap s x of Some etcb \<Rightarrow> transform_tcb (machine_state s) x t etcb) = Tcb a \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault)))) proof (prove)
goal (2 subgoals):
 1. \<And>x t payload. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s
 2. \<And>x t payload. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s \<longrightarrow> (\<exists>fault a. (case ekheap s x of Some etcb \<Rightarrow> transform_tcb (machine_state s) x t etcb) = Tcb a \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault))) proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s \<longrightarrow> (\<exists>fault a. (case ekheap s x of Some etcb \<Rightarrow> transform_tcb (machine_state s) x t etcb) = Tcb a \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault))) proof (prove)
goal (1 subgoal):
 1. \<And>x t payload. \<lbrakk>valid_idle s; kheap s x = Some (TCB t); tcb_state t = BlockedOnSend epptr payload; \<exists>etcb. ekheap s x = Some etcb\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread s \<longrightarrow> (\<exists>fault a. (case ekheap s x of Some etcb \<Rightarrow> transform_tcb (machine_state s) x t etcb) = Tcb a \<and> (\<exists>b call can_grant can_grant_reply. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncSendCap epptr b call can_grant can_grant_reply fault))) proof (prove)
goal:
No subgoals!