theory Noninterference

lemma kernel_entry_if_integrity:
  "\<lbrace>einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread
          and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag
          and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. integrity (aag :: 'a subject_label PAS) X st\<rbrace>" unfolding kernel_entry_if_def apply wp apply (rule valid_validE) apply (rule_tac Q="\<lambda>_ s. integrity aag X (st\<lparr>kheap :=
                         (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc)
                                                            (the (get_tcb (cur_thread st) st))))\<rparr>) s
                       \<and> is_subject aag (cur_thread s)
                       \<and> cur_thread s = cur_thread st" in hoare_strengthen_post) apply (wp handle_event_integrity handle_event_cur_thread | simp)+ apply (fastforce intro: integrity_update_reference_state) apply (wp thread_set_integrity_autarch thread_set_pas_refined guarded_pas_domain_lift
              thread_set_invs_trivial thread_set_not_state_valid_sched
           | simp add: tcb_cap_cases_def schact_is_rct_def arch_tcb_update_aux2)+ apply (wp (once) prop_of_two_valid[where f="ct_active" and g="cur_thread"]) apply (wp | simp)+ apply (wp thread_set_tcb_context_update_wp)+ apply (clarsimp simp: schact_is_rct_def) apply (rule conjI) apply (erule integrity_update_reference_state[where blah="the (kheap st (cur_thread st))",
                                                 OF _ integrity_refl]) apply simp apply (subgoal_tac "kheap st (cur_thread st) \<noteq> None") apply clarsimp apply (drule tcb_at_invs, clarsimp simp: tcb_at_def get_tcb_def
                                     split: kernel_object.splits option.splits) apply (clarsimp simp: invs_psp_aligned invs_vspace_objs invs_arch_state) apply (rule conjI) apply assumption apply (rule state.equality, simp_all) apply (rule ext, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st\<rbrace> do t <- gets cur_thread;
thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>t x. \<lbrace>?B2 t x\<rbrace> handle_event e \<lbrace>\<lambda>r. integrity aag X st\<rbrace>, \<lbrace>\<lambda>r. integrity aag X st\<rbrace>
 2. \<And>t. \<lbrace>?B1 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B2 t\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>t x. \<lbrace>?B2 t x\<rbrace> handle_event e \<lbrace>\<lambda>r. integrity aag X st\<rbrace>
 2. \<And>t. \<lbrace>?B1 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B2 t\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>t x. \<lbrace>?B2 t x\<rbrace> handle_event e \<lbrace>\<lambda>_ s. integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 2. \<And>t x rv s. integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st \<Longrightarrow> integrity aag X st s
 3. \<And>t. \<lbrace>?B1 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>?B2 t\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 5. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>s. integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st \<Longrightarrow> integrity aag X st s
 2. \<And>t. \<lbrace>?B1 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>x s. (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) (?st'13 t x) and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>)) s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 4. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?B1 t\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t \<lbrace>\<lambda>x s. (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) (?st'13 t x) and einvs and schact_is_rct and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>)) s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>?B1\<rbrace>
 3. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?P'65 t\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv s. (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> = s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>t s. (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and K (is_subject aag t)) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 t ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> ?P'65 t s\<rbrace>
 3. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>t P. \<lbrace>\<lambda>s. P (ct_active s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv s. P (ct_active s)\<rbrace>
 2. \<And>t P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>
 3. \<And>t. \<lbrace>?P'69 t\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv s. (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> = s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 4. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>t s. (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and K (is_subject aag t)) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 t ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<and> ?P'69 t s\<rbrace>
 5. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>t. \<lbrace>?P'84 t\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>rv s. st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> = s \<and> is_subject aag (cur_thread s) \<and> cur_thread s = cur_thread st\<rbrace>
 2. \<lbrace>?Q\<rbrace> gets cur_thread \<lbrace>\<lambda>t s. (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and K (is_subject aag t)) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 t ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> ?P'84 t s\<rbrace>
 3. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (einvs and schact_is_rct and pas_refined aag and is_subject aag \<circ> cur_thread and domain_sep_inv (pasMaySendIrqs aag) st' and guarded_pas_domain aag and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_active s) and (=) st) s \<Longrightarrow> (integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) and K (is_subject aag (cur_thread s))) s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state) s \<and> guarded_pas_domain aag s \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread s) ()) s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> scheduler_action s = resume_cur_thread \<and> (ct_active s \<longrightarrow> is_subject aag (cur_thread s)) \<and> (e \<noteq> Interrupt \<longrightarrow> ct_active s) \<and> st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> = s\<lparr>kheap := (kheap s)(cur_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread s) s))))\<rparr> \<and> is_subject aag (cur_thread (s\<lparr>kheap := (kheap s)(cur_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread s) s))))\<rparr>)) \<and> cur_thread (s\<lparr>kheap := (kheap s)(cur_thread s \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread s) s))))\<rparr>) = cur_thread st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) st \<and> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> integrity aag X (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>) st
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> st = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))), kheap := (kheap (st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr>))(cur_thread st \<mapsto> the (kheap st (cur_thread st)))\<rparr>
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> st = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> the (kheap st (cur_thread st)))\<rparr>
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (3 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st; kheap st (cur_thread st) \<noteq> None\<rbrakk> \<Longrightarrow> st = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> the (kheap st (cur_thread st)))\<rparr>
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> kheap st (cur_thread st) \<noteq> None
 3. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> kheap st (cur_thread st) \<noteq> None
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> pspace_aligned st \<and> valid_vspace_objs st \<and> valid_arch_state st \<and> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st \<and> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> domain_sep_inv (pasMaySendIrqs aag) (?st'34 (cur_thread st) ()) st
 2. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> st\<lparr>kheap := \<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a\<rparr> = st\<lparr>kheap := (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st))))\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs st; valid_list st; valid_sched_2 (ready_queues st) (ekheap st) resume_cur_thread (cur_domain st) (kheap st) (cur_thread st) (idle_thread st); scheduler_action st = resume_cur_thread; pas_refined aag st; is_subject aag (cur_thread st); domain_sep_inv (pasMaySendIrqs aag) st' st; guarded_pas_domain aag st; e \<noteq> Interrupt \<longrightarrow> ct_active st\<rbrakk> \<Longrightarrow> (\<lambda>a. if a = cur_thread st then Some (TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) else kheap st a) = (kheap st)(cur_thread st \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb (cur_thread st) st)))) proof (prove)
goal:
No subgoals!