theory Tcb_R

lemma restart_corres:
  "corres dc (einvs  and tcb_at t) (invs' and tcb_at' t)
      (Tcb_A.restart t) (ThreadDecls_H.restart t)" apply (simp add: Tcb_A.restart_def Thread_H.restart_def) apply (simp add: isStopped_def2 liftM_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres]) apply (clarsimp simp add: runnable_tsr idle_tsr when_def) apply (rule corres_split_nor[OF cancel_ipc_corres]) apply (rule corres_split_nor[OF setupReplyMaster_corres]) apply (rule corres_split_nor[OF setThreadState_corres]) apply clarsimp apply (rule corres_split[OF tcbSchedEnqueue_corres possibleSwitchTo_corres]) apply (wp set_thread_state_runnable_weak_valid_sched_action sts_st_tcb_at' sts_valid_queues sts_st_tcb'
                    | clarsimp simp: valid_tcb_state'_def)+ apply (rule_tac Q="\<lambda>rv. valid_sched and cur_tcb" in hoare_strengthen_post) apply wp apply (simp add: valid_sched_def valid_sched_action_def) apply (rule_tac Q="\<lambda>rv. invs' and tcb_at' t" in hoare_strengthen_post) apply wp apply (clarsimp simp: invs'_def valid_state'_def sch_act_wf_weak valid_pspace'_def) apply wp+ apply (simp add: valid_sched_def invs_def tcb_at_is_etcb_at) apply (clarsimp simp add: invs'_def valid_state'_def sch_act_wf_weak) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (Tcb_A.restart t) (ThreadDecls_H.restart t) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> Structures_A.thread_state.IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)
od) (do blocked <- isStopped t;
when blocked (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
od) proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and tcb_at t) (invs' and tcb_at' t) (do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> Structures_A.thread_state.IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)
od) (do x <- getThreadState t;
when (\<not> runnable' x \<and> x \<noteq> Structures_H.thread_state.IdleThreadState) (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do state <- get_thread_state t;
when (\<not> runnable state \<and> state \<noteq> Structures_A.thread_state.IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)
od) (do x <- getThreadState t;
when (\<not> runnable' x \<and> x \<noteq> Structures_H.thread_state.IdleThreadState) (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
od)
 2. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>state x. thread_state_relation state x \<Longrightarrow> corres dc (?R4 state) (?R'4 x) (when (\<not> runnable state \<and> state \<noteq> Structures_A.thread_state.IdleThreadState) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od)) (when (\<not> runnable' x \<and> x \<noteq> Structures_H.thread_state.IdleThreadState) (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od))
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> corres dc (?R4 state) (?R'4 x) (do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od) (do y <- cancelIPC t;
y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> corres dc (?R17 state x) (?R'17 state x) (do y <- setup_reply_master t;
y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od) (do y <- setupReplyMaster t;
y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>xa. ?R17 state x\<rbrace>
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>xa. ?R'17 state x\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and ?Q20 state\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> corres dc (?R26 state x) (?R'26 state x) (do y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od) (do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 state x\<rbrace> setup_reply_master t \<lbrace>\<lambda>xa. ?R26 state x\<rbrace>
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 state x\<rbrace> setupReplyMaster t \<lbrace>\<lambda>xa. ?R'26 state x\<rbrace>
 4. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>xa. einvs and tcb_at t and ?Q26 state x\<rbrace>
 5. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>xa. invs' and tcb_at' t and ?Q'26 state x\<rbrace>
 6. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and ?Q20 state\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 8. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 9. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (12 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> thread_state_relation Structures_A.thread_state.Restart Structures_H.thread_state.Restart
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> corres dc (?R31 state x) (?R'31 state x) (do y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od) (do y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 state x\<rbrace> set_thread_state t Structures_A.thread_state.Restart \<lbrace>\<lambda>xa. ?R31 state x\<rbrace>
 4. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 state x\<rbrace> setThreadState Structures_H.thread_state.Restart t \<lbrace>\<lambda>xa. ?R'31 state x\<rbrace>
 5. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 state x\<rbrace> setup_reply_master t \<lbrace>\<lambda>xa. tcb_at t and ?Q31 state x\<rbrace>
 6. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 state x\<rbrace> setupReplyMaster t \<lbrace>\<lambda>xa. tcb_at' t and ?Q'31 state x\<rbrace>
 7. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>xa. einvs and tcb_at t and ?Q26 state x\<rbrace>
 8. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>xa. invs' and tcb_at' t and ?Q'26 state x\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and ?Q20 state\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> corres dc (?R31 state x) (?R'31 state x) (do y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od) (do y <- tcbSchedEnqueue t;
possibleSwitchTo t
od)
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 state x\<rbrace> set_thread_state t Structures_A.thread_state.Restart \<lbrace>\<lambda>xa. ?R31 state x\<rbrace>
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 state x\<rbrace> setThreadState Structures_H.thread_state.Restart t \<lbrace>\<lambda>xa. ?R'31 state x\<rbrace>
 4. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 state x\<rbrace> setup_reply_master t \<lbrace>\<lambda>xa. tcb_at t and ?Q31 state x\<rbrace>
 5. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 state x\<rbrace> setupReplyMaster t \<lbrace>\<lambda>xa. tcb_at' t and ?Q'31 state x\<rbrace>
 6. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>xa. einvs and tcb_at t and ?Q26 state x\<rbrace>
 7. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>xa. invs' and tcb_at' t and ?Q'26 state x\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and ?Q20 state\<rbrace>
 9. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 10. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q37 state x\<rbrace> tcb_sched_action tcb_sched_enqueue t \<lbrace>\<lambda>y. valid_etcbs and weak_valid_sched_action and cur_tcb and st_tcb_at runnable t\<rbrace>
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'37 state x\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and cur_tcb' and tcb_at' t and st_tcb_at' runnable' t and valid_objs'\<rbrace>
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 state x\<rbrace> set_thread_state t Structures_A.thread_state.Restart \<lbrace>\<lambda>xa. is_etcb_at t and ?Q37 state x\<rbrace>
 4. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 state x\<rbrace> setThreadState Structures_H.thread_state.Restart t \<lbrace>\<lambda>xa. tcb_at' t and Invariants_H.valid_queues and valid_queues' and ?Q'37 state x\<rbrace>
 5. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q26 state x\<rbrace> setup_reply_master t \<lbrace>\<lambda>xa. tcb_at t and ?Q31 state x\<rbrace>
 6. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'26 state x\<rbrace> setupReplyMaster t \<lbrace>\<lambda>xa. tcb_at' t and ?Q'31 state x\<rbrace>
 7. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>xa. einvs and tcb_at t and ?Q26 state x\<rbrace>
 8. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>xa. invs' and tcb_at' t and ?Q'26 state x\<rbrace>
 9. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and ?Q20 state\<rbrace>
 10. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
A total of 12 subgoals... proof (prove)
goal (6 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?P'213 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> cur_tcb s\<rbrace>
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> ?P'213 state s)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?P'213 state\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv. valid_sched and cur_tcb\<rbrace>
 2. \<And>state x rv s. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState; (valid_sched and cur_tcb) s\<rbrakk> \<Longrightarrow> weak_valid_sched_action s \<and> cur_tcb s
 3. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> ?P'213 state s)\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 6. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 7. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>state x rv s. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState; (valid_sched and cur_tcb) s\<rbrakk> \<Longrightarrow> weak_valid_sched_action s \<and> cur_tcb s
 2. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)\<rbrace>
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>state x. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> \<lbrace>?Q'22 x\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. invs' and tcb_at' t\<rbrace>
 2. \<And>state x rv s. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)) s
 3. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s)\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and ?Q'22 x\<rbrace>
 5. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 6. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>state x rv s. \<lbrakk>thread_state_relation state x; \<not> runnable state; state \<noteq> Structures_A.thread_state.IdleThreadState; (invs' and tcb_at' t) s\<rbrakk> \<Longrightarrow> (invs' and tcb_at' t and (\<lambda>s. tcb_at' t s \<and> tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> cur_tcb' s \<and> tcb_at' t s \<and> (valid_objs' and pspace_aligned' and pspace_distinct' and tcb_at' t) s)) s
 2. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. (tcb_at' t and invs') s \<and> tcb_at' t s)\<rbrace>
 4. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 5. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_thread_state t \<lbrace>\<lambda>state. einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> getThreadState t \<lbrace>\<lambda>x. invs' and tcb_at' t and (\<lambda>s. (tcb_at' t and invs') s \<and> tcb_at' t s)\<rbrace>
 3. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and ?Q4) s
 4. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (einvs and tcb_at t) s \<Longrightarrow> (tcb_at t and (einvs and tcb_at t and (\<lambda>s. invs s \<and> valid_list s \<and> valid_sched s \<and> tcb_at t s \<and> tcb_at t s \<and> is_etcb_at t s \<and> valid_etcbs s \<and> valid_sched s \<and> cur_tcb s))) s
 2. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (invs' and tcb_at' t and (\<lambda>s. (tcb_at' t and invs') s \<and> tcb_at' t s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and tcb_at' t) s \<Longrightarrow> (tcb_at' t and (invs' and tcb_at' t and (\<lambda>s. (tcb_at' t and invs') s \<and> tcb_at' t s))) s proof (prove)
goal:
No subgoals!