theory ArchSchedule_AI

lemma stt_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: switch_to_thread_def) apply wp apply (simp add: trans_state_update[symmetric] del: trans_state_update) apply (rule_tac Q="\<lambda>_. invs and tcb_at t'" in hoare_strengthen_post, wp) apply (clarsimp simp: invs_def valid_state_def valid_idle_def
                          valid_irq_node_def valid_machine_state_def) apply (fastforce simp: cur_tcb_def obj_at_def
                     elim: valid_pspace_eqI ifunsafe_pspaceI) apply wp+ apply clarsimp apply (simp add: is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t' state = Some y);
y <- arch_switch_to_thread t';
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue t');
modify (cur_thread_update (\<lambda>_. t'))
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>state y ya s f. invs (trans_state f s\<lparr>cur_thread := t'\<rparr>) = invs (s\<lparr>cur_thread := t'\<rparr>)
 2. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>ya s. invs (s\<lparr>cur_thread := t'\<rparr>)\<rbrace>
 3. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t' state = Some y) \<lbrace>?B2 state\<rbrace>
 4. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state y. \<lbrace>?B2 state y\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>ya s. invs (s\<lparr>cur_thread := t'\<rparr>)\<rbrace>
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t' state = Some y) \<lbrace>?B2 state\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state y rv s. (invs and tcb_at t') s \<Longrightarrow> invs (s\<lparr>cur_thread := t'\<rparr>)
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t' state = Some y) \<lbrace>\<lambda>y s. invs s \<and> tcb_at t' s\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; tcb_at t' s\<rbrakk> \<Longrightarrow> cur_tcb (s\<lparr>cur_thread := t'\<rparr>)
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t' state = Some y) \<lbrace>\<lambda>y s. invs s \<and> tcb_at t' s\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t' state = Some y) \<lbrace>\<lambda>y s. invs s \<and> tcb_at t' s\<rbrace>
 2. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> (\<exists>y. get_tcb t' s = Some y) \<longrightarrow> invs s \<and> tcb_at t' s proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>invs s; get_tcb t' s = Some y\<rbrakk> \<Longrightarrow> is_tcb (TCB y) proof (prove)
goal:
No subgoals!