theory Ipc_AC

lemma set_original_respects_in_ipc_reply:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and
    K (st_tcb_at (\<lambda>st. direct_call {pasSubject aag} aag epptr st) receiver st)\<rbrace>
   set_original (receiver, tcb_cnode_index 3) orig
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" apply (wp set_original_wp) apply (clarsimp simp: integrity_tcb_in_ipc_def) apply (simp add: integrity_def tcb_states_of_state_def get_tcb_def) apply (fold get_tcb_def tcb_states_of_state_def) apply (clarsimp simp: st_tcb_at_tcb_states_of_state) apply (rule conjI) apply (rule integrity_cdt_change_allowed) apply (rule cca_reply; force) apply (subst (asm) integrity_asids_updates(6)[symmetric]) apply (subst integrity_asids_updates(4)[where f=id, symmetric]) apply (subst (asm) integrity_asids_updates(4)[where f=id, symmetric]) apply (fastforce simp: trans_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)\<rbrace> set_original (receiver, tcb_cnode_index 3) orig \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st)) s \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X 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>); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), 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>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; 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)) \<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> (\<forall>a b. cdt_list_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_list st (a, b)) (cdt_list s (a, b))) \<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 tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> cdt_integrity aag (cdt st) (\<lambda>p. map_option tcb_state (case kheap st p of None \<Rightarrow> None | Some (TCB xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None)) (receiver, tcb_cnode_index 3) (cdt st (receiver, tcb_cnode_index 3), is_original_cap st (receiver, tcb_cnode_index 3)) (cdt s (receiver, tcb_cnode_index 3), orig) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; 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)) \<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>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b))) \<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 tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)); tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st\<rbrakk> \<Longrightarrow> cdt_integrity aag (cdt st) (tcb_states_of_state st) (receiver, tcb_cnode_index 3) (cdt st (receiver, tcb_cnode_index 3), is_original_cap st (receiver, tcb_cnode_index 3)) (cdt s (receiver, tcb_cnode_index 3), orig) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> cdt_integrity aag (cdt st) (tcb_states_of_state st) (receiver, tcb_cnode_index 3) (cdt st (receiver, tcb_cnode_index 3), is_original_cap st (receiver, tcb_cnode_index 3)) (cdt s (receiver, tcb_cnode_index 3), orig) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> cdt_integrity aag (cdt st) (tcb_states_of_state st) (receiver, tcb_cnode_index 3) (cdt st (receiver, tcb_cnode_index 3), is_original_cap st (receiver, tcb_cnode_index 3)) (cdt s (receiver, tcb_cnode_index 3), orig)
 2. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> cdt_change_allowed' aag (receiver, tcb_cnode_index 3) st
 2. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 := (kheap s)(receiver := kheap st receiver)\<rparr>)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 (is_original_cap_update (?f47 s sta) (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 (is_original_cap_update (?f47 s sta) (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s sta. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); \<forall>x. object_integrity aag (pasObjectAbs aag x) (kheap st x) (if x = receiver then kheap st receiver else kheap s x); tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; \<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x); \<forall>a b. cdt_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt st (a, b), is_original_cap st (a, b)) (cdt s (a, b), is_original_cap s (a, b)); \<forall>a b. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) (a, b) (cdt_list st (a, b)) (cdt_list s (a, b)); \<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x); \<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p); \<forall>x. memory_integrity X aag x (tcb_states_of_state st) (\<lambda>p. map_option tcb_state (case if p = receiver then kheap st receiver else kheap s p of None \<Rightarrow> None | Some (TCB tcb) \<Rightarrow> Some tcb | 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 tcb) \<Rightarrow> Some tcb | 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 (trans_state id (is_original_cap_update (?f50 s s sta (?sta49 s sta)) (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>is_original_cap := (is_original_cap s)((receiver, tcb_cnode_index 3) := orig), kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal:
No subgoals!