theory Orphanage

lemma setThreadState_almost_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace>
   setThreadState state tcb_ptr
   \<lbrace> \<lambda>rv s. almost_no_orphans tcb_ptr s \<rbrace>" unfolding setThreadState_def apply (wp | clarsimp)+ apply (rule_tac Q="\<lambda>rv s. valid_queues' s \<and> almost_no_orphans tcb_ptr s" in hoare_post_imp) apply clarsimp apply (wp threadSet_valid_queues') apply (unfold no_orphans_disj almost_no_orphans_disj all_queued_tcb_ptrs_def) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift threadSet_pred_tcb_at_state) apply (auto simp: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> setThreadState state tcb_ptr \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> valid_queues' s\<rbrace> do threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr;
runnable <- isRunnable tcb_ptr;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = tcb_ptr \<and> action = ResumeCurrentThread) $ rescheduleRequired
od \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>x s. (\<not> st_tcb_at' runnable' tcb_ptr s \<and> ksCurThread s = tcb_ptr \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> almost_no_orphans tcb_ptr s \<and> valid_queues' s) \<and> ((ksCurThread s = tcb_ptr \<longrightarrow> st_tcb_at' runnable' tcb_ptr s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> almost_no_orphans tcb_ptr s)\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. valid_queues' s \<and> almost_no_orphans tcb_ptr s \<Longrightarrow> (\<not> st_tcb_at' runnable' tcb_ptr s \<and> ksCurThread s = tcb_ptr \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> almost_no_orphans tcb_ptr s \<and> valid_queues' s) \<and> ((ksCurThread s = tcb_ptr \<longrightarrow> st_tcb_at' runnable' tcb_ptr s \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread) \<longrightarrow> almost_no_orphans tcb_ptr s)
 2. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. valid_queues' s \<and> almost_no_orphans tcb_ptr s\<rbrace>
 3. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. valid_queues' s \<and> almost_no_orphans tcb_ptr s\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'27\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv. almost_no_orphans tcb_ptr\<rbrace>
 2. \<And>s. no_orphans s \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> ?P'27 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'27\<rbrace> threadSet (tcbState_update (\<lambda>_. state)) tcb_ptr \<lbrace>\<lambda>rv s. \<forall>ptr. ptr = ksCurThread s \<or> ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT ptr s \<or> st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) ptr s \<or> ptr = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread ptr\<rbrace>
 2. \<And>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> ?P'27 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>tcb_ptr. tcb_ptr = ksCurThread s \<or> tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT tcb_ptr s \<or> st_tcb_at' (\<lambda>state. \<not> is_active_thread_state state) tcb_ptr s \<or> ksSchedulerAction s = SwitchToThread tcb_ptr) \<and> valid_queues' s \<Longrightarrow> ((\<forall>ko qdom prio. ko_at' ko tcb_ptr s \<and> inQ qdom prio (tcbState_update (\<lambda>_. state) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (\<forall>x. x = ksCurThread s \<or> x \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} \<or> \<not> typ_at' TCBT x s \<or> (tcb_at' tcb_ptr s \<longrightarrow> (if x = tcb_ptr then obj_at' (\<lambda>tcb. \<not> is_active_thread_state (itcbState (tcb_to_itcb' (tcbState_update (\<lambda>_. state) tcb)))) tcb_ptr s else st_tcb_at' (\<lambda>thread_state. \<not> is_active_thread_state thread_state) x s)) \<or> x = tcb_ptr \<or> ksSchedulerAction s = SwitchToThread x) proof (prove)
goal:
No subgoals!