theory Interrupt_R

lemma timerTick_invs'[wp]:
  "\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: timerTick_def) apply (wpsimp wp: threadSet_invs_trivial threadSet_pred_tcb_no_state
                    rescheduleRequired_all_invs_but_ct_not_inQ
                    tcbSchedAppend_invs_but_ct_not_inQ'
                simp: tcb_cte_cases_def) apply (rule_tac Q="\<lambda>rv. invs'" in hoare_post_imp) apply (clarsimp simp add:invs'_def valid_state'_def) apply (simp add: decDomainTime_def) apply wp apply simp apply wpc apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs
                               rescheduleRequired_all_invs_but_ct_not_inQ
                               hoare_vcg_imp_lift threadSet_ct_idle_or_in_cur_domain'
                          del: tcbSchedAppend_sch_act_wf)+ apply (rule hoare_strengthen_post[OF tcbSchedAppend_invs_but_ct_not_inQ']) apply (wpsimp simp: valid_pspace'_def sch_act_wf_weak)+ apply (wpsimp wp: threadSet_pred_tcb_no_state threadSet_tcbDomain_triv
                             threadSet_valid_objs' threadSet_timeslice_invs)+ apply (wp threadGet_wp) apply (wp gts_wp')+ apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do thread <- getCurThread;
state <- getThreadState thread;
y <- 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 (Suc 0 < numDomains) (do y <- decDomainTime;
domainTime <- getDomainTime;
when (domainTime = 0) rescheduleRequired
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>thread state. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?Q6 thread state ()\<rbrace> decDomainTime \<lbrace>\<lambda>ya s. (ksDomainTime s = 0 \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (ksDomainTime s \<noteq> 0 \<longrightarrow> invs' s)\<rbrace>
 2. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. if Suc 0 < numDomains then ?Q6 thread state y else invs'\<rbrace>
 3. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 4. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (6 subgoals):
 1. \<And>thread state rv s. \<lbrakk>Suc 0 < numDomains; invs' s\<rbrakk> \<Longrightarrow> (ksDomainTime s = 0 \<longrightarrow> valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s) \<and> (ksDomainTime s \<noteq> 0 \<longrightarrow> invs' s)
 2. \<And>thread state. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?Q6 thread state ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. if Suc 0 < numDomains then ?Q6 thread state y else invs'\<rbrace>
 4. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 5. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 6. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>thread state. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?Q6 thread state ()\<rbrace> decDomainTime \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. if Suc 0 < numDomains then ?Q6 thread state y else invs'\<rbrace>
 3. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 4. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (5 subgoals):
 1. \<And>thread state. Suc 0 < numDomains \<Longrightarrow> \<lbrace>?Q6 thread state ()\<rbrace> modify (\<lambda>ks. ks\<lparr>ksDomainTime := ksDomainTime ks - 1\<rparr>) \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. if Suc 0 < numDomains then ?Q6 thread state y else invs'\<rbrace>
 3. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 4. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. if Suc 0 < numDomains then \<lambda>a. invs' (a\<lparr>ksDomainTime := ksDomainTime a - 1\<rparr>) else invs'\<rbrace>
 2. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 3. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (4 subgoals):
 1. \<And>thread state. \<lbrace>?B4 thread state\<rbrace> 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 () \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>?B4 thread\<rbrace>
 3. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 4. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (11 subgoals):
 1. \<And>thread state x11 x12. state = Structures_H.thread_state.BlockedOnReceive x11 x12 \<Longrightarrow> \<lbrace>?R86 thread state x11 x12\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>thread state. awaiting_reply' state \<Longrightarrow> \<lbrace>?R83 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>thread state x3. state = Structures_H.thread_state.BlockedOnNotification x3 \<Longrightarrow> \<lbrace>?R82 thread state x3\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>thread state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R80 thread state\<rbrace> 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 \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R86 thread state x xa s) \<and> (awaiting_reply' state \<longrightarrow> ?R83 thread state s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R82 thread state x s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R80 thread state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 10. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>thread state ts ts' x. \<lbrakk>state = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?P'113 thread state ts ts' x\<rbrace> tcbSchedAppend thread \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s\<rbrace>
 2. \<And>thread state ts ts'. \<lbrakk>state = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R107 thread state ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread \<lbrace>\<lambda>x s. valid_pspace' s \<and> ?P'113 thread state ts ts' x s\<rbrace>
 3. \<And>thread state ts. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?B105 thread state ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (invs' and tcb_at' thread) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R107 thread state ts ts' s)\<rbrace>
 4. \<And>thread state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R80 thread state\<rbrace> threadGet tcbTimeSlice thread \<lbrace>?B105 thread state\<rbrace>
 5. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' state \<longrightarrow> invs' s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R80 thread state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 10. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>thread state ts ts' x rv s. \<lbrakk>state = Structures_H.thread_state.Running; \<not> 0 < ts'; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s\<rbrakk> \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s
 2. \<And>thread state ts ts'. \<lbrakk>state = Structures_H.thread_state.Running; \<not> 0 < ts'\<rbrakk> \<Longrightarrow> \<lbrace>?R107 thread state ts ts'\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread \<lbrace>\<lambda>x s. valid_pspace' s \<and> (invs' and st_tcb_at' runnable' thread) s\<rbrace>
 3. \<And>thread state ts. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?B105 thread state ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (invs' and tcb_at' thread) s) \<and> (\<not> 0 < ts' \<longrightarrow> ?R107 thread state ts ts' s)\<rbrace>
 4. \<And>thread state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R80 thread state\<rbrace> threadGet tcbTimeSlice thread \<lbrace>?B105 thread state\<rbrace>
 5. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 9. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' state \<longrightarrow> invs' s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R80 thread state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 10. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread ts. \<lbrace>?P'152 thread (ds_id Structures_H.thread_state.Running) ts (ds_id 0)\<rbrace> threadSet (tcbTimeSlice_update (\<lambda>_. timeSlice)) thread \<lbrace>\<lambda>rv s. invs' s \<and> st_tcb_at' runnable' thread s\<rbrace>
 2. \<And>thread state ts. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?B105 thread state ts\<rbrace> return (ts - 1) \<lbrace>\<lambda>ts' s. (0 < ts' \<longrightarrow> (invs' and tcb_at' thread) s) \<and> (\<not> 0 < ts' \<longrightarrow> valid_pspace' s \<and> ?P'152 thread state ts ts' s)\<rbrace>
 3. \<And>thread state. state = Structures_H.thread_state.Running \<Longrightarrow> \<lbrace>?R80 thread state\<rbrace> threadGet tcbTimeSlice thread \<lbrace>?B105 thread state\<rbrace>
 4. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 7. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 8. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' state \<longrightarrow> invs' s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R80 thread state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 9. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 10. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (8 subgoals):
 1. \<And>thread. \<lbrace>?R80 thread (ds_id Structures_H.thread_state.Running)\<rbrace> threadGet tcbTimeSlice thread \<lbrace>\<lambda>ts a. (Suc 0 < ts \<longrightarrow> invs' a \<and> tcb_at' thread a) \<and> (\<not> Suc 0 < ts \<longrightarrow> valid_pspace' a \<and> invs' a \<and> tcb_at' thread a \<and> st_tcb_at' runnable' thread a)\<rbrace>
 2. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' state \<longrightarrow> invs' s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> ?R80 thread state s) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 7. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 8. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (7 subgoals):
 1. \<And>thread state. state = Structures_H.thread_state.Inactive \<Longrightarrow> \<lbrace>?R79 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 2. \<And>thread state. idle' state \<Longrightarrow> \<lbrace>?R78 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 3. \<And>thread state x71 x72 x73 x74 x75. state = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75 \<Longrightarrow> \<lbrace>?R77 thread state x71 x72 x73 x74 x75\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 4. \<And>thread state. state = Structures_H.thread_state.Restart \<Longrightarrow> \<lbrace>?R71 thread state\<rbrace> return () \<lbrace>\<lambda>y. invs'\<rbrace>
 5. \<And>thread. \<lbrace>?B3 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (\<forall>x xa. state = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' state \<longrightarrow> invs' s) \<and> (\<forall>x. state = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (state = Structures_H.thread_state.Running \<longrightarrow> tcb_at' thread s \<longrightarrow> (\<exists>tcb. ko_at' tcb thread s \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> invs' s \<and> tcb_at' thread s) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> valid_pspace' s \<and> invs' s \<and> tcb_at' thread s \<and> st_tcb_at' runnable' thread s))) \<and> (state = Structures_H.thread_state.Inactive \<longrightarrow> ?R79 thread state s) \<and> (idle' state \<longrightarrow> ?R78 thread state s) \<and> (\<forall>x xa xb xc xd. state = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R77 thread state x xa xb xc xd s) \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> ?R71 thread state s)\<rbrace>
 6. \<lbrace>?Q2\<rbrace> getCurThread \<lbrace>?B3\<rbrace>
 7. \<And>s. invs' s \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> \<forall>st. st_tcb_at' ((=) st) (ksCurThread s) s \<longrightarrow> (\<forall>x xa. st = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> invs' s) \<and> (awaiting_reply' st \<longrightarrow> invs' s) \<and> (\<forall>x. st = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> invs' s) \<and> (st = Structures_H.thread_state.Running \<longrightarrow> tcb_at' (ksCurThread s) s \<longrightarrow> (\<exists>tcb. ko_at' tcb (ksCurThread s) s \<and> (Suc 0 < tcbTimeSlice tcb \<longrightarrow> invs' s \<and> tcb_at' (ksCurThread s) s) \<and> (\<not> Suc 0 < tcbTimeSlice tcb \<longrightarrow> valid_pspace' s \<and> invs' s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s))) \<and> (st = Structures_H.thread_state.Inactive \<longrightarrow> invs' s) \<and> (idle' st \<longrightarrow> invs' s) \<and> (\<forall>x xa xb xc xd. st = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> invs' s) \<and> (st = Structures_H.thread_state.Restart \<longrightarrow> invs' s) proof (prove)
goal:
No subgoals!