theory Tcb_IF

lemma restart_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "reads_respects_f aag l (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs
                                             and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))
                                             and K (is_subject aag t)) (restart t)" apply (rule gen_asm_ev | elim conjE)+ apply (simp add: restart_def when_def) apply (wp reads_respects_f[OF set_thread_state_reads_respects, where Q="\<top>"]
            reads_respects_f[OF setup_reply_master_reads_respects setup_reply_master_silc_inv]
            gets_cur_thread_ev set_thread_state_pas_refined setup_reply_master_pas_refined
            reads_respects_f[OF possible_switch_to_reads_respects, where Q="\<top>"]
            reads_respects_f[OF tcb_sched_action_reads_respects, where Q="\<top>"]
            cancel_ipc_reads_respects_f setup_reply_master_silc_inv cancel_ipc_silc_inv
         | simp
         | strengthen invs_mdb)+ apply (simp add: get_thread_state_def thread_get_def) apply wp apply (wp hoare_drop_imps) apply clarsimp apply (rule requiv_get_tcb_eq | rule conjI | assumption | clarsimp simp: reads_equiv_f_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s)) and K (is_subject aag t)) (restart t) proof (prove)
goal (1 subgoal):
 1. is_subject aag t \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) (restart t) proof (prove)
goal (1 subgoal):
 1. is_subject aag t \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) (do state <- get_thread_state t;
if \<not> runnable state \<and> state \<noteq> IdleThreadState then do y <- cancel_ipc t;
y <- setup_reply_master t;
y <- set_thread_state t Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
possible_switch_to t
od else return ()
od) proof (prove)
goal (3 subgoals):
 1. is_subject aag t \<Longrightarrow> reads_respects_f aag l ?P'2 (get_thread_state t)
 2. is_subject aag t \<Longrightarrow> \<lbrace>?P''2\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. (\<not> runnable rv \<and> rv \<noteq> IdleThreadState \<longrightarrow> (silc_inv aag (?st120 rv) and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) s \<and> (silc_inv aag (?st129 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> K (is_subject aag t) s \<and> (silc_inv aag (?st138 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> is_subject aag (cur_thread s) \<and> True \<and> (silc_inv aag (?st149 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (silc_inv aag (?st100 rv ()) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)) \<and> (\<not> (\<not> runnable rv \<and> rv \<noteq> IdleThreadState) \<longrightarrow> True)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag t; (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (3 subgoals):
 1. is_subject aag t \<Longrightarrow> reads_respects_f aag l ?P'2 (do tcb <- gets_the (get_tcb t);
return (tcb_state tcb)
od)
 2. is_subject aag t \<Longrightarrow> \<lbrace>?P''2\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. (\<not> runnable rv \<and> rv \<noteq> IdleThreadState \<longrightarrow> (silc_inv aag (?st120 rv) and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) s \<and> (silc_inv aag (?st129 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> K (is_subject aag t) s \<and> (silc_inv aag (?st138 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> is_subject aag (cur_thread s) \<and> True \<and> (silc_inv aag (?st149 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (silc_inv aag (?st100 rv ()) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)) \<and> (\<not> (\<not> runnable rv \<and> rv \<noteq> IdleThreadState) \<longrightarrow> True)\<rbrace>
 3. \<And>s. \<lbrakk>is_subject aag t; (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> ?P'2 s \<and> ?P''2 s proof (prove)
goal (2 subgoals):
 1. is_subject aag t \<Longrightarrow> \<lbrace>?P''2\<rbrace> get_thread_state t \<lbrace>\<lambda>rv s. (\<not> runnable rv \<and> rv \<noteq> IdleThreadState \<longrightarrow> (silc_inv aag (?st120 rv) and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) s \<and> (silc_inv aag (?st129 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> K (is_subject aag t) s \<and> (silc_inv aag (?st138 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> is_subject aag (cur_thread s) \<and> True \<and> (silc_inv aag (?st149 rv) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (silc_inv aag (?st100 rv ()) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)) \<and> (\<not> (\<not> runnable rv \<and> rv \<noteq> IdleThreadState) \<longrightarrow> True)\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag t; (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> (K (\<forall>s ta. reads_equiv_f aag s ta \<and> affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta) s \<and> (get_tcb t s \<noteq> None \<longrightarrow> True)) \<and> ?P''2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag t; (silc_inv aag st and pas_refined aag and pas_cur_domain aag and invs and tcb_at t and (\<lambda>s. is_subject aag (cur_thread s))) s\<rbrakk> \<Longrightarrow> (K (\<forall>s ta. reads_equiv_f aag s ta \<and> affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta) s \<and> (get_tcb t s \<noteq> None \<longrightarrow> True)) \<and> ((silc_inv aag ?st252 and pas_refined aag and invs and tcb_at t and K (is_subject aag t)) s \<and> (silc_inv aag ?st250 and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> K (is_subject aag t) s \<and> (silc_inv aag ?st248 and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> is_subject aag (cur_thread s) \<and> True \<and> (silc_inv aag ?st246 and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> K (is_subject aag t) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> (silc_inv aag (?st245 ()) and valid_mdb and pas_refined aag and K (is_subject aag t)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at t and K (is_subject aag t))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_cur_domain aag s \<and> is_subject aag (cur_thread s)) \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag t; silc_inv aag st s; pas_refined aag s; pas_cur_domain aag s; invs s; tcb_at t s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> (\<forall>s ta. reads_equiv_f aag s ta \<and> affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta) \<and> silc_inv aag ?st252 s \<and> silc_inv aag ?st250 s \<and> valid_mdb s \<and> silc_inv aag ?st248 s \<and> valid_mdb s \<and> silc_inv aag ?st246 s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> silc_inv aag (?st245 ()) s \<and> valid_mdb s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!