theory Ipc_AC

lemma tcb_sched_action_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>
   tcb_sched_action tcb_sched_enqueue target
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: integrity_def integrity_tcb_in_ipc_def tcb_states_of_state_def get_tcb_def
                        integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def
                        tcb_at_def get_etcb_def tcb_sched_enqueue_def etcb_at_def
                 split: option.splits) apply (intro conjI impI) apply (fastforce intro: exists_cons_append) apply (subst (asm) integrity_asids_updates(4)[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) apply (fastforce intro: exists_cons_append) apply (subst (asm) integrity_asids_updates(4)[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\<rbrace> tcb_sched_action tcb_sched_enqueue target \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> do d <- ethread_get tcb_domain target;
prio <- ethread_get tcb_priority target;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (tcb_sched_enqueue target queue)
od \<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 s \<Longrightarrow> etcb_at (\<lambda>t. etcb_at (\<lambda>ta. integrity_tcb_in_ipc aag X receiver epptr ctxt st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain t \<and> p = tcb_priority ta then tcb_sched_enqueue target (ready_queues s (tcb_domain t) (tcb_priority ta)) else ready_queues s t' p) s)) target s) target s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2\<rbrakk> \<Longrightarrow> (target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = target # ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))) \<and> (target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2)) \<longrightarrow> (\<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = target # ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)
 3. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 4. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 3. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state (?f99 s x2) (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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 3. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state (?f99 s x2) (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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 3. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (trans_state (?f106 s s x2 (?x2.105 s x2)) (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); ekheap s target = Some x2; target \<notin> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then target # ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>))
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 3. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>d. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. (d = tcb_domain x2 \<and> p = tcb_priority x2 \<longrightarrow> (\<exists>threads. threads @ ready_queues st (tcb_domain x2) (tcb_priority x2) = ready_queues s (tcb_domain x2) (tcb_priority x2))) \<and> ((d = tcb_domain x2 \<longrightarrow> p \<noteq> tcb_priority x2) \<longrightarrow> (\<exists>threads. threads @ ready_queues st d p = ready_queues s d p)))
 2. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state (?f143 s x2) (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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state (?f143 s x2) (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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_wellformed aag; irq_map_wellformed aag st; \<forall>x\<in>domains_of_state st. case x of (ptr, d) \<Rightarrow> pasObjectAbs aag ptr \<in> pasDomainAbs aag d; state_objs_in_policy aag st; state_asids_to_policy aag st \<subseteq> pasPolicy aag; state_irqs_to_policy aag st \<subseteq> pasPolicy aag; \<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) (\<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)); \<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)); \<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. pasSubject aag \<notin> pasDomainAbs aag d \<longrightarrow> pasMayEditReadyQueues aag \<or> (\<forall>p. \<exists>threads. threads @ ready_queues st d p = ready_queues s d p); \<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); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (trans_state (?f146 s s x2 (?x2.145 s x2)) (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); ekheap s target = Some x2; target \<in> set (ready_queues s (tcb_domain x2) (tcb_priority x2))\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>ready_queues := \<lambda>t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then ready_queues s (tcb_domain x2) (tcb_priority x2) else ready_queues s t' p, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal:
No subgoals!