theory Ipc_AC

lemma send_upd_ctxintegrity:
  "\<lbrakk> direct_send {pasSubject aag} aag ep tcb
     \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb;
     integrity aag X st s; st_tcb_at ((=) Running) thread s;
     get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'\<rbrakk>
     \<Longrightarrow> integrity aag X st
                   (s\<lparr>kheap := (kheap s)
                               (thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>)" apply (clarsimp simp: integrity_def tcb_states_of_state_preserved st_tcb_def2) apply (rule conjI) prefer 2 apply (fastforce dest: get_tcb_ko_atI simp: integrity_asids_kh_upds obj_at_def) apply (drule get_tcb_SomeD)+ apply (drule spec[where x=thread], simp) apply (cases "is_subject aag thread") apply (rule tro_lrefl, solves\<open>simp\<close>) 
  (* slow 5s *)
   by (erule integrity_objE;
      (* eliminate all TCB unrelated cases and simplifies the other *)
      clarsimp;
        (* deal with the orefl case *)
      (solves \<open>simp add:direct_send_def indirect_send_def\<close>
      (* deal with the other case by applying either the reply,
         call or send rules and then the generic rule *)
      | rule tro_trans_spec,
        (rule tro_tcb_reply'[OF refl refl refl] tro_tcb_call[OF refl refl refl]
              tro_tcb_send[OF refl refl refl];
          blast),
        rule tro_trans_spec,
        (rule tro_tcb_generic'[OF refl refl refl]; simp),
        rule tro_orefl, simp, rule tcb.equality; solves simp))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; integrity aag X st s; st_tcb_at ((=) Running) thread s; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>)))
 2. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(thread \<mapsto> TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))\<rparr>)
 2. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; get_tcb thread st = Some tcb; get_tcb thread s = Some tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb')\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (kheap st thread) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb'))\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb')); is_subject aag thread\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>)))
 2. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb')); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb')); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>direct_send {pasSubject aag} aag ep tcb \<or> indirect_send {pasSubject aag} aag (the (tcb_bound_notification tcb)) ep tcb; Running = tcb_state tcb'; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; kheap st thread = Some (TCB tcb); kheap s thread = Some (TCB tcb'); object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB tcb')); pasObjectAbs aag thread \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag thread) (Some (TCB tcb)) (Some (TCB (tcb'\<lparr>tcb_arch := arch_tcb_context_set c' (tcb_arch tcb')\<rparr>)))