theory Ipc_AC

lemma set_cap_respects_in_ipc_reply:
   "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and
     K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller)\<rbrace>
    set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3)
    \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace>" unfolding set_cap_def apply simp apply (rule hoare_seq_ext[OF _ get_object_sp]) including no_pre apply (wp set_object_wp) apply (rule use_spec') apply (rule spec_valid_direct) apply (clarsimp simp:tcb_at_def get_tcb_def dest!:ko_atD split:kernel_object.splits) apply (simp add: spec_valid_def valid_def return_def) unfolding integrity_tcb_in_ipc_def apply (clarsimp simp:st_tcb_at_tcb_states_of_state ) apply (clarsimp simp:tcb_states_of_state_def direct_call_def dest!:get_tcb_SomeD) by (erule tcb_in_ipc.cases; (force intro:tii_call))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller)\<rbrace> set_cap (ReplyCap caller False R) (receiver, tcb_cnode_index 3) \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and K (st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller)\<rbrace> case (receiver, tcb_cnode_index 3) of (oref, cref) \<Rightarrow> do obj <- get_object oref;
(case obj of CNode sz cn \<Rightarrow> if cref \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(cref \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller)\<rbrace> do obj <- get_object receiver;
(case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object receiver
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller) and ko_at obj receiver\<rbrace> (case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object receiver \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller) and ko_at obj receiver\<rbrace> (case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object receiver \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr TRFinal st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller) and ko_at obj receiver\<rbrace> case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj s. s \<turnstile> \<lbrace>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller) and ko_at obj receiver\<rbrace> case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj s. (integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st and (\<lambda>y. st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st \<and> is_subject aag caller) and ko_at obj receiver) s \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> case obj of CNode sz cn \<Rightarrow> if tcb_cnode_index 3 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R) else fail | TCB tcb \<Rightarrow> if tcb_cnode_index 3 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := ReplyCap caller False R\<rparr> else if tcb_cnode_index 3 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := ReplyCap caller False R\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>obj s. \<lbrakk>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s; st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; is_subject aag caller; kheap s receiver = Some obj\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (tcb_cnode_index 3 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> return (CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R))) \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>) \<and> ((tcb_cnode_index 3 \<in> dom x12 \<longrightarrow> \<not> well_formed_cnode_n x11 x12) \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>)) \<and> (\<forall>x2. obj = TCB x2 \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> return (TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>)) \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>) \<and> ((\<exists>x3. obj = Endpoint x3) \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>) \<and> ((\<exists>x4. obj = Notification x4) \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>) \<and> ((\<exists>x5. obj = ArchObj x5) \<longrightarrow> s \<turnstile> \<lbrace>\<lambda>_. True\<rbrace> fail \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> x)\<rparr>)\<rbrace>) proof (prove)
goal (1 subgoal):
 1. \<And>obj s. \<lbrakk>integrity_tcb_in_ipc aag X receiver epptr TRFinalOrCall st s; st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; is_subject aag caller; kheap s receiver = Some obj\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (tcb_cnode_index 3 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R)))\<rparr>)) \<and> ((tcb_cnode_index 3 \<in> dom x12 \<longrightarrow> \<not> well_formed_cnode_n x11 x12) \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)))) \<and> (\<forall>x2. obj = TCB x2 \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>))\<rparr>)) \<and> ((\<exists>x3. obj = Endpoint x3) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))) \<and> ((\<exists>x4. obj = Notification x4) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))) \<and> ((\<exists>x5. obj = ArchObj x5) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). integrity_tcb_in_ipc aag X receiver epptr TRFinal st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>obj s. \<lbrakk>pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> 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>) \<and> tcb_in_ipc aag TRFinalOrCall (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); st_tcb_at (direct_call {pasSubject aag} aag epptr) receiver st; is_subject aag caller; kheap s receiver = Some obj\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (tcb_cnode_index 3 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R))), kheap := (kheap (s\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R)))\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R)))\<rparr>)\<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\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R)))\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>kheap := (kheap s)(receiver \<mapsto> CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R)))\<rparr>) receiver)) \<and> ((tcb_cnode_index 3 \<in> dom x12 \<longrightarrow> \<not> well_formed_cnode_n x11 x12) \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r), kheap := (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)\<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'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>) receiver)))) \<and> (\<forall>x2. obj = TCB x2 \<longrightarrow> pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>)), kheap := (kheap (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>))\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>))\<rparr>)\<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\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>))\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>))\<rparr>) receiver)) \<and> ((\<exists>x3. obj = Endpoint x3) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r), kheap := (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)\<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'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>) receiver))) \<and> ((\<exists>x4. obj = Notification x4) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r), kheap := (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)\<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'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>) receiver))) \<and> ((\<exists>x5. obj = ArchObj x5) \<longrightarrow> (\<forall>(r, s')\<in>fst (fail s). pasObjectAbs aag receiver \<noteq> pasSubject aag \<and> pas_refined aag st \<and> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r), kheap := (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>))(receiver := kheap st receiver), machine_state := machine_state (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)\<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'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>)) p\<rparr>\<rparr>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> r)\<rparr>) receiver))) proof (prove)
goal (1 subgoal):
 1. \<And>obj s sta. \<lbrakk>is_subject aag caller; kheap s receiver = Some obj; pasObjectAbs aag receiver \<noteq> pasSubject aag; tcb_states_of_state st receiver = Some sta; direct_call {pasSubject aag} aag epptr sta; 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 TRFinalOrCall (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some obj)\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (tcb_cnode_index 3 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some (CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R))))) \<and> ((tcb_cnode_index 3 \<in> dom x12 \<longrightarrow> \<not> well_formed_cnode_n x11 x12) \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some r)))) \<and> (\<forall>x2. obj = TCB x2 \<longrightarrow> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some (TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>)))) \<and> ((\<exists>x3. obj = Endpoint x3) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some r))) \<and> ((\<exists>x4. obj = Notification x4) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some r))) \<and> ((\<exists>x5. obj = ArchObj x5) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (kheap st receiver) (Some r))) proof (prove)
goal (1 subgoal):
 1. \<And>obj s z. \<lbrakk>is_subject aag caller; kheap s receiver = Some obj; pasObjectAbs aag receiver \<noteq> pasSubject aag; pas_refined aag st; integrity aag X st (s\<lparr>kheap := (kheap s)(receiver \<mapsto> TCB z), 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 TRFinalOrCall (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some obj); ep_recv_blocked epptr (tcb_state z); (pasSubject aag, Call, pasObjectAbs aag epptr) \<in> pasPolicy aag; kheap st receiver = Some (TCB z)\<rbrakk> \<Longrightarrow> (\<forall>x11 x12. (tcb_cnode_index 3 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some (CNode x11 (x12(tcb_cnode_index 3 \<mapsto> ReplyCap caller False R))))) \<and> ((tcb_cnode_index 3 \<in> dom x12 \<longrightarrow> \<not> well_formed_cnode_n x11 x12) \<longrightarrow> obj = CNode x11 x12 \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> TCB z), 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some r)))) \<and> (\<forall>x2. obj = TCB x2 \<longrightarrow> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some (TCB (x2\<lparr>tcb_caller := ReplyCap caller False R\<rparr>)))) \<and> ((\<exists>x3. obj = Endpoint x3) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> TCB z), 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some r))) \<and> ((\<exists>x4. obj = Notification x4) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> TCB z), 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some r))) \<and> ((\<exists>x5. obj = ArchObj x5) \<longrightarrow> (\<forall>x\<in>fst (fail s). case x of (r, s') \<Rightarrow> integrity aag X st (s'\<lparr>kheap := (kheap s')(receiver \<mapsto> TCB z), 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>) \<and> tcb_in_ipc aag TRFinal (pasObjectAbs aag receiver) epptr (Some (TCB z)) (Some r)))