theory Access_AC

lemma integrity_trans:
  assumes t1: "integrity_subjects subjects aag activate X s s'"
  and     t2: "integrity_subjects subjects aag activate X s' s''"
  shows  "integrity_subjects subjects aag activate X s s''" proof - from t1 have tro1: "integrity_obj_state aag activate subjects s s'" unfolding integrity_subjects_def by simp from t2 have tro2: "integrity_obj_state aag activate subjects s' s''" unfolding integrity_subjects_def by simp have intm: "\<forall>x. integrity_mem aag subjects x
                  (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X
                  (underlying_memory (machine_state s) x)
                  (underlying_memory (machine_state s'') x)" (is "\<forall>x. ?P x s s''") proof fix x from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto from m1 show "?P x s s''" proof cases case trm_lrefl thus ?thesis by (rule integrity_mem.intros) next case trm_globals thus ?thesis by (rule integrity_mem.intros) next case trm_orefl from m2 show ?thesis proof cases case (trm_ipc p') show ?thesis proof (rule integrity_mem.trm_ipc) from trm_ipc show "case_option False can_receive_ipc (tcb_states_of_state s p')" by (fastforce split: option.splits dest: can_receive_ipc_backward [OF tro1]) from trm_ipc show "x \<in> auth_ipc_buffers s p'" by (fastforce split: option.splits intro: auth_ipc_buffers_tro [OF tro1]) qed (simp_all add: trm_ipc) qed (auto simp add: trm_orefl intro: integrity_mem.intros) next case trm_write thus ?thesis by (rule integrity_mem.intros) next case (trm_ipc p') note trm_ipc1 = trm_ipc from m2 show ?thesis proof cases case trm_orefl thus ?thesis using trm_ipc1 by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated]) next case (trm_ipc p'') show ?thesis proof (cases "p' = p''") case True thus ?thesis using trm_ipc trm_ipc1 by (simp add: restrict_map_Some_iff) next 
          (* 2 tcbs sharing same IPC buffer, we can appeal to either t1 or t2 *)
           case False thus ?thesis using trm_ipc1 by (auto intro!: integrity_mem.trm_ipc simp add: restrict_map_Some_iff elim!: tsos_tro_running [OF tro2, rotated]) qed qed (auto simp add: trm_ipc intro: integrity_mem.intros) qed qed moreover have "\<forall>x. integrity_device aag subjects x
                  (tcb_states_of_state s) (tcb_states_of_state s'')
                  (device_state (machine_state s) x)
                  (device_state (machine_state s'') x)" (is "\<forall>x. ?P x s s''") proof fix x from t1 t2 have m1: "?P x s s'" and m2: "?P x s' s''" unfolding integrity_subjects_def by auto from m1 show "?P x s s''" proof cases case trd_lrefl thus ?thesis by (rule integrity_device.intros) next case torel1: trd_orefl from m2 show ?thesis proof cases case (trd_lrefl) thus ?thesis by (rule integrity_device.trd_lrefl) next case trd_orefl thus ?thesis by (simp add: torel1) next case trd_write thus ?thesis by (rule integrity_device.trd_write) qed next case trd_write thus ?thesis by (rule integrity_device.intros) qed qed thus ?thesis using tro_trans[OF tro1 tro2] t1 t2 intm apply (clarsimp simp add: integrity_subjects_def simp del:  split_paired_All) apply (frule(2) trcdt_trans) apply (frule(3) trcdtlist_trans) apply (frule(1) trinterrupts_trans[simplified]) apply (frule(1) trasids_trans[simplified]) apply (frule(1) tre_trans[simplified]) apply (frule(1) trrqs_trans[simplified]) by blast qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (state)
goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (chain)
picking this:
integrity_subjects subjects aag activate X s s' proof (prove)
using this:
integrity_subjects subjects aag activate X s s'

goal (1 subgoal):
 1. integrity_obj_state aag activate subjects s s' proof (prove)
using this:
integrity_obj_state aag activate subjects s s' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag subjects s s' \<and> integrity_cdt_list_state aag subjects s s' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s')

goal (1 subgoal):
 1. integrity_obj_state aag activate subjects s s' proof (state)
this:
integrity_obj_state aag activate subjects s s'

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (chain)
picking this:
integrity_subjects subjects aag activate X s' s'' proof (prove)
using this:
integrity_subjects subjects aag activate X s' s''

goal (1 subgoal):
 1. integrity_obj_state aag activate subjects s' s'' proof (prove)
using this:
integrity_obj_state aag activate subjects s' s'' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s' s'' \<and> integrity_cdt_list_state aag subjects s' s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s' s'')

goal (1 subgoal):
 1. integrity_obj_state aag activate subjects s' s'' proof (state)
this:
integrity_obj_state aag activate subjects s' s''

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (prove)
goal (1 subgoal):
 1. \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. \<And>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. \<And>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (chain)
picking this:
integrity_subjects subjects aag activate X s s'
integrity_subjects subjects aag activate X s' s'' proof (prove)
using this:
integrity_subjects subjects aag activate X s s'
integrity_subjects subjects aag activate X s' s''

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x) &&& integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
integrity_obj_state aag activate subjects s s' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag subjects s s' \<and> integrity_cdt_list_state aag subjects s s' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s')
integrity_obj_state aag activate subjects s' s'' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s' s'' \<and> integrity_cdt_list_state aag subjects s' s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s' s'')

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x) &&& integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)
integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. \<And>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (chain)
picking this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x) proof (prove)
using this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
pasObjectAbs aag x \<in> subjects

goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
pasObjectAbs aag x \<in> subjects

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
x \<in> X

goal (4 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (3 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (3 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
underlying_memory (machine_state s) x = underlying_memory (machine_state s') x

goal (3 subgoals):
 1. underlying_memory (machine_state s) x = underlying_memory (machine_state s') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (chain)
picking this:
integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p' = Some Running
x \<in> auth_ipc_buffers s' p'
pasObjectAbs aag p' \<notin> subjects

goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (4 subgoals):
 1. case tcb_states_of_state s ?p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
 2. tcb_states_of_state s'' ?p' = Some Running
 3. x \<in> auth_ipc_buffers s ?p'
 4. pasObjectAbs aag ?p' \<notin> subjects proof (chain)
picking this:
case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p' = Some Running
x \<in> auth_ipc_buffers s' p'
pasObjectAbs aag p' \<notin> subjects proof (prove)
using this:
case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p' = Some Running
x \<in> auth_ipc_buffers s' p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x proof (state)
this:
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x

goal (3 subgoals):
 1. tcb_states_of_state s'' p' = Some Running
 2. x \<in> auth_ipc_buffers s p'
 3. pasObjectAbs aag p' \<notin> subjects proof (chain)
picking this:
case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p' = Some Running
x \<in> auth_ipc_buffers s' p'
pasObjectAbs aag p' \<notin> subjects proof (prove)
using this:
case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p' = Some Running
x \<in> auth_ipc_buffers s' p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. x \<in> auth_ipc_buffers s p' proof (state)
this:
x \<in> auth_ipc_buffers s p'

goal (2 subgoals):
 1. tcb_states_of_state s'' p' = Some Running
 2. pasObjectAbs aag p' \<notin> subjects proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (4 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (2 subgoals):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (2 subgoals):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
aag_subjects_have_auth_to subjects aag Write x

goal (2 subgoals):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
aag_subjects_have_auth_to subjects aag Write x

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p' = Some Running
x \<in> auth_ipc_buffers s p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p' = Some Running
x \<in> auth_ipc_buffers s p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. \<And>p'. \<lbrakk>case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s' p' = Some Running; x \<in> auth_ipc_buffers s p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (chain)
picking this:
integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x

goal (5 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 5. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
underlying_memory (machine_state s') x = underlying_memory (machine_state s'') x
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p' = Some Running
x \<in> auth_ipc_buffers s p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (4 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (4 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
case tcb_states_of_state s' p'' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p'' = Some Running
x \<in> auth_ipc_buffers s' p''
pasObjectAbs aag p'' \<notin> subjects

goal (4 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 4. \<And>p'. \<lbrakk>case tcb_states_of_state s' p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x; tcb_states_of_state s'' p' = Some Running; x \<in> auth_ipc_buffers s' p'; pasObjectAbs aag p' \<notin> subjects\<rbrakk> \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (2 subgoals):
 1. p' = p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
p' = p''

goal (2 subgoals):
 1. p' = p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
p' = p''

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
p' = p''
case tcb_states_of_state s' p'' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s'' p'' = Some Running
x \<in> auth_ipc_buffers s' p''
pasObjectAbs aag p'' \<notin> subjects
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p' = Some Running
x \<in> auth_ipc_buffers s p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
p' \<noteq> p''

goal (1 subgoal):
 1. p' \<noteq> p'' \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
p' \<noteq> p''

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (prove)
using this:
p' \<noteq> p''
case tcb_states_of_state s p' of None \<Rightarrow> False | Some x \<Rightarrow> can_receive_ipc x
tcb_states_of_state s' p' = Some Running
x \<in> auth_ipc_buffers s p'
pasObjectAbs aag p' \<notin> subjects

goal (1 subgoal):
 1. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (3 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)
 3. x \<in> X \<Longrightarrow> integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x) proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (state)
this:
\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (prove)
goal (1 subgoal):
 1. \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. \<And>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. \<And>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (chain)
picking this:
integrity_subjects subjects aag activate X s s'
integrity_subjects subjects aag activate X s' s'' proof (prove)
using this:
integrity_subjects subjects aag activate X s s'
integrity_subjects subjects aag activate X s' s''

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x) &&& integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x) proof (prove)
using this:
integrity_obj_state aag activate subjects s s' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag subjects s s' \<and> integrity_cdt_list_state aag subjects s s' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s')
integrity_obj_state aag activate subjects s' s'' \<and> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s' s'' \<and> integrity_cdt_list_state aag subjects s' s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p)) \<and> (\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x)) \<and> (\<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x)) \<and> (\<forall>x a. integrity_asids aag subjects x a s' s'')

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x) &&& integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)
integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. \<And>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (chain)
picking this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x) proof (prove)
using this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (3 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. device_state (machine_state s) x = device_state (machine_state s') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
pasObjectAbs aag x \<in> subjects

goal (3 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. device_state (machine_state s) x = device_state (machine_state s') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (prove)
using this:
pasObjectAbs aag x \<in> subjects

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (2 subgoals):
 1. device_state (machine_state s) x = device_state (machine_state s') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (2 subgoals):
 1. device_state (machine_state s) x = device_state (machine_state s') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
device_state (machine_state s) x = device_state (machine_state s') x

goal (2 subgoals):
 1. device_state (machine_state s) x = device_state (machine_state s') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (chain)
picking this:
integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x) proof (prove)
using this:
integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (3 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. device_state (machine_state s') x = device_state (machine_state s'') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
pasObjectAbs aag x \<in> subjects

goal (3 subgoals):
 1. pasObjectAbs aag x \<in> subjects \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. device_state (machine_state s') x = device_state (machine_state s'') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 3. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (prove)
using this:
pasObjectAbs aag x \<in> subjects

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (2 subgoals):
 1. device_state (machine_state s') x = device_state (machine_state s'') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (2 subgoals):
 1. device_state (machine_state s') x = device_state (machine_state s'') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
device_state (machine_state s') x = device_state (machine_state s'') x

goal (2 subgoals):
 1. device_state (machine_state s') x = device_state (machine_state s'') x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
 2. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (prove)
using this:
device_state (machine_state s') x = device_state (machine_state s'') x

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
aag_subjects_have_auth_to subjects aag Write x

goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (prove)
using this:
aag_subjects_have_auth_to subjects aag Write x

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
aag_subjects_have_auth_to subjects aag Write x

goal (1 subgoal):
 1. aag_subjects_have_auth_to subjects aag Write x \<Longrightarrow> integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (prove)
using this:
aag_subjects_have_auth_to subjects aag Write x

goal (1 subgoal):
 1. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x) proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal:
No subgoals! proof (state)
this:
\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (prove)
using this:
\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (prove)
using this:
\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x)
integrity_obj_state aag activate subjects s s''
integrity_subjects subjects aag activate X s s'
integrity_subjects subjects aag activate X s' s''
\<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x)

goal (1 subgoal):
 1. integrity_subjects subjects aag activate X s s'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''; integrity_cdt_list_state aag subjects s s''\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''; integrity_cdt_list_state aag subjects s s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''; integrity_cdt_list_state aag subjects s s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>x a. integrity_asids aag subjects x a s s''\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''; integrity_cdt_list_state aag subjects s s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>x a. integrity_asids aag subjects x a s s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (device_state (machine_state s) x) (device_state (machine_state s'') x); integrity_obj_state aag activate subjects s s''; \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s'') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s'') x); integrity_obj_state aag activate subjects s s'; integrity_obj_state aag activate subjects s' s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s' x); \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s' x) (ekheap s'' x); integrity_cdt_state aag subjects s s'; integrity_cdt_state aag subjects s' s''; integrity_cdt_list_state aag subjects s s'; integrity_cdt_list_state aag subjects s' s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x); \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s' x, interrupt_states s' x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s' d p) (ready_queues s'' d p); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) X (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x); \<forall>x. integrity_mem aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (auth_ipc_buffers s') X (underlying_memory (machine_state s') x) (underlying_memory (machine_state s'') x); \<forall>x. integrity_device aag subjects x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x); \<forall>x a. integrity_asids aag subjects x a s s'; \<forall>x. integrity_device aag subjects x (tcb_states_of_state s') (tcb_states_of_state s'') (device_state (machine_state s') x) (device_state (machine_state s'') x); \<forall>x a. integrity_asids aag subjects x a s' s''; integrity_cdt_state aag subjects s s''; integrity_cdt_list_state aag subjects s s''; \<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x); \<forall>x a. integrity_asids aag subjects x a s s''; \<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x); \<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)\<rbrakk> \<Longrightarrow> (\<forall>x. integrity_eobj aag subjects (pasObjectAbs aag x) (ekheap s x) (ekheap s'' x)) \<and> integrity_cdt_state aag subjects s s'' \<and> integrity_cdt_list_state aag subjects s s'' \<and> (\<forall>x. integrity_interrupts aag subjects x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s'' x, interrupt_states s'' x)) \<and> (\<forall>d p. integrity_ready_queues aag subjects (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s'' d p)) \<and> (\<forall>x a. integrity_asids aag subjects x a s s'') proof (state)
this:
integrity_subjects subjects aag activate X s s''

goal:
No subgoals!