theory Tcb_AI

lemma (in Tcb_AI_1) activate_invs:
  "\<lbrace>(invs::'state_ext::state_ext state \<Rightarrow> bool)\<rbrace> activate_thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>" apply (unfold activate_thread_def) apply (rule hoare_seq_ext [OF _ gets_sp]) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (case_tac state, simp_all) apply wp apply (clarsimp elim!: pred_tcb_weakenE
                     simp: ct_in_state_def) apply (rule_tac Q="\<lambda>rv. invs and ct_running" in hoare_post_imp, simp) apply (rule hoare_pre) apply (wp sts_invs_minor ct_in_state_set) apply simp apply (simp | strengthen reply_cap_doesnt_exist_strg)+ apply (wp as_user_ct hoare_post_imp [OF disjI1]
          | assumption
          | clarsimp elim!: st_tcb_weakenE)+ apply (auto simp: invs_def valid_state_def
                         valid_idle_def valid_pspace_def
               elim: st_tcb_ex_cap pred_tcb_weakenE,
          auto simp: st_tcb_def2 pred_tcb_at_def obj_at_def)[1] apply (rule_tac Q="\<lambda>rv. invs and ct_idle" in hoare_post_imp, simp) apply (wp activate_idle_invs hoare_post_imp [OF disjI2]) apply (clarsimp simp: ct_in_state_def elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> activate_thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>invs and (\<lambda>s. cur_thread s = thread)\<rbrace> do state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread state. \<lbrace>st_tcb_at ((=) state) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>st_tcb_at ((=) Running) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> return () \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>
 2. \<And>thread. \<lbrace>st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Running
od \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>
 3. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread s. (st_tcb_at ((=) Running) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> invs s \<and> (ct_running s \<or> ct_idle s)
 2. \<And>thread. \<lbrace>st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Running
od \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>
 3. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Running
od \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace>
 2. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<lbrace>st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Running
od \<lbrace>\<lambda>rv. invs and ct_running\<rbrace>
 2. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?Q20 thread\<rbrace> do pc <- as_user thread getRestartPC;
y <- as_user thread (setNextPC pc);
set_thread_state thread Running
od \<lbrace>\<lambda>rv. invs and ct_running\<rbrace>
 2. \<And>thread s. (st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> ?Q20 thread s
 3. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread pc y. Running = Running
 2. \<And>thread pc. \<lbrace>?B25 thread pc\<rbrace> as_user thread (setNextPC pc) \<lbrace>\<lambda>y s. (st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of Running) thread and (\<lambda>s. \<not> halted Running \<longrightarrow> ex_nonz_cap_to thread s) and (\<lambda>s. \<forall>a data. Running = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s) and (\<lambda>s. thread \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted Running \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of Running) and (\<lambda>s. Running \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap thread s) and K (Running \<noteq> IdleThreadState) and invs) s \<and> cur_thread s = thread\<rbrace>
 3. \<And>thread. \<lbrace>?Q20 thread\<rbrace> as_user thread getRestartPC \<lbrace>?B25 thread\<rbrace>
 4. \<And>thread s. (st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> ?Q20 thread s
 5. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread pc. \<lbrace>?B25 thread pc\<rbrace> as_user thread (setNextPC pc) \<lbrace>\<lambda>y s. (st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of Running) thread and (\<lambda>s. \<not> halted Running \<longrightarrow> ex_nonz_cap_to thread s) and (\<lambda>s. \<forall>a data. Running = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (thread, tcb_cnode_index 3) s) and (\<lambda>s. thread \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> halted Running \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of Running) and (\<lambda>s. Running \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap thread s) and K (Running \<noteq> IdleThreadState) and invs) s \<and> cur_thread s = thread\<rbrace>
 2. \<And>thread. \<lbrace>?Q20 thread\<rbrace> as_user thread getRestartPC \<lbrace>?B25 thread\<rbrace>
 3. \<And>thread s. (st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> ?Q20 thread s
 4. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>thread pc. \<lbrace>?B25 thread pc\<rbrace> as_user thread (setNextPC pc) \<lbrace>\<lambda>r s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) thread s \<and> ex_nonz_cap_to thread s \<and> thread \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) thread s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = thread) (thread, tcb_cnode_index 2) s) \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) thread s \<and> invs s \<and> cur_thread s = thread\<rbrace>
 2. \<And>thread. \<lbrace>?Q20 thread\<rbrace> as_user thread getRestartPC \<lbrace>?B25 thread\<rbrace>
 3. \<And>thread s. (st_tcb_at ((=) Restart) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> ?Q20 thread s
 4. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at ((=) Restart) (cur_thread s) s; invs s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = {}) (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> cur_thread s \<noteq> idle_thread s \<and> st_tcb_at (\<lambda>st. \<not> halted st) (cur_thread s) s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) (cur_thread s) s
 2. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv s. invs s \<and> (ct_running s \<or> ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread. \<lbrace>st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))\<rbrace> arch_activate_idle_thread thread \<lbrace>\<lambda>rv. invs and ct_idle\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>thread s. (st_tcb_at ((=) IdleThreadState) thread and (invs and (\<lambda>s. cur_thread s = thread))) s \<Longrightarrow> (invs and ct_idle) s proof (prove)
goal:
No subgoals!