theory Orphanage

lemma timerTick_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   timerTick
   \<lbrace> \<lambda>_ s. no_orphans s \<rbrace>" unfolding timerTick_def getDomainTime_def supply if_split[split del] apply (subst threadState_case_if) apply (wpsimp wp: threadSet_no_orphans threadSet_valid_queues'
                    threadSet_valid_queues' tcbSchedAppend_almost_no_orphans
                    threadSet_almost_no_orphans threadSet_no_orphans tcbSchedAppend_sch_act_wf
                    hoare_drop_imp
                simp: if_apply_def2
         | strengthen sch_act_wf_weak)+ apply (rule_tac Q="\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s
                                \<and> sch_act_wf  (ksSchedulerAction s) s" in hoare_post_imp) apply (clarsimp simp: inQ_def) apply (wp hoare_drop_imps | clarsimp)+ apply (auto split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> timerTick \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) $ do decDomainTime;
domainTime <- gets ksDomainTime;
when (domainTime = 0) $ rescheduleRequired
od
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od | _ \<Rightarrow> return ();
when (1 < numDomains) $ do decDomainTime;
domainTime <- gets ksDomainTime;
when (domainTime = 0) $ rescheduleRequired
od
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
if state = Structures_H.thread_state.Running then do ts <- threadGet tcbTimeSlice thread;
ts' <- return (ts - 1);
if 0 < ts' then threadSet (tcbTimeSlice_update (\<lambda>_. ts')) thread else do threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread;
tcbSchedAppend thread;
rescheduleRequired
od
od else return ();
when (1 < numDomains) $ do decDomainTime;
domainTime <- gets ksDomainTime;
when (domainTime = 0) $ rescheduleRequired
od
od \<lbrace>\<lambda>_. no_orphans\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>?P'160 thread (ds_id Structures_H.thread_state.Running)\<rbrace> threadGet tcbTimeSlice thread \<lbrace>\<lambda>rv s. (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. rv - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> no_orphans s \<and> almost_no_orphans thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s \<and> sch_act_wf (ksSchedulerAction s) s \<and> almost_no_orphans thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s\<rbrace>
 2. \<And>thread state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R27 thread state\<rbrace> return () \<lbrace>\<lambda>x. if 1 < numDomains then \<lambda>a. (no_orphans a \<and> valid_queues' a) \<and> no_orphans a else no_orphans\<rbrace>
 3. \<And>thread. \<lbrace>?B2 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> no_orphans s \<and> ?P'160 thread state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R27 thread state s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>?B2\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal (6 subgoals):
 1. \<And>thread rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s \<and> sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. rv - Suc 0) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> no_orphans s \<and> almost_no_orphans thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s \<and> sch_act_wf (ksSchedulerAction s) s \<and> almost_no_orphans thread s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko thread s \<and> inQ qdom prio (tcbTimeSlice_update (\<lambda>_. timeSlice) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> thread \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s \<and> tcb_at' thread s
 2. \<And>thread. \<lbrace>?P'160 thread (ds_id Structures_H.thread_state.Running)\<rbrace> threadGet tcbTimeSlice thread \<lbrace>\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<And>thread state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R27 thread state\<rbrace> return () \<lbrace>\<lambda>x. if 1 < numDomains then \<lambda>a. (no_orphans a \<and> valid_queues' a) \<and> no_orphans a else no_orphans\<rbrace>
 4. \<And>thread. \<lbrace>?B2 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> no_orphans s \<and> ?P'160 thread state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R27 thread state s)\<rbrace>
 5. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>?B2\<rbrace>
 6. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>?P'160 thread (ds_id Structures_H.thread_state.Running)\<rbrace> threadGet tcbTimeSlice thread \<lbrace>\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>thread state. state \<noteq> Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R27 thread state\<rbrace> return () \<lbrace>\<lambda>x. if 1 < numDomains then \<lambda>a. (no_orphans a \<and> valid_queues' a) \<and> no_orphans a else no_orphans\<rbrace>
 3. \<And>thread. \<lbrace>?B2 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Running \<longrightarrow> no_orphans s \<and> ?P'160 thread state s) \<and> (state \<noteq> Structures_H.thread_state.Running \<longrightarrow> ?R27 thread state s)\<rbrace>
 4. \<lbrace>?Q1\<rbrace> getCurThread \<lbrace>?B2\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s\<rbrakk> \<Longrightarrow> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (if Suc 0 < numDomains then \<lambda>a. no_orphans a \<and> valid_queues' a \<and> no_orphans a else no_orphans) s proof (prove)
goal:
No subgoals!