theory Orphanage

lemma setPriority_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<rbrace>
   setPriority tptr prio
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding setPriority_def apply wpsimp apply (rule_tac Q="\<lambda>rv s. almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) apply clarsimp apply (clarsimp simp: is_active_tcb_ptr_runnable' pred_tcb_at'_def obj_at'_def
                           almost_no_orphans_no_orphans elim!: almost_no_orphans_no_orphans') apply (wp threadSet_almost_no_orphans threadSet_valid_queues' | clarsimp simp: inQ_def)+ apply (wpsimp wp: threadSet_weak_sch_act_wf) apply (wp tcbSchedDequeue_almost_no_orphans| clarsimp)+ apply (rule_tac Q="\<lambda>rv. obj_at' (Not \<circ> tcbQueued) tptr and invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp simp: obj_at'_def inQ_def) apply (wp tcbSchedDequeue_not_queued | clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s\<rbrace> setPriority tptr prio \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s\<rbrace> do tcbSchedDequeue tptr;
threadSet (tcbPriority_update (\<lambda>_. prio)) tptr;
runnable <- isRunnable tptr;
when runnable $ do curThread <- getCurThread;
if tptr = curThread then rescheduleRequired else possibleSwitchTo tptr
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B2 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. prio)) tptr \<lbrace>\<lambda>xa s. (st_tcb_at' runnable' tptr s \<longrightarrow> (tptr = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (tptr \<noteq> ksCurThread s \<longrightarrow> almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> st_tcb_at' runnable' tptr s \<longrightarrow> no_orphans s)\<rbrace>
 2. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>?B2\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>rv s. almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> (st_tcb_at' runnable' tptr s \<longrightarrow> (tptr = ksCurThread s \<longrightarrow> no_orphans s \<and> valid_queues' s) \<and> (tptr \<noteq> ksCurThread s \<longrightarrow> almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s)) \<and> (\<not> st_tcb_at' runnable' tptr s \<longrightarrow> no_orphans s)
 2. \<lbrace>?B2 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. prio)) tptr \<lbrace>\<lambda>rv s. almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>?B2\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>almost_no_orphans tptr s; valid_queues' s; weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> (st_tcb_at' runnable' tptr s \<longrightarrow> tptr = ksCurThread s \<longrightarrow> no_orphans s) \<and> (\<not> st_tcb_at' runnable' tptr s \<longrightarrow> no_orphans s)
 2. \<lbrace>?B2 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. prio)) tptr \<lbrace>\<lambda>rv s. almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>?B2\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B2 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. prio)) tptr \<lbrace>\<lambda>rv s. almost_no_orphans tptr s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>?B2\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'55 ()\<rbrace> threadSet (tcbPriority_update (\<lambda>_. prio)) tptr \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>a b. almost_no_orphans tptr b \<and> ((\<forall>ko qdom prioa. ko_at' ko tptr b \<and> inQ qdom prioa (tcbPriority_update (\<lambda>_. prio) ko) \<and> \<not> inQ qdom prioa ko \<longrightarrow> tptr \<in> set (ksReadyQueues b (qdom, prioa))) \<and> valid_queues' b) \<and> ?P'55 a b\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>a b. almost_no_orphans tptr b \<and> ((\<forall>ko qdom prioa. ko_at' ko tptr b \<and> inQ qdom prioa (tcbPriority_update (\<lambda>_. prio) ko) \<and> \<not> inQ qdom prioa ko \<longrightarrow> tptr \<in> set (ksReadyQueues b (qdom, prioa))) \<and> valid_queues' b) \<and> weak_sch_act_wf (ksSchedulerAction b) b\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'63\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>rv s. (\<forall>ko qdom prioa. ko_at' ko tptr s \<and> inQ qdom prioa (tcbPriority_update (\<lambda>_. prio) ko) \<and> \<not> inQ qdom prioa ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prioa))) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> no_orphans s \<and> ?P'63 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (obj_at' (Not \<circ> tcbQueued) tptr and invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) s \<Longrightarrow> (\<forall>ko qdom prioa. ko_at' ko tptr s \<and> inQ qdom prioa (tcbPriority_update (\<lambda>_. prio) ko) \<and> \<not> inQ qdom prioa ko \<longrightarrow> tptr \<in> set (ksReadyQueues s (qdom, prioa))) \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s
 2. \<lbrace>?P'63\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) tptr and invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> no_orphans s \<and> ?P'63 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'63\<rbrace> tcbSchedDequeue tptr \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) tptr and invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> tcb_at' tptr s \<Longrightarrow> no_orphans s \<and> ?P'63 s proof (prove)
goal:
No subgoals!