theory Schedule_DR

lemma switch_to_thread_same_corres:
  "dcorres dc (\<lambda>s. x = y) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs)
           (Schedule_D.switch_to_thread (Some y)) (Schedule_A.switch_to_thread x)" supply if_cong[cong] 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'="\<lambda>s. idle_thread s \<noteq> x"]) apply (clarsimp simp: transform_def transform_current_thread_def transform_asid_table_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>s. x = y) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (Schedule_D.switch_to_thread (Some y)) (Schedule_A.switch_to_thread x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. x = y) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (Schedule_D.switch_to_thread (Some y)) (Schedule_A.switch_to_thread x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. x = y) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (modify (cdl_current_thread_update (\<lambda>_. Some y))) (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>s. x = y) (invs and (\<lambda>s. idle_thread s \<noteq> x) and valid_etcbs) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some y))
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>s. x = y) (?Q'2 state) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some y))
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 ya. dcorres dc (\<lambda>s. x = y) (?Q'7 state ya) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some y))
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 ya. dcorres dc (?Q12 state ya) (?Q'12 state ya) (do return ?b;
modify (cdl_current_thread_update (\<lambda>_. Some y))
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 ya s. x = y \<Longrightarrow> ?Q12 state ya 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 ya rv yaa. dc rv yaa \<Longrightarrow> dcorres dc (?R16 state ya rv) (?R'16 state ya yaa) (K_bind (modify (cdl_current_thread_update (\<lambda>_. Some y))) 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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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 y))) (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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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 y))) (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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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>?Q21 state s; idle_thread s' \<noteq> x; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (s\<lparr>cdl_current_thread := Some y\<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. ?Q21 state\<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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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'. \<lbrakk>?Q21 state \<lparr>cdl_arch = ARM11, cdl_objects = transform_objects s', cdl_cdt = transform_cdt s', cdl_current_thread = if cur_thread s' \<noteq> idle_thread s' then Some (cur_thread s') else None, cdl_irq_node = interrupt_irq_node s', cdl_asid_table = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s'), cdl_current_domain = cur_domain s'\<rparr>; idle_thread s' \<noteq> x\<rbrakk> \<Longrightarrow> x = y
 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 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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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>ya a. x = y\<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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and ?Q16 state ya) 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 ya s. x = y \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. x = y)) 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!