theory ArchIpc_AC

lemma list_integ_lift_in_ipc[Ipc_AC_assms]:
  assumes li:
   "\<lbrace>list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and Q\<rbrace>
    f
    \<lbrace>\<lambda>_. list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st\<rbrace>"
  assumes ekh: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
  assumes rq: "\<And>P. \<lbrace> \<lambda>s. P (ready_queues s) \<rbrace> f \<lbrace> \<lambda>rv s. P (ready_queues s) \<rbrace>"
  shows "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace>
         f
         \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" apply (unfold integrity_tcb_in_ipc_def integrity_def[abs_def]) apply (simp del:split_paired_All) apply (rule hoare_pre) apply (simp only: integrity_cdt_list_as_list_integ) apply (rule hoare_lift_Pf2[where f="ekheap"]) apply (simp add: tcb_states_of_state_def get_tcb_def) apply (wp li[simplified tcb_states_of_state_def get_tcb_def] ekh rq)+ apply (simp only: integrity_cdt_list_as_list_integ) apply (simp add: tcb_states_of_state_def get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and Q\<rbrace> f \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> integrity_cdt_state aag {pasSubject aag} st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x, interrupt_states (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>))) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q\<rbrace> f \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> integrity_cdt_state aag {pasSubject aag} st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x, interrupt_states (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>))) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q\<rbrace> f \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q49\<rbrace> f \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> ?Q49 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q49\<rbrace> f \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st s \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> ?Q49 s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q52 x\<rbrace> f \<lbrace>\<lambda>_ a. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap a x)) \<and> (\<forall>xa. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag xa) (ekheap st xa) (x xa)) \<and> integrity_cdt_state aag {pasSubject aag} st a \<and> list_integ (\<lambda>a. cdt_change_allowed' aag a st) st a \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node a x, interrupt_states a x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues a d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (a\<lparr>kheap := (kheap a)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state a) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (a\<lparr>kheap := (kheap a)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state a) x)) \<and> (\<forall>aa. asid_table st (asid_high_bits_of aa) = asid_table a (asid_high_bits_of aa) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of aa \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap a receiver)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace>
 3. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> ?Q52 (ekheap s) s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?Q52 x\<rbrace> f \<lbrace>\<lambda>_ a. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap a x)) \<and> (\<forall>xa. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag xa) (ekheap st xa) (x xa)) \<and> (\<forall>aa b. cdt_integrity aag (cdt st) (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (aa, b) (cdt st (aa, b), is_original_cap st (aa, b)) (cdt a (aa, b), is_original_cap a (aa, b))) \<and> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st a \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node a x, interrupt_states a x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues a d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>aa. map_option tcb_state (case if aa = receiver then kheap st receiver else kheap a aa of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state a) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>aa. map_option tcb_state (case if aa = receiver then kheap st receiver else kheap a aa of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state a) x)) \<and> (\<forall>aa. asid_table st (asid_high_bits_of aa) = asid_table a (asid_high_bits_of aa) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of aa \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap a receiver)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ekheap s)\<rbrace>
 3. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> ?Q52 (ekheap s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> (\<forall>a b. cdt_integrity aag (cdt st) (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None))) st and Q) s \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (\<lambda>a. map_option tcb_state (case if a = receiver then kheap st receiver else kheap s a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (\<lambda>a. map_option tcb_state (case if a = receiver then kheap st receiver else kheap s a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st s \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)) and Q) s \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. x \<noteq> receiver \<longrightarrow> object_integrity aag (pasObjectAbs aag x) (kheap st x) (kheap s x)) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> (\<forall>a b. cdt_integrity aag (cdt st) (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | Some _ \<Rightarrow> None))) st and Q) s \<and> (\<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)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (\<lambda>a. map_option tcb_state (case if a = receiver then kheap st receiver else kheap s a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>a. map_option tcb_state (case kheap st a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (\<lambda>a. map_option tcb_state (case if a = receiver then kheap st receiver else kheap s a of None \<Rightarrow> None | Some (TCB a) \<Rightarrow> Some a | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>a. asid_table st (asid_high_bits_of a) = asid_table s (asid_high_bits_of a) \<or> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of a \<longrightarrow> is_subject_asid aag asid')) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver) proof (prove)
goal:
No subgoals!