theory Ipc_AC

lemma integrity_receive_blocked_chain_bound:
  "\<lbrakk> bound_tcb_at ((=) (Some ntfnptr)) p s; integrity aag X st s; \<not> is_subject aag p \<rbrakk>
     \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st" apply (clarsimp simp: integrity_def) apply (drule bound_tcb_at_thread_bound_ntfns) apply (drule tsos_tro' [where p = p], simp+ ) apply (clarsimp simp:tba_Some) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound_tcb_at ((=) (Some ntfnptr)) p s; integrity aag X st s; pasObjectAbs aag p \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>bound_tcb_at ((=) (Some ntfnptr)) p s; pasObjectAbs aag p \<noteq> pasSubject aag; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<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> bound_tcb_at ((=) (Some ntfnptr)) p st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag p \<noteq> pasSubject aag; integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} st s; \<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; thread_bound_ntfns s p = Some ntfnptr\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag p \<noteq> pasSubject aag; \<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; thread_bound_ntfns s p = Some ntfnptr; thread_bound_ntfns st p = Some ntfnptr\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) p st proof (prove)
goal:
No subgoals!