theory Tcb_DR

lemma not_idle_after_restart [wp]:
  "\<lbrace>invs and not_idle_thread obj_id' :: det_state \<Rightarrow> bool\<rbrace> Tcb_A.restart obj_id'
           \<lbrace>\<lambda>rv. valid_idle \<rbrace>" including no_pre supply if_cong[cong] apply (simp add:Tcb_A.restart_def) apply wp apply (simp add:cancel_ipc_def) apply (wp not_idle_after_blocked_cancel_ipc not_idle_after_reply_cancel_ipc
             not_idle_thread_cancel_signal | wpc)+ apply (rule hoare_strengthen_post[where Q="\<lambda>r. st_tcb_at ((=) r) obj_id'
                                                  and not_idle_thread obj_id' and invs"]) apply (wp gts_sp) apply (clarsimp simp: invs_def valid_state_def valid_pspace_def not_idle_thread_def | rule conjI)+ apply (rule hoare_strengthen_post, rule gts_inv) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> Tcb_A.restart obj_id' \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> Tcb_A.restart obj_id' \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> Tcb_A.restart obj_id' \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> do state <- get_thread_state obj_id';
when (\<not> runnable state \<and> state \<noteq> IdleThreadState) (do y <- IpcCancel_A.cancel_ipc obj_id';
y <- setup_reply_master obj_id';
y <- set_thread_state obj_id' Restart;
y <- tcb_sched_action tcb_sched_enqueue obj_id';
possible_switch_to obj_id'
od)
od \<lbrace>\<lambda>rv. valid_idle\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?Q1 state\<rbrace> IpcCancel_A.cancel_ipc obj_id' \<lbrace>\<lambda>y s. valid_idle s \<and> (obj_id' = idle_thread s \<longrightarrow> idle Restart)\<rbrace>
 2. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then ?Q1 state else valid_idle\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?Q1 state\<rbrace> do state <- get_thread_state obj_id';
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc state obj_id' | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc state obj_id' | BlockedOnReply \<Rightarrow> reply_cancel_ipc obj_id' | BlockedOnNotification event \<Rightarrow> cancel_signal obj_id' event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>y s. valid_idle s \<and> obj_id' \<noteq> idle_thread s\<rbrace>
 2. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then ?Q1 state else valid_idle\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?Q1 state\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>statea s. (statea = Running \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (inactive statea \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (statea = Restart \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. statea = BlockedOnReceive x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) statea) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. statea = BlockedOnSend x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) statea) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (awaiting_reply statea \<longrightarrow> (not_idle_thread obj_id' and invs) s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x. statea = BlockedOnNotification x \<longrightarrow> (not_idle_thread obj_id' and valid_idle) s \<and> obj_id' \<noteq> idle_thread s) \<and> (idle statea \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s)\<rbrace>
 2. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then ?Q1 state else valid_idle\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>state. \<not> runnable state \<and> state \<noteq> IdleThreadState \<Longrightarrow> \<lbrace>?Q1 state\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>r. st_tcb_at ((=) r) obj_id' and not_idle_thread obj_id' and invs\<rbrace>
 2. \<And>state rv s. \<lbrakk>\<not> runnable state \<and> state \<noteq> IdleThreadState; (st_tcb_at ((=) rv) obj_id' and not_idle_thread obj_id' and invs) s\<rbrakk> \<Longrightarrow> (rv = Running \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (inactive rv \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (rv = Restart \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) rv) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) rv) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (awaiting_reply rv \<longrightarrow> (not_idle_thread obj_id' and invs) s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x. rv = BlockedOnNotification x \<longrightarrow> (not_idle_thread obj_id' and valid_idle) s \<and> obj_id' \<noteq> idle_thread s) \<and> (idle rv \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s)
 3. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then ?Q1 state else valid_idle\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state rv s. \<lbrakk>\<not> runnable state \<and> state \<noteq> IdleThreadState; (st_tcb_at ((=) rv) obj_id' and not_idle_thread obj_id' and invs) s\<rbrakk> \<Longrightarrow> (rv = Running \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (inactive rv \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (rv = Restart \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. rv = BlockedOnReceive x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) rv) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x xa. rv = BlockedOnSend x xa \<longrightarrow> (valid_idle and not_idle_thread obj_id' and valid_objs and st_tcb_at ((=) rv) obj_id') s \<and> obj_id' \<noteq> idle_thread s) \<and> (awaiting_reply rv \<longrightarrow> (not_idle_thread obj_id' and invs) s \<and> obj_id' \<noteq> idle_thread s) \<and> (\<forall>x. rv = BlockedOnNotification x \<longrightarrow> (not_idle_thread obj_id' and valid_idle) s \<and> obj_id' \<noteq> idle_thread s) \<and> (idle rv \<longrightarrow> valid_idle s \<and> obj_id' \<noteq> idle_thread s)
 2. \<lbrace>invs and not_idle_thread obj_id'\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. not_idle_thread obj_id' s \<and> invs s else valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. obj_id' \<noteq> idle_thread s)\<rbrace> get_thread_state obj_id' \<lbrace>\<lambda>state. if \<not> runnable state \<and> state \<noteq> IdleThreadState then \<lambda>s. obj_id' \<noteq> idle_thread s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s else valid_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and (\<lambda>s. obj_id' \<noteq> idle_thread s)) s \<Longrightarrow> (if \<not> runnable rv \<and> rv \<noteq> IdleThreadState then \<lambda>s. obj_id' \<noteq> idle_thread s \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s else valid_idle) s proof (prove)
goal:
No subgoals!