theory Tcb_IF

lemma invoke_tcb_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes validE_valid[wp del] hoare_weak_lift_imp [wp]
  shows
    "reads_respects_f aag l
       (silc_inv aag st and only_timer_irq_inv irq st' and einvs
                        and simple_sched_action and pas_refined aag and pas_cur_domain aag
                        and tcb_inv_wf ti and is_subject aag \<circ> cur_thread
                        and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti))
       (invoke_tcb ti)" including no_pre apply (case_tac ti)
         \<comment> \<open>WriteRegisters\<close> apply (strengthen invs_mdb
                | wpsimp wp: when_ev restart_reads_respects_f reschedule_required_reads_respects_f
                             as_user_reads_respects_f restart_silc_inv restart_pas_refined hoare_vcg_if_lift)+ apply (rule hoare_strengthen_post[where Q="\<lambda>_ s. \<forall>rv. R rv s" and R=R for R, rotated]) apply (rename_tac rv s) apply (erule_tac x=rv in allE, assumption) apply wpsimp+ apply (solves \<open>auto intro!: det_zipWithM
                               simp: det_setRegister det_getRestartPC det_setNextPC
                                     authorised_tcb_inv_def reads_equiv_f_def\<close>) apply (wp as_user_reads_respects_f suspend_silc_inv when_ev  suspend_reads_respects_f
               | simp | elim conjE, assumption)+ apply (solves \<open>auto simp: authorised_tcb_inv_def  det_getRegister reads_equiv_f_def
                          intro!: det_mapM[OF _ subset_refl]\<close>) apply (wp when_ev mapM_x_ev'' reschedule_required_reads_respects_f[where st=st]
                 as_user_reads_respects_f[where st=st] hoare_vcg_ball_lift
                 restart_reads_respects_f restart_silc_inv hoare_vcg_if_lift
                 suspend_reads_respects_f suspend_silc_inv hoare_drop_imp
                 restart_silc_inv restart_pas_refined
              | simp split del: if_split add: det_setRegister det_setNextPC
              | strengthen invs_mdb
              | (rule hoare_strengthen_post[where Q="\<lambda>_. silc_inv aag st and pas_refined aag
                                                                         and pspace_aligned
                                                                         and valid_vspace_objs
                                                                         and valid_arch_state",
                                            OF mapM_x_wp', rotated], fastforce)
              | wp mapM_x_wp')+ apply (solves \<open>auto simp: authorised_tcb_inv_def det_getRestartPC det_getRegister
                                 idle_no_ex_cap[OF invs_valid_global_refs invs_valid_objs]\<close>) defer apply ((wp suspend_reads_respects_f[where st=st] restart_reads_respects_f[where st=st]
              | simp add: authorised_tcb_inv_def )+)[2]
    \<comment> \<open>NotificationControl\<close> apply (rename_tac option) apply (case_tac option, simp_all)[1] apply ((wp unbind_notification_is_subj_reads_respects
                unbind_notification_silc_inv bind_notification_reads_respects
             | clarsimp simp: authorised_tcb_inv_def
             | rule_tac Q=\<top> and st=st in reads_respects_f)+)[2]
   \<comment> \<open>SetTLSBase\<close> apply (rename_tac tcb tls_base) apply (wpsimp wp: when_ev reschedule_required_reads_respects_f
                     as_user_reads_respects_f hoare_drop_imps)+ apply (auto simp: det_setRegister authorised_tcb_inv_def)[1]
  \<comment> \<open>ThreadControl\<close> apply (fastforce intro: tc_reads_respects_f[OF assms]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (11 subgoals):
 1. \<And>x11 x12 x13 x14 rv. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P'203 x11 x12 x13 x14 rv\<rbrace> arch_get_sanitise_register_info x11 \<lbrace>\<lambda>rva s. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrace>
 2. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> reads_respects_f aag l (?P'3 x11 x12 x13 x14) (gets cur_thread)
 3. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P''3 x11 x12 x13 x14\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. True \<and> silc_inv aag (?st205 x11 x12 x13 x14 rv) s \<and> ?P'203 x11 x12 x13 x14 rv s\<rbrace>
 4. \<And>x11 x12 x13 x14 s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x11 and ex_nonz_cap_to x11) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14) \<and> authorised_tcb_inv_extra aag (WriteRegisters x11 x12 x13 x14))) s\<rbrakk> \<Longrightarrow> ?P'3 x11 x12 x13 x14 s \<and> ?P''3 x11 x12 x13 x14 s
 5. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 9. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 10. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x11 x12 x13 x14 rv rva s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; \<forall>rva. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrakk> \<Longrightarrow> det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))
 2. \<And>x11 x12 x13 x14 rv. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P'203 x11 x12 x13 x14 rv\<rbrace> arch_get_sanitise_register_info x11 \<lbrace>\<lambda>_ s. \<forall>rva. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrace>
 3. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> reads_respects_f aag l (?P'3 x11 x12 x13 x14) (gets cur_thread)
 4. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P''3 x11 x12 x13 x14\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. True \<and> silc_inv aag (?st205 x11 x12 x13 x14 rv) s \<and> ?P'203 x11 x12 x13 x14 rv s\<rbrace>
 5. \<And>x11 x12 x13 x14 s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x11 and ex_nonz_cap_to x11) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14) \<and> authorised_tcb_inv_extra aag (WriteRegisters x11 x12 x13 x14))) s\<rbrakk> \<Longrightarrow> ?P'3 x11 x12 x13 x14 s \<and> ?P''3 x11 x12 x13 x14 s
 6. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 9. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 10. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>x11 x12 x13 x14 rva rv s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; \<forall>rv. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rv r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rva rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rva \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rva (ds_id True) x13 x14 rva rv) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rva \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rva s \<and> is_subject aag rva) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rva (ds_id False) x13 x14 rva rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrakk> \<Longrightarrow> det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rv r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rva rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rva \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rva (ds_id True) x13 x14 rva rv) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rva \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rva s \<and> is_subject aag rva) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rva (ds_id False) x13 x14 rva rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))
 2. \<And>x11 x12 x13 x14 rv. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P'203 x11 x12 x13 x14 rv\<rbrace> arch_get_sanitise_register_info x11 \<lbrace>\<lambda>_ s. \<forall>rva. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrace>
 3. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> reads_respects_f aag l (?P'3 x11 x12 x13 x14) (gets cur_thread)
 4. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P''3 x11 x12 x13 x14\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. True \<and> silc_inv aag (?st205 x11 x12 x13 x14 rv) s \<and> ?P'203 x11 x12 x13 x14 rv s\<rbrace>
 5. \<And>x11 x12 x13 x14 s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x11 and ex_nonz_cap_to x11) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14) \<and> authorised_tcb_inv_extra aag (WriteRegisters x11 x12 x13 x14))) s\<rbrakk> \<Longrightarrow> ?P'3 x11 x12 x13 x14 s \<and> ?P''3 x11 x12 x13 x14 s
 6. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 9. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 10. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x11 x12 x13 x14 rv. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P'203 x11 x12 x13 x14 rv\<rbrace> arch_get_sanitise_register_info x11 \<lbrace>\<lambda>_ s. \<forall>rva. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rva r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x11 s \<and> is_subject aag (cur_thread s) \<and> is_subject aag x11) \<and> (x11 = rv \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id True) x13 x14 rv rva) s \<and> invs s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> is_subject aag rv \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s \<and> invs s \<and> tcb_at rv s \<and> is_subject aag rv) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 rv (ds_id False) x13 x14 rv rva) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> pas_refined aag s))\<rbrace>
 2. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> reads_respects_f aag l (?P'3 x11 x12 x13 x14) (gets cur_thread)
 3. \<And>x11 x12 x13 x14. ti = WriteRegisters x11 x12 x13 x14 \<Longrightarrow> \<lbrace>?P''3 x11 x12 x13 x14\<rbrace> gets cur_thread \<lbrace>\<lambda>rv s. True \<and> silc_inv aag (?st205 x11 x12 x13 x14 rv) s \<and> ?P'203 x11 x12 x13 x14 rv s\<rbrace>
 4. \<And>x11 x12 x13 x14 s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x11 and ex_nonz_cap_to x11) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14) \<and> authorised_tcb_inv_extra aag (WriteRegisters x11 x12 x13 x14))) s\<rbrakk> \<Longrightarrow> ?P'3 x11 x12 x13 x14 s \<and> ?P''3 x11 x12 x13 x14 s
 5. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 9. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 10. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
A total of 11 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 s. \<lbrakk>ti = WriteRegisters x11 x12 x13 x14; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; pas_cur_domain aag s; tcb_at x11 s; ex_nonz_cap_to x11 s; is_subject aag (cur_thread s); authorised_tcb_inv aag (WriteRegisters x11 x12 x13 x14); authorised_tcb_inv_extra aag (WriteRegisters x11 x12 x13 x14)\<rbrakk> \<Longrightarrow> silc_inv aag (?st234 x11 x12 x13 x14) s \<and> silc_inv aag (?st205 x11 x12 x13 x14 (cur_thread s)) s \<and> (\<forall>rv. det (do y <- zipWithM (\<lambda>r v. setRegister r (sanitise_register rv r v)) (frameRegisters @ gpRegisters) x13;
getRestartPC >>= setNextPC
od) \<and> is_subject aag x11 \<and> (x12 \<longrightarrow> silc_inv aag (?st129 x11 (ds_id True) x13 x14 (cur_thread s) rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag x11) \<and> (x11 = cur_thread s \<longrightarrow> (x12 \<longrightarrow> silc_inv aag (?st159 (cur_thread s) (ds_id True) x13 x14 (cur_thread s) rv) 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> tcb_at (cur_thread s) s) \<and> (\<not> x12 \<longrightarrow> silc_inv aag (?st159 (cur_thread s) (ds_id False) x13 x14 (cur_thread s) rv) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)))
 2. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 8. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24. ti = ReadRegisters x21 x22 x23 x24 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (7 subgoals):
 1. \<And>x21 x22 x23 x24 s. \<lbrakk>ti = ReadRegisters x21 x22 x23 x24; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> tcb_at x21 s \<and> ex_nonz_cap_to x21 s \<and> is_subject aag (cur_thread s) \<and> authorised_tcb_inv aag (ReadRegisters x21 x22 x23 x24) \<and> authorised_tcb_inv_extra aag (ReadRegisters x21 x22 x23 x24)\<rbrakk> \<Longrightarrow> (x22 \<longrightarrow> silc_inv aag (?st318 x21 True x23 x24) s \<and> is_subject aag x21 \<and> silc_inv aag (?st322 x21 True x23 x24) s \<and> valid_mdb s \<and> is_subject aag x21 \<and> silc_inv aag (?st331 x21 True x23 x24) s \<and> valid_mdb s \<and> is_subject aag x21 \<and> det (mapM getRegister (take (unat x23) frame_registers @ take (unat x23 - length frame_registers) gp_registers)) \<and> is_subject aag x21) \<and> (\<not> x22 \<longrightarrow> silc_inv aag (?st322 x21 False x23 x24) s \<and> silc_inv aag (?st331 x21 False x23 x24) s \<and> det (mapM getRegister (take (unat x23) frame_registers @ take (unat x23 - length frame_registers) gp_registers)) \<and> is_subject aag x21)
 2. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 7. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37. ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (6 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36 x37 s. \<lbrakk>ti = CopyRegisters x31 x32 x33 x34 x35 x36 x37; silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> tcb_at x31 s \<and> tcb_at x32 s \<and> ex_nonz_cap_to x32 s \<and> ex_nonz_cap_to x31 s \<and> is_subject aag (cur_thread s) \<and> authorised_tcb_inv aag (CopyRegisters x31 x32 x33 x34 x35 x36 x37) \<and> authorised_tcb_inv_extra aag (CopyRegisters x31 x32 x33 x34 x35 x36 x37)\<rbrakk> \<Longrightarrow> (x33 \<longrightarrow> silc_inv aag (?st887 x31 x32 True x34 x35 x36 x37) s \<and> is_subject aag x32) \<and> (if x33 then \<lambda>s. (silc_inv aag (?st907 x31 x32 x33 x34 x35 x36 x37) and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> pas_cur_domain aag s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> tcb_at x31 s \<and> is_subject aag (cur_thread s) \<and> K (is_subject aag x31) s else (\<lambda>s. silc_inv aag (?st907 x31 x32 x33 x34 x35 x36 x37) s \<and> pas_refined aag s \<and> pas_cur_domain aag s \<and> invs s \<and> tcb_at x31 s \<and> is_subject aag (cur_thread s) \<and> K (is_subject aag x31) s)) s \<and> (\<forall>x\<in>set frame_registers. (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> det (getRegister x) \<and> is_subject aag x32 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x31))) s \<and> is_subject aag x31)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> silc_inv aag st s \<and> is_subject aag x31)) s) \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> det getRestartPC \<and> is_subject aag x31 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> det getRestartPC \<and> is_subject aag x31 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x31))) s \<and> is_subject aag x31)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> det getRestartPC \<and> is_subject aag x31 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> det getRestartPC \<and> is_subject aag x31 \<and> silc_inv aag st s \<and> is_subject aag x31)) s \<and> (\<forall>x\<in>set gpRegisters. (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> det (getRegister x) \<and> is_subject aag x32 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> det (getRegister x) \<and> is_subject aag x32 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x31))) s \<and> is_subject aag x31)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> det (getRegister x) \<and> is_subject aag x32 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> det (getRegister x) \<and> is_subject aag x32 \<and> silc_inv aag st s \<and> is_subject aag x31)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> det (getRegister x) \<and> is_subject aag x32 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x31))) s \<and> is_subject aag x31)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (det (getRegister x) \<and> is_subject aag x32) \<and> silc_inv aag st s \<and> is_subject aag x31)) s) \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> tcb_at x31 s \<and> is_subject aag x31 \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> (pas_refined aag and invs and tcb_at x31 and K (is_subject aag x31)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> tcb_at x31 s \<and> is_subject aag x31 \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> (pas_refined aag and invs and tcb_at x31 and K (is_subject aag x31)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> tcb_at x31 s \<and> is_subject aag x31 \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> (pas_refined aag and invs and tcb_at x31 and K (is_subject aag x31)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s else (\<lambda>s. silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> is_subject aag x31 \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> (invs and tcb_at x32 and (\<lambda>s. x32 \<noteq> idle_thread s)) s \<and> tcb_at x31 s \<and> is_subject aag x31 else (\<lambda>s. silc_inv aag st s \<and> (valid_mdb and pas_refined aag and K (is_subject aag x31)) s \<and> True \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x31))) s \<and> (pas_refined aag and invs and tcb_at x31 and K (is_subject aag x31)) s \<and> True)) s \<and> (if x33 then \<lambda>s. (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> True \<and> (silc_inv aag st and (valid_mdb and pas_refined aag and K (is_subject aag x32))) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state and invs and tcb_at x32 and K (is_subject aag x32))) s \<and> True else (\<lambda>s. silc_inv aag st s \<and> True \<and> (silc_inv aag st s \<and> pas_refined aag s) \<and> True)) s
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 6. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (5 subgoals):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (5 subgoals):
 1. \<And>x5. ti = Suspend x5 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x6. ti = Resume x6 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 5. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (3 subgoals):
 1. \<And>x71 x72. ti = NotificationControl x71 x72 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (3 subgoals):
 1. \<And>x71 option. ti = NotificationControl x71 option \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 3. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (4 subgoals):
 1. \<And>x71 option. \<lbrakk>ti = NotificationControl x71 None; option = None\<rbrakk> \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x71 and ex_nonz_cap_to x71) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (NotificationControl x71 None) \<and> authorised_tcb_inv_extra aag (NotificationControl x71 None))) (liftE (do y <- unbind_notification x71;
return []
od))
 2. \<And>x71 option a. \<lbrakk>ti = NotificationControl x71 (Some a); option = Some a\<rbrakk> \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and (tcb_at x71 and ex_nonz_cap_to x71 and (obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) a and ex_nonz_cap_to a and bound_tcb_at ((=) None) x71)) and is_subject aag \<circ> cur_thread and (\<lambda>y. authorised_tcb_inv aag (NotificationControl x71 (Some a)) \<and> authorised_tcb_inv_extra aag (NotificationControl x71 (Some a)))) (liftE (do y <- bind_notification x71 a;
return []
od))
 3. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 4. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (2 subgoals):
 1. \<And>x81 x82. ti = SetTLSBase x81 x82 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (2 subgoals):
 1. \<And>tcb tls_base. ti = SetTLSBase tcb tls_base \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (2 subgoals):
 1. \<And>tcb tls_base s. \<lbrakk>ti = SetTLSBase tcb tls_base; silc_inv aag st s; only_timer_irq_inv irq st' s; invs s; valid_list s; valid_sched s; simple_sched_action s; pas_refined aag s; pas_cur_domain aag s; tcb_at tcb s; ex_nonz_cap_to tcb s; is_subject aag (cur_thread s); authorised_tcb_inv aag (SetTLSBase tcb tls_base); authorised_tcb_inv_extra aag (SetTLSBase tcb tls_base)\<rbrakk> \<Longrightarrow> silc_inv aag (?st2156 tcb tls_base) s \<and> det (setRegister tlsBaseRegister tls_base) \<and> is_subject aag tcb \<and> silc_inv aag (?st2159 tcb tls_base) s \<and> silc_inv aag (?st2166 tcb tls_base) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s
 2. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44 x45 x46 x47 x48. ti = ThreadControl x41 x42 x43 x44 x45 x46 x47 x48 \<Longrightarrow> reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and einvs and simple_sched_action and pas_refined aag and pas_cur_domain aag and tcb_inv_wf ti and is_subject aag \<circ> cur_thread and K (authorised_tcb_inv aag ti \<and> authorised_tcb_inv_extra aag ti)) (invoke_tcb ti) proof (prove)
goal:
No subgoals!