theory Ipc_AC

lemma cap_insert_ext_integrity_in_ipc_reply:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and
    K (is_subject aag (fst src_slot) \<and>
       st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
   cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" apply (rule hoare_gen_asm)+ apply (simp add: integrity_tcb_in_ipc_def fun_upd_def split del: if_split) apply (unfold integrity_def) apply (simp only: integrity_cdt_list_as_list_integ) apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def
                        tcb_states_of_state_def get_tcb_def
             split del: if_split cong: if_cong) apply wp apply (simp add: list_integ_def del: split_paired_All) apply (fold list_integ_def get_tcb_def tcb_states_of_state_def) apply (wp cap_insert_list_integrity hoare_vcg_all_lift) apply (simp add: list_integ_def del: split_paired_All) apply (fold list_integ_def get_tcb_def tcb_states_of_state_def) apply (clarsimp simp: st_tcb_at_tcb_states_of_state) apply (rule conjI) apply (rule cca_reply; force) apply clarsimp apply (erule_tac x=x in allE)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (is_subject aag (fst src_slot) \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst src_slot) \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<Longrightarrow> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_subject aag (fst src_slot) \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<Longrightarrow> \<lbrace>\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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. is_subject aag (fst src_slot) \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<Longrightarrow> \<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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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. is_subject aag (fst src_slot) \<and> st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<Longrightarrow> \<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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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 := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | 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 x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>_ s. pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | 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 x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> \<lbrace>?P'16\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>rv s. 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 x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | 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 x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p 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> ?P'16 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> \<lbrace>?P'16\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>rv s. (\<forall>x. cdt_change_allowed aag {pasSubject aag} (cdt st) (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) x \<or> filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt st) (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) (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 (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | 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>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | 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 x) \<Rightarrow> Some x | Some _ \<Rightarrow> None))) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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>p. map_option tcb_state (case kheap st p 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> ?P'16 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> \<lbrace>?P'16\<rbrace> cap_insert_ext src_parent src_slot (receiver, tcb_cnode_index 3) src_p dest_p \<lbrace>\<lambda>rv s. list_integ (\<lambda>x. cdt_change_allowed' aag x 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) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | 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 (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrace>
 2. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> ?P'16 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x, 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_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. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (list_integ (\<lambda>x. cdt_change_allowed' aag x st) st and K (cdt_change_allowed' aag (receiver, tcb_cnode_index 3) 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>x xa. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag x) (ready_queues st x xa) (ready_queues s x xa)) \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB b) \<Rightarrow> Some b | 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 (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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>x xa. integrity_asids aag {pasSubject aag} x xa st (s\<lparr>kheap := \<lambda>a. if a = receiver then kheap st receiver else kheap s a\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> (\<forall>x. cdt_change_allowed' aag x st \<or> filtered_eq (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) (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. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (receiver, tcb_cnode_index 3) st \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_subject aag (fst src_slot); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> (\<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else 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) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b))) \<and> list_integ (\<lambda>x. cdt_change_allowed' aag x 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. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)) \<and> tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (receiver, tcb_cnode_index 3) st \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (receiver, tcb_cnode_index 3) st \<and> (\<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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 s) x)) proof (prove)
goal (2 subgoals):
 1. \<And>s sta. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (receiver, tcb_cnode_index 3) st
 2. \<And>s sta. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> \<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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 s) x) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver)\<rbrakk> \<Longrightarrow> \<forall>x. x \<notin> auth_ipc_buffers st receiver \<longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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 s) x) proof (prove)
goal (1 subgoal):
 1. \<And>s sta x. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); \<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); x \<notin> auth_ipc_buffers st receiver\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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 s) x) proof (prove)
goal (1 subgoal):
 1. \<And>s sta x. \<lbrakk>is_subject aag (fst src_slot); pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; pas_refined aag st; list_integ (\<lambda>x. cdt_change_allowed' aag x st) st s; \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); x \<notin> auth_ipc_buffers st receiver; object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (x, b) (cdt st (x, b), is_original_cap st (x, b)) (cdt s (x, b), is_original_cap s (x, b)); memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (if x \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) x else underlying_memory (machine_state s) x); integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB x) \<Rightarrow> Some x | Some _ \<Rightarrow> None)) (device_state (machine_state st) x) (device_state (machine_state s) x); integrity_asids aag {pasSubject aag} x x st (s\<lparr>kheap := \<lambda>x. if x = receiver then kheap st receiver else kheap s x\<rparr>)\<rbrakk> \<Longrightarrow> memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p 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 s) x) proof (prove)
goal:
No subgoals!