theory CNode_AC

lemma set_cap_integrity_deletion_aux:
  "\<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and is_transferable_in slot
                       and cdt_change_allowed' aag slot and K(\<not> is_subject aag (fst slot))\<rbrace>
   set_cap NullCap slot
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (integrity_trans_start) apply (rule hoare_pre) apply (unfold integrity_subjects_def)[1] apply (wp hoare_wp_combs) apply (unfold set_cap_def)[1] apply (wpc) apply (wp set_object_wp) apply wpc apply wp+ apply (wp get_object_wp) apply wps apply (wp integrity_asids_set_cap_Nullcap hoare_vcg_all_lift) apply (safe ; clarsimp simp add: cte_wp_at_caps_of_state dest!: ko_atD) 
       (* cnode *)
        subgoal for s obj addr cnode_size content cap' apply (rule tro_cnode, simp, simp) apply (rule cnode_integrityI) apply simp apply (intro impI disjI2) apply (frule_tac addr=addr in caps_of_state_cnode, simp) apply clarsimp apply (erule is_transferable.cases, blast) apply (fastforce intro: reply_cap_deletion_integrity_intros) apply clarsimp apply (rule reply_cap_deletion_integrityI2[OF refl refl]) apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (drule reply_cap_no_grand_parent[where cs="caps_of_state s"]; fastforce?) apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                           dest: cap_auth_caps_of_state pas_refined_Control) apply (fastforce dest: tcb_states_of_state_kheapD descendant_of_caller_slot[OF _ _ tcb_atI]
                                parent_of_rtrancl_no_descendant) done 
       (* tcb_ctable *)
        subgoal for s obj tcb apply (rule_tac tro_tcb_empty_ctable, simp, simp, simp) apply (frule_tac addr="tcb_cnode_index 0" in caps_of_state_tcb) apply clarsimp apply (elim is_transferable.cases, simp) apply (fastforce intro: reply_cap_deletion_integrity_intros) apply clarsimp apply (rule reply_cap_deletion_integrityI2[OF refl refl]) apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (force simp: aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                       dest: reply_cap_no_grand_parent cap_auth_caps_of_state pas_refined_Control) apply (fastforce simp: direct_call_def
                          dest: tcb_caller_slot_empty_on_recieve parent_of_rtrancl_no_descendant
                                 descendant_of_caller_slot[OF _ _ tcb_atI] tcb_states_of_state_kheapD) done 
     (* tcb_vtable *)
      apply (rename_tac s obj tcb) apply (rule tro_orefl) apply (fastforce simp: caps_of_state_tcb valid_obj_def valid_tcb_def ran_tcb_cap_cases
                      elim:pspace_valid_objsE[OF _ invs_valid_objs] elim!:is_transferable.cases) 
    (* tcb_reply *)
     apply (rename_tac s obj tcb) apply (rule tro_orefl) apply (fastforce simp: is_cap_simps caps_of_state_tcb valid_obj_def valid_tcb_def
                           ran_tcb_cap_cases
                     elim: pspace_valid_objsE[OF _ invs_valid_objs] elim!:is_transferable.cases) 
   (* tcb_caller *)
    subgoal for s obj tcb apply (rule_tac tro_tcb_empty_caller, simp, simp, simp) apply (frule_tac addr="tcb_cnode_index 3" in caps_of_state_tcb) apply clarsimp apply (elim is_transferable.cases, simp) apply (fastforce intro: reply_cap_deletion_integrity_intros) apply clarsimp apply (rule reply_cap_deletion_integrityI2[OF refl refl]) apply (elim cdt_change_allowedE cdt_direct_change_allowed.cases) apply (force simp:aag_cap_auth_def cap_auth_conferred_def reply_cap_rights_to_auth_def
                   dest: reply_cap_no_grand_parent cap_auth_caps_of_state pas_refined_Control) apply (fastforce simp: direct_call_def
                      dest: tcb_caller_slot_empty_on_recieve parent_of_rtrancl_no_descendant
                            descendant_of_caller_slot[OF _ _ tcb_atI] tcb_states_of_state_kheapD) done 
  (* tcb_ipcframe*)
   apply (rename_tac s obj tcb) apply (rule tro_orefl) apply (fastforce simp: is_nondevice_page_cap_simps caps_of_state_tcb
                         valid_obj_def valid_tcb_def ran_tcb_cap_cases
                   elim: pspace_valid_objsE[OF _ invs_valid_objs] elim!:is_transferable.cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and valid_mdb and valid_objs and pas_refined aag and is_transferable_in slot and cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_. integrity aag X s\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?Q2 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>_ s'. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s s' \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap s' x)) \<and> integrity_cdt_state aag {pasSubject aag} s s' \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list s' x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node s' x, interrupt_states s' x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues s' d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state s') (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state s') x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state s') (device_state (machine_state s) x) (device_state (machine_state s') x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s s')\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?Q2 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s\<rbrace>
 2. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 3. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?P8 s sa \<and> ?P'8 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P8 s\<rbrace> case slot 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> NullCap) else fail | TCB tcb \<Rightarrow> if cref = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := NullCap\<rparr> else if cref = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := NullCap\<rparr> else if cref = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := NullCap\<rparr> else if cref = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := NullCap\<rparr> else if cref = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := NullCap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object oref
od \<lbrace>\<lambda>rv. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s\<rbrace>
 2. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 3. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> ?P8 s sa \<and> ?P'8 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R19 s x1 x2\<rbrace> do obj <- get_object x1;
(case obj of CNode sz cn \<Rightarrow> if x2 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(x2 \<mapsto> NullCap) else fail | TCB tcb \<Rightarrow> if x2 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := NullCap\<rparr> else if x2 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := NullCap\<rparr> else if x2 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := NullCap\<rparr> else if x2 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := NullCap\<rparr> else if x2 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := NullCap\<rparr> else fail | _ \<Rightarrow> fail) >>= set_object x1
od \<lbrace>\<lambda>rv. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s\<rbrace>
 2. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 3. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> ?R19 s x xa sa) \<and> ?P'8 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s x1 x2 obj. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?B21 s x1 x2 obj\<rbrace> case obj of CNode sz cn \<Rightarrow> if x2 \<in> dom cn \<and> well_formed_cnode_n sz cn then return $ CNode sz $ cn(x2 \<mapsto> NullCap) else fail | TCB tcb \<Rightarrow> if x2 = tcb_cnode_index 0 then return $ TCB $ tcb\<lparr>tcb_ctable := NullCap\<rparr> else if x2 = tcb_cnode_index 1 then return $ TCB $ tcb\<lparr>tcb_vtable := NullCap\<rparr> else if x2 = tcb_cnode_index 2 then return $ TCB $ tcb\<lparr>tcb_reply := NullCap\<rparr> else if x2 = tcb_cnode_index 3 then return $ TCB $ tcb\<lparr>tcb_caller := NullCap\<rparr> else if x2 = tcb_cnode_index 4 then return $ TCB $ tcb\<lparr>tcb_ipcframe := NullCap\<rparr> else fail | _ \<Rightarrow> fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 2. \<And>s x1 x2. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R19 s x1 x2\<rbrace> get_object x1 \<lbrace>?B21 s x1 x2\<rbrace>
 3. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 4. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> ?R19 s x xa sa) \<and> ?P'8 s sa proof (prove)
goal (8 subgoals):
 1. \<And>s x1 x2 obj x11 x12. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2); obj = CNode x11 x12\<rbrakk> \<Longrightarrow> \<lbrace>?R44 s x1 x2 obj x11 x12\<rbrace> if x2 \<in> dom x12 \<and> well_formed_cnode_n x11 x12 then return $ CNode x11 $ x12(x2 \<mapsto> NullCap) else fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 2. \<And>s x1 x2 obj x2a. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2); obj = TCB x2a\<rbrakk> \<Longrightarrow> \<lbrace>?R45 s x1 x2 obj x2a\<rbrace> if x2 = tcb_cnode_index 0 then return $ TCB $ x2a\<lparr>tcb_ctable := NullCap\<rparr> else if x2 = tcb_cnode_index 1 then return $ TCB $ x2a\<lparr>tcb_vtable := NullCap\<rparr> else if x2 = tcb_cnode_index 2 then return $ TCB $ x2a\<lparr>tcb_reply := NullCap\<rparr> else if x2 = tcb_cnode_index 3 then return $ TCB $ x2a\<lparr>tcb_caller := NullCap\<rparr> else if x2 = tcb_cnode_index 4 then return $ TCB $ x2a\<lparr>tcb_ipcframe := NullCap\<rparr> else fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 3. \<And>s x1 x2 obj x3. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2); obj = Endpoint x3\<rbrakk> \<Longrightarrow> \<lbrace>?R46 s x1 x2 obj x3\<rbrace> fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 4. \<And>s x1 x2 obj x4. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2); obj = Notification x4\<rbrakk> \<Longrightarrow> \<lbrace>?R47 s x1 x2 obj x4\<rbrace> fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 5. \<And>s x1 x2 obj x5. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2); obj = ArchObj x5\<rbrakk> \<Longrightarrow> \<lbrace>?R48 s x1 x2 obj x5\<rbrace> fail \<lbrace>\<lambda>obj' sa. integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> obj')\<rparr>)\<rbrace>
 6. \<And>s x1 x2. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R19 s x1 x2\<rbrace> get_object x1 \<lbrace>\<lambda>obj sa. (\<forall>x xa. obj = CNode x xa \<longrightarrow> ?R44 s x1 x2 obj x xa sa) \<and> (\<forall>x. obj = TCB x \<longrightarrow> ?R45 s x1 x2 obj x sa) \<and> (\<forall>x. obj = Endpoint x \<longrightarrow> ?R46 s x1 x2 obj x sa) \<and> (\<forall>x. obj = Notification x \<longrightarrow> ?R47 s x1 x2 obj x sa) \<and> (\<forall>x. obj = ArchObj x \<longrightarrow> ?R48 s x1 x2 obj x sa)\<rbrace>
 7. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 8. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> ?R19 s x xa sa) \<and> ?P'8 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s x1 x2. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; slot = (x1, x2)\<rbrakk> \<Longrightarrow> \<lbrace>?R19 s x1 x2\<rbrace> get_object x1 \<lbrace>\<lambda>obj sa. (\<forall>x xa. obj = CNode x xa \<longrightarrow> (x2 \<in> dom xa \<and> well_formed_cnode_n x xa \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> CNode x $ xa(x2 \<mapsto> NullCap))\<rparr>)) \<and> (\<not> (x2 \<in> dom xa \<and> well_formed_cnode_n x xa) \<longrightarrow> True)) \<and> (\<forall>x. obj = TCB x \<longrightarrow> (x2 = tcb_cnode_index 0 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> TCB $ x\<lparr>tcb_ctable := NullCap\<rparr>)\<rparr>)) \<and> (x2 \<noteq> tcb_cnode_index 0 \<longrightarrow> (x2 = tcb_cnode_index 1 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> TCB $ x\<lparr>tcb_vtable := NullCap\<rparr>)\<rparr>)) \<and> (x2 \<noteq> tcb_cnode_index 1 \<longrightarrow> (x2 = tcb_cnode_index 2 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> TCB $ x\<lparr>tcb_reply := NullCap\<rparr>)\<rparr>)) \<and> (x2 \<noteq> tcb_cnode_index 2 \<longrightarrow> (x2 = tcb_cnode_index 3 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> TCB $ x\<lparr>tcb_caller := NullCap\<rparr>)\<rparr>)) \<and> (x2 \<noteq> tcb_cnode_index 3 \<longrightarrow> (x2 = tcb_cnode_index 4 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x1 \<mapsto> TCB $ x\<lparr>tcb_ipcframe := NullCap\<rparr>)\<rparr>)) \<and> (x2 \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. obj = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. obj = Notification x \<longrightarrow> True) \<and> (\<forall>x. obj = ArchObj x \<longrightarrow> True)\<rbrace>
 2. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 3. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> ?R19 s x xa sa) \<and> ?P'8 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P'8 s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv sa. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues sa d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s sa)\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> (\<forall>ko. ko_at ko x sa \<longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> CNode xb $ xc(xa \<mapsto> NullCap))\<rparr>)) \<and> (\<not> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc) \<longrightarrow> True)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ctable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index 1 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_vtable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 1 \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_reply := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_caller := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> (xa = tcb_cnode_index 4 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ipcframe := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True))) \<and> ?P'8 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s prev_s. (valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s \<Longrightarrow> \<lbrace>?P91 s prev_s\<rbrace> set_cap NullCap slot \<lbrace>\<lambda>rv s'. (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap prev_s x)) \<and> integrity_cdt_state aag {pasSubject aag} s prev_s \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list prev_s x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node prev_s x, interrupt_states prev_s x)) \<and> (\<forall>d p. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag d) (ready_queues s d p) (ready_queues prev_s d p)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state prev_s) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state prev_s) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state prev_s) (device_state (machine_state s) x) (device_state (machine_state prev_s) x)) \<and> (\<forall>x a. integrity_asids aag {pasSubject aag} x a s s')\<rbrace>
 2. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> (\<forall>ko. ko_at ko x sa \<longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> CNode xb $ xc(xa \<mapsto> NullCap))\<rparr>)) \<and> (\<not> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc) \<longrightarrow> True)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ctable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index 1 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_vtable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 1 \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_reply := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_caller := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> (xa = tcb_cnode_index 4 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ipcframe := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True))) \<and> ?P91 s sa sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>(valid_mdb and (valid_objs and (pas_refined aag and (is_transferable_in slot and (cdt_change_allowed' aag slot and K (pasObjectAbs aag (fst slot) \<noteq> pasSubject aag)))))) s; s = sa\<rbrakk> \<Longrightarrow> (\<forall>x xa. slot = (x, xa) \<longrightarrow> (\<forall>ko. ko_at ko x sa \<longrightarrow> (\<forall>xb xc. ko = CNode xb xc \<longrightarrow> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> CNode xb $ xc(xa \<mapsto> NullCap))\<rparr>)) \<and> (\<not> (xa \<in> dom xc \<and> well_formed_cnode_n xb xc) \<longrightarrow> True)) \<and> (\<forall>xb. ko = TCB xb \<longrightarrow> (xa = tcb_cnode_index 0 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ctable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 0 \<longrightarrow> (xa = tcb_cnode_index 1 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_vtable := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 1 \<longrightarrow> (xa = tcb_cnode_index 2 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_reply := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 2 \<longrightarrow> (xa = tcb_cnode_index 3 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_caller := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 3 \<longrightarrow> (xa = tcb_cnode_index 4 \<longrightarrow> integrity_obj_state aag (pasMayActivate aag) {pasSubject aag} s (sa\<lparr>kheap := (kheap sa)(x \<mapsto> TCB $ xb\<lparr>tcb_ipcframe := NullCap\<rparr>)\<rparr>)) \<and> (xa \<noteq> tcb_cnode_index 4 \<longrightarrow> True)))))) \<and> (\<forall>x. ko = Endpoint x \<longrightarrow> True) \<and> (\<forall>x. ko = Notification x \<longrightarrow> True) \<and> (\<forall>x. ko = ArchObj x \<longrightarrow> True))) \<and> (\<forall>x. integrity_eobj aag {pasSubject aag} (pasObjectAbs aag x) (ekheap s x) (ekheap sa x)) \<and> integrity_cdt_state aag {pasSubject aag} s sa \<and> (\<forall>x. cdt_list_integrity aag (cdt s) (tcb_states_of_state s) x (cdt_list s x) (cdt_list sa x)) \<and> (\<forall>x. integrity_interrupts aag {pasSubject aag} x (interrupt_irq_node s x, interrupt_states s x) (interrupt_irq_node sa x, interrupt_states sa x)) \<and> (\<forall>x xa. integrity_ready_queues aag {pasSubject aag} (pasDomainAbs aag x) (ready_queues s x xa) (ready_queues sa x xa)) \<and> (\<forall>x. memory_integrity X aag x (tcb_states_of_state s) (tcb_states_of_state sa) (auth_ipc_buffers s) (underlying_memory (machine_state s) x) (underlying_memory (machine_state sa) x)) \<and> (\<forall>x. integrity_device aag {pasSubject aag} x (tcb_states_of_state s) (tcb_states_of_state sa) (device_state (machine_state s) x) (device_state (machine_state sa) x)) \<and> (\<forall>x xa. s = sa) proof (prove)
goal (6 subgoals):
 1. \<And>sa x xa xb xc y. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, xa) sa; cdt_change_allowed' aag (x, xa) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, xa); well_formed_cnode_n xb xc; xc xa = Some y; kheap sa x = Some (CNode xb xc)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (CNode xb xc)) (Some (CNode xb (\<lambda>a. if a = xa then Some NullCap else xc a)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 0) sa; cdt_change_allowed' aag (x, tcb_cnode_index 0) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 0); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ctable := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 5. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 6. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (6 subgoals):
 1. \<And>sa x xa xb xc y. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, xa) sa; cdt_change_allowed' aag (x, xa) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, xa); well_formed_cnode_n xb xc; xc xa = Some y; kheap sa x = Some (CNode xb xc)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (CNode xb xc)) (Some (CNode xb (\<lambda>a. if a = xa then Some NullCap else xc a)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 0) sa; cdt_change_allowed' aag (x, tcb_cnode_index 0) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 0); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ctable := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 5. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 6. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (CNode cnode_size content)) (Some (CNode cnode_size (\<lambda>a. if a = addr then Some NullCap else content a))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content)\<rbrakk> \<Longrightarrow> cnode_integrity {pasSubject aag} aag content (\<lambda>a. if a = addr then Some NullCap else content a) proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content)\<rbrakk> \<Longrightarrow> content l = (if l = addr then Some NullCap else content l) \<or> (\<exists>cap cap'. content l = Some cap \<and> (if l = addr then Some NullCap else content l) = Some cap' \<and> reply_cap_deletion_integrity {pasSubject aag} aag cap cap') proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content)\<rbrakk> \<Longrightarrow> l = addr \<longrightarrow> cap' = NullCap \<or> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); l = addr\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (1 subgoal):
 1. \<And>l. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, addr) s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); l = addr; caps_of_state s (obj, addr) = content addr\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_cap cap'; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some cap'\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some cap'; Some cap' = Some NullCap\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap
 2. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some cap'; Some cap' = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some cap'; kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some cap'; Some cap' = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag cap' NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (ReplyCap t False R) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, addr) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (2 subgoals):
 1. \<And>t R pptr. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, addr); pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag}
 2. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, addr); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (2 subgoals):
 1. \<And>t R pptr. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R; pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}; pptr = (obj, addr) \<or> cdt s \<Turnstile> pptr \<leadsto> (obj, addr) \<and> (\<exists>R'. caps_of_state s pptr = Some (ReplyCap t True R'))\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag}
 2. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, addr); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (1 subgoal):
 1. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, addr); well_formed_cnode_n cnode_size content; content addr = Some (ReplyCap t False R); kheap s obj = Some (CNode cnode_size content); caps_of_state s (obj, addr) = Some (ReplyCap t False R); cap' = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, addr); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal:
No subgoals! proof (prove)
goal (5 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 0) sa; cdt_change_allowed' aag (x, tcb_cnode_index 0) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 0); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ctable := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 5. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (5 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 0) sa; cdt_change_allowed' aag (x, tcb_cnode_index 0) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 0); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ctable := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 5. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 0) s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_ctable := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 0) s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 0) s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = tcb_cnode_map tcb (tcb_cnode_index 0)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_cap (tcb_ctable tcb); cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (tcb_ctable tcb)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (tcb_ctable tcb); Some (tcb_ctable tcb) = Some NullCap\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap
 2. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (tcb_ctable tcb); Some (tcb_ctable tcb) = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (tcb_ctable tcb); Some (tcb_ctable tcb) = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_ctable tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (ReplyCap t False R); tcb_ctable tcb = ReplyCap t False R\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (ReplyCap t False R) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 0) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (ReplyCap t False R); tcb_ctable tcb = ReplyCap t False R\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (2 subgoals):
 1. \<And>t R pptr. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (ReplyCap t False R); tcb_ctable tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 0); pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag}
 2. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (ReplyCap t False R); tcb_ctable tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 0); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (1 subgoal):
 1. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 0); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 0) = Some (ReplyCap t False R); tcb_ctable tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 0); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal:
No subgoals! proof (prove)
goal (4 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index (Suc 0)) sa; cdt_change_allowed' aag (x, tcb_cnode_index (Suc 0)) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index (Suc 0)); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_vtable := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index (Suc 0)) s; cdt_change_allowed' aag (obj, tcb_cnode_index (Suc 0)) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index (Suc 0)); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_vtable := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (4 subgoals):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index (Suc 0)) s; cdt_change_allowed' aag (obj, tcb_cnode_index (Suc 0)) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index (Suc 0)); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (tcb\<lparr>tcb_vtable := NullCap\<rparr>))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 4. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 2) sa; cdt_change_allowed' aag (x, tcb_cnode_index 2) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 2); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_reply := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 2) s; cdt_change_allowed' aag (obj, tcb_cnode_index 2) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 2); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_reply := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (3 subgoals):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 2) s; cdt_change_allowed' aag (obj, tcb_cnode_index 2) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 2); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (tcb\<lparr>tcb_reply := NullCap\<rparr>))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 3. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 3) sa; cdt_change_allowed' aag (x, tcb_cnode_index 3) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 3); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_caller := NullCap\<rparr>)))
 2. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 3) s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_caller := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 3) s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 3) s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = tcb_cnode_map tcb (tcb_cnode_index 3)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_cap (tcb_caller tcb); cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (tcb_caller tcb)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (tcb_caller tcb); Some (tcb_caller tcb) = Some NullCap\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap
 2. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (tcb_caller tcb); Some (tcb_caller tcb) = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (tcb_caller tcb); Some (tcb_caller tcb) = Some (ReplyCap t False R)\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (tcb_caller tcb) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (ReplyCap t False R); tcb_caller tcb = ReplyCap t False R\<rbrakk> \<Longrightarrow> reply_cap_deletion_integrity {pasSubject aag} aag (ReplyCap t False R) NullCap proof (prove)
goal (1 subgoal):
 1. \<And>t R. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; cdt_change_allowed' aag (obj, tcb_cnode_index 3) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (ReplyCap t False R); tcb_caller tcb = ReplyCap t False R\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (2 subgoals):
 1. \<And>t R pptr. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (ReplyCap t False R); tcb_caller tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 3); pasObjectAbs aag (fst pptr) \<in> {pasSubject aag}\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag}
 2. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (ReplyCap t False R); tcb_caller tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 3); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal (1 subgoal):
 1. \<And>t R pptr tcbst ep. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 3); kheap s obj = Some (TCB tcb); caps_of_state s (obj, tcb_cnode_index 3) = Some (ReplyCap t False R); tcb_caller tcb = ReplyCap t False R; cdt s \<Turnstile> pptr \<rightarrow>* (obj, tcb_cnode_index 3); tcb_states_of_state s (fst pptr) = Some tcbst; direct_call {pasSubject aag} aag ep tcbst; snd pptr = tcb_cnode_index 3\<rbrakk> \<Longrightarrow> pasObjectAbs aag t \<in> {pasSubject aag} proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>sa x xb. \<lbrakk>valid_mdb sa; valid_objs sa; pas_refined aag sa; is_transferable_in (x, tcb_cnode_index 4) sa; cdt_change_allowed' aag (x, tcb_cnode_index 4) sa; pasObjectAbs aag x \<noteq> pasSubject aag; slot = (x, tcb_cnode_index 4); kheap sa x = Some (TCB xb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag x) (Some (TCB xb)) (Some (TCB (xb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 4) s; cdt_change_allowed' aag (obj, tcb_cnode_index 4) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 4); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> object_integrity aag (pasObjectAbs aag obj) (Some (TCB tcb)) (Some (TCB (tcb\<lparr>tcb_ipcframe := NullCap\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj tcb. \<lbrakk>valid_mdb s; valid_objs s; pas_refined aag s; is_transferable_in (obj, tcb_cnode_index 4) s; cdt_change_allowed' aag (obj, tcb_cnode_index 4) s; pasObjectAbs aag obj \<noteq> pasSubject aag; slot = (obj, tcb_cnode_index 4); kheap s obj = Some (TCB tcb)\<rbrakk> \<Longrightarrow> Some (TCB tcb) = Some (TCB (tcb\<lparr>tcb_ipcframe := NullCap\<rparr>)) proof (prove)
goal:
No subgoals!