theory Ipc_AC

lemma set_endpoint_integrity_in_ipc:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K (aag_has_auth_to aag SyncSend epptr)\<rbrace>
   set_endpoint epptr ep'
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace>" apply (simp add: set_simple_ko_def set_object_def) apply (wp get_object_wp) apply (clarsimp split: kernel_object.splits
                  simp: obj_at_def is_tcb is_ep integrity_tcb_in_ipc_def
                        partial_inv_def a_type_def) apply (intro impI conjI) apply (erule integrity_trans) apply (clarsimp simp: integrity_def fun_upd_def) apply (erule tcb_in_ipc.cases, simp_all) apply (erule integrity_trans) apply (clarsimp simp: integrity_def) apply (rule conjI) apply (fastforce intro: tro_ep) apply (clarsimp simp: integrity_asids_kh_update integrity_asids_kh_upds) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and K ((pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> set_endpoint epptr ep' \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRContext st and (\<lambda>y. (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)\<rbrace> do obj <- get_object epptr;
y <- assert (a_type obj = AEndpoint \<or> a_type obj = ANTFN);
y <- assert (\<exists>y. Endpoint y = obj);
kobj <- get_object epptr;
y <- assert (a_type kobj = AEndpoint);
s <- get;
put (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Endpoint ep')\<rparr>)
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRContext st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr TRContext st and (\<lambda>y. (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag)) s \<Longrightarrow> \<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = AEndpoint \<or> a_type ko = ANTFN \<longrightarrow> (\<exists>y. Endpoint y = ko) \<longrightarrow> (\<forall>ko. ko_at ko epptr s \<longrightarrow> a_type ko = AEndpoint \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRContext st (s\<lparr>kheap := (kheap s)(epptr \<mapsto> Endpoint ep')\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (receiver = epptr \<longrightarrow> (\<exists>x3. kheap s epptr = Some (Endpoint x3)) \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(epptr := kheap st epptr), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st epptr then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRContext (pasObjectAbs aag epptr) epptr (kheap st epptr) (Some (Endpoint ep'))) \<and> (receiver \<noteq> epptr \<longrightarrow> (\<exists>x3. kheap s epptr = Some (Endpoint x3)) \<longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver = epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(epptr := kheap st epptr), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st epptr then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver = epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag epptr) epptr (kheap st epptr) (Some (Endpoint ep'))
 3. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver = epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(epptr := kheap st epptr), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st epptr then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>)
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver = epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag epptr) epptr (kheap st epptr) (Some (Endpoint ep'))
 3. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver = epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> tcb_in_ipc aag TRContext (pasObjectAbs aag epptr) epptr (kheap st epptr) (Some (Endpoint ep'))
 2. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>); tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; \<exists>x3. kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> integrity aag X (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver), machine_state := machine_state s\<lparr>underlying_memory := \<lambda>p. if p \<in> auth_ipc_buffers st receiver then underlying_memory (machine_state st) p else underlying_memory (machine_state s) p\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag epptr) (Some (Endpoint x3)) (Some (Endpoint ep')) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s x3. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag epptr) (Some (Endpoint x3)) (Some (Endpoint ep'))
 2. \<And>s x3. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x3. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; tcb_in_ipc aag TRContext (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); (pasSubject aag, SyncSend, pasObjectAbs aag epptr) \<in> pasPolicy aag; receiver \<noteq> epptr; kheap s epptr = Some (Endpoint x3)\<rbrakk> \<Longrightarrow> \<forall>x a. integrity_asids aag {pasSubject aag} x a (s\<lparr>kheap := (kheap s)(receiver := kheap st receiver)\<rparr>) (s\<lparr>kheap := (\<lambda>a. if a = epptr then Some (Endpoint ep') else kheap s a)(receiver := kheap st receiver)\<rparr>) proof (prove)
goal:
No subgoals!