theory KHeap_DR

lemma ntfn_waiting_set_lift:
  "\<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow>
  get_waiting_ntfn_recv_threads ntfnptr (transform s) =
  ntfn_waiting_set ntfnptr s" supply option.case_cong[cong] apply (rule set_eqI) apply (clarsimp simp: get_waiting_ntfn_recv_threads_def) apply (rule iffI) apply (clarsimp simp: transform_def transform_objects_def) apply (clarsimp simp: restrict_map_Some_iff) apply (clarsimp simp: infer_tcb_pending_op_def transform_object_def
                         transform_tcb_def restrict_map_Some_iff tcb_slots
                  split: Structures_A.kernel_object.splits nat.splits
                         Structures_A.thread_state.splits | drule(1) valid_etcbs_tcb_etcb)+ apply (clarsimp simp: ntfn_waiting_set_def) apply(drule(1) valid_etcbs_tcb_etcb, clarsimp) apply (simp split: arch_kernel_obj.splits) apply (clarsimp simp: ntfn_waiting_set_def
                 split: Structures_A.kernel_object.splits) apply (clarsimp simp: valid_idle_def obj_at_def pred_tcb_at_def) apply (clarsimp simp: transform_def transform_object_def
                        transform_tcb_def transform_objects_def tcb_slots
                        infer_tcb_pending_op_def map_add_def restrict_map_Some_iff
                 split: option.splits | drule(1) valid_etcbs_tcb_etcb)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> get_waiting_ntfn_recv_threads ntfnptr (transform s) = ntfn_waiting_set ntfnptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> get_waiting_ntfn_recv_threads ntfnptr (transform s) = ntfn_waiting_set ntfnptr s proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (x \<in> get_waiting_ntfn_recv_threads ntfnptr (transform s)) = (x \<in> ntfn_waiting_set ntfnptr s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr)) = (x \<in> ntfn_waiting_set ntfnptr s) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr)\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x a. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr); (\<exists>z. (kheap s |` (- {idle_thread s})) x = Some z \<and> transform_object (machine_state s) x ((ekheap s |` (- {idle_thread s})) x) z = Tcb a) \<or> (kheap s |` (- {idle_thread s})) x = None \<and> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s})) x = Some (Tcb a)\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x a z. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr); kheap s x = Some z; x \<noteq> idle_thread s; transform_object (machine_state s) x (ekheap s x) z = Tcb a\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (4 subgoals):
 1. \<And>x x2 etcb. \<lbrakk>valid_idle s; kheap s x = Some (TCB x2); x \<noteq> idle_thread s; tcb_state x2 = BlockedOnNotification ntfnptr; ekheap s x = Some etcb\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x a x2. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingNtfnRecvCap ntfnptr); kheap s x = Some (TCB x2); x \<noteq> idle_thread s; idle (tcb_state x2); (case ekheap s x of Some etcb \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable x2), Suc 0 \<mapsto> transform_cap (tcb_vtable x2), 2 \<mapsto> transform_cap (tcb_reply x2), 3 \<mapsto> transform_cap (tcb_caller x2), 4 \<mapsto> transform_cap (tcb_ipcframe x2), 5 \<mapsto> cdl_cap.NullCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = transform_full_intent (machine_state s) x x2, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = Tcb a\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 3. \<And>x a x5. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingNtfnRecvCap ntfnptr); 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> x \<in> ntfn_waiting_set ntfnptr s
 4. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x a x2. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingNtfnRecvCap ntfnptr); kheap s x = Some (TCB x2); x \<noteq> idle_thread s; idle (tcb_state x2); (case ekheap s x of Some etcb \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [0 \<mapsto> transform_cap (tcb_ctable x2), Suc 0 \<mapsto> transform_cap (tcb_vtable x2), 2 \<mapsto> transform_cap (tcb_reply x2), 3 \<mapsto> transform_cap (tcb_caller x2), 4 \<mapsto> transform_cap (tcb_ipcframe x2), 5 \<mapsto> cdl_cap.NullCap, 6 \<mapsto> infer_tcb_bound_notification (tcb_bound_notification x2)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler x2), cdl_tcb_intent = transform_full_intent (machine_state s) x x2, cdl_tcb_has_fault = \<exists>y. tcb_fault x2 = Some y, cdl_tcb_domain = tcb_domain etcb\<rparr>) = Tcb a\<rbrakk> \<Longrightarrow> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x a x5. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingNtfnRecvCap ntfnptr); 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> x \<in> ntfn_waiting_set ntfnptr s
 3. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x a x5. \<lbrakk>valid_idle s; valid_etcbs s; cdl_tcb_caps a 5 = Some (PendingNtfnRecvCap ntfnptr); 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> x \<in> ntfn_waiting_set ntfnptr s
 2. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>valid_idle s; valid_etcbs s; x \<in> ntfn_waiting_set ntfnptr s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>valid_idle s; valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t tcb. \<lbrakk>valid_etcbs s; kheap s x = Some (TCB t); tcb_state t = BlockedOnNotification ntfnptr; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> cdl_tcb_caps a tcb_pending_op_slot = Some (PendingNtfnRecvCap ntfnptr) proof (prove)
goal:
No subgoals!