theory Ipc_AC

lemma integrity_receive_blocked_chain':
  "\<lbrakk> st_tcb_at receive_blocked p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk>
     \<Longrightarrow> st_tcb_at receive_blocked p st" apply (clarsimp simp: integrity_def st_tcb_at_tcb_states_of_state receive_blocked_def) apply (simp split: thread_state.split_asm) apply (rename_tac word pl) apply (drule_tac ep=word in tsos_tro [where p = p], simp+ ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at receive_blocked p s; integrity aag X st s; pasObjectAbs aag p \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked p st proof (prove)
goal (1 subgoal):
 1. \<And>sta. \<lbrakk>pasObjectAbs aag p \<noteq> pasSubject aag; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; tcb_states_of_state s p = Some sta; case sta of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False; \<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) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s\<rbrakk> \<Longrightarrow> \<exists>sta. tcb_states_of_state st p = Some sta \<and> (case sta of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>sta x41 x42. \<lbrakk>\<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) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; pasObjectAbs aag p \<noteq> pasSubject aag; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; tcb_states_of_state s p = Some (BlockedOnReceive x41 x42); sta = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> \<exists>sta. tcb_states_of_state st p = Some sta \<and> (case sta of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal (1 subgoal):
 1. \<And>sta word pl. \<lbrakk>\<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) (tcb_states_of_state s) (auth_ipc_buffers st) (underlying_memory (machine_state st) x) (underlying_memory (machine_state s) x); \<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); \<forall>x a. integrity_asids aag {pasSubject aag} x a st s; pasObjectAbs aag p \<noteq> pasSubject aag; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; tcb_states_of_state s p = Some (BlockedOnReceive word pl); sta = BlockedOnReceive word pl\<rbrakk> \<Longrightarrow> \<exists>sta. tcb_states_of_state st p = Some sta \<and> (case sta of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!