theory ArchSyscall_AC

lemma integrity_exclusive_state_update[Syscall_AC_assms, simp]:
  "integrity aag X st (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) =
   integrity aag X st s" unfolding integrity_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. integrity aag X st (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) = integrity aag X st s proof (prove)
goal (1 subgoal):
 1. (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) x)) \<and> integrity_cdt_state aag {pasSubject aag} st (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) x, interrupt_states (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>) d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>)) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>)) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>)) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>machine_state := exclusive_state_update f (machine_state s)\<rparr>))) = (integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap st x) (ekheap s x)) \<and> integrity_cdt_state aag {pasSubject aag} st s \<and> (\<forall>x. cdt_list_integrity aag (cdt st) (tcb_states_of_state st) x (cdt_list st x) (cdt_list s x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node st x, interrupt_states st x) (interrupt_irq_node s x, interrupt_states s x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues st d p) (ready_queues s d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state st) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state st) (tcb_states_of_state s) (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))