theory Schedule_DR

lemma switch_to_thread_corres:
  "dcorres dc \<top> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs)
           (Schedule_D.switch_to_thread (Some x)) (Schedule_A.switch_to_thread x)" apply (clarsimp simp: Schedule_D.switch_to_thread_def Schedule_A.switch_to_thread_def) apply (rule corres_dummy_return_pl) apply (rule corres_symb_exec_r) apply (rule corres_symb_exec_r) apply (rule corres_guard_imp) apply (rule corres_split[OF arch_switch_to_thread_dcorres]) apply simp apply (rule dcorres_rhs_noop_above[OF tcb_sched_action_dcorres]) apply (rule corres_modify [where P=\<top> and P'="\<lambda>s. idle_thread s \<noteq> x"]) apply (clarsimp simp: transform_def) apply (simp add: transform_current_thread_def transform_asid_table_def) apply (wp+)[4] apply simp apply assumption apply (clarsimp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (Schedule_D.switch_to_thread (Some x)) (Schedule_A.switch_to_thread x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (modify (cdl_current_thread_update (\<lambda>_. Some x))) (do state <- get;
y <- assert (\<exists>y. get_tcb x state = Some y);
y <- arch_switch_to_thread x;
y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some x))
od) (do state <- get;
y <- assert (\<exists>y. get_tcb x state = Some y);
y <- arch_switch_to_thread x;
y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od) proof (prove)
goal (4 subgoals):
 1. \<And>state. dcorres dc (\<lambda>_. True) (?Q'2 state) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some x))
od) (do y <- assert (\<exists>y. get_tcb x state = Some y);
y <- arch_switch_to_thread x;
y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od)
 2. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 3. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal (7 subgoals):
 1. \<And>state y. dcorres dc (\<lambda>_. True) (?Q'7 state y) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some x))
od) (do y <- arch_switch_to_thread x;
y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od)
 2. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 3. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 5. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 6. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal (9 subgoals):
 1. \<And>state y. dcorres dc (?Q12 state y) (?Q'12 state y) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some x))
od) (do y <- arch_switch_to_thread x;
y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od)
 2. \<And>state y s. True \<Longrightarrow> ?Q12 state y s
 3. \<And>state y s. ?Q'7 state y s \<Longrightarrow> ?Q'12 state y s
 4. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 5. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 7. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 8. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal (11 subgoals):
 1. \<And>state y rv ya. dc rv ya \<Longrightarrow> dcorres dc (?R16 state y rv) (?R'16 state y ya) (K_bind (modify (cdl_current_thread_update (\<lambda>_. Some x))) rv) (do y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od)
 2. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 3. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 4. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 5. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 6. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 7. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 9. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 10. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>state. dcorres dc (?R16 state () ()) (?R'16 state () ()) (modify (cdl_current_thread_update (\<lambda>_. Some x))) (do y <- tcb_sched_action tcb_sched_dequeue x;
modify (cur_thread_update (\<lambda>_. x))
od)
 2. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 3. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 4. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 5. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 6. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 7. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 9. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 10. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
A total of 11 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>state. dcorres dc (?Q21 state) (?Q'21 state) (modify (cdl_current_thread_update (\<lambda>_. Some x))) (modify (cur_thread_update (\<lambda>_. x)))
 2. \<And>state. \<lbrace>?R16 state () ()\<rbrace> return () \<lbrace>\<lambda>y. ?Q21 state\<rbrace>
 3. \<And>state. \<lbrace>?R'16 state () ()\<rbrace> tcb_sched_action tcb_sched_dequeue x \<lbrace>\<lambda>y. ?Q'21 state\<rbrace>
 4. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 5. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 6. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 7. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 8. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 9. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>state s s'. \<lbrakk>True; idle_thread s' \<noteq> x; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (s\<lparr>cdl_current_thread := Some x\<rparr>, s'\<lparr>cur_thread := x\<rparr>) \<in> {ss'. transform (snd ss') = fst ss'}
 2. \<And>state. \<lbrace>?R16 state () ()\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>state. \<lbrace>?R'16 state () ()\<rbrace> tcb_sched_action tcb_sched_dequeue x \<lbrace>\<lambda>y s. idle_thread s \<noteq> x\<rbrace>
 4. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 5. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 6. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 7. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 8. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 9. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s'. idle_thread s' \<noteq> x \<Longrightarrow> transform_current_thread (s'\<lparr>cur_thread := x\<rparr>) = Some x \<and> transform_asid_table (s'\<lparr>cur_thread := x\<rparr>) = transform_asid_table s'
 2. \<And>state. \<lbrace>?R16 state () ()\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>state. \<lbrace>?R'16 state () ()\<rbrace> tcb_sched_action tcb_sched_dequeue x \<lbrace>\<lambda>y s. idle_thread s \<noteq> x\<rbrace>
 4. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 5. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 6. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 7. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 8. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 9. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state. \<lbrace>?R16 state () ()\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>state. \<lbrace>?R'16 state () ()\<rbrace> tcb_sched_action tcb_sched_dequeue x \<lbrace>\<lambda>y s. idle_thread s \<noteq> x\<rbrace>
 3. \<And>state y. \<lbrace>?Q16 state y\<rbrace> return () \<lbrace>?R16 state y\<rbrace>
 4. \<And>state y. \<lbrace>?Q'16 state y\<rbrace> arch_switch_to_thread x \<lbrace>?R'16 state y\<rbrace>
 5. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state y) s
 6. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and ?Q'16 state y) s
 7. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 8. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 10. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>state y s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 2. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and (\<lambda>s. idle_thread s \<noteq> x)) s
 3. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 4. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 6. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 7. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal (7 subgoals):
 1. \<And>state y s. ?Q'7 state y s \<Longrightarrow> (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and (\<lambda>s. idle_thread s \<noteq> x)) s
 2. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>?Q'7 state\<rbrace>
 3. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 5. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 6. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal (6 subgoals):
 1. \<And>state. \<lbrace>?Q'2 state\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>y. invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs and (\<lambda>s. idle_thread s \<noteq> x)\<rbrace>
 2. \<And>state s. ?Q'2 state s \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>y. get_tcb x state = Some y) \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>state. False \<Longrightarrow> no_fail (?Q'2 state) (assert (\<exists>y. get_tcb x state = Some y))
 4. \<lbrace>invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs\<rbrace> get \<lbrace>?Q'2\<rbrace>
 5. \<And>s. (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) get proof (prove)
goal:
No subgoals!