theory Ipc_AC

lemma empty_slot_respects_in_ipc_autarch:
  "\<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and
    valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace>
   empty_slot slot NullCap
   \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace>" unfolding empty_slot_def post_cap_deletion_def apply simp apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch) apply (wp empty_slot_extended_list_integ_lift_in_ipc empty_slot_list_integrity') apply simp apply wp+ apply (wp set_cdt_empty_slot_respects_in_ipc_autarch) apply (simp add: set_cdt_def) apply wp apply wp apply wp apply (wp get_cap_wp) apply (clarsimp simp: integrity_tcb_in_ipc_def cte_wp_at_caps_of_state is_cap_simps) apply (drule(1) reply_cap_no_children') by (force dest: valid_list_empty simp: no_children_empty_desc simp del: split_paired_All)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace> empty_slot slot NullCap \<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 valid_mdb and valid_list and cte_wp_at is_reply_cap slot and K (is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
set_cap NullCap slot;
case NullCap of IRQHandlerCap irq \<Rightarrow> deleted_irq_handler irq | ArchObjectCap acap \<Rightarrow> arch_post_cap_deletion acap | _ \<Rightarrow> return ()
od
od \<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 valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))\<rbrace> do cap <- get_cap slot;
if cap = NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
set_cap NullCap slot
od
od \<lbrace>\<lambda>_. integrity_tcb_in_ipc aag X receiver epptr ctxt st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>cap slot_p cdt x. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B10 cap slot_p cdt x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>y s. integrity_tcb_in_ipc aag X receiver epptr ctxt st s \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag (fst slot)) s\<rbrace>
 2. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B9 cap slot_p cdt\<rbrace> set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) \<lbrace>?B10 cap slot_p cdt\<rbrace>
 3. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>?B9 cap slot_p\<rbrace>
 4. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 5. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 6. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>cap slot_p cdta x s. \<lbrakk>cap \<noteq> NullCap; (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and ?Q21 cap slot_p cdta x) s\<rbrakk> \<Longrightarrow> (list_integ (cdt_change_allowed aag {pasSubject aag} (cdt st) (tcb_states_of_state st)) st and (\<lambda>s. cdt_list s slot = []) and K (cdt_change_allowed' aag slot st)) s
 2. \<And>cap slot_p cdt x P. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 3. \<And>cap slot_p cdt x P. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 4. \<And>cap slot_p cdt x. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'20 cap slot_p cdt x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. K (is_subject aag (fst slot)) s \<and> K (is_subject aag (fst slot)) s\<rbrace>
 5. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B9 cap slot_p cdt\<rbrace> set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) \<lbrace>\<lambda>x s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and ?Q21 cap slot_p cdt x) s \<and> ?P'20 cap slot_p cdt x s\<rbrace>
 6. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>?B9 cap slot_p\<rbrace>
 7. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 8. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 9. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>cap slot_p cdt x P. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>
 2. \<And>cap slot_p cdt x P. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>
 3. \<And>cap slot_p cdt x. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'20 cap slot_p cdt x\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>rv s. K (is_subject aag (fst slot)) s \<and> K (is_subject aag (fst slot)) s\<rbrace>
 4. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B9 cap slot_p cdt\<rbrace> set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) \<lbrace>\<lambda>x s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>a. cdt_list a slot = [] \<and> cdt_change_allowed' aag slot st)) s \<and> ?P'20 cap slot_p cdt x s\<rbrace>
 5. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>?B9 cap slot_p\<rbrace>
 6. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 7. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 8. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B9 cap slot_p cdt\<rbrace> set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) \<lbrace>\<lambda>x s. integrity_tcb_in_ipc aag X receiver epptr ctxt st s \<and> (cdt_list s slot = [] \<and> cdt_change_allowed' aag slot st) \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag (fst slot)) s\<rbrace>
 2. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>?B9 cap slot_p\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 5. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'46 cap slot_p cdt\<rbrace> set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)) \<lbrace>\<lambda>rv s. cdt_list s slot = [] \<and> cdt_change_allowed' aag slot st \<and> K (is_subject aag (fst slot)) s \<and> K (is_subject aag (fst slot)) s\<rbrace>
 2. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>\<lambda>cdta s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. cdta = cdt s) and (\<lambda>s. descendants_of slot cdta = {}) and K (is_subject aag (fst slot))) s \<and> ?P'46 cap slot_p cdta s\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 5. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (5 subgoals):
 1. \<And>cap slot_p cdt. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?P'46 cap slot_p cdt\<rbrace> do s <- get;
put (s\<lparr>cdt := (\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None)\<rparr>)
od \<lbrace>\<lambda>rv s. cdt_list s slot = [] \<and> cdt_change_allowed' aag slot st \<and> is_subject aag (fst slot)\<rbrace>
 2. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>\<lambda>cdta s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. cdta = cdt s) and (\<lambda>s. descendants_of slot cdta = {}) and K (is_subject aag (fst slot))) s \<and> ?P'46 cap slot_p cdta s\<rbrace>
 3. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 4. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 5. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (4 subgoals):
 1. \<And>cap slot_p. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?B8 cap slot_p\<rbrace> gets cdt \<lbrace>\<lambda>cdta s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>s. cdta = cdt s) and (\<lambda>s. descendants_of slot cdta = {}) and K (is_subject aag (fst slot))) s \<and> cdt_list (s\<lparr>cdt := (\<lambda>p. if cdta p = Some slot then cdta slot else cdta p)(slot := None)\<rparr>) slot = [] \<and> cdt_change_allowed' aag slot st \<and> is_subject aag (fst slot)\<rbrace>
 2. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>?B8 cap\<rbrace>
 3. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 4. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (3 subgoals):
 1. \<And>cap. cap \<noteq> NullCap \<Longrightarrow> \<lbrace>?R6 cap\<rbrace> gets (\<lambda>s. cdt s slot) \<lbrace>\<lambda>slot_p s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>sa. cdt s = cdt sa) and (\<lambda>sa. descendants_of slot (cdt s) = {}) and K (is_subject aag (fst slot))) s \<and> cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr>) slot = [] \<and> cdt_change_allowed' aag slot st \<and> is_subject aag (fst slot)\<rbrace>
 2. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> ?R6 cap s)\<rbrace>
 3. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> get_cap slot \<lbrace>\<lambda>cap s. (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>sa. cdt s = cdt sa) and (\<lambda>sa. descendants_of slot (cdt s) = {}) and K (is_subject aag (fst slot))) s \<and> cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr>) slot = [] \<and> cdt_change_allowed' aag slot st \<and> is_subject aag (fst slot))\<rbrace>
 2. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity_tcb_in_ipc aag X receiver epptr ctxt st and valid_mdb and valid_list and cte_wp_at is_reply_cap slot and (\<lambda>y. is_subject aag (fst slot))) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (cap = NullCap \<longrightarrow> integrity_tcb_in_ipc aag X receiver epptr ctxt st s) \<and> (cap \<noteq> NullCap \<longrightarrow> (integrity_tcb_in_ipc aag X receiver epptr ctxt st and (\<lambda>sa. cdt s = cdt sa) and (\<lambda>sa. descendants_of slot (cdt s) = {}) and K (is_subject aag (fst slot))) s \<and> cdt_list (s\<lparr>cdt := (\<lambda>p. if cdt s p = Some slot then cdt s slot else cdt s p)(slot := None)\<rparr>) slot = [] \<and> cdt_change_allowed' aag slot st \<and> is_subject aag (fst slot)) proof (prove)
goal (1 subgoal):
 1. \<And>s x R. \<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 ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); valid_mdb s; valid_list s; is_subject aag (fst slot); caps_of_state s slot = Some (ReplyCap x False R)\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} \<and> cdt_list s slot = [] \<and> cdt_change_allowed' aag slot st proof (prove)
goal (1 subgoal):
 1. \<And>s x R. \<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 ctxt (pasObjectAbs aag receiver) epptr (kheap st receiver) (kheap s receiver); valid_list s; is_subject aag (fst slot); caps_of_state s slot = Some (ReplyCap x False R); \<forall>p'. cdt s p' \<noteq> Some slot\<rbrakk> \<Longrightarrow> descendants_of slot (cdt s) = {} \<and> cdt_list s slot = [] \<and> cdt_change_allowed' aag slot st