theory Ipc_AC

lemma set_cdt_empty_slot_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. m = cdt s) and
    (\<lambda>s. descendants_of slot m = {}) and K (is_subject aag (fst slot))\<rbrace>
   set_cdt ((\<lambda>p. if m p = Some slot then m slot else m p)(slot := None))
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st \<rbrace>" unfolding set_cdt_def apply wp apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def no_children_empty_desc[symmetric]) apply (rule conjI, force) apply (subst (asm) integrity_asids_updates(2)[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 (\<lambda>s. m = cdt s) and (\<lambda>s. descendants_of slot m = {}) and K (is_subject aag (fst slot))\<rbrace> set_cdt ((\<lambda>p. if m p = Some slot then m slot else m p)(slot := None)) \<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 and (\<lambda>s. m = cdt s) and (\<lambda>s. descendants_of slot m = {}) and K (is_subject aag (fst slot))\<rbrace> do s <- get;
put $ s\<lparr>cdt := (\<lambda>p. if m p = Some slot then m slot else m p)(slot := None)\<rparr>
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 and (\<lambda>s. m = cdt s) and (\<lambda>s. descendants_of slot m = {}) and K (is_subject aag (fst slot))) s \<Longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st (s\<lparr>cdt := (\<lambda>p. if m p = Some slot then m slot else m p)(slot := None)\<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); \<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\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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); m = cdt s; \<forall>a b. cdt s (a, b) \<noteq> Some slot; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> ((\<exists>a b. (a, b) = slot) \<longrightarrow> cdt_integrity aag (cdt st) (tcb_states_of_state st) slot (cdt st slot, is_original_cap st slot) (None, is_original_cap s slot)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a, 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); \<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\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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); m = cdt s; \<forall>a b. cdt s (a, b) \<noteq> Some slot; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a, 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); \<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\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (cdt_update (?f72 s) (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); m = cdt s; \<forall>a b. cdt s (a, b) \<noteq> Some slot; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a, 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); \<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\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (device_state (machine_state st) x) (device_state (machine_state s) x); \<forall>x a. integrity_asids aag {pasSubject aag} x a st (cdt_update (?f72 s) (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); m = cdt s; \<forall>a b. cdt s (a, b) \<noteq> Some slot; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a, 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); \<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\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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) (tcb_states_of_state (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) (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 (cdt_update (?f74 s s) (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); m = cdt s; \<forall>a b. cdt s (a, b) \<noteq> Some slot; is_subject aag (fst slot)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a st (trans_state id (s\<lparr>cdt := \<lambda>a. if a = slot then None else if cdt s a = Some slot then cdt s slot else cdt s a, kheap := (kheap s)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal:
No subgoals!