theory Schedule_DR

lemma getActiveTCBs_subset:
  "\<lbrakk> getActiveTCB x s' = Some y; invs s'; valid_etcbs s' \<rbrakk> \<Longrightarrow>
   x \<in> all_active_tcbs (transform s')" supply option.case_cong[cong] apply (clarsimp simp: all_active_tcbs_def getActiveTCB_def) apply (clarsimp simp: transform_def transform_objects_def map_add_def domIff) apply (clarsimp dest!: get_tcb_SomeD split: option.splits if_split_asm) apply (rule context_conjI) apply (clarsimp simp: restrict_map_def) apply (frule invs_valid_idle) apply (clarsimp simp: valid_idle_def pred_tcb_def2 get_tcb_def) apply (clarsimp simp: restrict_map_def split: if_split_asm) apply (clarsimp simp: transform_object_def transform_tcb_def) apply (clarsimp simp: infer_tcb_pending_op_def) apply (frule(1) valid_etcbs_tcb_etcb) apply (case_tac "tcb_state y", auto simp: tcb_pending_op_slot_def tcb_boundntfn_slot_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getActiveTCB x s' = Some y; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x \<in> all_active_tcbs (transform s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>getActiveTCB x s' = Some y; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x \<in> all_active_tcbs (transform s') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case get_tcb x s' of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> x \<in> dom (cdl_objects (transform s')) \<and> (\<exists>a. cdl_objects (transform s') x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case get_tcb x s' of None \<Rightarrow> None | Some tcb \<Rightarrow> if runnable (tcb_state tcb) then Some tcb else None) = Some y; invs s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> (\<exists>y. (case (kheap s' |` (- {idle_thread s'})) x of None \<Rightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x | Some x2 \<Rightarrow> Some (transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2)) = Some y) \<and> (\<exists>a. (case (kheap s' |` (- {idle_thread s'})) x of None \<Rightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x | Some x2 \<Rightarrow> Some (transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2)) = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y)\<rbrakk> \<Longrightarrow> ((kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))) \<and> (\<forall>x2. (kheap s' |` (- {idle_thread s'})) x = Some x2 \<longrightarrow> (\<exists>a. transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2 = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y)\<rbrakk> \<Longrightarrow> (kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))
 2. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); (kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))\<rbrakk> \<Longrightarrow> \<forall>x2. (kheap s' |` (- {idle_thread s'})) x = Some x2 \<longrightarrow> (\<exists>a. transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2 = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' (idle_thread s') = Some (TCB y); x = idle_thread s'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); (kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))\<rbrakk> \<Longrightarrow> \<forall>x2. (kheap s' |` (- {idle_thread s'})) x = Some x2 \<longrightarrow> (\<exists>a. transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2 = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' (idle_thread s') = Some (TCB y); x = idle_thread s'; valid_idle s'\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); (kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))\<rbrakk> \<Longrightarrow> \<forall>x2. (kheap s' |` (- {idle_thread s'})) x = Some x2 \<longrightarrow> (\<exists>a. transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2 = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); (kheap s' |` (- {idle_thread s'})) x = None \<longrightarrow> (\<exists>y. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some y) \<and> (\<exists>a. ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'})) x = Some (Tcb a) \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap))\<rbrakk> \<Longrightarrow> \<forall>x2. (kheap s' |` (- {idle_thread s'})) x = Some x2 \<longrightarrow> (\<exists>a. transform_object (machine_state s') x ((ekheap s' |` (- {idle_thread s'})) x) x2 = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); x \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> \<exists>a. (case ekheap s' x of Some x2 \<Rightarrow> transform_tcb (machine_state s') x y x2) = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); x \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> \<exists>a. (case ekheap s' x of Some x2 \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable y), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable y), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply y), tcb_caller_slot \<mapsto> transform_cap (tcb_caller y), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe y), tcb_pending_op_slot \<mapsto> infer_tcb_pending_op x (tcb_state y), tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification y)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler y), cdl_tcb_intent = transform_full_intent (machine_state s') x y, cdl_tcb_has_fault = \<exists>ya. tcb_fault y = Some ya, cdl_tcb_domain = tcb_domain x2\<rparr>) = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); x \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> \<exists>a. (case ekheap s' x of Some x2 \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable y), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable y), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply y), tcb_caller_slot \<mapsto> transform_cap (tcb_caller y), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe y), tcb_pending_op_slot \<mapsto> case tcb_state y of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap x True False | BlockedOnNotification ptr \<Rightarrow> PendingNtfnRecvCap ptr | _ \<Rightarrow> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification y)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler y), cdl_tcb_intent = transform_full_intent (machine_state s') x y, cdl_tcb_has_fault = \<exists>ya. tcb_fault y = Some ya, cdl_tcb_domain = tcb_domain x2\<rparr>) = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s'; valid_etcbs s'; runnable (tcb_state y); kheap s' x = Some (TCB y); x \<noteq> idle_thread s'; \<exists>etcb. ekheap s' x = Some etcb\<rbrakk> \<Longrightarrow> \<exists>a. (case ekheap s' x of Some x2 \<Rightarrow> Tcb \<lparr>cdl_tcb_caps = [tcb_cspace_slot \<mapsto> transform_cap (tcb_ctable y), tcb_vspace_slot \<mapsto> transform_cap (tcb_vtable y), tcb_replycap_slot \<mapsto> transform_cap (tcb_reply y), tcb_caller_slot \<mapsto> transform_cap (tcb_caller y), tcb_ipcbuffer_slot \<mapsto> transform_cap (tcb_ipcframe y), tcb_pending_op_slot \<mapsto> case tcb_state y of Running \<Rightarrow> RunningCap | Restart \<Rightarrow> RestartCap | BlockedOnReceive ptr payload \<Rightarrow> PendingSyncRecvCap ptr False (receiver_can_grant payload) | BlockedOnSend ptr payload \<Rightarrow> PendingSyncSendCap ptr (sender_badge payload) (sender_is_call payload) (sender_can_grant payload) (sender_can_grant_reply payload) False | BlockedOnReply \<Rightarrow> PendingSyncRecvCap x True False | BlockedOnNotification ptr \<Rightarrow> PendingNtfnRecvCap ptr | _ \<Rightarrow> cdl_cap.NullCap, tcb_boundntfn_slot \<mapsto> infer_tcb_bound_notification (tcb_bound_notification y)], cdl_tcb_fault_endpoint = of_bl (tcb_fault_handler y), cdl_tcb_intent = transform_full_intent (machine_state s') x y, cdl_tcb_has_fault = \<exists>ya. tcb_fault y = Some ya, cdl_tcb_domain = tcb_domain x2\<rparr>) = Tcb a \<and> (cdl_tcb_caps a tcb_pending_op_slot = Some RunningCap \<or> cdl_tcb_caps a tcb_pending_op_slot = Some RestartCap) proof (prove)
goal:
No subgoals!